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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_mono_01.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,50 @@
+#2 := false
+decl up_35 :: (-> int bool)
+#112 := 1::int
+#113 := (up_35 1::int)
+#114 := (not #113)
+#297 := [asserted]: #114
+#103 := (:var 0 int)
+#104 := (up_35 #103)
+#911 := (pattern #104)
+#912 := (forall (vars (?x12 int)) (:pat #911) #104)
+#294 := (forall (vars (?x12 int)) #104)
+#915 := (iff #294 #912)
+#913 := (iff #104 #104)
+#914 := [refl]: #913
+#916 := [quant-intro #914]: #915
+#320 := (~ #294 #294)
+#361 := (~ #104 #104)
+#362 := [refl]: #361
+#321 := [nnf-pos #362]: #320
+decl up_32 :: (-> T13 bool)
+decl uf_36 :: (-> int T13 T13)
+decl uf_37 :: T13
+#105 := uf_37
+#106 := (uf_36 #103 uf_37)
+#107 := (up_32 #106)
+#108 := (not #107)
+#109 := (or #107 #108)
+#110 := (and #104 #109)
+#111 := (forall (vars (?x12 int)) #110)
+#295 := (iff #111 #294)
+#292 := (iff #110 #104)
+#1 := true
+#287 := (and #104 true)
+#290 := (iff #287 #104)
+#291 := [rewrite]: #290
+#288 := (iff #110 #287)
+#284 := (iff #109 true)
+#286 := [rewrite]: #284
+#289 := [monotonicity #286]: #288
+#293 := [trans #289 #291]: #292
+#296 := [quant-intro #293]: #295
+#283 := [asserted]: #111
+#299 := [mp #283 #296]: #294
+#363 := [mp~ #299 #321]: #294
+#917 := [mp #363 #916]: #912
+#418 := (not #912)
+#504 := (or #418 #113)
+#419 := [quant-inst]: #504
+[unit-resolution #419 #917 #297]: false
+unsat