Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav08:partial_congruences [2008/04/23 07:50]
vkuncak
sav08:partial_congruences [2015/04/21 17:30] (current)
Line 7: Line 7:
 **Proof:​** ​ **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.** **Proof End.**
Line 14: Line 24:
  
 We apply the congruence condition only to terms that already exist in the set, using congruence condition: We apply the congruence condition only to terms that already exist in the set, using congruence condition:
-\[+\begin{equation*}
 \begin{array}{l} \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 \\     ​\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     (f(x_1,​\ldots,​x_n),​f(y_1,​\ldots,​y_n)) \in r
-\]+\end{equation*}
  
 
sav08/partial_congruences.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice