Nuprl Lemma : tree_leaf-value_wf

[E:Type]. ∀[v:tree(E)].  tree_leaf-value(v) ∈ supposing ↑tree_leaf?(v)


Proof




Definitions occuring in Statement :  tree_leaf-value: tree_leaf-value(v) tree_leaf?: tree_leaf?(v) tree: tree(E) assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) sq_type: SQType(T) guard: {T} eq_atom: =a y ifthenelse: if then else fi  tree_leaf?: tree_leaf?(v) pi1: fst(t) assert: b tree_leaf-value: tree_leaf-value(v) pi2: snd(t) bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q bnot: ¬bb false: False
Lemmas referenced :  tree-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 assert_wf tree_leaf?_wf tree_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality promote_hyp productElimination hypothesis_subsumption hypothesis applyEquality sqequalRule tokenEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination instantiate cumulativity atomEquality dependent_functionElimination independent_functionElimination because_Cache dependent_pairFormation voidElimination universeEquality

Latex:
\mforall{}[E:Type].  \mforall{}[v:tree(E)].    tree\_leaf-value(v)  \mmember{}  E  supposing  \muparrow{}tree\_leaf?(v)



Date html generated: 2017_10_01-AM-08_30_29
Last ObjectModification: 2017_07_26-PM-04_24_35

Theory : tree_1


Home Index