Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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