### Nuprl Lemma : l_tree-definition

`∀[L,T,A:Type]. ∀[R:A ─→ l_tree(L;T) ─→ ℙ].`
`  ((∀val:L. {x:A| R[x;l_tree_leaf(val)]} )`
`  `` (∀val:T. ∀left_subtree,right_subtree:l_tree(L;T).`
`        ({x:A| R[x;left_subtree]} `
`        `` {x:A| R[x;right_subtree]} `
`        `` {x:A| R[x;l_tree_node(val;left_subtree;right_subtree)]} ))`
`  `` {∀v:l_tree(L;T). {x:A| R[x;v]} })`

Proof

Definitions occuring in Statement :  l_tree_node: `l_tree_node(val;left_subtree;right_subtree)` l_tree_leaf: `l_tree_leaf(val)` l_tree: `l_tree(L;T)` 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]` universe: `Type`
Lemmas :  l_tree-induction set_wf l_tree_wf all_wf l_tree_node_wf l_tree_leaf_wf
\mforall{}[L,T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  l\_tree(L;T)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}val:L.  \{x:A|  R[x;l\_tree\_leaf(val)]\}  )
{}\mRightarrow{}  (\mforall{}val:T.  \mforall{}left\$_{subtree}\$,right\$_{subtree}\$:l\_tree(L;T\000C).
(\{x:A|  R[x;left\$_{subtree}\$]\}
{}\mRightarrow{}  \{x:A|  R[x;right\$_{subtree}\$]\}
{}\mRightarrow{}  \{x:A|  R[x;l\_tree\_node(val;left\$_{subtree}\$;right\$_{subtre\000Ce}\$)]\}  ))
{}\mRightarrow{}  \{\mforall{}v:l\_tree(L;T).  \{x:A|  R[x;v]\}  \})

Date html generated: 2015_07_17-AM-07_41_40
Last ObjectModification: 2015_01_27-AM-09_31_14

Home Index