anchor.diff:             :use ((:instance box-semantics-semicorrect
                               (m m) (w w) (f f) (v v))))))
   
  -;here
  -
  -
  -
  -(defthm union-implies-disjunction-of-membership
  +(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) 'union)
  +                 (equal (first second) 'compose)
                    (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
  +              (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) 'union)
  +                 (equal (first second) 'compose)
                    (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)))))))
  +             (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)
  
positive.code:   (if (zp i)
        r
      (fooindsch (- i 1) r)))
  
  
  (defthm foobase
  
negative.code:                              (pdl-satisfies m v (third f))))))
  
  
  (defthm union-satisfiability-semicorrect
    (let ((first (first f))
          (second (second f))
          (third (third f)))
  