---

Step * 1 of Lemma add-cause_wf


1. M : Type ─→ Type
2. ev : ℕ × Id
3. ext : LabeledDAG(Id × pCom(P.M[P]))
⊢ lg-map(λx.<ev, x>;ext) ∈ LabeledDAG(ℤ × Id × Id × pCom(P.M[P]))
BY
{ (BLemma `lg-map-wf_dag` THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  ev  :  \mBbbN{}  \mtimes{}  Id
3.  ext  :  LabeledDAG(Id  \mtimes{}  pCom(P.M[P]))
\mvdash{}  lg-map(\mlambda{}x.<ev,  x>ext)  \mmember{}  LabeledDAG(\mBbbZ{}  \mtimes{}  Id  \mtimes{}  Id  \mtimes{}  pCom(P.M[P]))


By

---

Latex:
(BLemma  `lg-map-wf\_dag`  THEN  Auto)

---

Home Index