1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/SMT/Examples/cert/z3_linarith_21.proof Wed Nov 18 09:34:53 2009 +0100
1.3 @@ -0,0 +1,208 @@
1.4 +#2 := false
1.5 +#9 := 0::int
1.6 +#11 := 4::int
1.7 +decl uf_1 :: int
1.8 +#4 := uf_1
1.9 +#189 := (div uf_1 4::int)
1.10 +#210 := -4::int
1.11 +#211 := (* -4::int #189)
1.12 +#12 := (mod uf_1 4::int)
1.13 +#134 := -1::int
1.14 +#209 := (* -1::int #12)
1.15 +#212 := (+ #209 #211)
1.16 +#213 := (+ uf_1 #212)
1.17 +#214 := (<= #213 0::int)
1.18 +#215 := (not #214)
1.19 +#208 := (>= #213 0::int)
1.20 +#207 := (not #208)
1.21 +#216 := (or #207 #215)
1.22 +#217 := (not #216)
1.23 +#1 := true
1.24 +#36 := [true-axiom]: true
1.25 +#393 := (or false #217)
1.26 +#394 := [th-lemma]: #393
1.27 +#395 := [unit-resolution #394 #36]: #217
1.28 +#224 := (or #216 #214)
1.29 +#225 := [def-axiom]: #224
1.30 +#396 := [unit-resolution #225 #395]: #214
1.31 +#222 := (or #216 #208)
1.32 +#223 := [def-axiom]: #222
1.33 +#397 := [unit-resolution #223 #395]: #208
1.34 +#250 := (>= #12 4::int)
1.35 +#251 := (not #250)
1.36 +#398 := (or false #251)
1.37 +#399 := [th-lemma]: #398
1.38 +#400 := [unit-resolution #399 #36]: #251
1.39 +#13 := 3::int
1.40 +#90 := (>= #12 3::int)
1.41 +#92 := (not #90)
1.42 +#89 := (<= #12 3::int)
1.43 +#91 := (not #89)
1.44 +#93 := (or #91 #92)
1.45 +#94 := (not #93)
1.46 +#14 := (= #12 3::int)
1.47 +#95 := (iff #14 #94)
1.48 +#96 := [rewrite]: #95
1.49 +#38 := [asserted]: #14
1.50 +#97 := [mp #38 #96]: #94
1.51 +#99 := [not-or-elim #97]: #90
1.52 +#7 := 2::int
1.53 +#261 := (div uf_1 2::int)
1.54 +#140 := -2::int
1.55 +#276 := (* -2::int #261)
1.56 +#15 := (mod uf_1 2::int)
1.57 +#275 := (* -1::int #15)
1.58 +#277 := (+ #275 #276)
1.59 +#278 := (+ uf_1 #277)
1.60 +#279 := (<= #278 0::int)
1.61 +#280 := (not #279)
1.62 +#274 := (>= #278 0::int)
1.63 +#273 := (not #274)
1.64 +#281 := (or #273 #280)
1.65 +#282 := (not #281)
1.66 +#408 := (or false #282)
1.67 +#409 := [th-lemma]: #408
1.68 +#410 := [unit-resolution #409 #36]: #282
1.69 +#289 := (or #281 #279)
1.70 +#290 := [def-axiom]: #289
1.71 +#411 := [unit-resolution #290 #410]: #279
1.72 +#287 := (or #281 #274)
1.73 +#288 := [def-axiom]: #287
1.74 +#412 := [unit-resolution #288 #410]: #274
1.75 +#16 := 1::int
1.76 +#55 := (>= #15 1::int)
1.77 +#100 := (not #55)
1.78 +decl uf_2 :: int
1.79 +#5 := uf_2
1.80 +#18 := (mod uf_2 2::int)
1.81 +#61 := (<= #18 1::int)
1.82 +#102 := (not #61)
1.83 +#375 := [hypothesis]: #102
1.84 +#358 := (>= #18 2::int)
1.85 +#359 := (not #358)
1.86 +#403 := (or false #359)
1.87 +#404 := [th-lemma]: #403
1.88 +#405 := [unit-resolution #404 #36]: #359
1.89 +#406 := [th-lemma #405 #375]: false
1.90 +#407 := [lemma #406]: #61
1.91 +#413 := (or #100 #102)
1.92 +#62 := (>= #18 1::int)
1.93 +#315 := (div uf_2 2::int)
1.94 +#330 := (* -2::int #315)
1.95 +#329 := (* -1::int #18)
1.96 +#331 := (+ #329 #330)
1.97 +#332 := (+ uf_2 #331)
1.98 +#333 := (<= #332 0::int)
1.99 +#334 := (not #333)
1.100 +#328 := (>= #332 0::int)
1.101 +#327 := (not #328)
1.102 +#335 := (or #327 #334)
1.103 +#336 := (not #335)
1.104 +#376 := (or false #336)
1.105 +#377 := [th-lemma]: #376
1.106 +#378 := [unit-resolution #377 #36]: #336
1.107 +#343 := (or #335 #333)
1.108 +#344 := [def-axiom]: #343
1.109 +#379 := [unit-resolution #344 #378]: #333
1.110 +#341 := (or #335 #328)
1.111 +#342 := [def-axiom]: #341
1.112 +#380 := [unit-resolution #342 #378]: #328
1.113 +#103 := (not #62)
1.114 +#381 := [hypothesis]: #103
1.115 +#352 := (>= #18 0::int)
1.116 +#382 := (or false #352)
1.117 +#383 := [th-lemma]: #382
1.118 +#384 := [unit-resolution #383 #36]: #352
1.119 +#6 := (+ uf_1 uf_2)
1.120 +#116 := (div #6 2::int)
1.121 +#141 := (* -2::int #116)
1.122 +#8 := (mod #6 2::int)
1.123 +#139 := (* -1::int #8)
1.124 +#142 := (+ #139 #141)
1.125 +#143 := (+ uf_2 #142)
1.126 +#144 := (+ uf_1 #143)
1.127 +#138 := (<= #144 0::int)
1.128 +#136 := (not #138)
1.129 +#137 := (>= #144 0::int)
1.130 +#135 := (not #137)
1.131 +#145 := (or #135 #136)
1.132 +#146 := (not #145)
1.133 +#385 := (or false #146)
1.134 +#386 := [th-lemma]: #385
1.135 +#387 := [unit-resolution #386 #36]: #146
1.136 +#153 := (or #145 #138)
1.137 +#154 := [def-axiom]: #153
1.138 +#388 := [unit-resolution #154 #387]: #138
1.139 +#151 := (or #145 #137)
1.140 +#152 := [def-axiom]: #151
1.141 +#389 := [unit-resolution #152 #387]: #137
1.142 +#78 := (<= #8 0::int)
1.143 +#79 := (>= #8 0::int)
1.144 +#81 := (not #79)
1.145 +#80 := (not #78)
1.146 +#82 := (or #80 #81)
1.147 +#83 := (not #82)
1.148 +#10 := (= #8 0::int)
1.149 +#84 := (iff #10 #83)
1.150 +#85 := [rewrite]: #84
1.151 +#37 := [asserted]: #10
1.152 +#86 := [mp #37 #85]: #83
1.153 +#87 := [not-or-elim #86]: #78
1.154 +#390 := (or false #79)
1.155 +#391 := [th-lemma]: #390
1.156 +#392 := [unit-resolution #391 #36]: #79
1.157 +#401 := [th-lemma #99 #400 #397 #396 #392 #87 #389 #388 #384 #381 #380 #379]: false
1.158 +#402 := [lemma #401]: #62
1.159 +#57 := (<= #15 1::int)
1.160 +#101 := (not #57)
1.161 +#369 := [hypothesis]: #101
1.162 +#304 := (>= #15 2::int)
1.163 +#305 := (not #304)
1.164 +#370 := (or false #305)
1.165 +#371 := [th-lemma]: #370
1.166 +#372 := [unit-resolution #371 #36]: #305
1.167 +#373 := [th-lemma #372 #369]: false
1.168 +#374 := [lemma #373]: #57
1.169 +#104 := (or #100 #101 #102 #103)
1.170 +#69 := (and #55 #57 #61 #62)
1.171 +#74 := (not #69)
1.172 +#113 := (iff #74 #104)
1.173 +#105 := (not #104)
1.174 +#108 := (not #105)
1.175 +#111 := (iff #108 #104)
1.176 +#112 := [rewrite]: #111
1.177 +#109 := (iff #74 #108)
1.178 +#106 := (iff #69 #105)
1.179 +#107 := [rewrite]: #106
1.180 +#110 := [monotonicity #107]: #109
1.181 +#114 := [trans #110 #112]: #113
1.182 +#19 := (= #18 1::int)
1.183 +#17 := (= #15 1::int)
1.184 +#20 := (and #17 #19)
1.185 +#21 := (not #20)
1.186 +#75 := (iff #21 #74)
1.187 +#72 := (iff #20 #69)
1.188 +#63 := (and #61 #62)
1.189 +#58 := (and #55 #57)
1.190 +#66 := (and #58 #63)
1.191 +#70 := (iff #66 #69)
1.192 +#71 := [rewrite]: #70
1.193 +#67 := (iff #20 #66)
1.194 +#64 := (iff #19 #63)
1.195 +#65 := [rewrite]: #64
1.196 +#59 := (iff #17 #58)
1.197 +#60 := [rewrite]: #59
1.198 +#68 := [monotonicity #60 #65]: #67
1.199 +#73 := [trans #68 #71]: #72
1.200 +#76 := [monotonicity #73]: #75
1.201 +#39 := [asserted]: #21
1.202 +#77 := [mp #39 #76]: #74
1.203 +#115 := [mp #77 #114]: #104
1.204 +#414 := [unit-resolution #115 #374 #402]: #413
1.205 +#415 := [unit-resolution #414 #407]: #100
1.206 +#298 := (>= #15 0::int)
1.207 +#416 := (or false #298)
1.208 +#417 := [th-lemma]: #416
1.209 +#418 := [unit-resolution #417 #36]: #298
1.210 +[th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false
1.211 +unsat