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

provide standard isabelle make targets;
slightly more accurate dependencies;

#2 := false
#22 := 0::int
decl uf_6 :: (-> T3 T4 int)
decl uf_7 :: (-> T2 T4 T4)
decl uf_9 :: T4
#50 := uf_9
decl uf_2 :: T2
#4 := uf_2
#59 := (uf_7 uf_2 uf_9)
decl uf_8 :: T3
#49 := uf_8
#60 := (uf_6 uf_8 #59)
#204 := -2::int
#683 := (* -2::int #60)
decl uf_5 :: T2
#13 := uf_5
#54 := (uf_7 uf_5 uf_9)
#55 := (uf_6 uf_8 #54)
#172 := -1::int
#218 := (* -1::int #55)
#685 := (+ #218 #683)
#51 := (uf_6 uf_8 uf_9)
#686 := (+ #51 #685)
#679 := (>= #686 0::int)
#687 := (= #686 0::int)
#35 := (:var 0 T4)
#43 := (uf_7 uf_2 #35)
#34 := (:var 1 T3)
#44 := (uf_6 #34 #43)
#819 := (pattern #44)
#38 := (uf_7 uf_5 #35)
#39 := (uf_6 #34 #38)
#812 := (pattern #39)
#205 := (* -2::int #44)
#203 := (* -1::int #39)
#206 := (+ #203 #205)
#36 := (uf_6 #34 #35)
#207 := (+ #36 #206)
#208 := (= #207 0::int)
#820 := (forall (vars (?x8 T3) (?x9 T4)) (:pat #812 #819) #208)
#211 := (forall (vars (?x8 T3) (?x9 T4)) #208)
#823 := (iff #211 #820)
#821 := (iff #208 #208)
#822 := [refl]: #821
#824 := [quant-intro #822]: #823
#279 := (~ #211 #211)
#305 := (~ #208 #208)
#306 := [refl]: #305
#280 := [nnf-pos #306]: #279
#8 := 2::int
#45 := (* #44 2::int)
#46 := (+ #45 #39)
#47 := (= #46 #36)
#48 := (forall (vars (?x8 T3) (?x9 T4)) #47)
#214 := (iff #48 #211)
#171 := (* 2::int #44)
#187 := (+ #39 #171)
#195 := (= #36 #187)
#200 := (forall (vars (?x8 T3) (?x9 T4)) #195)
#212 := (iff #200 #211)
#209 := (iff #195 #208)
#210 := [rewrite]: #209
#213 := [quant-intro #210]: #212
#201 := (iff #48 #200)
#198 := (iff #47 #195)
#192 := (= #187 #36)
#196 := (iff #192 #195)
#197 := [rewrite]: #196
#193 := (iff #47 #192)
#190 := (= #46 #187)
#184 := (+ #171 #39)
#188 := (= #184 #187)
#189 := [rewrite]: #188
#185 := (= #46 #184)
#182 := (= #45 #171)
#183 := [rewrite]: #182
#186 := [monotonicity #183]: #185
#191 := [trans #186 #189]: #190
#194 := [monotonicity #191]: #193
#199 := [trans #194 #197]: #198
#202 := [quant-intro #199]: #201
#215 := [trans #202 #213]: #214
#170 := [asserted]: #48
#216 := [mp #170 #215]: #211
#307 := [mp~ #216 #280]: #211
#825 := [mp #307 #824]: #820
#689 := (not #820)
#675 := (or #689 #687)
#676 := [quant-inst]: #675
#536 := [unit-resolution #676 #825]: #687
#537 := (not #687)
#533 := (or #537 #679)
#538 := [th-lemma]: #533
#528 := [unit-resolution #538 #536]: #679
decl uf_10 :: int
#52 := uf_10
#219 := (+ uf_10 #218)
#222 := (div #219 2::int)
#251 := (* -1::int #222)
#252 := (+ #60 #251)
#449 := (<= #252 0::int)
#399 := (not #449)
#253 := (= #252 0::int)
#256 := (not #253)
#57 := (mod uf_10 2::int)
#243 := (* -1::int #57)
#56 := (mod #55 2::int)
#244 := (+ #56 #243)
#245 := (= #244 0::int)
#448 := (>= #244 0::int)
#688 := (mod #51 2::int)
#666 := (* -1::int #688)
#667 := (+ #56 #666)
#660 := (>= #667 0::int)
#668 := (= #667 0::int)
#40 := (mod #39 2::int)
#173 := (* -1::int #40)
#37 := (mod #36 2::int)
#174 := (+ #37 #173)
#175 := (= #174 0::int)
#813 := (forall (vars (?x6 T3) (?x7 T4)) (:pat #812) #175)
#178 := (forall (vars (?x6 T3) (?x7 T4)) #175)
#816 := (iff #178 #813)
#814 := (iff #175 #175)
#815 := [refl]: #814
#817 := [quant-intro #815]: #816
#277 := (~ #178 #178)
#302 := (~ #175 #175)
#303 := [refl]: #302
#278 := [nnf-pos #303]: #277
#41 := (= #37 #40)
#42 := (forall (vars (?x6 T3) (?x7 T4)) #41)
#179 := (iff #42 #178)
#176 := (iff #41 #175)
#177 := [rewrite]: #176
#180 := [quant-intro #177]: #179
#169 := [asserted]: #42
#181 := [mp #169 #180]: #178
#304 := [mp~ #181 #278]: #178
#818 := [mp #304 #817]: #813
#673 := (not #813)
#663 := (or #673 #668)
#756 := (* -1::int #56)
#684 := (+ #688 #756)
#680 := (= #684 0::int)
#674 := (or #673 #680)
#653 := (iff #674 #663)
#656 := (iff #663 #663)
#657 := [rewrite]: #656
#671 := (iff #680 #668)
#677 := (+ #756 #688)
#662 := (= #677 0::int)
#669 := (iff #662 #668)
#670 := [rewrite]: #669
#664 := (iff #680 #662)
#681 := (= #684 #677)
#661 := [rewrite]: #681
#665 := [monotonicity #661]: #664
#672 := [trans #665 #670]: #671
#655 := [monotonicity #672]: #653
#658 := [trans #655 #657]: #653
#652 := [quant-inst]: #674
#659 := [mp #652 #658]: #663
#394 := [unit-resolution #659 #818]: #668
#552 := (not #668)
#514 := (or #552 #660)
#517 := [th-lemma]: #514
#499 := [unit-resolution #517 #394]: #660
#503 := (not #448)
#414 := [hypothesis]: #503
#561 := (+ #57 #666)
#709 := (<= #561 0::int)
#602 := (= #57 #688)
#468 := (= #688 #57)
#53 := (= #51 uf_10)
#248 := (not #245)
#259 := (or #248 #256)
#362 := (mod #219 2::int)
#699 := (>= #362 0::int)
#1 := true
#81 := [true-axiom]: true
#604 := (or false #699)
#506 := [th-lemma]: #604
#507 := [unit-resolution #506 #81]: #699
#628 := (* -1::int uf_10)
#623 := (+ #51 #628)
#629 := (<= #623 0::int)
#498 := (not #629)
#597 := (>= #623 0::int)
#381 := (not #259)
#508 := [hypothesis]: #381
#450 := (or #259 #245)
#441 := [def-axiom]: #450
#509 := [unit-resolution #441 #508]: #245
#510 := (or #248 #448)
#511 := [th-lemma]: #510
#500 := [unit-resolution #511 #509]: #448
#743 := (div uf_10 2::int)
#723 := (* -2::int #743)
#545 := (* -2::int #688)
#546 := (+ #545 #723)
#646 := (div #51 2::int)
#645 := (* -2::int #646)
#547 := (+ #645 #546)
#605 := (* -2::int #57)
#549 := (+ #605 #547)
#594 := (* 2::int #56)
#550 := (+ #594 #549)
#598 := (* 2::int uf_10)
#551 := (+ #598 #550)
#563 := (>= #551 2::int)
#520 := (not #563)
#361 := (<= #244 0::int)
#512 := (or #248 #361)
#489 := [th-lemma]: #512
#491 := [unit-resolution #489 #509]: #361
#363 := (>= #252 0::int)
#452 := (or #259 #253)
#453 := [def-axiom]: #452
#492 := [unit-resolution #453 #508]: #253
#493 := (or #256 #363)
#494 := [th-lemma]: #493
#495 := [unit-resolution #494 #492]: #363
#556 := (not #361)
#573 := (not #363)
#521 := (or #520 #573 #556)
#703 := (>= #362 2::int)
#704 := (not #703)
#599 := (or false #704)
#620 := [th-lemma]: #599
#575 := [unit-resolution #620 #81]: #704
#654 := (<= #667 0::int)
#548 := (or #552 #654)
#553 := [th-lemma]: #548
#532 := [unit-resolution #553 #394]: #654
#651 := (+ #645 #666)
#624 := (+ #51 #651)
#626 := (<= #624 0::int)
#650 := (= #624 0::int)
#535 := (or false #650)
#539 := [th-lemma]: #535
#541 := [unit-resolution #539 #81]: #650
#542 := (not #650)
#540 := (or #542 #626)
#543 := [th-lemma]: #540
#531 := [unit-resolution #543 #541]: #626
#587 := [hypothesis]: #361
#724 := (+ #243 #723)
#725 := (+ uf_10 #724)
#727 := (<= #725 0::int)
#722 := (= #725 0::int)
#576 := (or false #722)
#581 := [th-lemma]: #576
#582 := [unit-resolution #581 #81]: #722
#583 := (not #722)
#584 := (or #583 #727)
#585 := [th-lemma]: #584
#586 := [unit-resolution #585 #582]: #727
#534 := [hypothesis]: #563
#555 := [hypothesis]: #363
#616 := (* -1::int #362)
#615 := (* -2::int #222)
#617 := (+ #615 #616)
#618 := (+ #218 #617)
#711 := (+ uf_10 #618)
#708 := (<= #711 0::int)
#606 := (= #711 0::int)
#562 := (or false #606)
#564 := [th-lemma]: #562
#565 := [unit-resolution #564 #81]: #606
#566 := (not #606)
#568 := (or #566 #708)
#569 := [th-lemma]: #568
#570 := [unit-resolution #569 #565]: #708
#518 := [th-lemma #570 #555 #528 #534 #586 #587 #531 #532 #575]: false
#524 := [lemma #518]: #521
#496 := [unit-resolution #524 #495 #491]: #520
#504 := (or #597 #563 #503)
#529 := (not #597)
#522 := [hypothesis]: #529
#519 := (>= #624 0::int)
#530 := (or #542 #519)
#523 := [th-lemma]: #530
#526 := [unit-resolution #523 #541]: #519
#527 := [hypothesis]: #448
#721 := (>= #725 0::int)
#513 := (or #583 #721)
#515 := [th-lemma]: #513
#516 := [unit-resolution #515 #582]: #721
#501 := [th-lemma #499 #516 #527 #526 #522]: #563
#525 := [hypothesis]: #520
#502 := [unit-resolution #525 #501]: false
#505 := [lemma #502]: #504
#497 := [unit-resolution #505 #496 #500]: #597
#485 := (or #498 #529)
#558 := (not #53)
#440 := (or #558 #259)
#262 := (iff #53 #259)
#61 := (- uf_10 #55)
#62 := (div #61 2::int)
#63 := (= #60 #62)
#64 := (not #63)
#58 := (= #56 #57)
#65 := (implies #58 #64)
#66 := (iff #53 #65)
#265 := (iff #66 #262)
#225 := (= #60 #222)
#228 := (not #225)
#234 := (not #58)
#235 := (or #234 #228)
#240 := (iff #53 #235)
#263 := (iff #240 #262)
#260 := (iff #235 #259)
#257 := (iff #228 #256)
#254 := (iff #225 #253)
#255 := [rewrite]: #254
#258 := [monotonicity #255]: #257
#249 := (iff #234 #248)
#246 := (iff #58 #245)
#247 := [rewrite]: #246
#250 := [monotonicity #247]: #249
#261 := [monotonicity #250 #258]: #260
#264 := [monotonicity #261]: #263
#241 := (iff #66 #240)
#238 := (iff #65 #235)
#231 := (implies #58 #228)
#236 := (iff #231 #235)
#237 := [rewrite]: #236
#232 := (iff #65 #231)
#229 := (iff #64 #228)
#226 := (iff #63 #225)
#223 := (= #62 #222)
#220 := (= #61 #219)
#221 := [rewrite]: #220
#224 := [monotonicity #221]: #223
#227 := [monotonicity #224]: #226
#230 := [monotonicity #227]: #229
#233 := [monotonicity #230]: #232
#239 := [trans #233 #237]: #238
#242 := [monotonicity #239]: #241
#266 := [trans #242 #264]: #265
#217 := [asserted]: #66
#267 := [mp #217 #266]: #262
#455 := (not #262)
#765 := (or #558 #259 #455)
#439 := [def-axiom]: #765
#772 := [unit-resolution #439 #267]: #440
#490 := [unit-resolution #772 #508]: #558
#483 := (or #53 #498 #529)
#484 := [th-lemma]: #483
#487 := [unit-resolution #484 #490]: #485
#486 := [unit-resolution #487 #497]: #498
#678 := (<= #686 0::int)
#488 := (or #537 #678)
#477 := [th-lemma]: #488
#478 := [unit-resolution #477 #536]: #678
#479 := (or #256 #449)
#471 := [th-lemma]: #479
#480 := [unit-resolution #471 #492]: #449
#712 := (>= #711 0::int)
#481 := (or #566 #712)
#472 := [th-lemma]: #481
#482 := [unit-resolution #472 #565]: #712
#463 := [th-lemma #482 #480 #478 #486 #507]: false
#464 := [lemma #463]: #259
#771 := (or #53 #381)
#434 := (or #53 #381 #455)
#769 := [def-axiom]: #434
#428 := [unit-resolution #769 #267]: #771
#442 := [unit-resolution #428 #464]: #53
#435 := [monotonicity #442]: #468
#437 := [symm #435]: #602
#438 := (not #602)
#419 := (or #438 #709)
#420 := [th-lemma]: #419
#421 := [unit-resolution #420 #437]: #709
#422 := [th-lemma #421 #414 #499]: false
#423 := [lemma #422]: #448
#410 := (or #245 #503)
#611 := (>= #561 0::int)
#682 := (or #438 #611)
#447 := [th-lemma]: #682
#430 := [unit-resolution #447 #437]: #611
#432 := [hypothesis]: #556
#433 := [th-lemma #532 #432 #430]: false
#412 := [lemma #433]: #361
#409 := (or #245 #556 #503)
#407 := [th-lemma]: #409
#398 := [unit-resolution #407 #412]: #410
#400 := [unit-resolution #398 #423]: #245
#454 := (or #381 #248 #256)
#451 := [def-axiom]: #454
#401 := [unit-resolution #451 #464]: #259
#404 := [unit-resolution #401 #400]: #256
#384 := (or #253 #399)
#429 := [hypothesis]: #573
#443 := (or #558 #597)
#444 := [th-lemma]: #443
#445 := [unit-resolution #444 #442]: #597
#446 := [th-lemma #445 #507 #482 #429 #478]: false
#436 := [lemma #446]: #363
#405 := (or #253 #399 #573)
#379 := [th-lemma]: #405
#385 := [unit-resolution #379 #436]: #384
#390 := [unit-resolution #385 #404]: #399
#392 := (or #558 #629)
#393 := [th-lemma]: #392
#395 := [unit-resolution #393 #442]: #629
[th-lemma #395 #575 #570 #390 #528]: false
unsat