Nuprl Lemma : fix-step

[T:Type]. ∀[eq:EqDecider(T)]. ∀[f:T ⟶ T]. ∀[x:T].  f**(f x) f**(x) ∈ supposing retraction(T;f)


Proof




Definitions occuring in Statement :  fix: f**(x) retraction: retraction(T;f) deq: EqDecider(T) uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: implies:  Q squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q fix: f**(x) ycomb: Y all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt eqof: eqof(d) deq: EqDecider(T) uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb assert: b false: False not: ¬A
Lemmas referenced :  retraction_wf equal_wf squash_wf true_wf fix_wf deq_wf iff_weakening_equal eqof_wf bool_wf eqtt_to_assert safe-assert-deq eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot assert_wf bnot_wf not_wf bool_cases iff_transitivity iff_weakening_uiff assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality functionExtensionality applyEquality sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry lambdaFormation lambdaEquality imageElimination universeEquality independent_isectElimination functionEquality imageMemberEquality baseClosed natural_numberEquality productElimination independent_functionElimination unionElimination equalityElimination setElimination rename dependent_pairFormation promote_hyp dependent_functionElimination instantiate voidElimination independent_pairFormation impliesFunctionality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[x:T].    f**(f  x)  =  f**(x)  supposing  retraction(T;f)



Date html generated: 2018_05_21-PM-07_47_07
Last ObjectModification: 2017_07_26-PM-05_24_39

Theory : general


Home Index