Differences

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

--- sav08:partial_congruences [2008/04/23 07:45]
vkuncak
+++ sav08:partial_congruences [2008/04/23 07:50]
vkuncak
@@ Line 7: / Line 7: @@
 **Proof:**
-Show that C^i(s) \cap T^2 = s$ for each $i \ge 0$.
+Show $C^i(s) \cap T^2 = s$ for all $i \ge 0$.
 **Proof End.**
+When checking a formula we compute congruences on a finite set of terms that occur in the formula.
+We apply the congruence condition only to terms that already exist in the set, using congruence condition:
+\[
+\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
+\]