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:notes_on_congruences [2009/05/06 10:04]
vkuncak
sav08:notes_on_congruences [2015/04/21 17:30] (current)
Line 6: Line 6:
  
 We assume no relation symbols other than congruence itself. ​ (We represent a predicate $p(x_1,​\ldots,​x_n)$ as $f_p(x_1,​\ldots,​x_n)=true$.) We assume no relation symbols other than congruence itself. ​ (We represent a predicate $p(x_1,​\ldots,​x_n)$ as $f_p(x_1,​\ldots,​x_n)=true$.)
 +
  
 ===== Intersection of Congruences ===== ===== Intersection of Congruences =====
Line 25: Line 26:
  
 Transitive: Transitive:
-\[\begin{array}{rcl}+\begin{equation*}\begin{array}{rcl}
 (x,y) \in \bigcap S \wedge (y,z) \in \bigcap S &​\rightarrow&​ (x,y) \in r_1,r_2 \wedge (y,z) \in r_1,r_2 \\ (x,y) \in \bigcap S \wedge (y,z) \in \bigcap S &​\rightarrow&​ (x,y) \in r_1,r_2 \wedge (y,z) \in r_1,r_2 \\
 r_1,r_2 ~~ \text{transitive} & \rightarrow & (x,z) \in r_1,r_2 \\ r_1,r_2 ~~ \text{transitive} & \rightarrow & (x,z) \in r_1,r_2 \\
  & \rightarrow & (x,z)\in \bigcap S  & \rightarrow & (x,z)\in \bigcap S
-\end{array} \]+\end{array} \end{equation*}
  
 Congruence conditions: Congruence conditions:
 $\forall x_1,​\ldots,​x_n,​y_1,​\ldots,​y_n.$ $\forall x_1,​\ldots,​x_n,​y_1,​\ldots,​y_n.$
-\[\begin{array}{rcl}+\begin{equation*}\begin{array}{rcl}
  ​\bigwedge_{i=0}^n (x_i,y_1) \in \bigcap S & \rightarrow & \bigwedge_{i=0}^n (x_i,y_1) \in r_1,r_2 \\  ​\bigwedge_{i=0}^n (x_i,y_1) \in \bigcap S & \rightarrow & \bigwedge_{i=0}^n (x_i,y_1) \in r_1,r_2 \\
- ​r_1,​r_2 ~~ \text{congruence relations} & \rightarrow & f(x_1,​\ldots,​ x_n) f(y_1,​\ldots,​ y_n) \in r_1,r_2 \\+ ​r_1,​r_2 ~~ \text{congruence relations} & \rightarrow & (f(x_1,​\ldots,​ x_n)f(y_1,​\ldots,​ y_n)) \in r_1,r_2 \\
  & \rightarrow & f(x_1,​\ldots,​ x_n) = f(y_1,​\ldots,​ y_n) \in \bigcap S  & \rightarrow & f(x_1,​\ldots,​ x_n) = f(y_1,​\ldots,​ y_n) \in \bigcap S
-\end{array} \]+\end{array} \end{equation*}
  
 **End of Proof.** **End of Proof.**
Line 51: Line 52:
  
 Define ​ Define ​
-\[\begin{array}{rcl}+\begin{equation*}\begin{array}{rcl}
    C(r) &=& r \cup \Delta_D \cup r^{-1} \cup r \circ r\ \cup \\    C(r) &=& r \cup \Delta_D \cup r^{-1} \cup r \circ r\ \cup \\
         & & \{ ((f(x_1,​\ldots,​x_n),​f(y_1,​\ldots,​y_n)) \mid \bigwedge_{i=1}^n (x_i,y_i) \in r \}          & & \{ ((f(x_1,​\ldots,​x_n),​f(y_1,​\ldots,​y_n)) \mid \bigwedge_{i=1}^n (x_i,y_i) \in r \} 
 \end{array} \end{array}
-\]+\end{equation*}
 Let $r_{n+1} = C(r_n)$ for $n \ge 0$.  Let $r_{n+1} = C(r_n)$ for $n \ge 0$. 
  
 
sav08/notes_on_congruences.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice