| author | paulson |
| Fri, 13 Nov 2009 11:33:33 +0000 | |
| changeset 33654 | abf780db30ea |
| parent 33010 | 39f73a59e855 |
| permissions | -rw-r--r-- |
#2 := false decl up_1 :: (-> T1 bool) #4 := (:var 0 T1) #5 := (up_1 #4) #6 := (forall (vars (?x1 T1)) #5) #7 := (not #6) #8 := (or #6 #7) #9 := (not #8) #33 := (iff #9 false) #1 := true #28 := (not true) #31 := (iff #28 false) #32 := [rewrite]: #31 #29 := (iff #9 #28) #26 := (iff #8 true) #27 := [rewrite]: #26 #30 := [monotonicity #27]: #29 #34 := [trans #30 #32]: #33 #25 := [asserted]: #9 [mp #25 #34]: false unsat