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

Named_Thms is not scalable;

#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