equal
deleted
inserted
replaced
10 consts |
10 consts |
11 "'/" :: "[i,i]=>i" (infixl 90) (*set of equiv classes*) |
11 "'/" :: "[i,i]=>i" (infixl 90) (*set of equiv classes*) |
12 congruent :: "[i,i=>i]=>o" |
12 congruent :: "[i,i=>i]=>o" |
13 congruent2 :: "[i,[i,i]=>i]=>o" |
13 congruent2 :: "[i,[i,i]=>i]=>o" |
14 |
14 |
15 rules |
15 defs |
16 quotient_def "A/r == {r``{x} . x:A}" |
16 quotient_def "A/r == {r``{x} . x:A}" |
17 congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)" |
17 congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)" |
18 |
18 |
19 congruent2_def |
19 congruent2_def |
20 "congruent2(r,b) == ALL y1 z1 y2 z2. \ |
20 "congruent2(r,b) == ALL y1 z1 y2 z2. \ |