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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_17.proof	Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,52 @@
+#2 := false
+#8 := 1::real
+decl uf_1 :: real
+#4 := uf_1
+#6 := 2::real
+#7 := (* 2::real uf_1)
+#9 := (+ #7 1::real)
+#5 := (+ uf_1 uf_1)
+#10 := (< #5 #9)
+#11 := (or false #10)
+#12 := (or #10 #11)
+#13 := (not #12)
+#64 := (iff #13 false)
+#32 := (+ 1::real #7)
+#35 := (< #7 #32)
+#52 := (not #35)
+#62 := (iff #52 false)
+#1 := true
+#57 := (not true)
+#60 := (iff #57 false)
+#61 := [rewrite]: #60
+#58 := (iff #52 #57)
+#55 := (iff #35 true)
+#56 := [rewrite]: #55
+#59 := [monotonicity #56]: #58
+#63 := [trans #59 #61]: #62
+#53 := (iff #13 #52)
+#50 := (iff #12 #35)
+#45 := (or #35 #35)
+#48 := (iff #45 #35)
+#49 := [rewrite]: #48
+#46 := (iff #12 #45)
+#43 := (iff #11 #35)
+#38 := (or false #35)
+#41 := (iff #38 #35)
+#42 := [rewrite]: #41
+#39 := (iff #11 #38)
+#36 := (iff #10 #35)
+#33 := (= #9 #32)
+#34 := [rewrite]: #33
+#30 := (= #5 #7)
+#31 := [rewrite]: #30
+#37 := [monotonicity #31 #34]: #36
+#40 := [monotonicity #37]: #39
+#44 := [trans #40 #42]: #43
+#47 := [monotonicity #37 #44]: #46
+#51 := [trans #47 #49]: #50
+#54 := [monotonicity #51]: #53
+#65 := [trans #54 #63]: #64
+#29 := [asserted]: #13
+[mp #29 #65]: false
+unsat