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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_arith_quant_13.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,180 @@
+#2 := false
+#4 := 0::int
+#5 := (:var 0 int)
+#48 := (<= #5 0::int)
+#49 := (not #48)
+#45 := (>= #5 0::int)
+#44 := (not #45)
+#52 := (or #44 #49)
+#55 := (forall (vars (?x1 int)) #52)
+#86 := (not #55)
+#604 := (<= 0::int 0::int)
+#264 := (not #604)
+#269 := (>= 0::int 0::int)
+#605 := (not #269)
+#265 := (or #605 #264)
+#588 := (or #86 #265)
+#584 := (iff #588 #86)
+#311 := (or #86 false)
+#314 := (iff #311 #86)
+#208 := [rewrite]: #314
+#312 := (iff #588 #311)
+#599 := (iff #265 false)
+#598 := (or false false)
+#241 := (iff #598 false)
+#601 := [rewrite]: #241
+#600 := (iff #265 #598)
+#597 := (iff #264 false)
+#1 := true
+#590 := (not true)
+#255 := (iff #590 false)
+#256 := [rewrite]: #255
+#596 := (iff #264 #590)
+#594 := (iff #604 true)
+#595 := [rewrite]: #594
+#591 := [monotonicity #595]: #596
+#235 := [trans #591 #256]: #597
+#592 := (iff #605 false)
+#253 := (iff #605 #590)
+#606 := (iff #269 true)
+#249 := [rewrite]: #606
+#254 := [monotonicity #249]: #253
+#593 := [trans #254 #256]: #592
+#240 := [monotonicity #593 #235]: #600
+#602 := [trans #240 #601]: #599
+#313 := [monotonicity #602]: #312
+#585 := [trans #313 #208]: #584
+#589 := [quant-inst]: #588
+#307 := [mp #589 #585]: #86
+decl z3name!0 :: bool
+#83 := z3name!0
+#12 := 3::int
+#32 := -1::int
+#92 := (ite z3name!0 -1::int 3::int)
+#290 := (= #92 3::int)
+#610 := (not #290)
+#607 := (>= #92 3::int)
+#609 := (not #607)
+#95 := (<= #92 0::int)
+#58 := (ite #55 -1::int 3::int)
+#64 := (<= #58 0::int)
+#96 := (~ #64 #95)
+#93 := (= #58 #92)
+#90 := (~ #55 z3name!0)
+#87 := (or z3name!0 #86)
+#84 := (not z3name!0)
+#85 := (or #84 #55)
+#88 := (and #85 #87)
+#89 := [intro-def]: #88
+#91 := [apply-def #89]: #90
+#94 := [monotonicity #91]: #93
+#97 := [monotonicity #94]: #96
+#10 := 1::int
+#11 := (- 1::int)
+#7 := (< 0::int #5)
+#6 := (< #5 0::int)
+#8 := (or #6 #7)
+#9 := (forall (vars (?x1 int)) #8)
+#13 := (ite #9 #11 3::int)
+#14 := (< 0::int #13)
+#15 := (not #14)
+#77 := (iff #15 #64)
+#35 := (ite #9 -1::int 3::int)
+#38 := (< 0::int #35)
+#41 := (not #38)
+#75 := (iff #41 #64)
+#65 := (not #64)
+#70 := (not #65)
+#73 := (iff #70 #64)
+#74 := [rewrite]: #73
+#71 := (iff #41 #70)
+#68 := (iff #38 #65)
+#61 := (< 0::int #58)
+#66 := (iff #61 #65)
+#67 := [rewrite]: #66
+#62 := (iff #38 #61)
+#59 := (= #35 #58)
+#56 := (iff #9 #55)
+#53 := (iff #8 #52)
+#50 := (iff #7 #49)
+#51 := [rewrite]: #50
+#46 := (iff #6 #44)
+#47 := [rewrite]: #46
+#54 := [monotonicity #47 #51]: #53
+#57 := [quant-intro #54]: #56
+#60 := [monotonicity #57]: #59
+#63 := [monotonicity #60]: #62
+#69 := [trans #63 #67]: #68
+#72 := [monotonicity #69]: #71
+#76 := [trans #72 #74]: #75
+#42 := (iff #15 #41)
+#39 := (iff #14 #38)
+#36 := (= #13 #35)
+#33 := (= #11 -1::int)
+#34 := [rewrite]: #33
+#37 := [monotonicity #34]: #36
+#40 := [monotonicity #37]: #39
+#43 := [monotonicity #40]: #42
+#78 := [trans #43 #76]: #77
+#31 := [asserted]: #15
+#79 := [mp #31 #78]: #64
+#126 := [mp~ #79 #97]: #95
+#266 := (not #95)
+#396 := (or #609 #266)
+#603 := [th-lemma]: #396
+#277 := [unit-resolution #603 #126]: #609
+#278 := [hypothesis]: #290
+#611 := (or #610 #607)
+#612 := [th-lemma]: #611
+#613 := [unit-resolution #612 #278 #277]: false
+#608 := [lemma #613]: #610
+#289 := (or z3name!0 #290)
+#293 := [def-axiom]: #289
+#308 := [unit-resolution #293 #608]: z3name!0
+#129 := (or #55 #84)
+decl ?x1!1 :: int
+#108 := ?x1!1
+#111 := (>= ?x1!1 0::int)
+#112 := (not #111)
+#109 := (<= ?x1!1 0::int)
+#110 := (not #109)
+#132 := (or #110 #112)
+#135 := (not #132)
+#138 := (or z3name!0 #135)
+#141 := (and #129 #138)
+#113 := (or #112 #110)
+#114 := (not #113)
+#119 := (or z3name!0 #114)
+#122 := (and #85 #119)
+#142 := (iff #122 #141)
+#139 := (iff #119 #138)
+#136 := (iff #114 #135)
+#133 := (iff #113 #132)
+#134 := [rewrite]: #133
+#137 := [monotonicity #134]: #136
+#140 := [monotonicity #137]: #139
+#130 := (iff #85 #129)
+#131 := [rewrite]: #130
+#143 := [monotonicity #131 #140]: #142
+#123 := (~ #88 #122)
+#120 := (~ #87 #119)
+#115 := (~ #86 #114)
+#116 := [sk]: #115
+#106 := (~ z3name!0 z3name!0)
+#107 := [refl]: #106
+#121 := [monotonicity #107 #116]: #120
+#104 := (~ #85 #85)
+#102 := (~ #55 #55)
+#100 := (~ #52 #52)
+#101 := [refl]: #100
+#103 := [nnf-pos #101]: #102
+#98 := (~ #84 #84)
+#99 := [refl]: #98
+#105 := [monotonicity #99 #103]: #104
+#124 := [monotonicity #105 #121]: #123
+#125 := [mp~ #89 #124]: #122
+#127 := [mp #125 #143]: #141
+#128 := [and-elim #127]: #129
+#582 := [unit-resolution #128 #308]: #55
+[unit-resolution #582 #307]: false
+unsat