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

fixed soundness bug in Nitpick related to sets of sets;
(detected thanks to the TPTP)

#2 := false
decl uf_2 :: (-> T1 int)
decl uf_1 :: (-> int T1)
decl uf_3 :: T1
#21 := uf_3
#22 := (uf_2 uf_3)
#23 := 1::int
#138 := (+ 1::int #22)
#141 := (uf_1 #138)
#656 := (uf_2 #141)
#26 := 2::int
#144 := (* 2::int #22)
#147 := (uf_1 #144)
#150 := (uf_2 #147)
#30 := 3::int
#156 := (+ 3::int #150)
#161 := (uf_1 #156)
#494 := (uf_2 #161)
#288 := (= #494 #656)
#266 := (= #161 #141)
#249 := (= #141 #161)
#9 := 0::int
#166 := (uf_1 0::int)
#251 := (= #161 #166)
#337 := (not #251)
#567 := (= #494 0::int)
#543 := (uf_2 #166)
#547 := (= #543 0::int)
#10 := (:var 0 int)
#12 := (uf_1 #10)
#673 := (pattern #12)
#78 := (>= #10 0::int)
#79 := (not #78)
#13 := (uf_2 #12)
#60 := (= #10 #13)
#85 := (or #60 #79)
#674 := (forall (vars (?x2 int)) (:pat #673) #85)
#90 := (forall (vars (?x2 int)) #85)
#677 := (iff #90 #674)
#675 := (iff #85 #85)
#676 := [refl]: #675
#678 := [quant-intro #676]: #677
#178 := (~ #90 #90)
#190 := (~ #85 #85)
#191 := [refl]: #190
#175 := [nnf-pos #191]: #178
#14 := (= #13 #10)
#11 := (<= 0::int #10)
#15 := (implies #11 #14)
#16 := (forall (vars (?x2 int)) #15)
#93 := (iff #16 #90)
#67 := (not #11)
#68 := (or #67 #60)
#73 := (forall (vars (?x2 int)) #68)
#91 := (iff #73 #90)
#88 := (iff #68 #85)
#82 := (or #79 #60)
#86 := (iff #82 #85)
#87 := [rewrite]: #86
#83 := (iff #68 #82)
#80 := (iff #67 #79)
#76 := (iff #11 #78)
#77 := [rewrite]: #76
#81 := [monotonicity #77]: #80
#84 := [monotonicity #81]: #83
#89 := [trans #84 #87]: #88
#92 := [quant-intro #89]: #91
#74 := (iff #16 #73)
#71 := (iff #15 #68)
#64 := (implies #11 #60)
#69 := (iff #64 #68)
#70 := [rewrite]: #69
#65 := (iff #15 #64)
#62 := (iff #14 #60)
#63 := [rewrite]: #62
#66 := [monotonicity #63]: #65
#72 := [trans #66 #70]: #71
#75 := [quant-intro #72]: #74
#94 := [trans #75 #92]: #93
#59 := [asserted]: #16
#95 := [mp #59 #94]: #90
#192 := [mp~ #95 #175]: #90
#679 := [mp #192 #678]: #674
#290 := (not #674)
#519 := (or #290 #547)
#540 := (>= 0::int 0::int)
#541 := (not #540)
#544 := (= 0::int #543)
#545 := (or #544 #541)
#520 := (or #290 #545)
#521 := (iff #520 #519)
#523 := (iff #519 #519)
#526 := [rewrite]: #523
#407 := (iff #545 #547)
#533 := (or #547 false)
#513 := (iff #533 #547)
#514 := [rewrite]: #513
#539 := (iff #545 #533)
#537 := (iff #541 false)
#1 := true
#530 := (not true)
#535 := (iff #530 false)
#536 := [rewrite]: #535
#531 := (iff #541 #530)
#548 := (iff #540 true)
#534 := [rewrite]: #548
#532 := [monotonicity #534]: #531
#538 := [trans #532 #536]: #537
#546 := (iff #544 #547)
#542 := [rewrite]: #546
#512 := [monotonicity #542 #538]: #539
#518 := [trans #512 #514]: #407
#522 := [monotonicity #518]: #521
#527 := [trans #522 #526]: #521
#525 := [quant-inst]: #520
#528 := [mp #525 #527]: #519
#316 := [unit-resolution #528 #679]: #547
#286 := (= #494 #543)
#287 := [hypothesis]: #251
#292 := [monotonicity #287]: #286
#267 := [trans #292 #316]: #567
#296 := (not #567)
#551 := (<= #494 0::int)
#300 := (not #551)
#501 := (>= #150 0::int)
#622 := (>= #144 0::int)
#302 := -1::int
#303 := (* -1::int #656)
#304 := (+ #22 #303)
#635 := (>= #304 -1::int)
#305 := (= #304 -1::int)
#644 := (>= #22 -1::int)
#511 := (>= #22 0::int)
#487 := (= #22 0::int)
#660 := (uf_1 #22)
#517 := (uf_2 #660)
#485 := (= #517 0::int)
#389 := (not #511)
#390 := [hypothesis]: #389
#492 := (or #485 #511)
#18 := (= #13 0::int)
#126 := (or #18 #78)
#680 := (forall (vars (?x3 int)) (:pat #673) #126)
#131 := (forall (vars (?x3 int)) #126)
#683 := (iff #131 #680)
#681 := (iff #126 #126)
#682 := [refl]: #681
#684 := [quant-intro #682]: #683
#179 := (~ #131 #131)
#193 := (~ #126 #126)
#194 := [refl]: #193
#180 := [nnf-pos #194]: #179
#17 := (< #10 0::int)
#19 := (implies #17 #18)
#20 := (forall (vars (?x3 int)) #19)
#134 := (iff #20 #131)
#97 := (= 0::int #13)
#103 := (not #17)
#104 := (or #103 #97)
#109 := (forall (vars (?x3 int)) #104)
#132 := (iff #109 #131)
#129 := (iff #104 #126)
#123 := (or #78 #18)
#127 := (iff #123 #126)
#128 := [rewrite]: #127
#124 := (iff #104 #123)
#121 := (iff #97 #18)
#122 := [rewrite]: #121
#119 := (iff #103 #78)
#114 := (not #79)
#117 := (iff #114 #78)
#118 := [rewrite]: #117
#115 := (iff #103 #114)
#112 := (iff #17 #79)
#113 := [rewrite]: #112
#116 := [monotonicity #113]: #115
#120 := [trans #116 #118]: #119
#125 := [monotonicity #120 #122]: #124
#130 := [trans #125 #128]: #129
#133 := [quant-intro #130]: #132
#110 := (iff #20 #109)
#107 := (iff #19 #104)
#100 := (implies #17 #97)
#105 := (iff #100 #104)
#106 := [rewrite]: #105
#101 := (iff #19 #100)
#98 := (iff #18 #97)
#99 := [rewrite]: #98
#102 := [monotonicity #99]: #101
#108 := [trans #102 #106]: #107
#111 := [quant-intro #108]: #110
#135 := [trans #111 #133]: #134
#96 := [asserted]: #20
#136 := [mp #96 #135]: #131
#195 := [mp~ #136 #180]: #131
#685 := [mp #195 #684]: #680
#637 := (not #680)
#484 := (or #637 #485 #511)
#486 := (or #637 #492)
#495 := (iff #486 #484)
#496 := [rewrite]: #495
#493 := [quant-inst]: #486
#497 := [mp #493 #496]: #484
#391 := [unit-resolution #497 #685]: #492
#392 := [unit-resolution #391 #390]: #485
#394 := (= #22 #517)
#661 := (= uf_3 #660)
#4 := (:var 0 T1)
#5 := (uf_2 #4)
#665 := (pattern #5)
#6 := (uf_1 #5)
#53 := (= #4 #6)
#666 := (forall (vars (?x1 T1)) (:pat #665) #53)
#56 := (forall (vars (?x1 T1)) #53)
#667 := (iff #56 #666)
#669 := (iff #666 #666)
#670 := [rewrite]: #669
#668 := [rewrite]: #667
#671 := [trans #668 #670]: #667
#187 := (~ #56 #56)
#185 := (~ #53 #53)
#186 := [refl]: #185
#188 := [nnf-pos #186]: #187
#7 := (= #6 #4)
#8 := (forall (vars (?x1 T1)) #7)
#57 := (iff #8 #56)
#54 := (iff #7 #53)
#55 := [rewrite]: #54
#58 := [quant-intro #55]: #57
#52 := [asserted]: #8
#61 := [mp #52 #58]: #56
#189 := [mp~ #61 #188]: #56
#672 := [mp #189 #671]: #666
#658 := (not #666)
#664 := (or #658 #661)
#654 := [quant-inst]: #664
#393 := [unit-resolution #654 #672]: #661
#395 := [monotonicity #393]: #394
#396 := [trans #395 #392]: #487
#397 := (not #487)
#398 := (or #397 #511)
#399 := [th-lemma]: #398
#388 := [unit-resolution #399 #390 #396]: false
#400 := [lemma #388]: #511
#366 := (or #389 #644)
#367 := [th-lemma]: #366
#352 := [unit-resolution #367 #400]: #644
#641 := (not #644)
#648 := (or #305 #641)
#651 := (or #290 #305 #641)
#313 := (>= #138 0::int)
#318 := (not #313)
#298 := (= #138 #656)
#640 := (or #298 #318)
#649 := (or #290 #640)
#363 := (iff #649 #651)
#638 := (or #290 #648)
#361 := (iff #638 #651)
#362 := [rewrite]: #361
#639 := (iff #649 #638)
#650 := (iff #640 #648)
#647 := (iff #318 #641)
#645 := (iff #313 #644)
#646 := [rewrite]: #645
#284 := [monotonicity #646]: #647
#642 := (iff #298 #305)
#643 := [rewrite]: #642
#289 := [monotonicity #643 #284]: #650
#346 := [monotonicity #289]: #639
#364 := [trans #346 #362]: #363
#652 := [quant-inst]: #649
#257 := [mp #652 #364]: #651
#424 := [unit-resolution #257 #679]: #648
#353 := [unit-resolution #424 #352]: #305
#439 := (not #305)
#281 := (or #439 #635)
#440 := [th-lemma]: #281
#330 := [unit-resolution #440 #353]: #635
#620 := (<= #656 0::int)
#441 := (not #620)
#634 := (<= #304 -1::int)
#344 := (or #439 #634)
#354 := [th-lemma]: #344
#355 := [unit-resolution #354 #353]: #634
#345 := (not #634)
#356 := (or #441 #389 #345)
#322 := [th-lemma]: #356
#324 := [unit-resolution #322 #355 #400]: #441
#432 := (not #635)
#331 := (or #622 #432 #620)
#319 := [th-lemma]: #331
#320 := [unit-resolution #319 #324 #330]: #622
#624 := (* -1::int #150)
#619 := (+ #144 #624)
#606 := (<= #619 0::int)
#625 := (= #619 0::int)
#617 := (not #622)
#612 := (or #617 #625)
#615 := (or #290 #617 #625)
#618 := (= #144 #150)
#623 := (or #618 #617)
#609 := (or #290 #623)
#604 := (iff #609 #615)
#445 := (or #290 #612)
#601 := (iff #445 #615)
#602 := [rewrite]: #601
#447 := (iff #609 #445)
#608 := (iff #623 #612)
#468 := (or #625 #617)
#613 := (iff #468 #612)
#607 := [rewrite]: #613
#610 := (iff #623 #468)
#466 := (iff #618 #625)
#467 := [rewrite]: #466
#611 := [monotonicity #467]: #610
#614 := [trans #611 #607]: #608
#448 := [monotonicity #614]: #447
#605 := [trans #448 #602]: #604
#616 := [quant-inst]: #609
#603 := [mp #616 #605]: #615
#480 := [unit-resolution #603 #679]: #612
#299 := [unit-resolution #480 #320]: #625
#406 := (not #625)
#408 := (or #406 #606)
#409 := [th-lemma]: #408
#301 := [unit-resolution #409 #299]: #606
#413 := (not #606)
#306 := (or #501 #413 #617)
#307 := [th-lemma]: #306
#308 := [unit-resolution #307 #301 #320]: #501
#506 := -3::int
#504 := (* -1::int #494)
#505 := (+ #150 #504)
#564 := (<= #505 -3::int)
#599 := (= #505 -3::int)
#587 := (>= #150 -3::int)
#417 := (or #587 #413 #617)
#410 := [th-lemma]: #417
#309 := [unit-resolution #410 #301 #320]: #587
#578 := (not #587)
#593 := (or #578 #599)
#579 := (or #290 #578 #599)
#449 := (>= #156 0::int)
#597 := (not #449)
#502 := (= #156 #494)
#503 := (or #502 #597)
#586 := (or #290 #503)
#572 := (iff #586 #579)
#571 := (or #290 #593)
#575 := (iff #571 #579)
#576 := [rewrite]: #575
#573 := (iff #586 #571)
#584 := (iff #503 #593)
#591 := (or #599 #578)
#582 := (iff #591 #593)
#583 := [rewrite]: #582
#592 := (iff #503 #591)
#580 := (iff #597 #578)
#589 := (iff #449 #587)
#581 := [rewrite]: #589
#590 := [monotonicity #581]: #580
#596 := (iff #502 #599)
#600 := [rewrite]: #596
#588 := [monotonicity #600 #590]: #592
#585 := [trans #588 #583]: #584
#574 := [monotonicity #585]: #573
#577 := [trans #574 #576]: #572
#570 := [quant-inst]: #586
#563 := [mp #570 #577]: #579
#458 := [unit-resolution #563 #679]: #593
#310 := [unit-resolution #458 #309]: #599
#460 := (not #599)
#461 := (or #460 #564)
#444 := [th-lemma]: #461
#311 := [unit-resolution #444 #310]: #564
#434 := (not #564)
#453 := (not #501)
#312 := (or #300 #453 #434)
#293 := [th-lemma]: #312
#295 := [unit-resolution #293 #311 #308]: #300
#294 := (or #296 #551)
#297 := [th-lemma]: #294
#285 := [unit-resolution #297 #295]: #296
#271 := [unit-resolution #285 #267]: false
#272 := [lemma #271]: #337
#282 := (or #249 #251)
#250 := (= #141 #166)
#336 := (not #250)
#357 := (= #656 0::int)
#332 := (= #656 #543)
#329 := [hypothesis]: #250
#333 := [monotonicity #329]: #332
#323 := [trans #333 #316]: #357
#429 := (not #357)
#430 := (or #429 #620)
#428 := [th-lemma]: #430
#325 := [unit-resolution #428 #324]: #429
#334 := [unit-resolution #325 #323]: false
#317 := [lemma #334]: #336
#279 := (or #249 #250 #251)
#335 := (not #249)
#328 := (and #335 #336 #337)
#339 := (not #328)
#169 := (distinct #141 #161 #166)
#172 := (not #169)
#33 := (- #22 #22)
#34 := (uf_1 #33)
#27 := (* #22 2::int)
#28 := (uf_1 #27)
#29 := (uf_2 #28)
#31 := (+ #29 3::int)
#32 := (uf_1 #31)
#24 := (+ #22 1::int)
#25 := (uf_1 #24)
#35 := (distinct #25 #32 #34)
#36 := (not #35)
#173 := (iff #36 #172)
#170 := (iff #35 #169)
#167 := (= #34 #166)
#164 := (= #33 0::int)
#165 := [rewrite]: #164
#168 := [monotonicity #165]: #167
#162 := (= #32 #161)
#159 := (= #31 #156)
#153 := (+ #150 3::int)
#157 := (= #153 #156)
#158 := [rewrite]: #157
#154 := (= #31 #153)
#151 := (= #29 #150)
#148 := (= #28 #147)
#145 := (= #27 #144)
#146 := [rewrite]: #145
#149 := [monotonicity #146]: #148
#152 := [monotonicity #149]: #151
#155 := [monotonicity #152]: #154
#160 := [trans #155 #158]: #159
#163 := [monotonicity #160]: #162
#142 := (= #25 #141)
#139 := (= #24 #138)
#140 := [rewrite]: #139
#143 := [monotonicity #140]: #142
#171 := [monotonicity #143 #163 #168]: #170
#174 := [monotonicity #171]: #173
#137 := [asserted]: #36
#177 := [mp #137 #174]: #172
#326 := (or #169 #339)
#327 := [def-axiom]: #326
#277 := [unit-resolution #327 #177]: #339
#659 := (or #328 #249 #250 #251)
#315 := [def-axiom]: #659
#280 := [unit-resolution #315 #277]: #279
#278 := [unit-resolution #280 #317]: #282
#283 := [unit-resolution #278 #272]: #249
#269 := [symm #283]: #266
#270 := [monotonicity #269]: #288
#508 := (+ #494 #303)
#473 := (<= #508 0::int)
#433 := (not #473)
#477 := [hypothesis]: #473
#421 := (or #622 #433)
#489 := (= #150 0::int)
#478 := [hypothesis]: #617
#490 := (or #489 #622)
#499 := (or #637 #489 #622)
#594 := (or #637 #490)
#598 := (iff #594 #499)
#483 := [rewrite]: #598
#595 := [quant-inst]: #594
#498 := [mp #595 #483]: #499
#465 := [unit-resolution #498 #685]: #490
#481 := [unit-resolution #465 #478]: #489
#442 := (not #489)
#443 := (or #442 #501)
#450 := [th-lemma]: #443
#452 := [unit-resolution #450 #481]: #501
#454 := (or #453 #587)
#456 := [th-lemma]: #454
#457 := [unit-resolution #456 #452]: #587
#459 := [unit-resolution #458 #457]: #599
#462 := [unit-resolution #444 #459]: #564
#435 := (or #432 #622 #433 #453 #434)
#437 := [th-lemma]: #435
#438 := [unit-resolution #437 #478 #452 #462 #477]: #432
#436 := [unit-resolution #440 #438]: #439
#420 := (or #441 #433 #453 #434)
#423 := [th-lemma]: #420
#427 := [unit-resolution #423 #452 #462 #477]: #441
#431 := [unit-resolution #428 #427]: #429
#632 := (or #357 #644)
#347 := (or #637 #357 #644)
#358 := (or #357 #313)
#348 := (or #637 #358)
#630 := (iff #348 #347)
#350 := (or #637 #632)
#343 := (iff #350 #347)
#626 := [rewrite]: #343
#628 := (iff #348 #350)
#636 := (iff #358 #632)
#633 := [monotonicity #646]: #636
#629 := [monotonicity #633]: #628
#627 := [trans #629 #626]: #630
#349 := [quant-inst]: #348
#631 := [mp #349 #627]: #347
#419 := [unit-resolution #631 #685]: #632
#422 := [unit-resolution #419 #431]: #644
#425 := [unit-resolution #424 #422 #436]: false
#426 := [lemma #425]: #421
#479 := [unit-resolution #426 #477]: #622
#416 := [unit-resolution #480 #479]: #625
#412 := [unit-resolution #409 #416]: #606
#418 := [unit-resolution #410 #412 #479]: #587
#411 := [unit-resolution #458 #418]: #599
#414 := [unit-resolution #444 #411]: #564
#415 := (or #644 #617)
#401 := [th-lemma]: #415
#403 := [unit-resolution #401 #479]: #644
#404 := [unit-resolution #424 #403]: #305
#402 := [unit-resolution #440 #404]: #635
#405 := [th-lemma #418 #402 #477 #414 #412]: false
#387 := [lemma #405]: #433
#273 := (not #288)
#274 := (or #273 #473)
#275 := [th-lemma]: #274
[unit-resolution #275 #387 #270]: false
unsat