---

Step * of Lemma pi_prefix-induction

∀[P:pi_prefix() ⟶ ℙ]
  ((∀chan,var:Name.  P[pisend(chan;var)]) ⇒ (∀chan,var:Name.  P[pircv(chan;var)]) ⇒ {∀v:pi_prefix(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[P:pi\_prefix()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}chan,var:Name.    P[pisend(chan;var)])
    {}\mRightarrow{}  (\mforall{}chan,var:Name.    P[pircv(chan;var)])
    {}\mRightarrow{}  \{\mforall{}v:pi\_prefix().  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index