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