---

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


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)
BY
{ ((Decide ⌜a = Private(A) ∈ Atom1⌝⋅ THEN Auto) THEN OrLeft 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))
13. ¬(a = Private(A) ∈ Atom1)
⊢ ∃e':Act. ((e' <loc e) ∧ (e' has a) ∧ e' ∈ thr)

---

Latex:

---

Latex:

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  \mmember{}  thr@i
10.  (e  has  a)@i
11.  Action(e)
12.  (a  \mmember{}  UsedAtoms(e))
\mvdash{}  (\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:
((Decide  \mkleeneopen{}a  =  Private(A)\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  OrLeft  THEN  Auto)

---

Home Index