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

merged

#2 := false
decl uf_6 :: (-> T4 T2)
decl uf_10 :: T4
#39 := uf_10
#44 := (uf_6 uf_10)
decl uf_2 :: (-> T1 T2)
decl uf_7 :: T1
#34 := uf_7
#43 := (uf_2 uf_7)
#45 := (= #43 #44)
decl uf_4 :: (-> T3 T2 T4)
decl uf_8 :: T2
#35 := uf_8
decl uf_9 :: T3
#36 := uf_9
#40 := (uf_4 uf_9 uf_8)
#204 := (uf_6 #40)
#598 := (= #204 #44)
#595 := (= #44 #204)
#41 := (= uf_10 #40)
decl uf_1 :: (-> T2 T3 T1)
#37 := (uf_1 uf_8 uf_9)
#38 := (= uf_7 #37)
#42 := (and #38 #41)
#109 := [asserted]: #42
#114 := [and-elim #109]: #41
#256 := [monotonicity #114]: #595
#599 := [symm #256]: #598
#596 := (= #43 #204)
#269 := (= uf_8 #204)
#23 := (:var 0 T2)
#22 := (:var 1 T3)
#24 := (uf_4 #22 #23)
#643 := (pattern #24)
#25 := (uf_6 #24)
#86 := (= #23 #25)
#644 := (forall (vars (?x5 T3) (?x6 T2)) (:pat #643) #86)
#90 := (forall (vars (?x5 T3) (?x6 T2)) #86)
#647 := (iff #90 #644)
#645 := (iff #86 #86)
#646 := [refl]: #645
#648 := [quant-intro #646]: #647
#119 := (~ #90 #90)
#144 := (~ #86 #86)
#145 := [refl]: #144
#120 := [nnf-pos #145]: #119
#26 := (= #25 #23)
#27 := (forall (vars (?x5 T3) (?x6 T2)) #26)
#91 := (iff #27 #90)
#88 := (iff #26 #86)
#89 := [rewrite]: #88
#92 := [quant-intro #89]: #91
#85 := [asserted]: #27
#95 := [mp #85 #92]: #90
#146 := [mp~ #95 #120]: #90
#649 := [mp #146 #648]: #644
#613 := (not #644)
#619 := (or #613 #269)
#609 := [quant-inst]: #619
#267 := [unit-resolution #609 #649]: #269
#600 := (= #43 uf_8)
#289 := (uf_2 #37)
#259 := (= #289 uf_8)
#296 := (= uf_8 #289)
#17 := (:var 0 T3)
#16 := (:var 1 T2)
#18 := (uf_1 #16 #17)
#636 := (pattern #18)
#28 := (uf_2 #18)
#94 := (= #16 #28)
#650 := (forall (vars (?x7 T2) (?x8 T3)) (:pat #636) #94)
#98 := (forall (vars (?x7 T2) (?x8 T3)) #94)
#653 := (iff #98 #650)
#651 := (iff #94 #94)
#652 := [refl]: #651
#654 := [quant-intro #652]: #653
#121 := (~ #98 #98)
#147 := (~ #94 #94)
#148 := [refl]: #147
#122 := [nnf-pos #148]: #121
#29 := (= #28 #16)
#30 := (forall (vars (?x7 T2) (?x8 T3)) #29)
#99 := (iff #30 #98)
#96 := (iff #29 #94)
#97 := [rewrite]: #96
#100 := [quant-intro #97]: #99
#93 := [asserted]: #30
#103 := [mp #93 #100]: #98
#149 := [mp~ #103 #122]: #98
#655 := [mp #149 #654]: #650
#615 := (not #650)
#616 := (or #615 #296)
#617 := [quant-inst]: #616
#618 := [unit-resolution #617 #655]: #296
#597 := [symm #618]: #259
#611 := (= #43 #289)
#113 := [and-elim #109]: #38
#252 := [monotonicity #113]: #611
#601 := [trans #252 #597]: #600
#602 := [trans #601 #267]: #596
#238 := [trans #602 #599]: #45
#46 := (not #45)
#110 := [asserted]: #46
[unit-resolution #110 #238]: false
unsat