src/HOL/SMT/Examples/cert/z3_hol_03.proof

--- a/src/HOL/SMT/Examples/cert/z3_hol_03.proof	Tue Dec 01 22:29:46 2009 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_hol_03.proof	Thu Dec 03 15:56:06 2009 +0100
@@ -1,120 +1,115 @@
 #2 := false
-decl uf_1 :: (-> T1 T1)
-decl uf_4 :: T1
-#15 := uf_4
-#16 := (uf_1 uf_4)
-#48 := (= uf_4 #16)
-#83 := (not #48)
-decl uf_2 :: (-> T2 T2)
+decl up_2 :: (-> T2 bool)
 decl uf_3 :: T2
 #10 := uf_3
-#18 := (uf_2 uf_3)
-#51 := (= uf_3 #18)
-#84 := (not #51)
-#556 := [hypothesis]: #84
-#8 := (:var 0 T2)
-#9 := (uf_2 #8)
-#575 := (pattern #9)
-#12 := (= #8 uf_3)
-#11 := (= #9 uf_3)
-#13 := (iff #11 #12)
-#576 := (forall (vars (?x2 T2)) (:pat #575) #13)
-#14 := (forall (vars (?x2 T2)) #13)
-#579 := (iff #14 #576)
-#577 := (iff #13 #13)
-#578 := [refl]: #577
-#580 := [quant-intro #578]: #579
-#70 := (~ #14 #14)
-#80 := (~ #13 #13)
-#81 := [refl]: #80
-#67 := [nnf-pos #81]: #70
-#45 := [asserted]: #14
-#82 := [mp~ #45 #67]: #14
-#581 := [mp #82 #580]: #576
-#242 := (not #576)
-#170 := (or #242 #51)
-#150 := (= uf_3 uf_3)
-#19 := (= #18 uf_3)
-#237 := (iff #19 #150)
-#243 := (or #242 #237)
-#244 := (iff #243 #170)
-#560 := (iff #170 #170)
-#562 := [rewrite]: #560
-#230 := (iff #237 #51)
-#1 := true
-#54 := (iff #51 true)
-#57 := (iff #54 #51)
-#58 := [rewrite]: #57
-#152 := (iff #237 #54)
-#151 := (iff #150 true)
-#238 := [rewrite]: #151
-#52 := (iff #19 #51)
-#53 := [rewrite]: #52
-#239 := [monotonicity #53 #238]: #152
-#241 := [trans #239 #58]: #230
-#223 := [monotonicity #241]: #244
-#217 := [trans #223 #562]: #244
-#240 := [quant-inst]: #243
-#349 := [mp #240 #217]: #170
-#228 := [unit-resolution #349 #581 #556]: false
-#229 := [lemma #228]: #51
-#71 := (or #83 #84)
-#61 := (and #48 #51)
-#64 := (not #61)
-#90 := (iff #64 #71)
-#72 := (not #71)
-#85 := (not #72)
-#88 := (iff #85 #71)
-#89 := [rewrite]: #88
-#86 := (iff #64 #85)
-#73 := (iff #61 #72)
-#74 := [rewrite]: #73
-#87 := [monotonicity #74]: #86
-#91 := [trans #87 #89]: #90
-#20 := (iff #19 true)
-#17 := (= #16 uf_4)
-#21 := (and #17 #20)
-#22 := (not #21)
-#65 := (iff #22 #64)
-#62 := (iff #21 #61)
-#59 := (iff #20 #51)
-#55 := (iff #20 #54)
-#56 := [monotonicity #53]: #55
-#60 := [trans #56 #58]: #59
-#49 := (iff #17 #48)
-#50 := [rewrite]: #49
-#63 := [monotonicity #50 #60]: #62
-#66 := [monotonicity #63]: #65
-#46 := [asserted]: #22
-#69 := [mp #46 #66]: #64
-#92 := [mp #69 #91]: #71
-#563 := [unit-resolution #92 #229]: #83
+#17 := (up_2 uf_3)
+#78 := (not #17)
+decl uf_1 :: (-> T1 T1)
+decl uf_4 :: T1
+#14 := uf_4
+#15 := (uf_1 uf_4)
+#46 := (= uf_4 #15)
+#79 := (not #46)
+#145 := [hypothesis]: #79
 #4 := (:var 0 T1)
 #5 := (uf_1 #4)
-#568 := (pattern #5)
-#39 := (= #4 #5)
-#569 := (forall (vars (?x1 T1)) (:pat #568) #39)
-#42 := (forall (vars (?x1 T1)) #39)
-#572 := (iff #42 #569)
-#570 := (iff #39 #39)
-#571 := [refl]: #570
-#573 := [quant-intro #571]: #572
-#77 := (~ #42 #42)
-#75 := (~ #39 #39)
-#76 := [refl]: #75
-#78 := [nnf-pos #76]: #77
+#563 := (pattern #5)
+#37 := (= #4 #5)
+#564 := (forall (vars (?x1 T1)) (:pat #563) #37)
+#40 := (forall (vars (?x1 T1)) #37)
+#567 := (iff #40 #564)
+#565 := (iff #37 #37)
+#566 := [refl]: #565
+#568 := [quant-intro #566]: #567
+#72 := (~ #40 #40)
+#70 := (~ #37 #37)
+#71 := [refl]: #70
+#73 := [nnf-pos #71]: #72
 #6 := (= #5 #4)
 #7 := (forall (vars (?x1 T1)) #6)
-#43 := (iff #7 #42)
-#40 := (iff #6 #39)
-#41 := [rewrite]: #40
-#44 := [quant-intro #41]: #43
-#38 := [asserted]: #7
-#47 := [mp #38 #44]: #42
-#79 := [mp~ #47 #78]: #42
-#574 := [mp #79 #573]: #569
-#565 := (not #569)
-#566 := (or #565 #48)
-#561 := [quant-inst]: #566
-[unit-resolution #561 #574 #563]: false
+#41 := (iff #7 #40)
+#38 := (iff #6 #37)
+#39 := [rewrite]: #38
+#42 := [quant-intro #39]: #41
+#36 := [asserted]: #7
+#45 := [mp #36 #42]: #40
+#74 := [mp~ #45 #73]: #40
+#569 := [mp #74 #568]: #564
+#146 := (not #564)
+#233 := (or #146 #46)
+#147 := [quant-inst]: #233
+#232 := [unit-resolution #147 #569 #145]: false
+#234 := [lemma #232]: #46
+#66 := (or #78 #79)
+#54 := (and #17 #46)
+#59 := (not #54)
+#85 := (iff #59 #66)
+#67 := (not #66)
+#80 := (not #67)
+#83 := (iff #80 #66)
+#84 := [rewrite]: #83
+#81 := (iff #59 #80)
+#68 := (iff #54 #67)
+#69 := [rewrite]: #68
+#82 := [monotonicity #69]: #81
+#86 := [trans #82 #84]: #85
+#1 := true
+#18 := (iff #17 true)
+#16 := (= #15 uf_4)
+#19 := (and #16 #18)
+#20 := (not #19)
+#60 := (iff #20 #59)
+#57 := (iff #19 #54)
+#51 := (and #46 #17)
+#55 := (iff #51 #54)
+#56 := [rewrite]: #55
+#52 := (iff #19 #51)
+#49 := (iff #18 #17)
+#50 := [rewrite]: #49
+#47 := (iff #16 #46)
+#48 := [rewrite]: #47
+#53 := [monotonicity #48 #50]: #52
+#58 := [trans #53 #56]: #57
+#61 := [monotonicity #58]: #60
+#44 := [asserted]: #20
+#64 := [mp #44 #61]: #59
+#87 := [mp #64 #86]: #66
+#561 := [unit-resolution #87 #234]: #78
+#8 := (:var 0 T2)
+#9 := (up_2 #8)
+#570 := (pattern #9)
+#11 := (= #8 uf_3)
+#12 := (iff #9 #11)
+#571 := (forall (vars (?x2 T2)) (:pat #570) #12)
+#13 := (forall (vars (?x2 T2)) #12)
+#574 := (iff #13 #571)
+#572 := (iff #12 #12)
+#573 := [refl]: #572
+#575 := [quant-intro #573]: #574
+#65 := (~ #13 #13)
+#75 := (~ #12 #12)
+#76 := [refl]: #75
+#62 := [nnf-pos #76]: #65
+#43 := [asserted]: #13
+#77 := [mp~ #43 #62]: #13
+#576 := [mp #77 #575]: #571
+#555 := (not #571)
+#557 := (or #555 #17)
+#225 := (= uf_3 uf_3)
+#236 := (iff #17 #225)
+#212 := (or #555 #236)
+#551 := (iff #212 #557)
+#224 := (iff #557 #557)
+#558 := [rewrite]: #224
+#239 := (iff #236 #17)
+#238 := (iff #236 #18)
+#237 := (iff #225 true)
+#165 := [rewrite]: #237
+#235 := [monotonicity #165]: #238
+#218 := [trans #235 #50]: #239
+#223 := [monotonicity #218]: #551
+#559 := [trans #223 #558]: #551
+#344 := [quant-inst]: #212
+#560 := [mp #344 #559]: #557
+[unit-resolution #560 #576 #561]: false
 unsat