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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_05.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,35 @@
+#2 := false
+#5 := 3::int
+#6 := 8::int
+#7 := (<= 3::int 8::int)
+#8 := (ite #7 8::int 3::int)
+#4 := 5::int
+#9 := (< 5::int #8)
+#10 := (not #9)
+#50 := (iff #10 false)
+#1 := true
+#45 := (not true)
+#48 := (iff #45 false)
+#49 := [rewrite]: #48
+#46 := (iff #10 #45)
+#43 := (iff #9 true)
+#38 := (< 5::int 8::int)
+#41 := (iff #38 true)
+#42 := [rewrite]: #41
+#39 := (iff #9 #38)
+#36 := (= #8 8::int)
+#31 := (ite true 8::int 3::int)
+#34 := (= #31 8::int)
+#35 := [rewrite]: #34
+#32 := (= #8 #31)
+#29 := (iff #7 true)
+#30 := [rewrite]: #29
+#33 := [monotonicity #30]: #32
+#37 := [trans #33 #35]: #36
+#40 := [monotonicity #37]: #39
+#44 := [trans #40 #42]: #43
+#47 := [monotonicity #44]: #46
+#51 := [trans #47 #49]: #50
+#26 := [asserted]: #10
+[mp #26 #51]: false
+unsat