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

Removed obsolete code.

#2 := false
#9 := 0::int
decl uf_3 :: int
#21 := uf_3
#130 := -1::int
#131 := (* -1::int uf_3)
#154 := (>= uf_3 0::int)
#161 := (ite #154 uf_3 #131)
#648 := (* -1::int #161)
#651 := (+ #131 #648)
#657 := (<= #651 0::int)
#341 := (= #131 #161)
#155 := (not #154)
#649 := (+ uf_3 #648)
#650 := (<= #649 0::int)
#254 := (= uf_3 #161)
#646 := [hypothesis]: #154
#255 := (or #155 #254)
#342 := [def-axiom]: #255
#652 := [unit-resolution #342 #646]: #254
#290 := (not #254)
#653 := (or #290 #650)
#655 := [th-lemma]: #653
#295 := [unit-resolution #655 #652]: #650
#346 := (>= #161 0::int)
#274 := (not #346)
decl uf_2 :: (-> T1 int)
decl uf_1 :: (-> int T1)
#166 := (uf_1 #161)
#169 := (uf_2 #166)
#172 := (= #161 #169)
#175 := (not #172)
#23 := (- uf_3)
#22 := (< uf_3 0::int)
#24 := (ite #22 #23 uf_3)
#25 := (uf_1 #24)
#26 := (uf_2 #25)
#27 := (= #26 #24)
#28 := (not #27)
#178 := (iff #28 #175)
#134 := (ite #22 #131 uf_3)
#137 := (uf_1 #134)
#140 := (uf_2 #137)
#146 := (= #134 #140)
#151 := (not #146)
#176 := (iff #151 #175)
#173 := (iff #146 #172)
#170 := (= #140 #169)
#167 := (= #137 #166)
#164 := (= #134 #161)
#158 := (ite #155 #131 uf_3)
#162 := (= #158 #161)
#163 := [rewrite]: #162
#159 := (= #134 #158)
#156 := (iff #22 #155)
#157 := [rewrite]: #156
#160 := [monotonicity #157]: #159
#165 := [trans #160 #163]: #164
#168 := [monotonicity #165]: #167
#171 := [monotonicity #168]: #170
#174 := [monotonicity #165 #171]: #173
#177 := [monotonicity #174]: #176
#152 := (iff #28 #151)
#149 := (iff #27 #146)
#143 := (= #140 #134)
#147 := (iff #143 #146)
#148 := [rewrite]: #147
#144 := (iff #27 #143)
#135 := (= #24 #134)
#132 := (= #23 #131)
#133 := [rewrite]: #132
#136 := [monotonicity #133]: #135
#141 := (= #26 #140)
#138 := (= #25 #137)
#139 := [monotonicity #136]: #138
#142 := [monotonicity #139]: #141
#145 := [monotonicity #142 #136]: #144
#150 := [trans #145 #148]: #149
#153 := [monotonicity #150]: #152
#179 := [trans #153 #177]: #178
#129 := [asserted]: #28
#180 := [mp #129 #179]: #175
#10 := (:var 0 int)
#12 := (uf_1 #10)
#678 := (pattern #12)
#70 := (>= #10 0::int)
#71 := (not #70)
#13 := (uf_2 #12)
#52 := (= #10 #13)
#77 := (or #52 #71)
#679 := (forall (vars (?x2 int)) (:pat #678) #77)
#82 := (forall (vars (?x2 int)) #77)
#682 := (iff #82 #679)
#680 := (iff #77 #77)
#681 := [refl]: #680
#683 := [quant-intro #681]: #682
#183 := (~ #82 #82)
#195 := (~ #77 #77)
#196 := [refl]: #195
#181 := [nnf-pos #196]: #183
#14 := (= #13 #10)
#11 := (<= 0::int #10)
#15 := (implies #11 #14)
#16 := (forall (vars (?x2 int)) #15)
#85 := (iff #16 #82)
#59 := (not #11)
#60 := (or #59 #52)
#65 := (forall (vars (?x2 int)) #60)
#83 := (iff #65 #82)
#80 := (iff #60 #77)
#74 := (or #71 #52)
#78 := (iff #74 #77)
#79 := [rewrite]: #78
#75 := (iff #60 #74)
#72 := (iff #59 #71)
#68 := (iff #11 #70)
#69 := [rewrite]: #68
#73 := [monotonicity #69]: #72
#76 := [monotonicity #73]: #75
#81 := [trans #76 #79]: #80
#84 := [quant-intro #81]: #83
#66 := (iff #16 #65)
#63 := (iff #15 #60)
#56 := (implies #11 #52)
#61 := (iff #56 #60)
#62 := [rewrite]: #61
#57 := (iff #15 #56)
#54 := (iff #14 #52)
#55 := [rewrite]: #54
#58 := [monotonicity #55]: #57
#64 := [trans #58 #62]: #63
#67 := [quant-intro #64]: #66
#86 := [trans #67 #84]: #85
#51 := [asserted]: #16
#87 := [mp #51 #86]: #82
#197 := [mp~ #87 #181]: #82
#684 := [mp #197 #683]: #679
#321 := (not #679)
#451 := (or #321 #172 #274)
#327 := (or #172 #274)
#658 := (or #321 #327)
#333 := (iff #658 #451)
#665 := [rewrite]: #333
#332 := [quant-inst]: #658
#666 := [mp #332 #665]: #451
#296 := [unit-resolution #666 #684 #180]: #274
#656 := [th-lemma #646 #296 #295]: false
#654 := [lemma #656]: #155
#256 := (or #154 #341)
#343 := [def-axiom]: #256
#644 := [unit-resolution #343 #654]: #341
#366 := (not #341)
#367 := (or #366 #657)
#368 := [th-lemma]: #367
#369 := [unit-resolution #368 #644]: #657
#647 := (<= #161 0::int)
#262 := (or #647 #346)
#639 := [th-lemma]: #262
#640 := [unit-resolution #639 #296]: #647
[th-lemma #654 #640 #369]: false
unsat