---

Step * 1 1 1 4 1 of Lemma es-causl_weakening_p-locl

.....wf..... 
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. causal-predecessor(es;p)@i
4. n : ℕ+@i
⊢ ℕ+ ∈ Type
BY
{ Auto }

---

Latex:


.....wf..... 
1.  es  :  EO@i'
2.  p  :  E  {}\mrightarrow{}  (E  +  Top)@i
3.  causal-predecessor(es;p)@i
4.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  \mBbbN{}\msupplus{}  \mmember{}  Type


By

Auto

---

Home Index