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: 
  
  
  (defun negation-semantics-correct-induction (m w f ws flg)
    (declare (ignorable m w)
             (xargs :well-founded-relation l<
                    :measure (list (acl2-count f) (acl2-count ws))))
    (if flg
        (if (atom f)
            f
          (if (equal (len f) 2)
              (not (negation-semantics-correct-induction m w (second f) ws flg))
            (if (equal (first f) 'diamond)
                (negation-semantics-correct-induction m w (third f) ws flg)
              (or (negation-semantics-correct-induction m w (second f) ws flg)
                  (negation-semantics-correct-induction m w (third f) ws flg)))))
      (if (consp ws)
          (if (negation-semantics-correct-induction m (car ws) f nil t)
              t
            (negation-semantics-correct-induction m w f (car ws) nil))
        nil)))
  
  
  
  
  (defun neg-sem-correct-ind (m w f ws flg)
    (declare (ignorable m w ws flg))
    (if (equal (len f) 2)
        (not (neg-sem-correct-ind m w (second f) ws flg))
      nil))
  
  
  (defthm negation-semantics-correct
    (implies (pdl-satisfies-aux M W '(~ F) nil t)
             (not (pdl-satisfies-aux M W F nil t)))
    :hints (("Goal" :induct (neg-sem-correct-ind m w f nil t))))
  
  
  
  
negative.code:             t
            (pdl-satisfies-aux m w f (cdr worlds) nil))
        nil)))
  
  
  
  