a:
q*. a E a5. Sym x,y:
q*. x E y & Trans x,y:q*. x E y6.
x,y:q*. Dec(x E y)7. q = 0
8. x:
q*9. y:
q*
(nil E nil) 
nil = nil 
q*
0 < qq*
q*Propq*;x,y.x E y) & Sym x,y:q*. x E y & Trans x,y:q*. x E yx,y:q*. Dec(x E y)q*q* (nil E nil) nil = nil q*| 1 | 4. a:q*. a E a 5. Sym x,y: q*. x E y & Trans x,y:q*. x E y6. x,y:q*. Dec(x E y)7. q = 0 8. x: q*9. y: q* (nil E nil) nil = nil q* |
About:
 |  |  |  |  |
 |  |  |  |  |