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

A number of theorems contributed by Jeremy Avigad

#2 := false
#5 := (:var 0 int)
#7 := 0::int
#9 := (<= 0::int #5)
#8 := (< #5 0::int)
#10 := (or #8 #9)
#4 := (:var 1 int)
#6 := (< #4 #5)
#11 := (implies #6 #10)
#12 := (forall (vars (?x2 int)) #11)
#13 := (exists (vars (?x1 int)) #12)
#14 := (not #13)
#95 := (iff #14 false)
#31 := (not #6)
#32 := (or #31 #10)
#35 := (forall (vars (?x2 int)) #32)
#38 := (exists (vars (?x1 int)) #35)
#41 := (not #38)
#93 := (iff #41 false)
#1 := true
#88 := (not true)
#91 := (iff #88 false)
#92 := [rewrite]: #91
#89 := (iff #41 #88)
#86 := (iff #38 true)
#81 := (exists (vars (?x1 int)) true)
#84 := (iff #81 true)
#85 := [elim-unused]: #84
#82 := (iff #38 #81)
#79 := (iff #35 true)
#74 := (forall (vars (?x2 int)) true)
#77 := (iff #74 true)
#78 := [elim-unused]: #77
#75 := (iff #35 #74)
#72 := (iff #32 true)
#46 := (>= #5 0::int)
#44 := (not #46)
#64 := (or #44 #46)
#50 := -1::int
#53 := (* -1::int #5)
#54 := (+ #4 #53)
#52 := (>= #54 0::int)
#67 := (or #52 #64)
#70 := (iff #67 true)
#71 := [rewrite]: #70
#68 := (iff #32 #67)
#65 := (iff #10 #64)
#48 := (iff #9 #46)
#49 := [rewrite]: #48
#45 := (iff #8 #44)
#47 := [rewrite]: #45
#66 := [monotonicity #47 #49]: #65
#62 := (iff #31 #52)
#51 := (not #52)
#57 := (not #51)
#60 := (iff #57 #52)
#61 := [rewrite]: #60
#58 := (iff #31 #57)
#55 := (iff #6 #51)
#56 := [rewrite]: #55
#59 := [monotonicity #56]: #58
#63 := [trans #59 #61]: #62
#69 := [monotonicity #63 #66]: #68
#73 := [trans #69 #71]: #72
#76 := [quant-intro #73]: #75
#80 := [trans #76 #78]: #79
#83 := [quant-intro #80]: #82
#87 := [trans #83 #85]: #86
#90 := [monotonicity #87]: #89
#94 := [trans #90 #92]: #93
#42 := (iff #14 #41)
#39 := (iff #13 #38)
#36 := (iff #12 #35)
#33 := (iff #11 #32)
#34 := [rewrite]: #33
#37 := [quant-intro #34]: #36
#40 := [quant-intro #37]: #39
#43 := [monotonicity #40]: #42
#96 := [trans #43 #94]: #95
#30 := [asserted]: #14
[mp #30 #96]: false
unsat