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

code cache without copy; tuned

#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
decl uf_1 :: (-> int T1)
decl uf_3 :: T1
#22 := uf_3
#23 := (uf_2 uf_3)
#21 := 1::int
#24 := (+ 1::int #23)
#25 := (uf_1 #24)
#26 := (uf_2 #25)
#138 := -1::int
#139 := (+ -1::int #26)
#142 := (uf_1 #139)
#289 := (uf_2 #142)
#383 := (* -1::int #289)
#542 := (+ #23 #383)
#544 := (>= #542 0::int)
#541 := (= #23 #289)
#148 := (= uf_3 #142)
#167 := (<= #26 0::int)
#168 := (not #167)
#174 := (iff #148 #168)
#189 := (not #174)
#220 := (iff #189 #148)
#210 := (not #148)
#215 := (not #210)
#218 := (iff #215 #148)
#219 := [rewrite]: #218
#216 := (iff #189 #215)
#213 := (iff #174 #210)
#207 := (iff #148 false)
#211 := (iff #207 #210)
#212 := [rewrite]: #211
#208 := (iff #174 #207)
#205 := (iff #168 false)
#1 := true
#200 := (not true)
#203 := (iff #200 false)
#204 := [rewrite]: #203
#201 := (iff #168 #200)
#198 := (iff #167 true)
#179 := (or #168 #174)
#182 := (not #179)
#27 := (< 0::int #26)
#28 := (ite #27 true false)
#29 := (- #26 1::int)
#30 := (uf_1 #29)
#31 := (= #30 uf_3)
#32 := (iff #28 #31)
#33 := (or #32 #28)
#34 := (not #33)
#185 := (iff #34 #182)
#153 := (iff #27 #148)
#159 := (or #27 #153)
#164 := (not #159)
#183 := (iff #164 #182)
#180 := (iff #159 #179)
#177 := (iff #153 #174)
#171 := (iff #168 #148)
#175 := (iff #171 #174)
#176 := [rewrite]: #175
#172 := (iff #153 #171)
#169 := (iff #27 #168)
#170 := [rewrite]: #169
#173 := [monotonicity #170]: #172
#178 := [trans #173 #176]: #177
#181 := [monotonicity #170 #178]: #180
#184 := [monotonicity #181]: #183
#165 := (iff #34 #164)
#162 := (iff #33 #159)
#156 := (or #153 #27)
#160 := (iff #156 #159)
#161 := [rewrite]: #160
#157 := (iff #33 #156)
#136 := (iff #28 #27)
#137 := [rewrite]: #136
#154 := (iff #32 #153)
#151 := (iff #31 #148)
#145 := (= #142 uf_3)
#149 := (iff #145 #148)
#150 := [rewrite]: #149
#146 := (iff #31 #145)
#143 := (= #30 #142)
#140 := (= #29 #139)
#141 := [rewrite]: #140
#144 := [monotonicity #141]: #143
#147 := [monotonicity #144]: #146
#152 := [trans #147 #150]: #151
#155 := [monotonicity #137 #152]: #154
#158 := [monotonicity #155 #137]: #157
#163 := [trans #158 #161]: #162
#166 := [monotonicity #163]: #165
#186 := [trans #166 #184]: #185
#135 := [asserted]: #34
#187 := [mp #135 #186]: #182
#188 := [not-or-elim #187]: #167
#199 := [iff-true #188]: #198
#202 := [monotonicity #199]: #201
#206 := [trans #202 #204]: #205
#209 := [monotonicity #206]: #208
#214 := [trans #209 #212]: #213
#217 := [monotonicity #214]: #216
#221 := [trans #217 #219]: #220
#190 := [not-or-elim #187]: #189
#222 := [mp #190 #221]: #148
#624 := [monotonicity #222]: #541
#618 := (not #541)
#625 := (or #618 #544)
#609 := [th-lemma]: #625
#610 := [unit-resolution #609 #624]: #544
#698 := (* -1::int #26)
#355 := (+ #23 #698)
#324 := (<= #355 -1::int)
#485 := (= #355 -1::int)
#367 := (>= #23 -1::int)
#533 := (>= #289 0::int)
#643 := (= #289 0::int)
#659 := (>= #26 1::int)
#656 := (not #659)
#612 := (or #656 #168)
#613 := [th-lemma]: #612
#614 := [unit-resolution #613 #188]: #656
#10 := (:var 0 int)
#12 := (uf_1 #10)
#712 := (pattern #12)
#76 := (>= #10 0::int)
#13 := (uf_2 #12)
#18 := (= #13 0::int)
#124 := (or #18 #76)
#719 := (forall (vars (?x3 int)) (:pat #712) #124)
#129 := (forall (vars (?x3 int)) #124)
#722 := (iff #129 #719)
#720 := (iff #124 #124)
#721 := [refl]: #720
#723 := [quant-intro #721]: #722
#229 := (~ #129 #129)
#227 := (~ #124 #124)
#228 := [refl]: #227
#230 := [nnf-pos #228]: #229
#17 := (< #10 0::int)
#19 := (implies #17 #18)
#20 := (forall (vars (?x3 int)) #19)
#132 := (iff #20 #129)
#95 := (= 0::int #13)
#101 := (not #17)
#102 := (or #101 #95)
#107 := (forall (vars (?x3 int)) #102)
#130 := (iff #107 #129)
#127 := (iff #102 #124)
#121 := (or #76 #18)
#125 := (iff #121 #124)
#126 := [rewrite]: #125
#122 := (iff #102 #121)
#119 := (iff #95 #18)
#120 := [rewrite]: #119
#117 := (iff #101 #76)
#77 := (not #76)
#112 := (not #77)
#115 := (iff #112 #76)
#116 := [rewrite]: #115
#113 := (iff #101 #112)
#110 := (iff #17 #77)
#111 := [rewrite]: #110
#114 := [monotonicity #111]: #113
#118 := [trans #114 #116]: #117
#123 := [monotonicity #118 #120]: #122
#128 := [trans #123 #126]: #127
#131 := [quant-intro #128]: #130
#108 := (iff #20 #107)
#105 := (iff #19 #102)
#98 := (implies #17 #95)
#103 := (iff #98 #102)
#104 := [rewrite]: #103
#99 := (iff #19 #98)
#96 := (iff #18 #95)
#97 := [rewrite]: #96
#100 := [monotonicity #97]: #99
#106 := [trans #100 #104]: #105
#109 := [quant-intro #106]: #108
#133 := [trans #109 #131]: #132
#94 := [asserted]: #20
#134 := [mp #94 #133]: #129
#231 := [mp~ #134 #230]: #129
#724 := [mp #231 #723]: #719
#402 := (not #719)
#528 := (or #402 #643 #659)
#388 := (>= #139 0::int)
#644 := (or #643 #388)
#529 := (or #402 #644)
#522 := (iff #529 #528)
#642 := (or #643 #659)
#636 := (or #402 #642)
#634 := (iff #636 #528)
#637 := [rewrite]: #634
#538 := (iff #529 #636)
#645 := (iff #644 #642)
#660 := (iff #388 #659)
#661 := [rewrite]: #660
#527 := [monotonicity #661]: #645
#633 := [monotonicity #527]: #538
#537 := [trans #633 #637]: #522
#488 := [quant-inst]: #529
#539 := [mp #488 #537]: #528
#615 := [unit-resolution #539 #724 #614]: #643
#611 := (not #643)
#616 := (or #611 #533)
#602 := [th-lemma]: #616
#603 := [unit-resolution #602 #615]: #533
#606 := (not #544)
#605 := (not #533)
#607 := (or #367 #605 #606)
#604 := [th-lemma]: #607
#608 := [unit-resolution #604 #603 #610]: #367
#701 := (not #367)
#358 := (or #701 #485)
#58 := (= #10 #13)
#83 := (or #58 #77)
#713 := (forall (vars (?x2 int)) (:pat #712) #83)
#88 := (forall (vars (?x2 int)) #83)
#716 := (iff #88 #713)
#714 := (iff #83 #83)
#715 := [refl]: #714
#717 := [quant-intro #715]: #716
#191 := (~ #88 #88)
#195 := (~ #83 #83)
#193 := [refl]: #195
#225 := [nnf-pos #193]: #191
#14 := (= #13 #10)
#11 := (<= 0::int #10)
#15 := (implies #11 #14)
#16 := (forall (vars (?x2 int)) #15)
#91 := (iff #16 #88)
#65 := (not #11)
#66 := (or #65 #58)
#71 := (forall (vars (?x2 int)) #66)
#89 := (iff #71 #88)
#86 := (iff #66 #83)
#80 := (or #77 #58)
#84 := (iff #80 #83)
#85 := [rewrite]: #84
#81 := (iff #66 #80)
#78 := (iff #65 #77)
#74 := (iff #11 #76)
#75 := [rewrite]: #74
#79 := [monotonicity #75]: #78
#82 := [monotonicity #79]: #81
#87 := [trans #82 #85]: #86
#90 := [quant-intro #87]: #89
#72 := (iff #16 #71)
#69 := (iff #15 #66)
#62 := (implies #11 #58)
#67 := (iff #62 #66)
#68 := [rewrite]: #67
#63 := (iff #15 #62)
#60 := (iff #14 #58)
#61 := [rewrite]: #60
#64 := [monotonicity #61]: #63
#70 := [trans #64 #68]: #69
#73 := [quant-intro #70]: #72
#92 := [trans #73 #90]: #91
#57 := [asserted]: #16
#93 := [mp #57 #92]: #88
#226 := [mp~ #93 #225]: #88
#718 := [mp #226 #717]: #713
#679 := (not #713)
#342 := (or #679 #701 #485)
#380 := (>= #24 0::int)
#381 := (not #380)
#361 := (= #24 #26)
#696 := (or #361 #381)
#343 := (or #679 #696)
#685 := (iff #343 #342)
#345 := (or #679 #358)
#683 := (iff #345 #342)
#684 := [rewrite]: #683
#681 := (iff #343 #345)
#695 := (iff #696 #358)
#703 := (or #485 #701)
#694 := (iff #703 #358)
#354 := [rewrite]: #694
#693 := (iff #696 #703)
#702 := (iff #381 #701)
#699 := (iff #380 #367)
#700 := [rewrite]: #699
#697 := [monotonicity #700]: #702
#692 := (iff #361 #485)
#366 := [rewrite]: #692
#353 := [monotonicity #366 #697]: #693
#338 := [trans #353 #354]: #695
#682 := [monotonicity #338]: #681
#680 := [trans #682 #684]: #685
#344 := [quant-inst]: #343
#686 := [mp #344 #680]: #342
#588 := [unit-resolution #686 #718]: #358
#589 := [unit-resolution #588 #608]: #485
#591 := (not #485)
#592 := (or #591 #324)
#593 := [th-lemma]: #592
#594 := [unit-resolution #593 #589]: #324
[th-lemma #603 #188 #594 #610]: false
unsat