anchor.diff:  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   
   
  -
  -(defthm neg-sem-correct
  +(defthm negation-semantics-correct
     (implies (and (modelp m)
  -                (pdl-formulap m (get-prop-atoms m) (get-prog-atoms m)))
  -           (implies (equal (len f) 2)
  -                    (not (pdl-satisfies-aux m w f nil t)))))
  +                (pdl-formulap m (get-prop-atoms m) (get-prog-atoms m))
  +                (equal (first f) '~))
  +           (not (pdl-satisfies m w f))))
   
   
   
  
positive.code: 
  
  
  
  
  
  
  
  (defthm negation-semantics-correct
    (implies (and (modelp M)
                  (pdl-formulap F (get-prop-atoms M) (get-prog-atoms M)))
             (implies (pdl-satisfies M W '(~ F))
                      (not (pdl-satisfies M W F)))))
  
  
  ;(defthm negation-semantics-correct
  ;  (implies (and (modelp M)
  ;                (world-valid-in-model M W)
  ;                (pdl-formulap F (get-prop-atoms M) (get-prog-atoms M)))
  ;           (implies (pdl-satisfies M W '(~ F))
  ;                    (not (pdl-satisfies M W F)))))
negative.code:             t
            (pdl-satisfies-aux m w f (cdr worlds) nil))
        nil)))
  
  
  
  