### Nuprl Lemma : max_w_unit_l_tree_wf

`∀[T:Type]. ∀[u1,u2:T?]. ∀[f:T ⟶ ℤ].  (max_w_unit_l_tree(u1;u2;f) ∈ T?)`

Proof

Definitions occuring in Statement :  max_w_unit_l_tree: `max_w_unit_l_tree(u1;u2;f)` uall: `∀[x:A]. B[x]` unit: `Unit` member: `t ∈ T` function: `x:A ⟶ B[x]` union: `left + right` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` max_w_unit_l_tree: `max_w_unit_l_tree(u1;u2;f)` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  max_w_ord_wf unit_wf2 equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule hypothesisEquality equalityTransitivity hypothesis equalitySymmetry thin because_Cache lambdaFormation unionElimination inlEquality extract_by_obid sqequalHypSubstitution isectElimination dependent_functionElimination independent_functionElimination axiomEquality functionEquality intEquality isect_memberEquality unionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[u1,u2:T?].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (max\_w\_unit\_l\_tree(u1;u2;f)  \mmember{}  T?)

Date html generated: 2019_10_31-AM-06_25_42
Last ObjectModification: 2018_08_21-PM-02_01_02

Theory : labeled!trees

Home Index