--- a/src/HOL/SMT/Examples/cert/z3_nat_arith_01.proof Tue Feb 02 18:11:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,246 +0,0 @@
-#2 := false
-#9 := 0::int
-decl uf_2 :: (-> T1 int)
-decl uf_1 :: (-> int T1)
-decl uf_3 :: T1
-#22 := uf_3
-#23 := (uf_2 uf_3)
-#21 := 2::int
-#24 := (* 2::int #23)
-#25 := (uf_1 #24)
-#293 := (uf_2 #25)
-#292 := -1::int
-#296 := (* -1::int #293)
-#275 := (+ #24 #296)
-#258 := (<= #275 0::int)
-#611 := (= #275 0::int)
-#204 := (>= #24 0::int)
-#596 := (= #293 0::int)
-#541 := (not #596)
-#300 := (<= #293 0::int)
-#460 := (not #300)
-#26 := 1::int
-#570 := (>= #293 1::int)
-#569 := (= #293 1::int)
-#27 := (uf_1 1::int)
-#318 := (uf_2 #27)
-#311 := (= #318 1::int)
-#10 := (:var 0 int)
-#12 := (uf_1 #10)
-#627 := (pattern #12)
-#70 := (>= #10 0::int)
-#71 := (not #70)
-#13 := (uf_2 #12)
-#52 := (= #10 #13)
-#77 := (or #52 #71)
-#628 := (forall (vars (?x2 int)) (:pat #627) #77)
-#82 := (forall (vars (?x2 int)) #77)
-#631 := (iff #82 #628)
-#629 := (iff #77 #77)
-#630 := [refl]: #629
-#632 := [quant-intro #630]: #631
-#132 := (~ #82 #82)
-#144 := (~ #77 #77)
-#145 := [refl]: #144
-#130 := [nnf-pos #145]: #132
-#14 := (= #13 #10)
-#11 := (<= 0::int #10)
-#15 := (implies #11 #14)
-#16 := (forall (vars (?x2 int)) #15)
-#85 := (iff #16 #82)
-#59 := (not #11)
-#60 := (or #59 #52)
-#65 := (forall (vars (?x2 int)) #60)
-#83 := (iff #65 #82)
-#80 := (iff #60 #77)
-#74 := (or #71 #52)
-#78 := (iff #74 #77)
-#79 := [rewrite]: #78
-#75 := (iff #60 #74)
-#72 := (iff #59 #71)
-#68 := (iff #11 #70)
-#69 := [rewrite]: #68
-#73 := [monotonicity #69]: #72
-#76 := [monotonicity #73]: #75
-#81 := [trans #76 #79]: #80
-#84 := [quant-intro #81]: #83
-#66 := (iff #16 #65)
-#63 := (iff #15 #60)
-#56 := (implies #11 #52)
-#61 := (iff #56 #60)
-#62 := [rewrite]: #61
-#57 := (iff #15 #56)
-#54 := (iff #14 #52)
-#55 := [rewrite]: #54
-#58 := [monotonicity #55]: #57
-#64 := [trans #58 #62]: #63
-#67 := [quant-intro #64]: #66
-#86 := [trans #67 #84]: #85
-#51 := [asserted]: #16
-#87 := [mp #51 #86]: #82
-#146 := [mp~ #87 #130]: #82
-#633 := [mp #146 #632]: #628
-#612 := (not #628)
-#575 := (or #612 #311)
-#316 := (>= 1::int 0::int)
-#317 := (not #316)
-#211 := (= 1::int #318)
-#588 := (or #211 #317)
-#576 := (or #612 #588)
-#572 := (iff #576 #575)
-#578 := (iff #575 #575)
-#573 := [rewrite]: #578
-#585 := (iff #588 #311)
-#583 := (or #311 false)
-#584 := (iff #583 #311)
-#581 := [rewrite]: #584
-#297 := (iff #588 #583)
-#304 := (iff #317 false)
-#1 := true
-#587 := (not true)
-#302 := (iff #587 false)
-#303 := [rewrite]: #302
-#591 := (iff #317 #587)
-#586 := (iff #316 true)
-#590 := [rewrite]: #586
-#301 := [monotonicity #590]: #591
-#582 := [trans #301 #303]: #304
-#589 := (iff #211 #311)
-#312 := [rewrite]: #589
-#580 := [monotonicity #312 #582]: #297
-#574 := [trans #580 #581]: #585
-#577 := [monotonicity #574]: #572
-#579 := [trans #577 #573]: #572
-#571 := [quant-inst]: #576
-#420 := [mp #571 #579]: #575
-#437 := [unit-resolution #420 #633]: #311
-#452 := (= #293 #318)
-#28 := (= #25 #27)
-#129 := [asserted]: #28
-#454 := [monotonicity #129]: #452
-#455 := [trans #454 #437]: #569
-#448 := (not #569)
-#456 := (or #448 #570)
-#457 := [th-lemma]: #456
-#458 := [unit-resolution #457 #455]: #570
-#459 := (not #570)
-#553 := (or #459 #460)
-#550 := [th-lemma]: #553
-#554 := [unit-resolution #550 #458]: #460
-#543 := (or #541 #300)
-#535 := [th-lemma]: #543
-#532 := [unit-resolution #535 #554]: #541
-#598 := (or #204 #596)
-#18 := (= #13 0::int)
-#118 := (or #18 #70)
-#634 := (forall (vars (?x3 int)) (:pat #627) #118)
-#123 := (forall (vars (?x3 int)) #118)
-#637 := (iff #123 #634)
-#635 := (iff #118 #118)
-#636 := [refl]: #635
-#638 := [quant-intro #636]: #637
-#133 := (~ #123 #123)
-#147 := (~ #118 #118)
-#148 := [refl]: #147
-#134 := [nnf-pos #148]: #133
-#17 := (< #10 0::int)
-#19 := (implies #17 #18)
-#20 := (forall (vars (?x3 int)) #19)
-#126 := (iff #20 #123)
-#89 := (= 0::int #13)
-#95 := (not #17)
-#96 := (or #95 #89)
-#101 := (forall (vars (?x3 int)) #96)
-#124 := (iff #101 #123)
-#121 := (iff #96 #118)
-#115 := (or #70 #18)
-#119 := (iff #115 #118)
-#120 := [rewrite]: #119
-#116 := (iff #96 #115)
-#113 := (iff #89 #18)
-#114 := [rewrite]: #113
-#111 := (iff #95 #70)
-#106 := (not #71)
-#109 := (iff #106 #70)
-#110 := [rewrite]: #109
-#107 := (iff #95 #106)
-#104 := (iff #17 #71)
-#105 := [rewrite]: #104
-#108 := [monotonicity #105]: #107
-#112 := [trans #108 #110]: #111
-#117 := [monotonicity #112 #114]: #116
-#122 := [trans #117 #120]: #121
-#125 := [quant-intro #122]: #124
-#102 := (iff #20 #101)
-#99 := (iff #19 #96)
-#92 := (implies #17 #89)
-#97 := (iff #92 #96)
-#98 := [rewrite]: #97
-#93 := (iff #19 #92)
-#90 := (iff #18 #89)
-#91 := [rewrite]: #90
-#94 := [monotonicity #91]: #93
-#100 := [trans #94 #98]: #99
-#103 := [quant-intro #100]: #102
-#127 := [trans #103 #125]: #126
-#88 := [asserted]: #20
-#128 := [mp #88 #127]: #123
-#149 := [mp~ #128 #134]: #123
-#639 := [mp #149 #638]: #634
-#595 := (not #634)
-#601 := (or #595 #204 #596)
-#597 := (or #596 #204)
-#238 := (or #595 #597)
-#606 := (iff #238 #601)
-#604 := (or #595 #598)
-#605 := (iff #604 #601)
-#603 := [rewrite]: #605
-#243 := (iff #238 #604)
-#599 := (iff #597 #598)
-#600 := [rewrite]: #599
-#244 := [monotonicity #600]: #243
-#592 := [trans #244 #603]: #606
-#602 := [quant-inst]: #238
-#593 := [mp #602 #592]: #601
-#534 := [unit-resolution #593 #639]: #598
-#544 := [unit-resolution #534 #532]: #204
-#290 := (not #204)
-#281 := (or #290 #611)
-#618 := (or #612 #290 #611)
-#294 := (= #24 #293)
-#295 := (or #294 #290)
-#608 := (or #612 #295)
-#594 := (iff #608 #618)
-#272 := (or #612 #281)
-#610 := (iff #272 #618)
-#252 := [rewrite]: #610
-#609 := (iff #608 #272)
-#616 := (iff #295 #281)
-#400 := (or #611 #290)
-#614 := (iff #400 #281)
-#615 := [rewrite]: #614
-#607 := (iff #295 #400)
-#613 := (iff #294 #611)
-#269 := [rewrite]: #613
-#280 := [monotonicity #269]: #607
-#617 := [trans #280 #615]: #616
-#268 := [monotonicity #617]: #609
-#256 := [trans #268 #252]: #594
-#267 := [quant-inst]: #608
-#257 := [mp #267 #256]: #618
-#545 := [unit-resolution #257 #633]: #281
-#546 := [unit-resolution #545 #544]: #611
-#542 := (not #611)
-#547 := (or #542 #258)
-#536 := [th-lemma]: #547
-#537 := [unit-resolution #536 #546]: #258
-#259 := (>= #275 0::int)
-#538 := (or #542 #259)
-#539 := [th-lemma]: #538
-#533 := [unit-resolution #539 #546]: #259
-#563 := (<= #293 1::int)
-#540 := (or #448 #563)
-#524 := [th-lemma]: #540
-#525 := [unit-resolution #524 #455]: #563
-[th-lemma #458 #525 #533 #537]: false
-unsat