---

Step * 1 1 1 of Lemma event-has*-iff


1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. a : Atom1@i
5. e' : E@i
6. (e' has a)@i
7. n : ℕ@i
8. z : E
9. 0 < n c∧ ((e' ->>^n - 1 z) ∧ (z ->> e))
10. z ->> e
⊢ z has* a
BY
{ ((With ⌈e'⌉ (D 0)⋅ THEN Auto) THEN RepUR ``rel_star`` 0) }

1
1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. a : Atom1@i
5. e' : E@i
6. (e' has a)@i
7. n : ℕ@i
8. z : E
9. 0 < n c∧ ((e' ->>^n - 1 z) ∧ (z ->> e))
10. z ->> e
11. (e' has a)
⊢ ∃n:ℕ. (e' ->>^n z)

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  a  :  Atom1@i
5.  e'  :  E@i
6.  (e'  has  a)@i
7.  n  :  \mBbbN{}@i
8.  z  :  E
9.  0  <  n  c\mwedge{}  ((e'  rel\_exp(E;  ->>  n  -  1)  z)  \mwedge{}  (z  ->>  e))
10.  z  ->>  e
\mvdash{}  z  has*  a


By

---

Latex:
((With  \mkleeneopen{}e'\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)  THEN  RepUR  ``rel\_star``  0)

---

Home Index