Nuprl Lemma : retraction-fun-path-before

`∀[T:Type]. ∀f:T ⟶ T. (retraction(T;f) `` (∀L:T List. ∀x,y,a,b:T.  a before b ∈ L `` a = f+(b) supposing x=f*(y) via L))`

Proof

Definitions occuring in Statement :  retraction: `retraction(T;f)` strict-fun-connected: `y = f+(x)` fun-path: `y=f*(x) via L` l_before: `x before y ∈ l` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` uimplies: `b supposing a` member: `t ∈ T` fun-path: `y=f*(x) via L` and: `P ∧ Q` not: `¬A` false: `False` int_seg: `{i..j-}` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` prop: `ℙ` less_than: `a < b` squash: `↓T` strict-fun-connected: `y = f+(x)` uiff: `uiff(P;Q)`
Lemmas referenced :  member-less_than length_wf equal_wf select_wf 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 intformless_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_subtract_lemma int_seg_wf fun-path-before l_before_wf fun-path_wf list_wf retraction_wf no_repeats_iff fun-path-no_repeats
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality extract_by_obid isectElimination natural_numberEquality cumulativity hypothesisEquality hypothesis independent_isectElimination axiomEquality lambdaEquality dependent_functionElimination voidElimination equalityTransitivity equalitySymmetry because_Cache addEquality setElimination rename unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidEquality independent_pairFormation computeAll imageElimination independent_functionElimination functionExtensionality applyEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type]
\mforall{}f:T  {}\mrightarrow{}  T
(retraction(T;f)
{}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}x,y,a,b:T.    a  before  b  \mmember{}  L  {}\mRightarrow{}  a  =  f+(b)  supposing  x=f*(y)  via  L))

Date html generated: 2018_05_21-PM-07_47_40
Last ObjectModification: 2017_07_26-PM-05_25_36

Theory : general

Home Index