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)


Definitions occuring in Statement :  fun-path: y=f*(x) via L l_member: (x ∈ l) list: List 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 so_lambda: λ2x.t[x] uimplies: supposing a prop: so_apply: x[s] implies:  Q all: x:A. B[x] fun-path: y=f*(x) via L select: L[n] nil: [] it: so_lambda: λ2y.t[x; y] top: Top so_apply: x[s1;s2] subtract: m and: P ∧ Q less_than: a < b squash: T less_than': less_than'(a;b) false: False iff: ⇐⇒ 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

\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