---

Step * of Lemma bs_tree-definition

∀[E,A:Type]. ∀[R:A ⟶ bs_tree(E) ⟶ ℙ].
  ({x:A| R[x;bst_null()]} 
  ⇒ (∀value:E. {x:A| R[x;bst_leaf(value)]} )
  ⇒ (∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
        ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;bst_node(left;value;right)]} ))
  ⇒ {∀v:bs_tree(E). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `bs_tree-induction` }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeDefinition  `bs\_tree-induction`

---

Home Index