101 "(P | True) = True", "(True | P) = True", |
101 "(P | True) = True", "(True | P) = True", |
102 "(P | False) = P", "(False | P) = P", |
102 "(P | False) = P", "(False | P) = P", |
103 "(P | P) = P", "(P | (P | Q)) = (P | Q)", |
103 "(P | P) = P", "(P | (P | Q)) = (P | Q)", |
104 "((~P) = (~Q)) = (P=Q)", |
104 "((~P) = (~Q)) = (P=Q)", |
105 "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", |
105 "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", |
106 "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", |
106 "(? x. x=t & P(x)) = P(t)", (*"(? x. t=x & P(x)) = P(t)",*) |
107 "(! x. t=x --> P(x)) = P(t)" ]; |
107 "(! x. t=x --> P(x)) = P(t)" ]; |
108 |
108 |
109 (*Add congruence rules for = (instead of ==) *) |
109 (*Add congruence rules for = (instead of ==) *) |
110 infix 4 addcongs delcongs; |
110 infix 4 addcongs delcongs; |
111 fun ss addcongs congs = ss addeqcongs (map standard (congs RL [eq_reflection])); |
111 fun ss addcongs congs = ss addeqcongs (map standard (congs RL [eq_reflection])); |