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

tuned structure; moved non-related quickcheck.setup to Code_Generator.thy

#2 := false
decl uf_2 :: (-> T2 T3 T3)
decl uf_4 :: T3
#15 := uf_4
decl uf_6 :: (-> int T2)
#48 := 2::int
#49 := (uf_6 2::int)
#50 := (uf_2 #49 uf_4)
#23 := 1::int
#44 := (uf_6 1::int)
#51 := (uf_2 #44 #50)
decl uf_1 :: (-> T1 T3 T3)
#45 := (uf_2 #44 uf_4)
#31 := 0::int
#43 := (uf_6 0::int)
#46 := (uf_2 #43 #45)
decl uf_5 :: T1
#19 := uf_5
#47 := (uf_1 uf_5 #46)
#52 := (= #47 #51)
#266 := (uf_1 uf_5 #45)
decl uf_3 :: (-> T1 T2 T2)
#352 := (uf_3 uf_5 #43)
#267 := (uf_2 #352 #266)
#797 := (= #267 #51)
#795 := (= #51 #267)
#758 := (= #50 #266)
#521 := (uf_1 uf_5 uf_4)
#522 := (uf_3 uf_5 #44)
#523 := (uf_2 #522 #521)
#756 := (= #523 #266)
#616 := (= #266 #523)
#6 := (:var 0 T3)
#4 := (:var 2 T1)
#10 := (uf_1 #4 #6)
#5 := (:var 1 T2)
#9 := (uf_3 #4 #5)
#11 := (uf_2 #9 #10)
#683 := (pattern #11)
#7 := (uf_2 #5 #6)
#8 := (uf_1 #4 #7)
#682 := (pattern #8)
#12 := (= #8 #11)
#684 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3)) (:pat #682 #683) #12)
#13 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3)) #12)
#687 := (iff #13 #684)
#685 := (iff #12 #12)
#686 := [refl]: #685
#688 := [quant-intro #686]: #687
#195 := (~ #13 #13)
#193 := (~ #12 #12)
#194 := [refl]: #193
#196 := [nnf-pos #194]: #195
#69 := [asserted]: #13
#197 := [mp~ #69 #196]: #13
#689 := [mp #197 #688]: #684
#345 := (not #684)
#604 := (or #345 #616)
#606 := [quant-inst]: #604
#277 := [unit-resolution #606 #689]: #616
#757 := [symm #277]: #756
#754 := (= #50 #523)
#569 := (= uf_4 #521)
#14 := (:var 0 T1)
#16 := (uf_1 #14 uf_4)
#690 := (pattern #16)
#71 := (= uf_4 #16)
#691 := (forall (vars (?x4 T1)) (:pat #690) #71)
#74 := (forall (vars (?x4 T1)) #71)
#694 := (iff #74 #691)
#692 := (iff #71 #71)
#693 := [refl]: #692
#695 := [quant-intro #693]: #694
#180 := (~ #74 #74)
#198 := (~ #71 #71)
#199 := [refl]: #198
#178 := [nnf-pos #199]: #180
#17 := (= #16 uf_4)
#18 := (forall (vars (?x4 T1)) #17)
#75 := (iff #18 #74)
#72 := (iff #17 #71)
#73 := [rewrite]: #72
#76 := [quant-intro #73]: #75
#70 := [asserted]: #18
#79 := [mp #70 #76]: #74
#200 := [mp~ #79 #178]: #74
#696 := [mp #200 #695]: #691
#572 := (not #691)
#573 := (or #572 #569)
#574 := [quant-inst]: #573
#282 := [unit-resolution #574 #696]: #569
#752 := (= #49 #522)
decl uf_7 :: (-> T2 int)
#666 := (uf_7 #44)
#595 := (+ 1::int #666)
#597 := (uf_6 #595)
#748 := (= #597 #522)
#605 := (= #522 #597)
#20 := (:var 0 T2)
#22 := (uf_7 #20)
#698 := (pattern #22)
#21 := (uf_3 uf_5 #20)
#697 := (pattern #21)
#78 := (+ 1::int #22)
#82 := (uf_6 #78)
#85 := (= #21 #82)
#699 := (forall (vars (?x5 T2)) (:pat #697 #698) #85)
#88 := (forall (vars (?x5 T2)) #85)
#702 := (iff #88 #699)
#700 := (iff #85 #85)
#701 := [refl]: #700
#703 := [quant-intro #701]: #702
#181 := (~ #88 #88)
#201 := (~ #85 #85)
#202 := [refl]: #201
#182 := [nnf-pos #202]: #181
#24 := (+ #22 1::int)
#25 := (uf_6 #24)
#26 := (= #21 #25)
#27 := (forall (vars (?x5 T2)) #26)
#89 := (iff #27 #88)
#86 := (iff #26 #85)
#83 := (= #25 #82)
#80 := (= #24 #78)
#81 := [rewrite]: #80
#84 := [monotonicity #81]: #83
#87 := [monotonicity #84]: #86
#90 := [quant-intro #87]: #89
#77 := [asserted]: #27
#93 := [mp #77 #90]: #88
#203 := [mp~ #93 #182]: #88
#704 := [mp #203 #703]: #699
#607 := (not #699)
#600 := (or #607 #605)
#601 := [quant-inst]: #600
#269 := [unit-resolution #601 #704]: #605
#749 := [symm #269]: #748
#750 := (= #49 #597)
#499 := (uf_7 #597)
#337 := (uf_6 #499)
#318 := (= #337 #597)
#28 := (uf_6 #22)
#92 := (= #20 #28)
#705 := (forall (vars (?x6 T2)) (:pat #698) #92)
#96 := (forall (vars (?x6 T2)) #92)
#706 := (iff #96 #705)
#708 := (iff #705 #705)
#709 := [rewrite]: #708
#707 := [rewrite]: #706
#710 := [trans #707 #709]: #706
#183 := (~ #96 #96)
#204 := (~ #92 #92)
#205 := [refl]: #204
#184 := [nnf-pos #205]: #183
#29 := (= #28 #20)
#30 := (forall (vars (?x6 T2)) #29)
#97 := (iff #30 #96)
#94 := (iff #29 #92)
#95 := [rewrite]: #94
#98 := [quant-intro #95]: #97
#91 := [asserted]: #30
#101 := [mp #91 #98]: #96
#206 := [mp~ #101 #184]: #96
#711 := [mp #206 #710]: #705
#376 := (not #705)
#325 := (or #376 #318)
#316 := (= #597 #337)
#326 := (or #376 #316)
#328 := (iff #326 #325)
#329 := (iff #325 #325)
#310 := [rewrite]: #329
#323 := (iff #316 #318)
#324 := [rewrite]: #323
#317 := [monotonicity #324]: #328
#312 := [trans #317 #310]: #328
#327 := [quant-inst]: #326
#313 := [mp #327 #312]: #325
#271 := [unit-resolution #313 #711]: #318
#746 := (= #49 #337)
#744 := (= 2::int #499)
#742 := (= #499 2::int)
#578 := -1::int
#513 := (* -1::int #666)
#514 := (+ #499 #513)
#474 := (<= #514 1::int)
#512 := (= #514 1::int)
#504 := (>= #666 -1::int)
#586 := (>= #666 1::int)
#378 := (= #666 1::int)
#32 := (:var 0 int)
#34 := (uf_6 #32)
#712 := (pattern #34)
#118 := (>= #32 0::int)
#119 := (not #118)
#35 := (uf_7 #34)
#100 := (= #32 #35)
#125 := (or #100 #119)
#713 := (forall (vars (?x7 int)) (:pat #712) #125)
#130 := (forall (vars (?x7 int)) #125)
#716 := (iff #130 #713)
#714 := (iff #125 #125)
#715 := [refl]: #714
#717 := [quant-intro #715]: #716
#185 := (~ #130 #130)
#207 := (~ #125 #125)
#208 := [refl]: #207
#186 := [nnf-pos #208]: #185
#36 := (= #35 #32)
#33 := (<= 0::int #32)
#37 := (implies #33 #36)
#38 := (forall (vars (?x7 int)) #37)
#133 := (iff #38 #130)
#107 := (not #33)
#108 := (or #107 #100)
#113 := (forall (vars (?x7 int)) #108)
#131 := (iff #113 #130)
#128 := (iff #108 #125)
#122 := (or #119 #100)
#126 := (iff #122 #125)
#127 := [rewrite]: #126
#123 := (iff #108 #122)
#120 := (iff #107 #119)
#116 := (iff #33 #118)
#117 := [rewrite]: #116
#121 := [monotonicity #117]: #120
#124 := [monotonicity #121]: #123
#129 := [trans #124 #127]: #128
#132 := [quant-intro #129]: #131
#114 := (iff #38 #113)
#111 := (iff #37 #108)
#104 := (implies #33 #100)
#109 := (iff #104 #108)
#110 := [rewrite]: #109
#105 := (iff #37 #104)
#102 := (iff #36 #100)
#103 := [rewrite]: #102
#106 := [monotonicity #103]: #105
#112 := [trans #106 #110]: #111
#115 := [quant-intro #112]: #114
#134 := [trans #115 #132]: #133
#99 := [asserted]: #38
#135 := [mp #99 #134]: #130
#209 := [mp~ #135 #186]: #130
#718 := [mp #209 #717]: #713
#673 := (not #713)
#365 := (or #673 #378)
#307 := (>= 1::int 0::int)
#668 := (not #307)
#669 := (= 1::int #666)
#655 := (or #669 #668)
#366 := (or #673 #655)
#645 := (iff #366 #365)
#360 := (iff #365 #365)
#643 := [rewrite]: #360
#654 := (iff #655 #378)
#374 := (or #378 false)
#653 := (iff #374 #378)
#650 := [rewrite]: #653
#375 := (iff #655 #374)
#651 := (iff #668 false)
#1 := true
#670 := (not true)
#677 := (iff #670 false)
#678 := [rewrite]: #677
#381 := (iff #668 #670)
#379 := (iff #307 true)
#380 := [rewrite]: #379
#274 := [monotonicity #380]: #381
#652 := [trans #274 #678]: #651
#656 := (iff #669 #378)
#363 := [rewrite]: #656
#649 := [monotonicity #363 #652]: #375
#364 := [trans #649 #650]: #654
#646 := [monotonicity #364]: #645
#647 := [trans #646 #643]: #645
#367 := [quant-inst]: #366
#644 := [mp #367 #647]: #365
#272 := [unit-resolution #644 #718]: #378
#270 := (not #378)
#273 := (or #270 #586)
#725 := [th-lemma]: #273
#726 := [unit-resolution #725 #272]: #586
#727 := (not #586)
#728 := (or #727 #504)
#729 := [th-lemma]: #728
#730 := [unit-resolution #729 #726]: #504
#481 := (not #504)
#496 := (or #673 #481 #512)
#509 := (>= #595 0::int)
#468 := (not #509)
#501 := (= #595 #499)
#503 := (or #501 #468)
#497 := (or #673 #503)
#470 := (iff #497 #496)
#491 := (or #481 #512)
#498 := (or #673 #491)
#467 := (iff #498 #496)
#469 := [rewrite]: #467
#459 := (iff #497 #498)
#494 := (iff #503 #491)
#488 := (or #512 #481)
#492 := (iff #488 #491)
#493 := [rewrite]: #492
#489 := (iff #503 #488)
#486 := (iff #468 #481)
#525 := (iff #509 #504)
#480 := [rewrite]: #525
#487 := [monotonicity #480]: #486
#510 := (iff #501 #512)
#524 := [rewrite]: #510
#490 := [monotonicity #524 #487]: #489
#495 := [trans #490 #493]: #494
#460 := [monotonicity #495]: #459
#471 := [trans #460 #469]: #470
#482 := [quant-inst]: #497
#473 := [mp #482 #471]: #496
#731 := [unit-resolution #473 #718 #730]: #512
#732 := (not #512)
#733 := (or #732 #474)
#734 := [th-lemma]: #733
#735 := [unit-resolution #734 #731]: #474
#475 := (>= #514 1::int)
#736 := (or #732 #475)
#737 := [th-lemma]: #736
#738 := [unit-resolution #737 #731]: #475
#582 := (<= #666 1::int)
#739 := (or #270 #582)
#740 := [th-lemma]: #739
#741 := [unit-resolution #740 #272]: #582
#743 := [th-lemma #726 #741 #738 #735]: #742
#745 := [symm #743]: #744
#747 := [monotonicity #745]: #746
#751 := [trans #747 #271]: #750
#753 := [trans #751 #749]: #752
#755 := [monotonicity #753 #282]: #754
#759 := [trans #755 #757]: #758
#792 := (= #44 #352)
#358 := (uf_7 #43)
#613 := (+ 1::int #358)
#617 := (uf_6 #613)
#788 := (= #617 #352)
#598 := (= #352 #617)
#608 := (or #607 #598)
#609 := [quant-inst]: #608
#760 := [unit-resolution #609 #704]: #598
#789 := [symm #760]: #788
#790 := (= #44 #617)
#575 := (uf_7 #617)
#390 := (uf_6 #575)
#382 := (= #390 #617)
#385 := (or #376 #382)
#392 := (= #617 #390)
#386 := (or #376 #392)
#387 := (iff #386 #385)
#369 := (iff #385 #385)
#370 := [rewrite]: #369
#383 := (iff #392 #382)
#384 := [rewrite]: #383
#368 := [monotonicity #384]: #387
#361 := [trans #368 #370]: #387
#377 := [quant-inst]: #386
#371 := [mp #377 #361]: #385
#761 := [unit-resolution #371 #711]: #382
#786 := (= #44 #390)
#784 := (= 1::int #575)
#782 := (= #575 1::int)
#568 := (* -1::int #575)
#579 := (+ #358 #568)
#535 := (<= #579 -1::int)
#557 := (= #579 -1::int)
#561 := (>= #358 -1::int)
#585 := (>= #358 0::int)
#676 := (= #358 0::int)
#315 := (or #673 #676)
#268 := (>= 0::int 0::int)
#354 := (not #268)
#355 := (= 0::int #358)
#359 := (or #355 #354)
#657 := (or #673 #359)
#320 := (iff #657 #315)
#322 := (iff #315 #315)
#659 := [rewrite]: #322
#672 := (iff #359 #676)
#675 := (or #676 false)
#330 := (iff #675 #676)
#335 := [rewrite]: #330
#681 := (iff #359 #675)
#679 := (iff #354 false)
#343 := (iff #354 #670)
#332 := (iff #268 true)
#463 := [rewrite]: #332
#344 := [monotonicity #463]: #343
#680 := [trans #344 #678]: #679
#338 := (iff #355 #676)
#674 := [rewrite]: #338
#671 := [monotonicity #674 #680]: #681
#331 := [trans #671 #335]: #672
#321 := [monotonicity #331]: #320
#660 := [trans #321 #659]: #320
#319 := [quant-inst]: #657
#661 := [mp #319 #660]: #315
#762 := [unit-resolution #661 #718]: #676
#763 := (not #676)
#764 := (or #763 #585)
#765 := [th-lemma]: #764
#766 := [unit-resolution #765 #762]: #585
#767 := (not #585)
#768 := (or #767 #561)
#769 := [th-lemma]: #768
#770 := [unit-resolution #769 #766]: #561
#564 := (not #561)
#549 := (or #673 #557 #564)
#570 := (>= #613 0::int)
#571 := (not #570)
#576 := (= #613 #575)
#577 := (or #576 #571)
#552 := (or #673 #577)
#530 := (iff #552 #549)
#551 := (or #557 #564)
#554 := (or #673 #551)
#556 := (iff #554 #549)
#529 := [rewrite]: #556
#555 := (iff #552 #554)
#547 := (iff #577 #551)
#559 := (iff #571 #564)
#562 := (iff #570 #561)
#563 := [rewrite]: #562
#565 := [monotonicity #563]: #559
#558 := (iff #576 #557)
#560 := [rewrite]: #558
#548 := [monotonicity #560 #565]: #547
#550 := [monotonicity #548]: #555
#531 := [trans #550 #529]: #530
#553 := [quant-inst]: #552
#424 := [mp #553 #531]: #549
#771 := [unit-resolution #424 #718 #770]: #557
#772 := (not #557)
#773 := (or #772 #535)
#774 := [th-lemma]: #773
#775 := [unit-resolution #774 #771]: #535
#536 := (>= #579 -1::int)
#776 := (or #772 #536)
#777 := [th-lemma]: #776
#778 := [unit-resolution #777 #771]: #536
#584 := (<= #358 0::int)
#779 := (or #763 #584)
#780 := [th-lemma]: #779
#781 := [unit-resolution #780 #762]: #584
#783 := [th-lemma #766 #781 #778 #775]: #782
#785 := [symm #783]: #784
#787 := [monotonicity #785]: #786
#791 := [trans #787 #761]: #790
#793 := [trans #791 #789]: #792
#796 := [monotonicity #793 #759]: #795
#798 := [symm #796]: #797
#353 := (= #47 #267)
#356 := (or #345 #353)
#357 := [quant-inst]: #356
#794 := [unit-resolution #357 #689]: #353
#799 := [trans #794 #798]: #52
#53 := (not #52)
#177 := [asserted]: #53
[unit-resolution #177 #799]: false
unsat