anchor.diff:  
   
   
  -(defthm foo
  -  (implies (equal (nth n A
   
   (defthm composition-prog-value-correct
    (implies (and (equal (len p) 3)
  
positive.code:            (equal (pdl-prog-value m p) (cdr (assoc p (get-atomic-programs
                                                        (get-frame m)))))))
  
  (defthm composition-right-length
    (equal (len (rel-compose r1 r2))
           (len r1)))
  
negative.code: (defun get-prop-atoms (m) (nth 2 m))
  (defun get-prog-atoms (m) (nth 3 m))
  
  (defun symbol-list-listp (li)
    (if (endp li)
        t
  