### Nuprl Lemma : l_tree-ext

`∀[L,T:Type].`
`  l_tree(L;T) ≡ lbl:Atom × if lbl =a "leaf" then L`
`                           if lbl =a "node" then val:T × left_subtree:l_tree(L;T) × l_tree(L;T)`
`                           else Void`
`                           fi `

Proof

Definitions occuring in Statement :  l_tree: `l_tree(L;T)` ifthenelse: `if b then t else f fi ` eq_atom: `x =a y` ext-eq: `A ≡ B` uall: `∀[x:A]. B[x]` product: `x:A × B[x]` token: `"\$token"` atom: `Atom` void: `Void` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` member: `t ∈ T` l_tree: `l_tree(L;T)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` sq_type: `SQType(T)` guard: `{T}` eq_atom: `x =a y` bfalse: `ff` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` bnot: `¬bb` assert: `↑b` false: `False` l_treeco_size: `l_treeco_size(p)` spreadn: spread3 nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` has-value: `(a)↓` l_tree_size: `l_tree_size(p)` le: `A ≤ B` less_than': `less_than'(a;b)` not: `¬A` nequal: `a ≠ b ∈ T ` decidable: `Dec(P)` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top`
Lemmas referenced :  l_treeco-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom ifthenelse_wf l_tree_wf int_subtype_base l_treeco_size_wf subtype_partial_sqtype_base nat_wf set_subtype_base le_wf base_wf value-type-has-value int-value-type has-value_wf-partial set-value-type l_treeco_wf false_wf nat_properties l_tree_size_wf decidable__le satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformnot_wf itermAdd_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_term_value_add_lemma int_formula_prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation independent_pairFormation universeEquality lambdaEquality sqequalHypSubstitution setElimination thin rename cut introduction extract_by_obid hypothesis isectElimination hypothesisEquality promote_hyp productElimination hypothesis_subsumption applyEquality sqequalRule dependent_pairEquality tokenEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination because_Cache instantiate cumulativity atomEquality dependent_functionElimination independent_functionElimination dependent_pairFormation voidElimination productEquality voidEquality dependent_set_memberEquality natural_numberEquality intEquality baseApply closedConclusion baseClosed callbyvalueAdd addEquality applyLambdaEquality int_eqEquality isect_memberEquality computeAll

Latex:
\mforall{}[L,T:Type].
l\_tree(L;T)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "leaf"  then  L
if  lbl  =a  "node"  then  val:T  \mtimes{}  left\$_{subtree}\$:l\_tree\000C(L;T)  \mtimes{}  l\_tree(L;T)
else  Void
fi

Date html generated: 2018_05_22-PM-09_38_29
Last ObjectModification: 2017_03_04-PM-07_25_31

Theory : labeled!trees

Home Index