diff options
| author | guykatzz <katz911@gmail.com> | 2017-03-09 14:46:33 -0800 |
|---|---|---|
| committer | guykatzz <katz911@gmail.com> | 2017-03-09 14:46:33 -0800 |
| commit | 58df458f5c5c8d318254f8d6b3b43b42883445d8 (patch) | |
| tree | 8d2854fc47c20acc7233fc32b89b2d0782135d10 /proofs/signatures/smt.plf | |
| parent | 2f287a59e9c775d9087cddd8c72be5169c2706e1 (diff) | |
bug fix
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 |