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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_nlarith_03.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,62 @@
+#2 := false
+decl uf_2 :: real
+#6 := uf_2
+decl uf_1 :: real
+#4 := uf_1
+#12 := 2::real
+#13 := (* 2::real uf_1)
+#14 := (* #13 uf_2)
+#5 := 1::real
+#9 := (- 1::real uf_2)
+#10 := (* uf_1 #9)
+#7 := (+ 1::real uf_2)
+#8 := (* uf_1 #7)
+#11 := (- #8 #10)
+#15 := (= #11 #14)
+#16 := (not #15)
+#73 := (iff #16 false)
+#1 := true
+#68 := (not true)
+#71 := (iff #68 false)
+#72 := [rewrite]: #71
+#69 := (iff #16 #68)
+#66 := (iff #15 true)
+#33 := (* uf_1 uf_2)
+#55 := (* 2::real #33)
+#61 := (= #55 #55)
+#64 := (iff #61 true)
+#65 := [rewrite]: #64
+#62 := (iff #15 #61)
+#59 := (= #14 #55)
+#60 := [rewrite]: #59
+#57 := (= #11 #55)
+#37 := -1::real
+#45 := (* -1::real #33)
+#46 := (+ uf_1 #45)
+#34 := (+ uf_1 #33)
+#51 := (- #34 #46)
+#54 := (= #51 #55)
+#56 := [rewrite]: #54
+#52 := (= #11 #51)
+#49 := (= #10 #46)
+#38 := (* -1::real uf_2)
+#39 := (+ 1::real #38)
+#42 := (* uf_1 #39)
+#47 := (= #42 #46)
+#48 := [rewrite]: #47
+#43 := (= #10 #42)
+#40 := (= #9 #39)
+#41 := [rewrite]: #40
+#44 := [monotonicity #41]: #43
+#50 := [trans #44 #48]: #49
+#35 := (= #8 #34)
+#36 := [rewrite]: #35
+#53 := [monotonicity #36 #50]: #52
+#58 := [trans #53 #56]: #57
+#63 := [monotonicity #58 #60]: #62
+#67 := [trans #63 #65]: #66
+#70 := [monotonicity #67]: #69
+#74 := [trans #70 #72]: #73
+#32 := [asserted]: #16
+[mp #32 #74]: false
+unsat