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

tuned structure; moved non-related quickcheck.setup to Code_Generator.thy

#2 := false
decl up_1 :: (-> T1 T2 bool)
#5 := (:var 0 T2)
decl uf_4 :: T1
#18 := uf_4
#19 := (up_1 uf_4 #5)
#635 := (pattern #19)
#116 := (not #19)
#636 := (forall (vars (?x6 T2)) (:pat #635) #116)
decl uf_3 :: T2
#14 := uf_3
#21 := (up_1 uf_4 uf_3)
decl uf_2 :: T1
#7 := uf_2
#195 := (= uf_2 uf_4)
#602 := (iff #21 #195)
#4 := (:var 1 T1)
#6 := (up_1 #4 #5)
#612 := (pattern #6)
#8 := (= #4 uf_2)
#9 := (iff #6 #8)
#613 := (forall (vars (?x1 T1) (?x2 T2)) (:pat #612) #9)
#10 := (forall (vars (?x1 T1) (?x2 T2)) #9)
#616 := (iff #10 #613)
#614 := (iff #9 #9)
#615 := [refl]: #614
#617 := [quant-intro #615]: #616
#56 := (~ #10 #10)
#54 := (~ #9 #9)
#55 := [refl]: #54
#57 := [nnf-pos #55]: #56
#39 := [asserted]: #10
#58 := [mp~ #39 #57]: #10
#618 := [mp #58 #617]: #613
#286 := (not #613)
#244 := (or #286 #602)
#194 := (= uf_4 uf_2)
#264 := (iff #21 #194)
#587 := (or #286 #264)
#249 := (iff #587 #244)
#251 := (iff #244 #244)
#589 := [rewrite]: #251
#260 := (iff #264 #602)
#282 := (iff #194 #195)
#196 := [rewrite]: #282
#603 := [monotonicity #196]: #260
#250 := [monotonicity #603]: #249
#590 := [trans #250 #589]: #249
#248 := [quant-inst]: #587
#591 := [mp #248 #590]: #244
#598 := [unit-resolution #591 #618]: #602
decl ?x6!3 :: T2
#63 := ?x6!3
#64 := (up_1 uf_4 ?x6!3)
#283 := (iff #64 #195)
#214 := (or #286 #283)
#281 := (iff #64 #194)
#287 := (or #286 #281)
#288 := (iff #287 #214)
#604 := (iff #214 #214)
#606 := [rewrite]: #604
#274 := (iff #281 #283)
#285 := [monotonicity #196]: #274
#267 := [monotonicity #285]: #288
#261 := [trans #267 #606]: #288
#284 := [quant-inst]: #287
#393 := [mp #284 #261]: #214
#596 := [unit-resolution #393 #618]: #283
#600 := (not #283)
#586 := (or #600 #195)
#122 := (not #21)
#599 := [hypothesis]: #122
#127 := (or #21 #64)
#119 := (forall (vars (?x6 T2)) #116)
#128 := (or #122 #119)
#135 := (and #127 #128)
#129 := (and #128 #127)
#136 := (iff #129 #135)
#137 := [rewrite]: #136
#20 := (exists (vars (?x6 T2)) #19)
#42 := (not #20)
#43 := (iff #21 #42)
#130 := (~ #43 #129)
#120 := (~ #42 #119)
#117 := (~ #116 #116)
#118 := [refl]: #117
#121 := [nnf-neg #118]: #120
#113 := (not #42)
#114 := (~ #113 #64)
#88 := (~ #20 #64)
#89 := [sk]: #88
#115 := [nnf-neg #89]: #114
#125 := (~ #21 #21)
#126 := [refl]: #125
#123 := (~ #122 #122)
#124 := [refl]: #123
#131 := [nnf-pos #124 #126 #115 #121]: #130
#22 := (iff #20 #21)
#23 := (not #22)
#44 := (iff #23 #43)
#45 := [rewrite]: #44
#41 := [asserted]: #23
#48 := [mp #41 #45]: #43
#132 := [mp~ #48 #131]: #129
#133 := [mp #132 #137]: #135
#134 := [and-elim #133]: #127
#585 := [unit-resolution #134 #599]: #64
#608 := (not #64)
#609 := (or #600 #608 #195)
#610 := [def-axiom]: #609
#292 := [unit-resolution #610 #585]: #586
#308 := [unit-resolution #292 #596]: #195
#272 := (not #195)
#592 := (not #602)
#309 := (or #592 #272)
#593 := (or #592 #21 #272)
#588 := [def-axiom]: #593
#310 := [unit-resolution #588 #599]: #309
#296 := [unit-resolution #310 #308 #598]: false
#311 := [lemma #296]: #21
#641 := (or #122 #636)
#642 := (iff #128 #641)
#639 := (iff #119 #636)
#637 := (iff #116 #116)
#638 := [refl]: #637
#640 := [quant-intro #638]: #639
#643 := [monotonicity #640]: #642
#138 := [and-elim #133]: #128
#644 := [mp #138 #643]: #641
#594 := [unit-resolution #644 #311]: #636
#595 := (not #636)
#597 := (or #595 #122)
#235 := [quant-inst]: #597
[unit-resolution #235 #311 #594]: false
unsat