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

tuned structure; moved non-related quickcheck.setup to Code_Generator.thy

#2 := false
#4 := 0::int
decl ?x2!1 :: int
#83 := ?x2!1
decl ?x3!0 :: int
#82 := ?x3!0
#108 := (+ ?x3!0 ?x2!1)
#111 := (<= #108 0::int)
#114 := (not #111)
#89 := (<= ?x2!1 0::int)
#90 := (not #89)
#87 := (<= ?x3!0 0::int)
#88 := (not #87)
#102 := (and #88 #90)
#105 := (not #102)
#117 := (or #105 #114)
#120 := (not #117)
#84 := (+ ?x2!1 ?x3!0)
#85 := (<= #84 0::int)
#86 := (not #85)
#91 := (and #90 #88)
#92 := (not #91)
#93 := (or #92 #86)
#94 := (not #93)
#121 := (iff #94 #120)
#118 := (iff #93 #117)
#115 := (iff #86 #114)
#112 := (iff #85 #111)
#109 := (= #84 #108)
#110 := [rewrite]: #109
#113 := [monotonicity #110]: #112
#116 := [monotonicity #113]: #115
#106 := (iff #92 #105)
#103 := (iff #91 #102)
#104 := [rewrite]: #103
#107 := [monotonicity #104]: #106
#119 := [monotonicity #107 #116]: #118
#122 := [monotonicity #119]: #121
#7 := (:var 0 int)
#5 := (:var 1 int)
#10 := (+ #5 #7)
#63 := (<= #10 0::int)
#64 := (not #63)
#53 := (<= #7 0::int)
#54 := (not #53)
#49 := (<= #5 0::int)
#50 := (not #49)
#57 := (and #50 #54)
#60 := (not #57)
#67 := (or #60 #64)
#70 := (forall (vars (?x2 int) (?x3 int)) #67)
#73 := (not #70)
#95 := (~ #73 #94)
#96 := [sk]: #95
#11 := (< 0::int #10)
#8 := (< 0::int #7)
#6 := (< 0::int #5)
#9 := (and #6 #8)
#12 := (implies #9 #11)
#13 := (forall (vars (?x2 int) (?x3 int)) #12)
#14 := (exists (vars (?x1 int)) #13)
#15 := (not #14)
#76 := (iff #15 #73)
#32 := (not #9)
#33 := (or #32 #11)
#36 := (forall (vars (?x2 int) (?x3 int)) #33)
#46 := (not #36)
#74 := (iff #46 #73)
#71 := (iff #36 #70)
#68 := (iff #33 #67)
#65 := (iff #11 #64)
#66 := [rewrite]: #65
#61 := (iff #32 #60)
#58 := (iff #9 #57)
#55 := (iff #8 #54)
#56 := [rewrite]: #55
#51 := (iff #6 #50)
#52 := [rewrite]: #51
#59 := [monotonicity #52 #56]: #58
#62 := [monotonicity #59]: #61
#69 := [monotonicity #62 #66]: #68
#72 := [quant-intro #69]: #71
#75 := [monotonicity #72]: #74
#47 := (iff #15 #46)
#44 := (iff #14 #36)
#39 := (exists (vars (?x1 int)) #36)
#42 := (iff #39 #36)
#43 := [elim-unused]: #42
#40 := (iff #14 #39)
#37 := (iff #13 #36)
#34 := (iff #12 #33)
#35 := [rewrite]: #34
#38 := [quant-intro #35]: #37
#41 := [quant-intro #38]: #40
#45 := [trans #41 #43]: #44
#48 := [monotonicity #45]: #47
#77 := [trans #48 #75]: #76
#31 := [asserted]: #15
#78 := [mp #31 #77]: #73
#99 := [mp~ #78 #96]: #94
#100 := [mp #99 #122]: #120
#125 := [not-or-elim #100]: #111
#101 := [not-or-elim #100]: #102
#124 := [and-elim #101]: #90
#123 := [and-elim #101]: #88
[th-lemma #123 #124 #125]: false
unsat