---

Step * 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 has* a@i
⊢ (e has a) ∨ (∃z:E. ((z ->> e) ∧ z has* a))
BY
{ (RepeatFor 2 (D -1) THEN (RepUR ``rel_star`` -1 THEN ExRepD) THEN (RWO "rel_exp_iff" (-1) THENA Auto) THEN D -1) }

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. (0 < n c∧ ((e' ->>^n - 1 z) ∧ (z ->> e)))
⊢ (e has a) ∨ (∃z:E. ((z ->> e) ∧ z has* a))

2
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. (n = 0 ∈ ℤ) ∧ (e' = e ∈ E)
⊢ (e has a) ∨ (∃z:E. ((z ->> e) ∧ z has* a))

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  e  :  E@i
4.  a  :  Atom1@i
5.  e  has*  a@i
\mvdash{}  (e  has  a)  \mvee{}  (\mexists{}z:E.  ((z  ->>  e)  \mwedge{}  z  has*  a))


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  (RepUR  ``rel\_star``  -1  THEN  ExRepD)
  THEN  (RWO  "rel\_exp\_iff"  (-1)  THENA  Auto)
  THEN  D  -1)

---

Home Index