anchor.diff:  ; REFLEXIVITY TOY EXAMPLE
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   
  +
  +(defun bar (n)
  +  (if (zp n)
  +      (list 0)
  +    (append (bar (- n 1)) (list n))))
  +
  +(defthm barlemma1
  +  (implies (and (natp i))
  +           (equal (car (bar i)) i)))
  +
  +
  +(thm
  + (implies (and (natp i))
  +          (equal (nth i (bar n))
  +                 i))
  + :hints (("Goal"
  +          :induct (bar i))))
  +
  +
  +
  +
   (defun foo (i r)
     (declare (xargs :measure (nfix (- (len r) (nfix i)))))
     (if (< (nfix i) (len r))
  
positive.code:   (if (zp i)
        r
      (fooindsch (- i 1) r)))
  
  
  (defthm foobase
  
negative.code:            :use ((:instance box-semantics-semicorrect
                              (m m) (w w) (f f) (v v))))))
  
  (defthm composition-satisfiability-semicorrect-lemma1
   (let ((first (first f))
         (second (second f)))
     (implies (and (equal (len f) 3)
                   (equal first 'box)
                   (equal (len second) 3)
                   (equal (first second) 'compose)
                   (natp w)
                   (< w (len (pdl-prog-value m second))))
              (implies
               (pdl-satisfies m w f)
               (implies
                (and (member x (prog-accessible-worlds m w (second second)))
                     (member y (prog-accessible-worlds m x (third second))))
                (member y (prog-accessible-worlds m w second))))))
   :hints (("Goal"
            :in-theory (disable compose-prog-value-semicorrect)
            :use ((:instance compose-prog-value-semicorrect
                             (m m) (w w) (p (second f)) (x x) (y y))))))
  
  (defthm composition-satisfiability-semicorrect-lemma2
   (let ((first (first f))
         (second (second f))
         (third (third f)))
     (implies (and (equal (len f) 3)
                   (equal first 'box)
                   (equal (len second) 3)
                   (equal (first second) 'compose)
                   (natp w)
                   (< w (len (pdl-prog-value m second))))
              (implies
               (pdl-satisfies m w f)
               (implies (member y (prog-accessible-worlds m w second))
                        (pdl-satisfies m y third)))))
   :hints (("Goal"
            :in-theory (disable box-semantics-semicorrect)
            :use ((:instance box-semantics-semicorrect
                             (m m) (w w) (f f) (v y))))))
  
  (defthm composition-satisfiability-semicorrect
   (let ((first (first f))
         (second (second f))
         (third (third f)))
     (implies (and (equal (len f) 3)
                   (equal first 'box)
                   (equal (len second) 3)
                   (equal (first second) 'compose)
                   (natp w)
                   (< w (len (pdl-prog-value m second))))
              (implies
               (pdl-satisfies m w f)
               (implies
                (and (member x (prog-accessible-worlds m w (second second)))
                     (member y (prog-accessible-worlds m x (third second))))
                (pdl-satisfies m y third)))))
   :hints (("Goal"
            :in-theory (disable composition-satisfiability-semicorrect-lemma1
                                composition-satisfiability-semicorrect-lemma2)
            :use ((:instance composition-satisfiability-semicorrect-lemma1
                             (m m) (w w) (f f) (x x) (y y))
                  (:instance composition-satisfiability-semicorrect-lemma2
                             (m m) (w w) (f f) (y y))))))
  
  
  
  ;here
  
  
  
  
  
  ; half of correctness of program satisfiability semantics (we can't get the
  ; other half until we get the other half of the box semantics correctness).
  
  
  
  (defthm union-prog-value-correct
    (implies (and (equal (len p) 3)
  