---

Step * of Lemma binary-tree-induction

∀[P:binary-tree() ─→ ℙ]
  ((∀val:ℤ. P[btr_Leaf(val)])
  ⇒ (∀left,right:binary-tree().  (P[left] ⇒ P[right] ⇒ P[btr_Node(left;right)]))
  ⇒ {∀v:binary-tree(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[P:binary-tree()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}val:\mBbbZ{}.  P[btr\_Leaf(val)])
    {}\mRightarrow{}  (\mforall{}left,right:binary-tree().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[btr\_Node(left;right)]))
    {}\mRightarrow{}  \{\mforall{}v:binary-tree().  P[v]\})


By

ProveDatatypeInd

---

Home Index