Step * of Lemma binary-tree-definition

[A:Type]. ∀[R:A ⟶ binary-tree() ⟶ ℙ].
  ((∀val:ℤ{x:A| R[x;btr_Leaf(val)]} )
   (∀left,right:binary-tree().  ({x:A| R[x;left]}   {x:A| R[x;right]}   {x:A| R[x;btr_Node(left;right)]} ))
   {∀v:binary-tree(). {x:A| R[x;v]} })
BY
ProveDatatypeDefinition `binary-tree-induction` }


Latex:


Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  binary-tree()  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}val:\mBbbZ{}.  \{x:A|  R[x;btr\_Leaf(val)]\}  )
    {}\mRightarrow{}  (\mforall{}left,right:binary-tree().
                (\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;btr\_Node(left;right)]\}  ))
    {}\mRightarrow{}  \{\mforall{}v:binary-tree().  \{x:A|  R[x;v]\}  \})


By


Latex:
ProveDatatypeDefinition  `binary-tree-induction`




Home Index