---

Step * of Lemma pi_term-induction

∀[P:pi_term() ⟶ ℙ]
  (P[pizero()]
  ⇒ (∀pre:pi_prefix(). ∀body:pi_term().  (P[body] ⇒ P[picomm(pre;body)]))
  ⇒ (∀left,right:pi_term().  (P[left] ⇒ P[right] ⇒ P[pioption(left;right)]))
  ⇒ (∀left,right:pi_term().  (P[left] ⇒ P[right] ⇒ P[pipar(left;right)]))
  ⇒ (∀body:pi_term(). (P[body] ⇒ P[pirep(body)]))
  ⇒ (∀name:Name. ∀body:pi_term().  (P[body] ⇒ P[pinew(name;body)]))
  ⇒ {∀v:pi_term(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[P:pi\_term()  {}\mrightarrow{}  \mBbbP{}]
    (P[pizero()]
    {}\mRightarrow{}  (\mforall{}pre:pi\_prefix().  \mforall{}body:pi\_term().    (P[body]  {}\mRightarrow{}  P[picomm(pre;body)]))
    {}\mRightarrow{}  (\mforall{}left,right:pi\_term().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[pioption(left;right)]))
    {}\mRightarrow{}  (\mforall{}left,right:pi\_term().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[pipar(left;right)]))
    {}\mRightarrow{}  (\mforall{}body:pi\_term().  (P[body]  {}\mRightarrow{}  P[pirep(body)]))
    {}\mRightarrow{}  (\mforall{}name:Name.  \mforall{}body:pi\_term().    (P[body]  {}\mRightarrow{}  P[pinew(name;body)]))
    {}\mRightarrow{}  \{\mforall{}v:pi\_term().  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index