### Nuprl Lemma : retraction-fun-path

`∀[T:Type]`
`  ∀f:T ⟶ T. ∀h:T ⟶ ℕ.`
`    ((∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)) `` (∀L:T List. ∀x,y:T.  (x = y ∈ T) ∨ h y < h x supposing y=f*(x) via L))`

Proof

Definitions occuring in Statement :  fun-path: `y=f*(x) via L` list: `T List` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` prop: `ℙ` subtype_rel: `A ⊆r B` so_apply: `x[s]` fun-path: `y=f*(x) via L` and: `P ∧ Q` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` length: `||as||` list_ind: list_ind nil: `[]` it: `⋅` false: `False` not: `¬A` int_seg: `{i..j-}` top: `Top` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` uiff: `uiff(P;Q)` nat: `ℕ` select: `L[n]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` subtract: `n - m` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction all_wf isect_wf fun-path_wf or_wf equal_wf less_than_wf list_wf member-less_than nil_wf length_wf cons_wf select_wf length_of_cons_lemma int_seg_properties subtract_wf decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt add-is-int-iff intformless_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_subtract_lemma false_wf int_seg_wf nat_wf length_of_nil_lemma stuck-spread base_wf fun-path-cons squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity because_Cache functionExtensionality applyEquality hypothesis independent_functionElimination productElimination independent_pairEquality imageElimination voidElimination independent_isectElimination axiomEquality dependent_functionElimination rename natural_numberEquality equalityTransitivity equalitySymmetry addEquality setElimination isect_memberEquality voidEquality unionElimination dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed functionEquality universeEquality inlFormation hyp_replacement applyLambdaEquality inrFormation imageMemberEquality

Latex:
\mforall{}[T:Type]
\mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}h:T  {}\mrightarrow{}  \mBbbN{}.
((\mforall{}x:T.  (((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x))
{}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}x,y:T.    (x  =  y)  \mvee{}  h  y  <  h  x  supposing  y=f*(x)  via  L))

Date html generated: 2018_05_21-PM-07_46_34
Last ObjectModification: 2017_07_26-PM-05_24_00

Theory : general

Home Index