---

Step * of Lemma add-cause_wf

∀[M:Type ─→ Type]. ∀[ev:ℕ × Id]. ∀[ext:pExt(P.M[P])].  (add-cause(ev;ext) ∈ LabeledDAG(pInTransit(P.M[P])))
BY
{ (RepUR ``pInTransit pExt`` 0 THEN ProveWfLemma) }

1
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]))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[ev:\mBbbN{}  \mtimes{}  Id].  \mforall{}[ext:pExt(P.M[P])].
    (add-cause(ev;ext)  \mmember{}  LabeledDAG(pInTransit(P.M[P])))


By

---

Latex:
(RepUR  ``pInTransit  pExt``  0  THEN  ProveWfLemma)

---

Home Index