diff --git a/src/internals/incompatibilities.md b/src/internals/incompatibilities.md
index 5a83a8a..4461742 100644
--- a/src/internals/incompatibilities.md
+++ b/src/internals/incompatibilities.md
@@ -89,28 +89,32 @@ With incompatibilities, we would note
 \Rightarrow \quad \\{ a: T_a, c: \overline{T_c} \\}. \\]
 
 This is the simplified version of the rule of resolution.
-For the generalization, let's reuse the "more mathematical" notation of conjunctions
-for incompatibilities \\( T_a \land T_b \\) and the above rule would be
+For the generalization, let's write them as [boolean expressions][boolean_expression].
 
-\\[               T_a \land \overline{T_b}, \quad
-                  T_b \land \overline{T_c}  \quad
-\Rightarrow \quad T_a \land \overline{T_c}. \\]
+\\[               \neg (T_a \land \overline{T_b}) \quad \land \quad
+                  \neg (T_b \land \overline{T_c}) \quad
+\Rightarrow \quad \neg (T_a \land \overline{T_c}). \\]
 
 In fact, the above rule can also be expressed as follows
 
-\\[               T_a \land \overline{T_b}, \quad
-                  T_b \land \overline{T_c}  \quad
-\Rightarrow \quad T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c} \\]
+\\[               \neg (T_a \land \overline{T_b}) \quad \land \quad
+                  \neg (T_b \land \overline{T_c}) \quad
+\Rightarrow \quad \neg (T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c}) \\]
 
 since for any term \\( T \\), the disjunction \\( T \lor \overline{T} \\) is always true.
-In general, for any two incompatibilities \\( T_a^1 \land T_b^1 \land \cdots \land T_z^1 \\)
-and \\( T_a^2 \land T_b^2 \land \cdots \land T_z^2 \\) we can deduce a third,
-called the resolvent whose expression is
+In general, for any two incompatibilities \\( \\{ a: T_a^1, \cdots, z: T_z^1 \\} \\) and
+\\(  \\{ a: T_a^2, \cdots, z: T_z^2 \\}, \\)
+or
 
-\\[ (T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land T_z^2). \\]
+\\[ \neg (T_a^1 \land T_b^1 \land \cdots \land T_z^1) \land  \neg (T_a^2 \land T_b^2 \land \cdots \land T_z^2), \\]
+we can deduce a third, called the resolvent whose expression is
+
+\\[ \neg ((T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land T_z^2)). \\]
 
 In that expression, only one pair of package terms is regrouped as a union (a disjunction),
 the others are all intersected (conjunction).
 If a term for a package does not exist in one incompatibility,
 it can safely be replaced by the term \\( \neg [\varnothing] \\) in the expression above
 as we have already explained before.
+
+[boolean_expression]: https://en.wikipedia.org/wiki/Boolean_expression#Boolean_operators
diff --git a/src/internals/terms.md b/src/internals/terms.md
index e4b2042..7d2e784 100644
--- a/src/internals/terms.md
+++ b/src/internals/terms.md
@@ -24,6 +24,7 @@ In this guide, for any given range \\(r\\),
 we will note \\([r]\\) its associated positive term,
 and \\(\neg [r]\\) its associated negative term.
 And for any term \\(T\\), we will note \\(\overline{T}\\) the negation of that term.
+(\\( \neg A \\) and \\( \overline{A} \\) are different notations for the same thing.)
 Therefore we have the following rules,
 
 \\[\begin{eqnarray}
@@ -58,7 +59,10 @@ based on those ranges is defined as follows,
 \neg [r_1] \land \neg [r_2] &=& \neg [r_1 \cup r_2].  \nonumber \\\\
 \end{eqnarray}\\]
 
-And for any two terms \\(T_1\\) and \\(T_2\\), their union and intersection are related by
+In rust terms, "\\( \neg \\)" means "not"/`!` (\\( \neg T \\),
+"\\( \land \\)" means "and"/, "\\( \lor \\)" means "or"/`||`.
+
+And for any two terms \\(T_1\\) and \\(T_2\\), their union and intersection are related by De Morgan's laws
 
 \\[ \overline{T_1 \lor T_2} = \overline{T_1} \land \overline{T_1}. \\]