---

Step * 1 1 1 4 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
{ RepUR ``p-graph p-fun-exp p-compose p-id can-apply do-apply`` 0 }

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

---

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

RepUR  ``p-graph  p-fun-exp  p-compose  p-id  can-apply  do-apply``  0

---

Home Index