equal
deleted
inserted
replaced
15 defs |
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. |
21 \ <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)" |
21 <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)" |
22 |
22 |
23 end |
23 end |