--- a/src/HOL/SMT/Examples/cert/z3_hol_05.proof Tue Feb 02 18:11:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,464 +0,0 @@
-#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