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

adopting Sequences

#2 := false
#7 := 1::int
decl ?x1!1 :: int
#74 := ?x1!1
#51 := -2::int
#96 := (* -2::int ?x1!1)
decl ?x2!0 :: int
#73 := ?x2!0
#4 := 2::int
#95 := (* 2::int ?x2!0)
#97 := (+ #95 #96)
#166 := (<= #97 1::int)
#94 := (= #97 1::int)
#53 := -1::int
#75 := (* -2::int ?x2!0)
#76 := (* 2::int ?x1!1)
#77 := (+ #76 #75)
#78 := (= #77 -1::int)
#79 := (not #78)
#80 := (not #79)
#110 := (iff #80 #94)
#102 := (not #94)
#105 := (not #102)
#108 := (iff #105 #94)
#109 := [rewrite]: #108
#106 := (iff #80 #105)
#103 := (iff #79 #102)
#100 := (iff #78 #94)
#88 := (+ #75 #76)
#91 := (= #88 -1::int)
#98 := (iff #91 #94)
#99 := [rewrite]: #98
#92 := (iff #78 #91)
#89 := (= #77 #88)
#90 := [rewrite]: #89
#93 := [monotonicity #90]: #92
#101 := [trans #93 #99]: #100
#104 := [monotonicity #101]: #103
#107 := [monotonicity #104]: #106
#111 := [trans #107 #109]: #110
#9 := (:var 0 int)
#55 := (* -2::int #9)
#5 := (:var 1 int)
#6 := (* 2::int #5)
#56 := (+ #6 #55)
#54 := (= #56 -1::int)
#58 := (not #54)
#61 := (forall (vars (?x1 int) (?x2 int)) #58)
#64 := (not #61)
#81 := (~ #64 #80)
#82 := [sk]: #81
#10 := (* 2::int #9)
#8 := (+ #6 1::int)
#11 := (= #8 #10)
#12 := (not #11)
#13 := (forall (vars (?x1 int) (?x2 int)) #12)
#14 := (not #13)
#67 := (iff #14 #64)
#31 := (+ 1::int #6)
#37 := (= #10 #31)
#42 := (not #37)
#45 := (forall (vars (?x1 int) (?x2 int)) #42)
#48 := (not #45)
#65 := (iff #48 #64)
#62 := (iff #45 #61)
#59 := (iff #42 #58)
#52 := (iff #37 #54)
#57 := [rewrite]: #52
#60 := [monotonicity #57]: #59
#63 := [quant-intro #60]: #62
#66 := [monotonicity #63]: #65
#49 := (iff #14 #48)
#46 := (iff #13 #45)
#43 := (iff #12 #42)
#40 := (iff #11 #37)
#34 := (= #31 #10)
#38 := (iff #34 #37)
#39 := [rewrite]: #38
#35 := (iff #11 #34)
#32 := (= #8 #31)
#33 := [rewrite]: #32
#36 := [monotonicity #33]: #35
#41 := [trans #36 #39]: #40
#44 := [monotonicity #41]: #43
#47 := [quant-intro #44]: #46
#50 := [monotonicity #47]: #49
#68 := [trans #50 #66]: #67
#30 := [asserted]: #14
#69 := [mp #30 #68]: #64
#85 := [mp~ #69 #82]: #80
#86 := [mp #85 #111]: #94
#168 := (or #102 #166)
#169 := [th-lemma]: #168
#170 := [unit-resolution #169 #86]: #166
#167 := (>= #97 1::int)
#171 := (or #102 #167)
#172 := [th-lemma]: #171
#173 := [unit-resolution #172 #86]: #167
[th-lemma #173 #170]: false
unsat