--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_nat_arith_03.proof Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,367 @@
+#2 := false
+#9 := 0::int
+decl uf_2 :: (-> T1 int)
+decl uf_3 :: T1
+#22 := uf_3
+#23 := (uf_2 uf_3)
+#469 := (= #23 0::int)
+decl uf_1 :: (-> int T1)
+#251 := (uf_1 #23)
+#557 := (uf_2 #251)
+#558 := (= #557 0::int)
+#556 := (>= #23 0::int)
+#477 := (not #556)
+#144 := -1::int
+#348 := (>= #23 -1::int)
+#628 := (not #348)
+#21 := 1::int
+#24 := (+ 1::int #23)
+#25 := (uf_1 #24)
+#26 := (uf_2 #25)
+#632 := (* -1::int #26)
+#636 := (+ #23 #632)
+#633 := (= #636 -1::int)
+#471 := (not #633)
+#613 := (<= #636 -1::int)
+#527 := (not #613)
+#145 := (* -1::int #23)
+#146 := (+ #145 #26)
+#149 := (uf_1 #146)
+#152 := (uf_2 #149)
+#504 := (+ #632 #152)
+#505 := (+ #23 #504)
+#573 := (>= #505 0::int)
+#502 := (= #505 0::int)
+#599 := (<= #636 0::int)
+#526 := [hypothesis]: #613
+#491 := (or #527 #599)
+#515 := [th-lemma]: #491
+#516 := [unit-resolution #515 #526]: #599
+#587 := (not #599)
+#578 := (or #502 #587)
+#10 := (:var 0 int)
+#12 := (uf_1 #10)
+#673 := (pattern #12)
+#76 := (>= #10 0::int)
+#77 := (not #76)
+#13 := (uf_2 #12)
+#58 := (= #10 #13)
+#83 := (or #58 #77)
+#674 := (forall (vars (?x2 int)) (:pat #673) #83)
+#88 := (forall (vars (?x2 int)) #83)
+#677 := (iff #88 #674)
+#675 := (iff #83 #83)
+#676 := [refl]: #675
+#678 := [quant-intro #676]: #677
+#179 := (~ #88 #88)
+#191 := (~ #83 #83)
+#192 := [refl]: #191
+#177 := [nnf-pos #192]: #179
+#14 := (= #13 #10)
+#11 := (<= 0::int #10)
+#15 := (implies #11 #14)
+#16 := (forall (vars (?x2 int)) #15)
+#91 := (iff #16 #88)
+#65 := (not #11)
+#66 := (or #65 #58)
+#71 := (forall (vars (?x2 int)) #66)
+#89 := (iff #71 #88)
+#86 := (iff #66 #83)
+#80 := (or #77 #58)
+#84 := (iff #80 #83)
+#85 := [rewrite]: #84
+#81 := (iff #66 #80)
+#78 := (iff #65 #77)
+#74 := (iff #11 #76)
+#75 := [rewrite]: #74
+#79 := [monotonicity #75]: #78
+#82 := [monotonicity #79]: #81
+#87 := [trans #82 #85]: #86
+#90 := [quant-intro #87]: #89
+#72 := (iff #16 #71)
+#69 := (iff #15 #66)
+#62 := (implies #11 #58)
+#67 := (iff #62 #66)
+#68 := [rewrite]: #67
+#63 := (iff #15 #62)
+#60 := (iff #14 #58)
+#61 := [rewrite]: #60
+#64 := [monotonicity #61]: #63
+#70 := [trans #64 #68]: #69
+#73 := [quant-intro #70]: #72
+#92 := [trans #73 #90]: #91
+#57 := [asserted]: #16
+#93 := [mp #57 #92]: #88
+#193 := [mp~ #93 #177]: #88
+#679 := [mp #193 #678]: #674
+#644 := (not #674)
+#591 := (or #644 #502 #587)
+#498 := (>= #146 0::int)
+#500 := (not #498)
+#501 := (= #146 #152)
+#494 := (or #501 #500)
+#592 := (or #644 #494)
+#579 := (iff #592 #591)
+#593 := (or #644 #578)
+#584 := (iff #593 #591)
+#585 := [rewrite]: #584
+#582 := (iff #592 #593)
+#580 := (iff #494 #578)
+#589 := (iff #500 #587)
+#596 := (iff #498 #599)
+#600 := [rewrite]: #596
+#581 := [monotonicity #600]: #589
+#503 := (iff #501 #502)
+#506 := [rewrite]: #503
+#590 := [monotonicity #506 #581]: #580
+#583 := [monotonicity #590]: #582
+#586 := [trans #583 #585]: #579
+#588 := [quant-inst]: #592
+#570 := [mp #588 #586]: #591
+#511 := [unit-resolution #570 #679]: #578
+#517 := [unit-resolution #511 #516]: #502
+#485 := (not #502)
+#492 := (or #485 #573)
+#451 := [th-lemma]: #492
+#482 := [unit-resolution #451 #517]: #573
+#554 := (<= #152 0::int)
+#163 := (* -1::int #152)
+#138 := (uf_1 0::int)
+#141 := (uf_2 #138)
+#164 := (+ #141 #163)
+#162 := (>= #164 0::int)
+#30 := (- #26 #23)
+#31 := (uf_1 #30)
+#32 := (uf_2 #31)
+#27 := (* 0::int #26)
+#28 := (uf_1 #27)
+#29 := (uf_2 #28)
+#33 := (< #29 #32)
+#34 := (not #33)
+#174 := (iff #34 #162)
+#155 := (< #141 #152)
+#158 := (not #155)
+#172 := (iff #158 #162)
+#161 := (not #162)
+#167 := (not #161)
+#170 := (iff #167 #162)
+#171 := [rewrite]: #170
+#168 := (iff #158 #167)
+#165 := (iff #155 #161)
+#166 := [rewrite]: #165
+#169 := [monotonicity #166]: #168
+#173 := [trans #169 #171]: #172
+#159 := (iff #34 #158)
+#156 := (iff #33 #155)
+#153 := (= #32 #152)
+#150 := (= #31 #149)
+#147 := (= #30 #146)
+#148 := [rewrite]: #147
+#151 := [monotonicity #148]: #150
+#154 := [monotonicity #151]: #153
+#142 := (= #29 #141)
+#139 := (= #28 #138)
+#136 := (= #27 0::int)
+#137 := [rewrite]: #136
+#140 := [monotonicity #137]: #139
+#143 := [monotonicity #140]: #142
+#157 := [monotonicity #143 #154]: #156
+#160 := [monotonicity #157]: #159
+#175 := [trans #160 #173]: #174
+#135 := [asserted]: #34
+#176 := [mp #135 #175]: #162
+#651 := (<= #141 0::int)
+#662 := (= #141 0::int)
+#645 := (or #644 #662)
+#316 := (>= 0::int 0::int)
+#446 := (not #316)
+#328 := (= 0::int #141)
+#660 := (or #328 #446)
+#646 := (or #644 #660)
+#647 := (iff #646 #645)
+#648 := (iff #645 #645)
+#650 := [rewrite]: #648
+#642 := (iff #660 #662)
+#640 := (or #662 false)
+#305 := (iff #640 #662)
+#306 := [rewrite]: #305
+#303 := (iff #660 #640)
+#656 := (iff #446 false)
+#1 := true
+#654 := (not true)
+#655 := (iff #654 false)
+#315 := [rewrite]: #655
+#314 := (iff #446 #654)
+#658 := (iff #316 true)
+#664 := [rewrite]: #658
+#319 := [monotonicity #664]: #314
+#299 := [trans #319 #315]: #656
+#661 := (iff #328 #662)
+#663 := [rewrite]: #661
+#304 := [monotonicity #663 #299]: #303
+#643 := [trans #304 #306]: #642
+#285 := [monotonicity #643]: #647
+#290 := [trans #285 #650]: #647
+#641 := [quant-inst]: #646
+#291 := [mp #641 #290]: #645
+#484 := [unit-resolution #291 #679]: #662
+#486 := (not #662)
+#493 := (or #486 #651)
+#495 := [th-lemma]: #493
+#496 := [unit-resolution #495 #484]: #651
+#497 := (not #651)
+#507 := (or #554 #497 #161)
+#487 := [th-lemma]: #507
+#508 := [unit-resolution #487 #496 #176]: #554
+#463 := [th-lemma #508 #526 #482]: false
+#464 := [lemma #463]: #527
+#472 := (or #471 #613)
+#473 := [th-lemma]: #472
+#474 := [unit-resolution #473 #464]: #471
+#631 := (or #628 #633)
+#618 := (or #644 #628 #633)
+#634 := (>= #24 0::int)
+#635 := (not #634)
+#357 := (= #24 #26)
+#358 := (or #357 #635)
+#623 := (or #644 #358)
+#610 := (iff #623 #618)
+#619 := (or #644 #631)
+#467 := (iff #619 #618)
+#468 := [rewrite]: #467
+#625 := (iff #623 #619)
+#622 := (iff #358 #631)
+#626 := (or #633 #628)
+#620 := (iff #626 #631)
+#621 := [rewrite]: #620
+#630 := (iff #358 #626)
+#629 := (iff #635 #628)
+#349 := (iff #634 #348)
+#350 := [rewrite]: #349
+#344 := [monotonicity #350]: #629
+#637 := (iff #357 #633)
+#347 := [rewrite]: #637
+#627 := [monotonicity #347 #344]: #630
+#617 := [trans #627 #621]: #622
+#466 := [monotonicity #617]: #625
+#611 := [trans #466 #468]: #610
+#624 := [quant-inst]: #623
+#612 := [mp #624 #611]: #618
+#475 := [unit-resolution #612 #679]: #631
+#476 := [unit-resolution #475 #474]: #628
+#478 := (or #477 #348)
+#479 := [th-lemma]: #478
+#480 := [unit-resolution #479 #476]: #477
+#560 := (or #556 #558)
+#18 := (= #13 0::int)
+#124 := (or #18 #76)
+#680 := (forall (vars (?x3 int)) (:pat #673) #124)
+#129 := (forall (vars (?x3 int)) #124)
+#683 := (iff #129 #680)
+#681 := (iff #124 #124)
+#682 := [refl]: #681
+#684 := [quant-intro #682]: #683
+#180 := (~ #129 #129)
+#194 := (~ #124 #124)
+#195 := [refl]: #194
+#181 := [nnf-pos #195]: #180
+#17 := (< #10 0::int)
+#19 := (implies #17 #18)
+#20 := (forall (vars (?x3 int)) #19)
+#132 := (iff #20 #129)
+#95 := (= 0::int #13)
+#101 := (not #17)
+#102 := (or #101 #95)
+#107 := (forall (vars (?x3 int)) #102)
+#130 := (iff #107 #129)
+#127 := (iff #102 #124)
+#121 := (or #76 #18)
+#125 := (iff #121 #124)
+#126 := [rewrite]: #125
+#122 := (iff #102 #121)
+#119 := (iff #95 #18)
+#120 := [rewrite]: #119
+#117 := (iff #101 #76)
+#112 := (not #77)
+#115 := (iff #112 #76)
+#116 := [rewrite]: #115
+#113 := (iff #101 #112)
+#110 := (iff #17 #77)
+#111 := [rewrite]: #110
+#114 := [monotonicity #111]: #113
+#118 := [trans #114 #116]: #117
+#123 := [monotonicity #118 #120]: #122
+#128 := [trans #123 #126]: #127
+#131 := [quant-intro #128]: #130
+#108 := (iff #20 #107)
+#105 := (iff #19 #102)
+#98 := (implies #17 #95)
+#103 := (iff #98 #102)
+#104 := [rewrite]: #103
+#99 := (iff #19 #98)
+#96 := (iff #18 #95)
+#97 := [rewrite]: #96
+#100 := [monotonicity #97]: #99
+#106 := [trans #100 #104]: #105
+#109 := [quant-intro #106]: #108
+#133 := [trans #109 #131]: #132
+#94 := [asserted]: #20
+#134 := [mp #94 #133]: #129
+#196 := [mp~ #134 #181]: #129
+#685 := [mp #196 #684]: #680
+#604 := (not #680)
+#562 := (or #604 #556 #558)
+#559 := (or #558 #556)
+#540 := (or #604 #559)
+#542 := (iff #540 #562)
+#543 := (or #604 #560)
+#546 := (iff #543 #562)
+#547 := [rewrite]: #546
+#544 := (iff #540 #543)
+#561 := (iff #559 #560)
+#551 := [rewrite]: #561
+#545 := [monotonicity #551]: #544
+#548 := [trans #545 #547]: #542
+#541 := [quant-inst]: #540
+#534 := [mp #541 #548]: #562
+#465 := [unit-resolution #534 #685]: #560
+#481 := [unit-resolution #465 #480]: #558
+#443 := (= #23 #557)
+#337 := (= uf_3 #251)
+#4 := (:var 0 T1)
+#5 := (uf_2 #4)
+#665 := (pattern #5)
+#6 := (uf_1 #5)
+#51 := (= #4 #6)
+#666 := (forall (vars (?x1 T1)) (:pat #665) #51)
+#54 := (forall (vars (?x1 T1)) #51)
+#667 := (iff #54 #666)
+#669 := (iff #666 #666)
+#670 := [rewrite]: #669
+#668 := [rewrite]: #667
+#671 := [trans #668 #670]: #667
+#188 := (~ #54 #54)
+#186 := (~ #51 #51)
+#187 := [refl]: #186
+#189 := [nnf-pos #187]: #188
+#7 := (= #6 #4)
+#8 := (forall (vars (?x1 T1)) #7)
+#55 := (iff #8 #54)
+#52 := (iff #7 #51)
+#53 := [rewrite]: #52
+#56 := [quant-intro #53]: #55
+#50 := [asserted]: #8
+#59 := [mp #50 #56]: #54
+#190 := [mp~ #59 #189]: #54
+#672 := [mp #190 #671]: #666
+#252 := (not #666)
+#342 := (or #252 #337)
+#339 := [quant-inst]: #342
+#442 := [unit-resolution #339 #672]: #337
+#450 := [monotonicity #442]: #443
+#452 := [trans #450 #481]: #469
+#453 := (not #469)
+#454 := (or #453 #556)
+#456 := [th-lemma]: #454
+[unit-resolution #456 #480 #452]: false
+unsat