---

Step * of Lemma bs_tree-induction

∀[E:Type]. ∀[P:bs_tree(E) ⟶ ℙ].
  (P[bst_null()]
  ⇒ (∀value:E. P[bst_leaf(value)])
  ⇒ (∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).  (P[left] ⇒ P[right] ⇒ P[bst_node(left;value;right)]))
  ⇒ {∀v:bs_tree(E). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[E:Type].  \mforall{}[P:bs\_tree(E)  {}\mrightarrow{}  \mBbbP{}].
    (P[bst\_null()]
    {}\mRightarrow{}  (\mforall{}value:E.  P[bst\_leaf(value)])
    {}\mRightarrow{}  (\mforall{}left:bs\_tree(E).  \mforall{}value:E.  \mforall{}right:bs\_tree(E).
                (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[bst\_node(left;value;right)]))
    {}\mRightarrow{}  \{\mforall{}v:bs\_tree(E).  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index