Differences

This shows you the differences between two versions of the page.

--- sav08:partial_congruences [2008/04/23 07:49]
vkuncak
+++ sav08:partial_congruences [2015/04/21 17:30] (current)
@@ Line 7: / Line 7: @@
 **Proof:**
-Show $C^i(s) \cap T^2 = s$ for all $i \ge 0$.
+Show $C^i(s) \cap T^2 = s$ for all $i \ge 0$, by induction.
+  * $i = 0$: s = s
+  * $i \rightarrow i+1$:
+$C^{i+1}(s) \cap T^2 = C(C^i(s) \cap T^2) \cap T^2 $, by induction hypothesis $C^i(s) \cap T^2 =s$.
+Thus $C(C^i(s) \cap T^2) \cap T^2 = C(s) \cap T^2$.
+As $C$ adds only needed term for congruence, the added term are either not in $T^2$ or $s$ in not a congruence.
+By hypothesis $s$ is a congruence, so $C(s) \cap T^2 = s$.
+Therefore $C^{i+1}(s) \cap T^2 = s$.
 **Proof End.**
@@ Line 14: / Line 24: @@
 We apply the congruence condition only to terms that already exist in the set, using congruence condition:
-\[
+\begin{equation*}
-   \forall x_1,\ldots,x_n,y_1,\ldots,y_n. \bigwedge_{i=1}^n (x_i,y_i) \in r \land f(x_1,\ldots,x_n) \in T \land f(y_1,\ldots,y_n) \in T  \rightarrow (f(x_1,\ldots,x_n),f(y_1,\ldots,y_n)) \in r
+\begin{array}{l}
-\]
+   \forall x_1,\ldots,x_n,y_1,\ldots,y_n. \bigwedge_{i=1}^n (x_i,y_i) \in r\ \land \ f(x_1,\ldots,x_n) \in T \land f(y_1,\ldots,y_n) \in T  \rightarrow \\
+    (f(x_1,\ldots,x_n),f(y_1,\ldots,y_n)) \in r
+\end{equation*}