### Nuprl Lemma : l_tree_ind_wf_simple

`∀[L,T,A:Type]. ∀[v:l_tree(L;T)]. ∀[leaf:val:L ⟶ A]. ∀[node:val:T`
`                                                            ⟶ left_subtree:l_tree(L;T)`
`                                                            ⟶ right_subtree:l_tree(L;T)`
`                                                            ⟶ A`
`                                                            ⟶ A`
`                                                            ⟶ A].`
`  (l_tree_ind(v;`
`              Leaf(val)`` leaf[val];`
`              Node(val,left_subtree,right_subtree)`` rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2])  ∈ A)`

Proof

Definitions occuring in Statement :  l_tree_ind: l_tree_ind l_tree: `l_tree(L;T)` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2;s3;s4;s5]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` prop: `ℙ` uimplies: `b supposing a` all: `∀x:A. B[x]` true: `True` guard: `{T}`
Lemmas referenced :  l_tree_ind_wf true_wf l_tree_wf subtype_rel_dep_function set_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality because_Cache setEquality independent_isectElimination lambdaFormation dependent_set_memberEquality natural_numberEquality functionEquality setElimination rename equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[L,T,A:Type].  \mforall{}[v:l\_tree(L;T)].  \mforall{}[leaf:val:L  {}\mrightarrow{}  A].  \mforall{}[node:val:T
{}\mrightarrow{}  left\$_{subtree}\$:\000Cl\_tree(L;T)
{}\mrightarrow{}  right\$_{subtree}\$\000C:l\_tree(L;T)
{}\mrightarrow{}  A
{}\mrightarrow{}  A
{}\mrightarrow{}  A].
(l\_tree\_ind(v;
Leaf(val){}\mRightarrow{}  leaf[val];
Node(val,left\$_{subtree}\$,right\$_{subtree}\$){}\mRightarrow{}\000C  rec1,rec2.node[val;left\$_{subtree}\$;...;rec1;rec2])
\mmember{}  A)

Date html generated: 2018_05_22-PM-09_39_22
Last ObjectModification: 2015_12_28-PM-06_41_42

Theory : labeled!trees

Home Index