Nuprl Lemma : fun-path-append1

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


Definitions occuring in Statement :  fun-path: y=f*(x) via L append: as bs cons: [a b] nil: [] list: List uimplies: supposing a uall: [x:A]. B[x] not: ¬A 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 append: as bs all: x:A. B[x] so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3] 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] less_than: a < b squash: T uiff: uiff(P;Q) select: L[n] nil: [] it: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] subtract: m less_than': less_than'(a;b) cons: [a b] true: True last: last(L) cand: c∧ B sq_type: SQType(T) nat_plus: + nat: ge: i ≥ 
Lemmas referenced :  list_induction uall_wf isect_wf fun-path_wf equal_wf not_wf append_wf cons_wf nil_wf list_wf list_ind_nil_lemma list_ind_cons_lemma member-less_than length_wf select_wf length-append length_of_cons_lemma length_of_nil_lemma 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 add-is-int-iff intformless_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_subtract_lemma false_wf int_seg_wf stuck-spread base_wf add-subtract-cancel fun-path-cons list-cases product_subtype_list reduce_hd_cons_lemma less_than_wf decidable__equal_int subtype_base_sq int_subtype_base intformeq_wf int_formula_prop_eq_lemma add_nat_plus length_wf_nat nat_plus_wf nat_plus_properties nat_wf nat_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality cumulativity because_Cache functionExtensionality applyEquality hypothesis independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation rename productElimination independent_pairEquality independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry functionEquality natural_numberEquality addEquality setElimination unionElimination dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll pointwiseFunctionality promote_hyp imageElimination baseApply closedConclusion baseClosed universeEquality hypothesis_subsumption imageMemberEquality instantiate dependent_set_memberEquality applyLambdaEquality

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

Date html generated: 2018_05_21-PM-07_43_57
Last ObjectModification: 2017_07_26-PM-05_21_40

Theory : general

Home Index