equal
deleted
inserted
replaced
1048 "(P & ~P) = False" "(~P & P) = False" |
1048 "(P & ~P) = False" "(~P & P) = False" |
1049 "(P | True) = True" "(True | P) = True" |
1049 "(P | True) = True" "(True | P) = True" |
1050 "(P | False) = P" "(False | P) = P" |
1050 "(P | False) = P" "(False | P) = P" |
1051 "(P | P) = P" "(P | (P | Q)) = (P | Q)" and |
1051 "(P | P) = P" "(P | (P | Q)) = (P | Q)" and |
1052 "(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" |
1052 "(ALL x. P) = P" "(EX x. P) = P" "EX x. x=t" "EX x. t=x" |
1053 -- {* needed for the one-point-rule quantifier simplification procs *} |
1053 and |
1054 -- {* essential for termination!! *} and |
|
1055 "!!P. (EX x. x=t & P(x)) = P(t)" |
1054 "!!P. (EX x. x=t & P(x)) = P(t)" |
1056 "!!P. (EX x. t=x & P(x)) = P(t)" |
1055 "!!P. (EX x. t=x & P(x)) = P(t)" |
1057 "!!P. (ALL x. x=t --> P(x)) = P(t)" |
1056 "!!P. (ALL x. x=t --> P(x)) = P(t)" |
1058 "!!P. (ALL x. t=x --> P(x)) = P(t)" |
1057 "!!P. (ALL x. t=x --> P(x)) = P(t)" |
1059 by (blast, blast, blast, blast, blast, iprover+) |
1058 by (blast, blast, blast, blast, blast, iprover+) |