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

+#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