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

merged

#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 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
#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
#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
unsat