anchor.diff:                               (pdl-satisfies m v (third f))))))
   
   
  -(defthm union-formula-satisfied-implies-disjunction-of-membership-satisfies
  +(defthm union-satisfiability-semicorrect
     (let ((first (first f))
           (second (second f))
           (third (third f)))
  
positive.code:            :use ((:instance box-semantics-semicorrect
                              (m m) (w w) (f f) (v v))))))
  
  ;here
  
  
  
  (defthm union-implies-disjunction-of-membership
   (let ((first (first f))
         (second (second f)))
     (implies (and (equal (len f) 3)
                   (equal first 'box)
                   (equal (len second) 3)
                   (equal (first second) 'union)
                   (natp w)
                   (< w (len (pdl-prog-value m second))))
              (implies
               (pdl-satisfies m w f)
               (implies
                (member v (prog-accessible-worlds m w second))
                (or (member v (prog-accessible-worlds m w (second second)))
                    (member v (prog-accessible-worlds m w (third second)))))))))
  
  
  ; 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).
  
  (thm
   (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) 'union)
                   (natp w)
                   (< w (len (pdl-prog-value m second))))
              (implies
               (pdl-satisfies m w f)
               (or (pdl-satisfies m w (list 'box (second second) third))
                   (pdl-satisfies m w (list 'box (third second) third)))))))
  
  (defthm union-prog-value-correct
    (implies (and (equal (len p) 3)
  
negative.code:   (if (zp i)
        r
      (fooindsch (- i 1) r)))
  
  (defthm foolemma2
   (implies (and (natp i)
                 (< i (len R)))
            (equal (car (foo i R)) i)))
  
  
  
  
  ;base2
  (defthm foolemmabase2
   (implies (and (natp i)
                 (< i (len R))
                 (zp i))
            (equal (nthcdr i (foo 0 R))
                   (cons i (foo (+ 1 (nfix i)) R)))))
  
  ;ind 
  (thm
   (implies (and (natp i)
                 (< i (len R))
                 (not (zp i))
                 (equal (nthcdr (+ -1 i) (foo 0 R))
                        (cons (+ -1 i) (foo (+ 1 (nfix (+ -1 i))) R))))
            (equal (nthcdr i (foo 0 R))
                   (cons i (foo (+ 1 (nfix i)) R))))
   :hints (("Goal"
            :induct (foo i R))))
  
  
  
  (thm
   (implies (and (natp i)
                 (< i (len R)))
            (equal (nthcdr i (foo 0 R))
                   (cons i (foo (+ 1 (nfix i)) R))))
   :hints (("Goal"
            :induct (foo i R))))
  
  
  (thm
   (implies (and (natp i)
                 (< i (len R)))
            (equal (nthcdr i (foo 0 R))
                   (cons i (foo (+ 1 (nfix i)) R))))
   :hints (("Goal"
            :induct (fooindsch i R))))
  
  
  
  
  
  (defthm foolemma1
   (implies (< 0 (len R))
            (consp (foo 0 R))))
  
  ;base
  (defthm foolemmabase
   (implies (and (natp i)
                 (< i (len R))
                 (zp i))
            (equal (nth i (foo 0 R))
                   i)))
  
  ;ind
  (thm
   (implies (and (natp i)
                 (< i (len R))
                 (not (zp i))
                 (equal (nth (+ -1 i) (foo 0 R))
                        (+ -1 i)))
            (equal (nth i (foo 0 R))
                   i)))
  
  
  (thm
   (implies (and (natp i)
                 (< i (len R)))
            (equal (nth i (foo 0 R))
                   i))
   :hints (("Goal"
            :induct (fooindsch i R))))
  
  
  
  
  
  (defthm foobase
  