### Nuprl 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]} })`

Proof

Definitions occuring in Statement :  btr_Node: `btr_Node(left;right)` btr_Leaf: `btr_Leaf(val)` binary-tree: `binary-tree()` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` int: `ℤ` universe: `Type`
Lemmas :  binary-tree-induction set_wf all_wf binary-tree_wf btr_Node_wf btr_Leaf_wf
\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]\}  \})

Date html generated: 2015_07_17-AM-07_52_19
Last ObjectModification: 2015_01_27-AM-09_35_43

Home Index