anchor.diff:                  (or (member v (prog-accessible-worlds m w (second p)))
                       (member v (prog-accessible-worlds m w (third p)))))))
   
  +(defthm membership-preserved-under-append
  +  (implies (member x A)
  +           (member x (append B A))))
  +
  +(defthm single-rel-composition-semicorrect
  +  (implies (and (natp x)
  +                (< x (len R2)))
  +           (implies (and (member x A)
  +                         (member y (nth x R2)))
  +                    (member y (composition-of-single-rel A R2)))))
  +
  +(defthm rel-compose-semicorrect
  +  (implies (and (natp n)
  +                (< n (len A))
  +                (< x (len B))
  +                (integer-list-listp A)
  +                (integer-list-listp B))
  +           (implies (and (member x (nth n A))
  +                         (member y (nth x B)))
  +                    (member y (nth n (rel-compose A B))))))
  +
  +(defthm compose-prog-value-semicorrect
  +  (implies (and (equal (len p) 3)
  +                (equal (first p) 'compose)
  +                (natp w)
  +                (< w (len (pdl-prog-value m (second p)))))
  +           (implies (and (member x (prog-accessible-worlds m w (second p)))
  +                         (member y (prog-accessible-worlds m x (third p))))
  +                    (member y (prog-accessible-worlds m w p)))))
   
   
   
  
positive.code:                              (pdl-satisfies m v (third f))))))
  
  
  (defthm membership-preserved-under-append
    (implies (member x A)
             (member x (append B A))))
  
  (defthm single-rel-composition-semicorrect
    (implies (and (natp x)
                  (< x (len R2)))
             (implies (and (member x A)
                           (member y (nth x R2)))
                      (member y (composition-of-single-rel A R2)))))
  
  (defthm rel-compose-semicorrect
    (implies (and (natp n)
                  (< n (len A))
                  (< x (len B))
                  (integer-list-listp A)
                  (integer-list-listp B))
             (implies (and (member x (nth n A))
                           (member y (nth x B)))
                      (member y (nth n (rel-compose A B))))))
  
  
  
  ;here
  
  
  
  
negative.code:   (nth w (pdl-prog-value m p)))
  
  
    
  ; FORMULAS
  
  