diff options
Diffstat (limited to 'proofs/signatures/smt.plf')
-rw-r--r-- | proofs/signatures/smt.plf | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 6d04c3004..38428dd1e 100644 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -80,6 +80,30 @@ (! f formula (term Bool))) +(declare true_preds_equal + (! x1 (term Bool) + (! x2 (term Bool) + (! u1 (th_holds (p_app x1)) + (! u2 (th_holds (p_app x2)) + (th_holds (= Bool x1 x2))))))) + +(declare false_preds_equal + (! x1 (term Bool) + (! x2 (term Bool) + (! u1 (th_holds (not (p_app x1))) + (! u2 (th_holds (not (p_app x2))) + (th_holds (= Bool x1 x2))))))) + +(declare pred_refl_pos + (! x1 (term Bool) + (! u1 (th_holds (p_app x1)) + (th_holds (= Bool x1 x1))))) + +(declare pred_refl_neg + (! x1 (term Bool) + (! u1 (th_holds (not (p_app x1))) + (th_holds (= Bool x1 x1))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; ; CNF Clausification |