equal
deleted
inserted
replaced
369 "(P \<longrightarrow> P) = True" |
369 "(P \<longrightarrow> P) = True" |
370 "(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)" |
370 "(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)" |
371 by auto |
371 by auto |
372 |
372 |
373 lemma [z3_rule]: |
373 lemma [z3_rule]: |
374 "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not> P)))" |
374 "((P = Q) \<longrightarrow> R) = (R \<or> (Q = (\<not> P)))" |
375 by auto |
375 by auto |
376 |
376 |
377 lemma [z3_rule]: |
377 lemma [z3_rule]: |
378 "(\<not> True) = False" |
378 "(\<not> True) = False" |
379 "(\<not> False) = True" |
379 "(\<not> False) = True" |