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

+#2 := false
+decl uf_17 :: (-> T8 T3)
+decl uf_18 :: (-> T1 T8)
+decl uf_19 :: T1
+#104 := uf_19
+#105 := (uf_18 uf_19)
+#106 := (uf_17 #105)
+decl uf_15 :: (-> T7 T3)
+decl uf_16 :: (-> int T7)
+#101 := 3::int
+#102 := (uf_16 3::int)
+#103 := (uf_15 #102)
+#107 := (= #103 #106)
+decl uf_13 :: (-> T2 T3)
+decl uf_2 :: (-> T1 T2 T2)
+decl uf_7 :: T2
+#29 := uf_7
+#857 := (uf_2 uf_19 uf_7)
+#859 := (uf_13 #857)
+#599 := (= #859 #106)
+#526 := (= #106 #859)
+#79 := (:var 0 T1)
+#82 := (uf_2 #79 uf_7)
+#932 := (pattern #82)
+#80 := (uf_18 #79)
+#931 := (pattern #80)
+#83 := (uf_13 #82)
+#81 := (uf_17 #80)
+#84 := (= #81 #83)
+#933 := (forall (vars (?x16 T1)) (:pat #931 #932) #84)
+#85 := (forall (vars (?x16 T1)) #84)
+#936 := (iff #85 #933)
+#934 := (iff #84 #84)
+#935 := [refl]: #934
+#937 := [quant-intro #935]: #936
+#347 := (~ #85 #85)
+#384 := (~ #84 #84)
+#385 := [refl]: #384
+#348 := [nnf-pos #385]: #347
+#238 := [asserted]: #85
+#386 := [mp~ #238 #348]: #85
+#938 := [mp #386 #937]: #933
+#861 := (not #933)
+#862 := (or #861 #526)
+#863 := [quant-inst]: #862
+#601 := [unit-resolution #863 #938]: #526
+#588 := [symm #601]: #599
+#586 := (= #103 #859)
+decl uf_1 :: (-> T2 T3)
+#558 := (uf_1 #857)
+#832 := (= #558 #859)
+#5 := (:var 0 T2)
+#66 := (uf_13 #5)
+#908 := (pattern #66)
+#8 := (uf_1 #5)
+#907 := (pattern #8)
+#222 := (= #8 #66)
+#909 := (forall (vars (?x13 T2)) (:pat #907 #908) #222)
+#226 := (forall (vars (?x13 T2)) #222)
+#912 := (iff #226 #909)
+#910 := (iff #222 #222)
+#911 := [refl]: #910
+#913 := [quant-intro #911]: #912
+#341 := (~ #226 #226)
+#375 := (~ #222 #222)
+#376 := [refl]: #375
+#342 := [nnf-pos #376]: #341
+#67 := (= #66 #8)
+#68 := (forall (vars (?x13 T2)) #67)
+#227 := (iff #68 #226)
+#224 := (iff #67 #222)
+#225 := [rewrite]: #224
+#228 := [quant-intro #225]: #227
+#221 := [asserted]: #68
+#231 := [mp #221 #228]: #226
+#377 := [mp~ #231 #342]: #226
+#914 := [mp #377 #913]: #909
+#451 := (not #909)
+#837 := (or #451 #832)
+#547 := [quant-inst]: #837
+#615 := [unit-resolution #547 #914]: #832
+#585 := (= #103 #558)
+decl uf_3 :: (-> int T3)
+decl uf_4 :: (-> T3 int)
+#30 := (uf_1 uf_7)
+#806 := (uf_4 #30)
+#11 := 1::int
+#127 := (uf_3 1::int)
+#130 := (uf_4 #127)
+#649 := (+ #130 #806)
+#794 := (uf_3 #649)
+#597 := (= #794 #558)
+#683 := (= #558 #794)
+#4 := (:var 1 T1)
+#6 := (uf_2 #4 #5)
+#865 := (pattern #6)
+#9 := (uf_4 #8)
+#133 := (+ #9 #130)
+#136 := (uf_3 #133)
+#7 := (uf_1 #6)
+#139 := (= #7 #136)
+#866 := (forall (vars (?x1 T1) (?x2 T2)) (:pat #865) #139)
+#142 := (forall (vars (?x1 T1) (?x2 T2)) #139)
+#869 := (iff #142 #866)
+#867 := (iff #139 #139)
+#868 := [refl]: #867
+#870 := [quant-intro #868]: #869
+#361 := (~ #142 #142)
+#359 := (~ #139 #139)
+#360 := [refl]: #359
+#362 := [nnf-pos #360]: #361
+#10 := 0::int
+#12 := (+ 0::int 1::int)
+#13 := (uf_3 #12)
+#14 := (uf_4 #13)
+#15 := (+ #9 #14)
+#16 := (uf_3 #15)
+#17 := (= #7 #16)
+#18 := (forall (vars (?x1 T1) (?x2 T2)) #17)
+#143 := (iff #18 #142)
+#140 := (iff #17 #139)
+#137 := (= #16 #136)
+#134 := (= #15 #133)
+#131 := (= #14 #130)
+#128 := (= #13 #127)
+#125 := (= #12 1::int)
+#126 := [rewrite]: #125
+#129 := [monotonicity #126]: #128
+#132 := [monotonicity #129]: #131
+#135 := [monotonicity #132]: #134
+#138 := [monotonicity #135]: #137
+#141 := [monotonicity #138]: #140
+#144 := [quant-intro #141]: #143
+#124 := [asserted]: #18
+#147 := [mp #124 #144]: #142
+#363 := [mp~ #147 #362]: #142
+#871 := [mp #363 #870]: #866
+#701 := (not #866)
+#694 := (or #701 #683)
+#688 := (+ #806 #130)
+#689 := (uf_3 #688)
+#690 := (= #558 #689)
+#702 := (or #701 #690)
+#704 := (iff #702 #694)
+#706 := (iff #694 #694)
+#799 := [rewrite]: #706
+#698 := (iff #690 #683)
+#795 := (= #689 #794)
+#797 := (= #688 #649)
+#699 := [rewrite]: #797
+#798 := [monotonicity #699]: #795
+#700 := [monotonicity #798]: #698
+#705 := [monotonicity #700]: #704
+#796 := [trans #705 #799]: #704
+#703 := [quant-inst]: #702
+#800 := [mp #703 #796]: #694
+#614 := [unit-resolution #800 #871]: #683
+#598 := [symm #614]: #597
+#583 := (= #103 #794)
+#595 := (= #127 #794)
+#605 := (= #794 #127)
+#618 := (= #649 1::int)
+#780 := (<= #806 0::int)
+#778 := (= #806 0::int)
+#31 := (uf_3 0::int)
+#858 := (uf_4 #31)
+#855 := (= #858 0::int)
+#72 := (:var 0 int)
+#92 := (uf_3 #72)
+#947 := (pattern #92)
+#266 := (>= #72 0::int)
+#267 := (not #266)
+#93 := (uf_4 #92)
+#248 := (= #72 #93)
+#273 := (or #248 #267)
+#948 := (forall (vars (?x18 int)) (:pat #947) #273)
+#278 := (forall (vars (?x18 int)) #273)
+#951 := (iff #278 #948)
+#949 := (iff #273 #273)
+#950 := [refl]: #949
+#952 := [quant-intro #950]: #951
+#351 := (~ #278 #278)
+#390 := (~ #273 #273)
+#391 := [refl]: #390
+#352 := [nnf-pos #391]: #351
+#94 := (= #93 #72)
+#91 := (<= 0::int #72)
+#95 := (implies #91 #94)
+#96 := (forall (vars (?x18 int)) #95)
+#281 := (iff #96 #278)
+#255 := (not #91)
+#256 := (or #255 #248)
+#261 := (forall (vars (?x18 int)) #256)
+#279 := (iff #261 #278)
+#276 := (iff #256 #273)
+#270 := (or #267 #248)
+#274 := (iff #270 #273)
+#275 := [rewrite]: #274
+#271 := (iff #256 #270)
+#268 := (iff #255 #267)
+#264 := (iff #91 #266)
+#265 := [rewrite]: #264
+#269 := [monotonicity #265]: #268
+#272 := [monotonicity #269]: #271
+#277 := [trans #272 #275]: #276
+#280 := [quant-intro #277]: #279
+#262 := (iff #96 #261)
+#259 := (iff #95 #256)
+#252 := (implies #91 #248)
+#257 := (iff #252 #256)
+#258 := [rewrite]: #257
+#253 := (iff #95 #252)
+#250 := (iff #94 #248)
+#251 := [rewrite]: #250
+#254 := [monotonicity #251]: #253
+#260 := [trans #254 #258]: #259
+#263 := [quant-intro #260]: #262
+#282 := [trans #263 #280]: #281
+#247 := [asserted]: #96
+#283 := [mp #247 #282]: #278
+#392 := [mp~ #283 #352]: #278
+#953 := [mp #392 #952]: #948
+#848 := (not #948)
+#850 := (or #848 #855)
+#527 := (>= 0::int 0::int)
+#860 := (not #527)
+#864 := (= 0::int #858)
+#854 := (or #864 #860)
+#489 := (or #848 #854)
+#851 := (iff #489 #850)
+#852 := (iff #850 #850)
+#838 := [rewrite]: #852
+#847 := (iff #854 #855)
+#843 := (or #855 false)
+#846 := (iff #843 #855)
+#841 := [rewrite]: #846
+#844 := (iff #854 #843)
+#505 := (iff #860 false)
+#1 := true
+#498 := (not true)
+#503 := (iff #498 false)
+#504 := [rewrite]: #503
+#840 := (iff #860 #498)
+#514 := (iff #527 true)
+#856 := [rewrite]: #514
+#502 := [monotonicity #856]: #840
+#842 := [trans #502 #504]: #505
+#513 := (iff #864 #855)
+#518 := [rewrite]: #513
+#845 := [monotonicity #518 #842]: #844
+#484 := [trans #845 #841]: #847
+#849 := [monotonicity #484]: #851
+#839 := [trans #849 #838]: #851
+#490 := [quant-inst]: #489
+#546 := [mp #490 #839]: #850
+#644 := [unit-resolution #546 #953]: #855
+#621 := (= #806 #858)
+#32 := (= #30 #31)
+#159 := [asserted]: #32
+#626 := [monotonicity #159]: #621
+#616 := [trans #626 #644]: #778
+#606 := (not #778)
+#608 := (or #606 #780)
+#609 := [th-lemma]: #608
+#612 := [unit-resolution #609 #616]: #780
+#790 := (>= #806 0::int)
+#613 := (or #606 #790)
+#617 := [th-lemma]: #613
+#610 := [unit-resolution #617 #616]: #790
+#723 := (<= #130 1::int)
+#746 := (= #130 1::int)
+#713 := (or #848 #746)
+#755 := (>= 1::int 0::int)
+#756 := (not #755)
+#743 := (= 1::int #130)
+#744 := (or #743 #756)
+#714 := (or #848 #744)
+#718 := (iff #714 #713)
+#720 := (iff #713 #713)
+#725 := [rewrite]: #720
+#739 := (iff #744 #746)
+#735 := (or #746 false)
+#738 := (iff #735 #746)
+#733 := [rewrite]: #738
+#736 := (iff #744 #735)
+#731 := (iff #756 false)
+#734 := (iff #756 #498)
+#742 := (iff #755 true)
+#748 := [rewrite]: #742
+#730 := [monotonicity #748]: #734
+#732 := [trans #730 #504]: #731
+#745 := (iff #743 #746)
+#747 := [rewrite]: #745
+#737 := [monotonicity #747 #732]: #736
+#712 := [trans #737 #733]: #739
+#719 := [monotonicity #712]: #718
+#721 := [trans #719 #725]: #718
+#607 := [quant-inst]: #714
+#722 := [mp #607 #721]: #713
+#641 := [unit-resolution #722 #953]: #746
+#620 := (not #746)
+#623 := (or #620 #723)
+#627 := [th-lemma]: #623
+#629 := [unit-resolution #627 #641]: #723
+#726 := (>= #130 1::int)
+#630 := (or #620 #726)
+#628 := [th-lemma]: #630
+#631 := [unit-resolution #628 #641]: #726
+#611 := [th-lemma #631 #629 #610 #612]: #618
+#587 := [monotonicity #611]: #605
+#596 := [symm #587]: #595
+#581 := (= #103 #127)
+decl uf_5 :: (-> T4 T3)
+decl uf_8 :: T4
+#33 := uf_8
+#34 := (uf_5 uf_8)
+#822 := (uf_4 #34)
+#824 := (+ #130 #822)
+#666 := (uf_3 #824)
+#593 := (= #666 #127)
+#589 := (= #127 #666)
+#624 := (= 1::int #824)
+#619 := (= #824 1::int)
+#789 := (<= #822 0::int)
+#787 := (= #822 0::int)
+#632 := (= #822 #858)
+#35 := (= #34 #31)
+#162 := (= #31 #34)
+#163 := (iff #35 #162)
+#164 := [rewrite]: #163
+#160 := [asserted]: #35
+#167 := [mp #160 #164]: #162
+#662 := [symm #167]: #35
+#633 := [monotonicity #662]: #632
+#634 := [trans #633 #644]: #787
+#635 := (not #787)
+#637 := (or #635 #789)
+#638 := [th-lemma]: #637
+#639 := [unit-resolution #638 #634]: #789
+#781 := (>= #822 0::int)
+#481 := (or #635 #781)
+#640 := [th-lemma]: #481
+#636 := [unit-resolution #640 #634]: #781
+#622 := [th-lemma #631 #629 #636 #639]: #619
+#625 := [symm #622]: #624
+#590 := [monotonicity #625]: #589
+#594 := [symm #590]: #593
+#579 := (= #103 #666)
+decl uf_6 :: (-> int T4 T4)
+#539 := (uf_6 3::int uf_8)
+#836 := (uf_5 #539)
+#810 := (= #836 #666)
+#813 := (= #666 #836)
+#20 := (:var 0 T4)
+#19 := (:var 1 int)
+#21 := (uf_6 #19 #20)
+#872 := (pattern #21)
+#23 := (uf_5 #20)
+#24 := (uf_4 #23)
+#146 := (+ #24 #130)
+#150 := (uf_3 #146)
+#22 := (uf_5 #21)
+#153 := (= #22 #150)
+#873 := (forall (vars (?x3 int) (?x4 T4)) (:pat #872) #153)
+#156 := (forall (vars (?x3 int) (?x4 T4)) #153)
+#876 := (iff #156 #873)
+#874 := (iff #153 #153)
+#875 := [refl]: #874
+#877 := [quant-intro #875]: #876
+#328 := (~ #156 #156)
+#364 := (~ #153 #153)
+#365 := [refl]: #364
+#326 := [nnf-pos #365]: #328
+#25 := (+ #24 #14)
+#26 := (uf_3 #25)
+#27 := (= #22 #26)
+#28 := (forall (vars (?x3 int) (?x4 T4)) #27)
+#157 := (iff #28 #156)
+#154 := (iff #27 #153)
+#151 := (= #26 #150)
+#148 := (= #25 #146)
+#149 := [monotonicity #132]: #148
+#152 := [monotonicity #149]: #151
+#155 := [monotonicity #152]: #154
+#158 := [quant-intro #155]: #157
+#145 := [asserted]: #28
+#161 := [mp #145 #158]: #156
+#366 := [mp~ #161 #326]: #156
+#878 := [mp #366 #877]: #873
+#809 := (not #873)
+#816 := (or #809 #813)
+#817 := (+ #822 #130)
+#818 := (uf_3 #817)
+#823 := (= #836 #818)
+#645 := (or #809 #823)
+#648 := (iff #645 #816)
+#802 := (iff #816 #816)
+#804 := [rewrite]: #802
+#814 := (iff #823 #813)
+#807 := (iff #810 #813)
+#808 := [rewrite]: #807
+#811 := (iff #823 #810)
+#667 := (= #818 #666)
+#819 := (= #817 #824)
+#825 := [rewrite]: #819
+#668 := [monotonicity #825]: #667
+#812 := [monotonicity #668]: #811
+#815 := [trans #812 #808]: #814
+#801 := [monotonicity #815]: #648
+#805 := [trans #801 #804]: #648
+#647 := [quant-inst]: #645
+#803 := [mp #647 #805]: #816
+#658 := [unit-resolution #803 #878]: #813
+#592 := [symm #658]: #810
+#600 := (= #103 #836)
+decl uf_14 :: (-> T4 T3)
+#540 := (uf_14 #539)
+#548 := (= #540 #836)
+#69 := (uf_14 #20)
+#916 := (pattern #69)
+#915 := (pattern #23)
+#230 := (= #23 #69)
+#917 := (forall (vars (?x14 T4)) (:pat #915 #916) #230)
+#234 := (forall (vars (?x14 T4)) #230)
+#920 := (iff #234 #917)
+#918 := (iff #230 #230)
+#919 := [refl]: #918
+#921 := [quant-intro #919]: #920
+#343 := (~ #234 #234)
+#378 := (~ #230 #230)
+#379 := [refl]: #378
+#344 := [nnf-pos #379]: #343
+#70 := (= #69 #23)
+#71 := (forall (vars (?x14 T4)) #70)
+#235 := (iff #71 #234)
+#232 := (iff #70 #230)
+#233 := [rewrite]: #232
+#236 := [quant-intro #233]: #235
+#229 := [asserted]: #71
+#239 := [mp #229 #236]: #234
+#380 := [mp~ #239 #344]: #234
+#922 := [mp #380 #921]: #917
+#541 := (not #917)
+#828 := (or #541 #548)
+#833 := (= #836 #540)
+#829 := (or #541 #833)
+#826 := (iff #829 #828)
+#827 := (iff #828 #828)
+#831 := [rewrite]: #827
+#549 := (iff #833 #548)
+#550 := [rewrite]: #549
+#830 := [monotonicity #550]: #826
+#820 := [trans #830 #831]: #826
+#543 := [quant-inst]: #829
+#821 := [mp #543 #820]: #828
+#657 := [unit-resolution #821 #922]: #548
+#521 := (= #103 #540)
+#75 := (uf_6 #72 uf_8)
+#924 := (pattern #75)
+#73 := (uf_16 #72)
+#923 := (pattern #73)
+#76 := (uf_14 #75)
+#74 := (uf_15 #73)
+#77 := (= #74 #76)
+#925 := (forall (vars (?x15 int)) (:pat #923 #924) #77)
+#78 := (forall (vars (?x15 int)) #77)
+#928 := (iff #78 #925)
+#926 := (iff #77 #77)
+#927 := [refl]: #926
+#929 := [quant-intro #927]: #928
+#345 := (~ #78 #78)
+#381 := (~ #77 #77)
+#382 := [refl]: #381
+#346 := [nnf-pos #382]: #345
+#237 := [asserted]: #78
+#383 := [mp~ #237 #346]: #78
+#930 := [mp #383 #929]: #925
+#515 := (not #925)
+#646 := (or #515 #521)
+#853 := [quant-inst]: #646
+#603 := [unit-resolution #853 #930]: #521
+#577 := [trans #603 #657]: #600
+#580 := [trans #577 #592]: #579
+#582 := [trans #580 #594]: #581
+#584 := [trans #582 #596]: #583
+#578 := [trans #584 #598]: #585
+#571 := [trans #578 #615]: #586
+#572 := [trans #571 #588]: #107
+#108 := (not #107)
+#325 := [asserted]: #108
+[unit-resolution #325 #572]: false
+unsat