anchor.diff:             (equal (pdl-prog-value m p) (cdr (assoc p (get-atomic-programs
                                                         (get-frame m)))))))
   
  +; complex programs are right length:
  +
   (defthm composition-right-length
     (equal (len (rel-compose r1 r2))
            (len r1)))
  
positive.code: 
  
  
  (defthm foo
    (implies (equal (nth n A
  
  (defthm composition-prog-value-correct
   (implies (and (equal (len p) 3)
  
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
  