Step
*
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. (0 < n c∧ ((e' ->>^n - 1 z) ∧ (z ->> e)))
⊢ (e has a) ∨ (∃z:E. ((z ->> e) ∧ z has* a))
BY
{ ((OrRight THEN Auto) THEN ParallelLast THEN Auto) }
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
⊢ z has* a
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. \mexists{}z:E. (0 < n c\mwedge{} ((e' rel\_exp(E; ->> n - 1) z) \mwedge{} (z ->> e)))
\mvdash{} (e has a) \mvee{} (\mexists{}z:E. ((z ->> e) \mwedge{} z has* a))
By
Latex:
((OrRight THEN Auto) THEN ParallelLast THEN Auto)
Home
Index