### Nuprl Lemma : fun-path-append1

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

Proof

Definitions occuring in Statement :  fun-path: `y=f*(x) via L` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` 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` 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: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` subtract: `n - m` less_than': `less_than'(a;b)` cons: `[a / b]` true: `True` last: `last(L)` cand: `A c∧ B` sq_type: `SQType(T)` nat_plus: `ℕ+` nat: `ℕ` ge: `i ≥ j `
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

Latex:
\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