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 Both sides next revision
sav07_lecture_4 [2007/03/27 16:46]
leander.eyer
sav07_lecture_4 [2007/03/27 16:48]
leander.eyer
Line 289: Line 289:
  
 ===== Proving formulas with uninterpreted functions ===== ===== Proving formulas with uninterpreted functions =====
 +
  
  
Line 314: Line 315:
   a ≡ b (mod n) is a congruence in respect to addition. Indeed:   a ≡ b (mod n) is a congruence in respect to addition. Indeed:
  
- a ≡ b (mod n) ∧ c ≡ d (mod n) -> a + c ≡ b + d (mod n)+  ​a ≡ b (mod n) ∧ c ≡ d (mod n) -> a + c ≡ b + d (mod n)
  
 Equality is a congruence with respect to all function symbols. Equality is a congruence with respect to all function symbols.