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