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

adapted Function_Lib (cf. b8cdd3d73022);

#2 := false
#169 := 0::int
decl uf_2 :: int
#5 := uf_2
#166 := -1::int
#202 := (* -1::int uf_2)
decl uf_1 :: int
#4 := uf_1
#203 := (+ uf_1 #202)
#218 := (>= #203 0::int)
decl uf_3 :: int
#7 := uf_3
#167 := (* -1::int uf_3)
#168 := (+ uf_1 #167)
#178 := (>= #168 0::int)
#217 := (not #218)
#204 := (<= #203 0::int)
#205 := (not #204)
#692 := [hypothesis]: #205
#177 := (not #178)
#693 := (or #177 #204)
#170 := (<= #168 0::int)
#191 := (+ uf_2 #167)
#237 := (<= #191 0::int)
#238 := (not #237)
#171 := (not #170)
#685 := [hypothesis]: #171
#190 := (>= #191 0::int)
#455 := (or #170 #190)
#189 := (not #190)
#197 := (and #171 #189)
#354 := (not #197)
#464 := (iff #354 #455)
#456 := (not #455)
#459 := (not #456)
#462 := (iff #459 #455)
#463 := [rewrite]: #462
#460 := (iff #354 #459)
#457 := (iff #197 #456)
#458 := [rewrite]: #457
#461 := [monotonicity #458]: #460
#465 := [trans #461 #463]: #464
#287 := (and #189 #217)
#10 := (= uf_2 uf_3)
#279 := (and #10 #217)
#273 := (and #177 #238)
#15 := (= uf_1 uf_3)
#268 := (and #15 #238)
#17 := (= uf_1 uf_2)
#260 := (and #17 #189)
#252 := (and #205 #238)
#244 := (and #17 #238)
#232 := (and #171 #217)
#224 := (and #15 #217)
#214 := (and #10 #205)
#211 := (and #177 #205)
#208 := (and #15 #205)
#184 := (and #17 #177)
#174 := (and #10 #171)
#115 := (and #10 #17)
#337 := (or #115 #174 #184 #197 #208 #211 #214 #224 #232 #244 #252 #260 #268 #273 #279 #287)
#342 := (not #337)
#21 := (= uf_2 uf_1)
#27 := (= uf_3 uf_2)
#34 := (and #27 #21)
#23 := (< uf_3 uf_1)
#33 := (and #10 #23)
#35 := (or #33 #34)
#12 := (< uf_1 uf_3)
#32 := (and #21 #12)
#36 := (or #32 #35)
#8 := (< uf_2 uf_3)
#31 := (and #8 #23)
#37 := (or #31 #36)
#25 := (= uf_3 uf_1)
#19 := (< uf_2 uf_1)
#30 := (and #19 #25)
#38 := (or #30 #37)
#29 := (and #19 #12)
#39 := (or #29 #38)
#28 := (and #27 #19)
#40 := (or #28 #39)
#6 := (< uf_1 uf_2)
#26 := (and #25 #6)
#41 := (or #26 #40)
#24 := (and #23 #6)
#42 := (or #24 #41)
#13 := (< uf_3 uf_2)
#22 := (and #13 #21)
#43 := (or #22 #42)
#20 := (and #13 #19)
#44 := (or #20 #43)
#18 := (and #17 #8)
#45 := (or #18 #44)
#16 := (and #15 #13)
#46 := (or #16 #45)
#14 := (and #12 #13)
#47 := (or #14 #46)
#11 := (and #6 #10)
#48 := (or #11 #47)
#9 := (and #6 #8)
#49 := (or #9 #48)
#50 := (not #49)
#345 := (iff #50 #342)
#118 := (or #33 #115)
#110 := (and #12 #17)
#121 := (or #110 #118)
#124 := (or #31 #121)
#102 := (and #15 #19)
#127 := (or #102 #124)
#96 := (and #12 #19)
#130 := (or #96 #127)
#93 := (and #10 #19)
#133 := (or #93 #130)
#86 := (and #6 #15)
#136 := (or #86 #133)
#78 := (and #6 #23)
#139 := (or #78 #136)
#75 := (and #13 #17)
#142 := (or #75 #139)
#145 := (or #20 #142)
#70 := (and #8 #17)
#148 := (or #70 #145)
#67 := (and #13 #15)
#151 := (or #67 #148)
#154 := (or #14 #151)
#157 := (or #11 #154)
#160 := (or #9 #157)
#163 := (not #160)
#343 := (iff #163 #342)
#340 := (iff #160 #337)
#292 := (or #174 #115)
#295 := (or #184 #292)
#298 := (or #197 #295)
#301 := (or #208 #298)
#304 := (or #211 #301)
#307 := (or #214 #304)
#310 := (or #224 #307)
#313 := (or #232 #310)
#316 := (or #244 #313)
#319 := (or #252 #316)
#322 := (or #260 #319)
#325 := (or #268 #322)
#328 := (or #273 #325)
#331 := (or #279 #328)
#334 := (or #287 #331)
#338 := (iff #334 #337)
#339 := [rewrite]: #338
#335 := (iff #160 #334)
#332 := (iff #157 #331)
#329 := (iff #154 #328)
#326 := (iff #151 #325)
#323 := (iff #148 #322)
#320 := (iff #145 #319)
#317 := (iff #142 #316)
#314 := (iff #139 #313)
#311 := (iff #136 #310)
#308 := (iff #133 #307)
#305 := (iff #130 #304)
#302 := (iff #127 #301)
#299 := (iff #124 #298)
#296 := (iff #121 #295)
#293 := (iff #118 #292)
#175 := (iff #33 #174)
#172 := (iff #23 #171)
#173 := [rewrite]: #172
#176 := [monotonicity #173]: #175
#294 := [monotonicity #176]: #293
#187 := (iff #110 #184)
#181 := (and #177 #17)
#185 := (iff #181 #184)
#186 := [rewrite]: #185
#182 := (iff #110 #181)
#179 := (iff #12 #177)
#180 := [rewrite]: #179
#183 := [monotonicity #180]: #182
#188 := [trans #183 #186]: #187
#297 := [monotonicity #188 #294]: #296
#200 := (iff #31 #197)
#194 := (and #189 #171)
#198 := (iff #194 #197)
#199 := [rewrite]: #198
#195 := (iff #31 #194)
#192 := (iff #8 #189)
#193 := [rewrite]: #192
#196 := [monotonicity #193 #173]: #195
#201 := [trans #196 #199]: #200
#300 := [monotonicity #201 #297]: #299
#209 := (iff #102 #208)
#206 := (iff #19 #205)
#207 := [rewrite]: #206
#210 := [monotonicity #207]: #209
#303 := [monotonicity #210 #300]: #302
#212 := (iff #96 #211)
#213 := [monotonicity #180 #207]: #212
#306 := [monotonicity #213 #303]: #305
#215 := (iff #93 #214)
#216 := [monotonicity #207]: #215
#309 := [monotonicity #216 #306]: #308
#227 := (iff #86 #224)
#221 := (and #217 #15)
#225 := (iff #221 #224)
#226 := [rewrite]: #225
#222 := (iff #86 #221)
#219 := (iff #6 #217)
#220 := [rewrite]: #219
#223 := [monotonicity #220]: #222
#228 := [trans #223 #226]: #227
#312 := [monotonicity #228 #309]: #311
#235 := (iff #78 #232)
#229 := (and #217 #171)
#233 := (iff #229 #232)
#234 := [rewrite]: #233
#230 := (iff #78 #229)
#231 := [monotonicity #220 #173]: #230
#236 := [trans #231 #234]: #235
#315 := [monotonicity #236 #312]: #314
#247 := (iff #75 #244)
#241 := (and #238 #17)
#245 := (iff #241 #244)
#246 := [rewrite]: #245
#242 := (iff #75 #241)
#239 := (iff #13 #238)
#240 := [rewrite]: #239
#243 := [monotonicity #240]: #242
#248 := [trans #243 #246]: #247
#318 := [monotonicity #248 #315]: #317
#255 := (iff #20 #252)
#249 := (and #238 #205)
#253 := (iff #249 #252)
#254 := [rewrite]: #253
#250 := (iff #20 #249)
#251 := [monotonicity #240 #207]: #250
#256 := [trans #251 #254]: #255
#321 := [monotonicity #256 #318]: #320
#263 := (iff #70 #260)
#257 := (and #189 #17)
#261 := (iff #257 #260)
#262 := [rewrite]: #261
#258 := (iff #70 #257)
#259 := [monotonicity #193]: #258
#264 := [trans #259 #262]: #263
#324 := [monotonicity #264 #321]: #323
#271 := (iff #67 #268)
#265 := (and #238 #15)
#269 := (iff #265 #268)
#270 := [rewrite]: #269
#266 := (iff #67 #265)
#267 := [monotonicity #240]: #266
#272 := [trans #267 #270]: #271
#327 := [monotonicity #272 #324]: #326
#274 := (iff #14 #273)
#275 := [monotonicity #180 #240]: #274
#330 := [monotonicity #275 #327]: #329
#282 := (iff #11 #279)
#276 := (and #217 #10)
#280 := (iff #276 #279)
#281 := [rewrite]: #280
#277 := (iff #11 #276)
#278 := [monotonicity #220]: #277
#283 := [trans #278 #281]: #282
#333 := [monotonicity #283 #330]: #332
#290 := (iff #9 #287)
#284 := (and #217 #189)
#288 := (iff #284 #287)
#289 := [rewrite]: #288
#285 := (iff #9 #284)
#286 := [monotonicity #220 #193]: #285
#291 := [trans #286 #289]: #290
#336 := [monotonicity #291 #333]: #335
#341 := [trans #336 #339]: #340
#344 := [monotonicity #341]: #343
#164 := (iff #50 #163)
#161 := (iff #49 #160)
#158 := (iff #48 #157)
#155 := (iff #47 #154)
#152 := (iff #46 #151)
#149 := (iff #45 #148)
#146 := (iff #44 #145)
#143 := (iff #43 #142)
#140 := (iff #42 #139)
#137 := (iff #41 #136)
#134 := (iff #40 #133)
#131 := (iff #39 #130)
#128 := (iff #38 #127)
#125 := (iff #37 #124)
#122 := (iff #36 #121)
#119 := (iff #35 #118)
#116 := (iff #34 #115)
#73 := (iff #21 #17)
#74 := [rewrite]: #73
#91 := (iff #27 #10)
#92 := [rewrite]: #91
#117 := [monotonicity #92 #74]: #116
#120 := [monotonicity #117]: #119
#113 := (iff #32 #110)
#107 := (and #17 #12)
#111 := (iff #107 #110)
#112 := [rewrite]: #111
#108 := (iff #32 #107)
#109 := [monotonicity #74]: #108
#114 := [trans #109 #112]: #113
#123 := [monotonicity #114 #120]: #122
#126 := [monotonicity #123]: #125
#105 := (iff #30 #102)
#99 := (and #19 #15)
#103 := (iff #99 #102)
#104 := [rewrite]: #103
#100 := (iff #30 #99)
#81 := (iff #25 #15)
#82 := [rewrite]: #81
#101 := [monotonicity #82]: #100
#106 := [trans #101 #104]: #105
#129 := [monotonicity #106 #126]: #128
#97 := (iff #29 #96)
#98 := [rewrite]: #97
#132 := [monotonicity #98 #129]: #131
#94 := (iff #28 #93)
#95 := [monotonicity #92]: #94
#135 := [monotonicity #95 #132]: #134
#89 := (iff #26 #86)
#83 := (and #15 #6)
#87 := (iff #83 #86)
#88 := [rewrite]: #87
#84 := (iff #26 #83)
#85 := [monotonicity #82]: #84
#90 := [trans #85 #88]: #89
#138 := [monotonicity #90 #135]: #137
#79 := (iff #24 #78)
#80 := [rewrite]: #79
#141 := [monotonicity #80 #138]: #140
#76 := (iff #22 #75)
#77 := [monotonicity #74]: #76
#144 := [monotonicity #77 #141]: #143
#147 := [monotonicity #144]: #146
#71 := (iff #18 #70)
#72 := [rewrite]: #71
#150 := [monotonicity #72 #147]: #149
#68 := (iff #16 #67)
#69 := [rewrite]: #68
#153 := [monotonicity #69 #150]: #152
#156 := [monotonicity #153]: #155
#159 := [monotonicity #156]: #158
#162 := [monotonicity #159]: #161
#165 := [monotonicity #162]: #164
#346 := [trans #165 #344]: #345
#66 := [asserted]: #50
#347 := [mp #66 #346]: #342
#355 := [not-or-elim #347]: #354
#466 := [mp #355 #465]: #455
#686 := [unit-resolution #466 #685]: #190
#427 := (or #170 #189 #238)
#350 := (not #174)
#430 := (iff #350 #427)
#382 := (or #189 #238)
#414 := (or #170 #382)
#428 := (iff #414 #427)
#429 := [rewrite]: #428
#425 := (iff #350 #414)
#415 := (not #414)
#420 := (not #415)
#423 := (iff #420 #414)
#424 := [rewrite]: #423
#421 := (iff #350 #420)
#418 := (iff #174 #415)
#380 := (not #382)
#411 := (and #380 #171)
#416 := (iff #411 #415)
#417 := [rewrite]: #416
#412 := (iff #174 #411)
#383 := (iff #10 #380)
#384 := [rewrite]: #383
#413 := [monotonicity #384]: #412
#419 := [trans #413 #417]: #418
#422 := [monotonicity #419]: #421
#426 := [trans #422 #424]: #425
#431 := [trans #426 #429]: #430
#351 := [not-or-elim #347]: #350
#432 := [mp #351 #431]: #427
#687 := [unit-resolution #432 #686 #685]: #238
#549 := (or #170 #218)
#364 := (not #232)
#558 := (iff #364 #549)
#550 := (not #549)
#553 := (not #550)
#556 := (iff #553 #549)
#557 := [rewrite]: #556
#554 := (iff #364 #553)
#551 := (iff #232 #550)
#552 := [rewrite]: #551
#555 := [monotonicity #552]: #554
#559 := [trans #555 #557]: #558
#365 := [not-or-elim #347]: #364
#560 := [mp #365 #559]: #549
#688 := [unit-resolution #560 #685]: #218
#577 := (or #205 #217 #237)
#366 := (not #244)
#580 := (iff #366 #577)
#385 := (or #205 #217)
#564 := (or #237 #385)
#578 := (iff #564 #577)
#579 := [rewrite]: #578
#575 := (iff #366 #564)
#565 := (not #564)
#570 := (not #565)
#573 := (iff #570 #564)
#574 := [rewrite]: #573
#571 := (iff #366 #570)
#568 := (iff #244 #565)
#386 := (not #385)
#561 := (and #386 #238)
#566 := (iff #561 #565)
#567 := [rewrite]: #566
#562 := (iff #244 #561)
#387 := (iff #17 #386)
#388 := [rewrite]: #387
#563 := [monotonicity #388]: #562
#569 := [trans #563 #567]: #568
#572 := [monotonicity #569]: #571
#576 := [trans #572 #574]: #575
#581 := [trans #576 #579]: #580
#367 := [not-or-elim #347]: #366
#582 := [mp #367 #581]: #577
#689 := [unit-resolution #582 #688 #687]: #205
#583 := (or #204 #237)
#368 := (not #252)
#592 := (iff #368 #583)
#584 := (not #583)
#587 := (not #584)
#590 := (iff #587 #583)
#591 := [rewrite]: #590
#588 := (iff #368 #587)
#585 := (iff #252 #584)
#586 := [rewrite]: #585
#589 := [monotonicity #586]: #588
#593 := [trans #589 #591]: #592
#369 := [not-or-elim #347]: #368
#594 := [mp #369 #593]: #583
#690 := [unit-resolution #594 #689 #687]: false
#691 := [lemma #690]: #170
#487 := (or #171 #177 #204)
#356 := (not #208)
#490 := (iff #356 #487)
#467 := (or #171 #177)
#474 := (or #204 #467)
#488 := (iff #474 #487)
#489 := [rewrite]: #488
#485 := (iff #356 #474)
#475 := (not #474)
#480 := (not #475)
#483 := (iff #480 #474)
#484 := [rewrite]: #483
#481 := (iff #356 #480)
#478 := (iff #208 #475)
#468 := (not #467)
#471 := (and #468 #205)
#476 := (iff #471 #475)
#477 := [rewrite]: #476
#472 := (iff #208 #471)
#469 := (iff #15 #468)
#470 := [rewrite]: #469
#473 := [monotonicity #470]: #472
#479 := [trans #473 #477]: #478
#482 := [monotonicity #479]: #481
#486 := [trans #482 #484]: #485
#491 := [trans #486 #489]: #490
#357 := [not-or-elim #347]: #356
#492 := [mp #357 #491]: #487
#694 := [unit-resolution #492 #691]: #693
#695 := [unit-resolution #694 #692]: #177
#493 := (or #178 #204)
#358 := (not #211)
#502 := (iff #358 #493)
#494 := (not #493)
#497 := (not #494)
#500 := (iff #497 #493)
#501 := [rewrite]: #500
#498 := (iff #358 #497)
#495 := (iff #211 #494)
#496 := [rewrite]: #495
#499 := [monotonicity #496]: #498
#503 := [trans #499 #501]: #502
#359 := [not-or-elim #347]: #358
#504 := [mp #359 #503]: #493
#696 := [unit-resolution #504 #695 #692]: false
#697 := [lemma #696]: #204
#698 := [hypothesis]: #177
#449 := (or #178 #205 #217)
#352 := (not #184)
#452 := (iff #352 #449)
#436 := (or #178 #385)
#450 := (iff #436 #449)
#451 := [rewrite]: #450
#447 := (iff #352 #436)
#437 := (not #436)
#442 := (not #437)
#445 := (iff #442 #436)
#446 := [rewrite]: #445
#443 := (iff #352 #442)
#440 := (iff #184 #437)
#433 := (and #386 #177)
#438 := (iff #433 #437)
#439 := [rewrite]: #438
#434 := (iff #184 #433)
#435 := [monotonicity #388]: #434
#441 := [trans #435 #439]: #440
#444 := [monotonicity #441]: #443
#448 := [trans #444 #446]: #447
#453 := [trans #448 #451]: #452
#353 := [not-or-elim #347]: #352
#454 := [mp #353 #453]: #449
#699 := [unit-resolution #454 #698 #697]: #217
#639 := (or #178 #237)
#374 := (not #273)
#648 := (iff #374 #639)
#640 := (not #639)
#643 := (not #640)
#646 := (iff #643 #639)
#647 := [rewrite]: #646
#644 := (iff #374 #643)
#641 := (iff #273 #640)
#642 := [rewrite]: #641
#645 := [monotonicity #642]: #644
#649 := [trans #645 #647]: #648
#375 := [not-or-elim #347]: #374
#650 := [mp #375 #649]: #639
#700 := [unit-resolution #650 #698]: #237
#667 := (or #189 #218 #238)
#376 := (not #279)
#670 := (iff #376 #667)
#654 := (or #218 #382)
#668 := (iff #654 #667)
#669 := [rewrite]: #668
#665 := (iff #376 #654)
#655 := (not #654)
#660 := (not #655)
#663 := (iff #660 #654)
#664 := [rewrite]: #663
#661 := (iff #376 #660)
#658 := (iff #279 #655)
#651 := (and #380 #217)
#656 := (iff #651 #655)
#657 := [rewrite]: #656
#652 := (iff #279 #651)
#653 := [monotonicity #384]: #652
#659 := [trans #653 #657]: #658
#662 := [monotonicity #659]: #661
#666 := [trans #662 #664]: #665
#671 := [trans #666 #669]: #670
#377 := [not-or-elim #347]: #376
#672 := [mp #377 #671]: #667
#701 := [unit-resolution #672 #699 #700]: #189
#673 := (or #190 #218)
#378 := (not #287)
#682 := (iff #378 #673)
#674 := (not #673)
#677 := (not #674)
#680 := (iff #677 #673)
#681 := [rewrite]: #680
#678 := (iff #378 #677)
#675 := (iff #287 #674)
#676 := [rewrite]: #675
#679 := [monotonicity #676]: #678
#683 := [trans #679 #681]: #682
#379 := [not-or-elim #347]: #378
#684 := [mp #379 #683]: #673
#702 := [unit-resolution #684 #701 #699]: false
#703 := [lemma #702]: #178
#704 := (or #177 #218)
#543 := (or #171 #177 #218)
#362 := (not #224)
#546 := (iff #362 #543)
#530 := (or #218 #467)
#544 := (iff #530 #543)
#545 := [rewrite]: #544
#541 := (iff #362 #530)
#531 := (not #530)
#536 := (not #531)
#539 := (iff #536 #530)
#540 := [rewrite]: #539
#537 := (iff #362 #536)
#534 := (iff #224 #531)
#527 := (and #468 #217)
#532 := (iff #527 #531)
#533 := [rewrite]: #532
#528 := (iff #224 #527)
#529 := [monotonicity #470]: #528
#535 := [trans #529 #533]: #534
#538 := [monotonicity #535]: #537
#542 := [trans #538 #540]: #541
#547 := [trans #542 #545]: #546
#363 := [not-or-elim #347]: #362
#548 := [mp #363 #547]: #543
#705 := [unit-resolution #548 #691]: #704
#706 := [unit-resolution #705 #703]: #218
#707 := (or #177 #237)
#633 := (or #171 #177 #237)
#372 := (not #268)
#636 := (iff #372 #633)
#620 := (or #237 #467)
#634 := (iff #620 #633)
#635 := [rewrite]: #634
#631 := (iff #372 #620)
#621 := (not #620)
#626 := (not #621)
#629 := (iff #626 #620)
#630 := [rewrite]: #629
#627 := (iff #372 #626)
#624 := (iff #268 #621)
#617 := (and #468 #238)
#622 := (iff #617 #621)
#623 := [rewrite]: #622
#618 := (iff #268 #617)
#619 := [monotonicity #470]: #618
#625 := [trans #619 #623]: #624
#628 := [monotonicity #625]: #627
#632 := [trans #628 #630]: #631
#637 := [trans #632 #635]: #636
#373 := [not-or-elim #347]: #372
#638 := [mp #373 #637]: #633
#708 := [unit-resolution #638 #691]: #707
#709 := [unit-resolution #708 #703]: #237
#611 := (or #190 #205 #217)
#370 := (not #260)
#614 := (iff #370 #611)
#598 := (or #190 #385)
#612 := (iff #598 #611)
#613 := [rewrite]: #612
#609 := (iff #370 #598)
#599 := (not #598)
#604 := (not #599)
#607 := (iff #604 #598)
#608 := [rewrite]: #607
#605 := (iff #370 #604)
#602 := (iff #260 #599)
#595 := (and #386 #189)
#600 := (iff #595 #599)
#601 := [rewrite]: #600
#596 := (iff #260 #595)
#597 := [monotonicity #388]: #596
#603 := [trans #597 #601]: #602
#606 := [monotonicity #603]: #605
#610 := [trans #606 #608]: #609
#615 := [trans #610 #613]: #614
#371 := [not-or-elim #347]: #370
#616 := [mp #371 #615]: #611
#710 := [unit-resolution #616 #706 #697]: #190
#405 := (or #189 #205 #217 #238)
#348 := (not #115)
#408 := (iff #348 #405)
#392 := (or #382 #385)
#406 := (iff #392 #405)
#407 := [rewrite]: #406
#403 := (iff #348 #392)
#393 := (not #392)
#398 := (not #393)
#401 := (iff #398 #392)
#402 := [rewrite]: #401
#399 := (iff #348 #398)
#396 := (iff #115 #393)
#389 := (and #380 #386)
#394 := (iff #389 #393)
#395 := [rewrite]: #394
#390 := (iff #115 #389)
#391 := [monotonicity #384 #388]: #390
#397 := [trans #391 #395]: #396
#400 := [monotonicity #397]: #399
#404 := [trans #400 #402]: #403
#409 := [trans #404 #407]: #408
#349 := [not-or-elim #347]: #348
#410 := [mp #349 #409]: #405
[unit-resolution #410 #710 #709 #697 #706]: false
unsat