---

Step * of Lemma norm-system_wf

∀[M:Type ─→ Type]. norm-system ∈ id-fun(System(P.M[P])) supposing M[Top]
BY
{ (Unfold `System` 0 THEN ProveWfLemma) }

1
1. M : Type ─→ Type
2. M[Top]
3. component(P.M[P]) List@i
⊢ value-type(LabeledGraph(pInTransit(P.M[P])))

2
1. M : Type ─→ Type
2. M[Top]
3. a : component(P.M[P]) List
⊢ norm-lg(λx.x) ∈ id-fun(LabeledDAG(pInTransit(P.M[P])))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  norm-system  \mmember{}  id-fun(System(P.M[P]))  supposing  M[Top]


By

---

Latex:
(Unfold  `System`  0  THEN  ProveWfLemma)

---

Home Index