### Nuprl Lemma : retraction-fun-path-squash

`∀[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]` squash: `↓T` 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]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` prop: `ℙ` subtype_rel: `A ⊆r B` so_apply: `x[s]` squash: `↓T` nat: `ℕ` or: `P ∨ Q` fun-path: `y=f*(x) via L` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` subtract: `n - m` and: `P ∧ Q` less_than: `a < b` less_than': `less_than'(a;b)` false: `False` uiff: `uiff(P;Q)` guard: `{T}` decidable: `Dec(P)` not: `¬A` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]`
Lemmas referenced :  list_induction all_wf isect_wf fun-path_wf squash_wf or_wf equal_wf less_than_wf list_wf nil_wf cons_wf nat_wf length_of_nil_lemma stuck-spread base_wf fun-path-cons decidable__lt length_wf iff_weakening_equal satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity because_Cache functionExtensionality applyEquality hypothesis independent_functionElimination imageElimination imageMemberEquality baseClosed rename dependent_functionElimination functionEquality isect_memberEquality equalityTransitivity equalitySymmetry setElimination universeEquality independent_isectElimination voidElimination voidEquality productElimination natural_numberEquality unionElimination inlFormation hyp_replacement Error :applyLambdaEquality,  inrFormation dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll

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

Date html generated: 2016_10_25-AM-11_03_48
Last ObjectModification: 2016_07_12-AM-07_11_02

Theory : general

Home Index