---

Step * 1 1 1 1 1 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 : Act List@i
6. \\%25 : ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])@i
7. ∀i:ℕ||thr||. UsedAtoms(thr[i]) ⊆ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]@i
8. a : Atom1@i
9. e : Act@i
10. i : ℕ||thr||@i
11. e = thr[i] ∈ E@i
12. (e has a)@i
13. Action(e)
14. (a ∈ UsedAtoms(e))
15. ¬(a = Private(A) ∈ Atom1)
16. ∀i,j:ℕ||thr||.  (thr[i] <loc thr[j]) supposing i < j
17. ∀a:Atom1. ((a ∈ UsedAtoms(thr[i])) ⇒ (a ∈ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]))
18. l : Atom1 List
19. (l ∈ map(λj.UseableAtoms(thr[j]);[0, i)))
20. (a ∈ l)
⊢ ∃e':Act. ((e' <loc e) ∧ (e' has a) ∧ e' ∈ thr)
BY
{ ((RWW "member_map" (-2) THEN Auto) THEN ExRepD)⋅ }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Act List@i
6. \\%25 : ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])@i
7. ∀i:ℕ||thr||. UsedAtoms(thr[i]) ⊆ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]@i
8. a : Atom1@i
9. e : Act@i
10. i : ℕ||thr||@i
11. e = thr[i] ∈ E@i
12. (e has a)@i
13. Action(e)
14. (a ∈ UsedAtoms(e))
15. ¬(a = Private(A) ∈ Atom1)
16. ∀i,j:ℕ||thr||.  (thr[i] <loc thr[j]) supposing i < j
17. ∀a:Atom1. ((a ∈ UsedAtoms(thr[i])) ⇒ (a ∈ [Private(A) / concat(map(λj.UseableAtoms(thr[j]);[0, i)))]))
18. l : Atom1 List
19. y : {x:ℤ| (0 ≤ x) ∧ x < i} 
20. (y ∈ [0, i))
21. l = ((λj.UseableAtoms(thr[j])) y) ∈ (Atom1 List)
22. (a ∈ l)
⊢ ∃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  :  Act  List@i
6.  \mbackslash{}\mbackslash{}\%25  :  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])@i
7.  \mforall{}i:\mBbbN{}||thr||.  UsedAtoms(thr[i])  \msubseteq{}  [Private(A)  /  concat(map(\mlambda{}j.UseableAtoms(thr[j]);[0,  i)))]@i
8.  a  :  Atom1@i
9.  e  :  Act@i
10.  i  :  \mBbbN{}||thr||@i
11.  e  =  thr[i]@i
12.  (e  has  a)@i
13.  Action(e)
14.  (a  \mmember{}  UsedAtoms(e))
15.  \mneg{}(a  =  Private(A))
16.  \mforall{}i,j:\mBbbN{}||thr||.    (thr[i]  <loc  thr[j])  supposing  i  <  j
17.  \mforall{}a:Atom1
            ((a  \mmember{}  UsedAtoms(thr[i]))  {}\mRightarrow{}  (a  \mmember{}  [Private(A)  /  concat(map(\mlambda{}j.UseableAtoms(thr[j]);[0,  i)))]))
18.  l  :  Atom1  List
19.  (l  \mmember{}  map(\mlambda{}j.UseableAtoms(thr[j]);[0,  i)))
20.  (a  \mmember{}  l)
\mvdash{}  \mexists{}e':Act.  ((e'  <loc  e)  \mwedge{}  (e'  has  a)  \mwedge{}  e'  \mmember{}  thr)


By

---

Latex:
((RWW  "member\_map"  (-2)  THEN  Auto)  THEN  ExRepD)\mcdot{}

---

Home Index