---

Step * of Lemma ses-legal-thread-has-atom

∀s:SES
  (ActionsDisjoint
  ⇒ (∀es:EO+(Info). ∀A:Id. ∀thr:Thread.
        (Legal(thr)@A
        ⇒ (∀a:Atom1. ∀e:Act.
              (e ∈ thr
              ⇒ (e has a)
              ⇒ ((∃e':Act. ((e' <loc e) ∧ (e' has a) ∧ e' ∈ thr))
                 ∨ (a ∈ UseableAtoms(e))
                 ∨ (a = Private(A) ∈ Atom1)))))))
BY
{ (Auto
   THEN (Assert Action(e) BY
               (DVar `e' THEN Unhide THEN Auto))
   THEN (FLemma `ses-act-has-atom` [-2] THENA Auto)
   THEN D -1
   THEN Auto) }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. a : Atom1@i
8. e : Act@i
9. e ∈ thr@i
10. (e has a)@i
11. Action(e)
12. (a ∈ UsedAtoms(e))
⊢ (∃e':Act. ((e' <loc e) ∧ (e' has a) ∧ e' ∈ thr)) ∨ (a ∈ UseableAtoms(e)) ∨ (a = Private(A) ∈ Atom1)

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}A:Id.  \mforall{}thr:Thread.
                (Legal(thr)@A
                {}\mRightarrow{}  (\mforall{}a:Atom1.  \mforall{}e:Act.
                            (e  \mmember{}  thr
                            {}\mRightarrow{}  (e  has  a)
                            {}\mRightarrow{}  ((\mexists{}e':Act.  ((e'  <loc  e)  \mwedge{}  (e'  has  a)  \mwedge{}  e'  \mmember{}  thr))
                                  \mvee{}  (a  \mmember{}  UseableAtoms(e))
                                  \mvee{}  (a  =  Private(A))))))))


By

---

Latex:
(Auto
  THEN  (Assert  Action(e)  BY
                          (DVar  `e'  THEN  Unhide  THEN  Auto))
  THEN  (FLemma  `ses-act-has-atom`  [-2]  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index