### Nuprl Lemma : fun-path-fixedpoint

`∀[T:Type]. ∀[f:T ⟶ T]. ∀[L:T List]. ∀[x,y,z:T].  (y = z ∈ T) supposing (((f y) = y ∈ T) and (y ∈ L) and z=f*(x) via L)`

Proof

Definitions occuring in Statement :  fun-path: `y=f*(x) via L` l_member: `(x ∈ l)` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` 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` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` prop: `ℙ` so_apply: `x[s]` implies: `P `` Q` all: `∀x:A. B[x]` 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` squash: `↓T` less_than': `less_than'(a;b)` false: `False` iff: `P `⇐⇒` Q` or: `P ∨ Q` cons: `[a / b]` not: `¬A` uiff: `uiff(P;Q)` guard: `{T}` nat_plus: `ℕ+` true: `True` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]`
Lemmas referenced :  list_induction uall_wf isect_wf fun-path_wf l_member_wf equal_wf list_wf length_of_nil_lemma stuck-spread base_wf nil_wf less_than_wf equal-wf-T-base all_wf int_seg_wf equal-wf-base-T not_wf equal-wf-base cons_member reduce_hd_cons_lemma cons_wf list-cases product_subtype_list null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse fun-path-cons length_of_cons_lemma add_nat_plus length_wf_nat nat_plus_wf nat_plus_properties decidable__lt add-is-int-iff full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_wf false_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality hypothesis applyEquality independent_functionElimination lambdaFormation rename because_Cache dependent_functionElimination isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality universeEquality baseClosed independent_isectElimination voidElimination voidEquality productElimination imageElimination productEquality natural_numberEquality minusEquality unionElimination promote_hyp hypothesis_subsumption dependent_set_memberEquality independent_pairFormation imageMemberEquality applyLambdaEquality setElimination pointwiseFunctionality baseApply closedConclusion approximateComputation dependent_pairFormation int_eqEquality intEquality

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[L:T  List].  \mforall{}[x,y,z:T].
(y  =  z)  supposing  (((f  y)  =  y)  and  (y  \mmember{}  L)  and  z=f*(x)  via  L)

Date html generated: 2018_05_21-PM-07_43_26
Last ObjectModification: 2018_05_19-PM-04_48_52

Theory : general

Home Index