| author | haftmann |
| Wed, 27 Jan 2010 14:02:52 +0100 | |
| changeset 34968 | ceeffca32eb0 |
| 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