---

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


1. s : SES@i'
2. es : EO+(Info)@i'
3. e : E@i
4. a : Atom1@i
5. z : E@i
6. z ->> e@i
7. e' : E@i
8. (e' has a)@i
9. e' (->>^*) z@i
10. (e' has a)
⊢ e' (->>^*) e
BY
{ ((RWO "rel_star_iff" 0 THEN Auto) THEN OrLeft THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "rel\_star\_iff"  0  THEN  Auto)  THEN  OrLeft  THEN  Auto)

---

Home Index