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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_hol_01.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,181 @@
+#2 := false
+decl uf_1 :: (-> T1 T2 T3)
+decl uf_3 :: T2
+#22 := uf_3
+decl uf_6 :: T1
+#30 := uf_6
+#36 := (uf_1 uf_6 uf_3)
+decl uf_2 :: (-> T1 T2 T3 T1)
+decl uf_8 :: T3
+#33 := uf_8
+decl uf_5 :: T2
+#26 := uf_5
+decl uf_7 :: T3
+#31 := uf_7
+decl uf_4 :: T2
+#23 := uf_4
+#32 := (uf_2 uf_6 uf_4 uf_7)
+#34 := (uf_2 #32 uf_5 uf_8)
+#35 := (uf_1 #34 uf_3)
+#37 := (= #35 #36)
+#223 := (uf_1 #32 uf_4)
+#214 := (uf_2 uf_6 uf_4 #223)
+#552 := (uf_1 #214 uf_3)
+#555 := (= #552 #36)
+#560 := (= #36 #552)
+#556 := (= #223 #552)
+#24 := (= uf_3 uf_4)
+#561 := (ite #24 #556 #560)
+#8 := (:var 0 T2)
+#6 := (:var 1 T3)
+#5 := (:var 2 T2)
+#4 := (:var 3 T1)
+#7 := (uf_2 #4 #5 #6)
+#9 := (uf_1 #7 #8)
+#575 := (pattern #9)
+#11 := (uf_1 #4 #8)
+#100 := (= #9 #11)
+#99 := (= #6 #9)
+#55 := (= #5 #8)
+#83 := (ite #55 #99 #100)
+#576 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) (:pat #575) #83)
+#90 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #83)
+#579 := (iff #90 #576)
+#577 := (iff #83 #83)
+#578 := [refl]: #577
+#580 := [quant-intro #578]: #579
+#58 := (ite #55 #6 #11)
+#61 := (= #9 #58)
+#64 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #61)
+#87 := (iff #64 #90)
+#84 := (iff #61 #83)
+#89 := [rewrite]: #84
+#88 := [quant-intro #89]: #87
+#93 := (~ #64 #64)
+#91 := (~ #61 #61)
+#92 := [refl]: #91
+#94 := [nnf-pos #92]: #93
+#10 := (= #8 #5)
+#12 := (ite #10 #6 #11)
+#13 := (= #9 #12)
+#14 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #13)
+#65 := (iff #14 #64)
+#62 := (iff #13 #61)
+#59 := (= #12 #58)
+#56 := (iff #10 #55)
+#57 := [rewrite]: #56
+#60 := [monotonicity #57]: #59
+#63 := [monotonicity #60]: #62
+#66 := [quant-intro #63]: #65
+#54 := [asserted]: #14
+#69 := [mp #54 #66]: #64
+#95 := [mp~ #69 #94]: #64
+#85 := [mp #95 #88]: #90
+#581 := [mp #85 #580]: #576
+#250 := (not #576)
+#548 := (or #250 #561)
+#551 := (= uf_4 uf_3)
+#557 := (ite #551 #556 #555)
+#549 := (or #250 #557)
+#271 := (iff #549 #548)
+#273 := (iff #548 #548)
+#259 := [rewrite]: #273
+#559 := (iff #557 #561)
+#198 := (iff #555 #560)
+#199 := [rewrite]: #198
+#193 := (iff #551 #24)
+#558 := [rewrite]: #193
+#562 := [monotonicity #558 #199]: #559
+#272 := [monotonicity #562]: #271
+#274 := [trans #272 #259]: #271
+#255 := [quant-inst]: #549
+#165 := [mp #255 #274]: #548
+#510 := [unit-resolution #165 #581]: #561
+#544 := (not #561)
+#497 := (or #544 #560)
+#25 := (not #24)
+#27 := (= uf_3 uf_5)
+#28 := (not #27)
+#29 := (and #25 #28)
+#75 := [asserted]: #29
+#79 := [and-elim #75]: #25
+#268 := (or #544 #24 #560)
+#542 := [def-axiom]: #268
+#499 := [unit-resolution #542 #79]: #497
+#491 := [unit-resolution #499 #510]: #560
+#493 := [symm #491]: #555
+#494 := (= #35 #552)
+#157 := (uf_1 #32 uf_3)
+#503 := (= #157 #552)
+#502 := (= #552 #157)
+#509 := (= #214 #32)
+#415 := (= #223 uf_7)
+#566 := (= uf_7 #223)
+#17 := (:var 0 T3)
+#16 := (:var 1 T2)
+#15 := (:var 2 T1)
+#18 := (uf_2 #15 #16 #17)
+#582 := (pattern #18)
+#19 := (uf_1 #18 #16)
+#68 := (= #17 #19)
+#584 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) (:pat #582) #68)
+#72 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) #68)
+#583 := (iff #72 #584)
+#586 := (iff #584 #584)
+#587 := [rewrite]: #586
+#585 := [rewrite]: #583
+#588 := [trans #585 #587]: #583
+#82 := (~ #72 #72)
+#96 := (~ #68 #68)
+#97 := [refl]: #96
+#78 := [nnf-pos #97]: #82
+#20 := (= #19 #17)
+#21 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) #20)
+#73 := (iff #21 #72)
+#70 := (iff #20 #68)
+#71 := [rewrite]: #70
+#74 := [quant-intro #71]: #73
+#67 := [asserted]: #21
+#77 := [mp #67 #74]: #72
+#98 := [mp~ #77 #78]: #72
+#589 := [mp #98 #588]: #584
+#211 := (not #584)
+#212 := (or #211 #566)
+#213 := [quant-inst]: #212
+#414 := [unit-resolution #213 #589]: #566
+#416 := [symm #414]: #415
+#506 := [monotonicity #416]: #509
+#498 := [monotonicity #506]: #502
+#492 := [symm #498]: #503
+#244 := (= #35 #157)
+#158 := (= uf_8 #35)
+#248 := (ite #27 #158 #244)
+#247 := (or #250 #248)
+#245 := (= uf_5 uf_3)
+#159 := (ite #245 #158 #244)
+#251 := (or #250 #159)
+#567 := (iff #251 #247)
+#224 := (iff #247 #247)
+#356 := [rewrite]: #224
+#249 := (iff #159 #248)
+#246 := (iff #245 #27)
+#237 := [rewrite]: #246
+#177 := [monotonicity #237]: #249
+#569 := [monotonicity #177]: #567
+#563 := [trans #569 #356]: #567
+#230 := [quant-inst]: #251
+#235 := [mp #230 #563]: #247
+#488 := [unit-resolution #235 #581]: #248
+#236 := (not #248)
+#490 := (or #236 #244)
+#80 := [and-elim #75]: #28
+#572 := (or #236 #27 #244)
+#573 := [def-axiom]: #572
+#500 := [unit-resolution #573 #80]: #490
+#501 := [unit-resolution #500 #488]: #244
+#495 := [trans #501 #492]: #494
+#489 := [trans #495 #493]: #37
+#38 := (not #37)
+#76 := [asserted]: #38
+[unit-resolution #76 #489]: false
+unsat