Nuprl Lemma : linearization-value

[L:ℤ List List]. ∀[p:iPolynomial()].
  ∀f:ℤ ⟶ ℤ
    linearization(p;L) ⋅ map(λvs.accumulate (with value and list item v):
                                    (f v)
                                   over list:
                                   with starting value:
    ∈ ℤ
  supposing (∀m∈p.(snd(m) ∈ L)) ∧ no_repeats(ℤ List;L)


Definitions occuring in Statement :  linearization: linearization(p;L) ipolynomial-term: ipolynomial-term(p) iPolynomial: iPolynomial() int_term_value: int_term_value(f;t) integer-dot-product: as ⋅ bs l_all: (∀x∈L.P[x]) no_repeats: no_repeats(T;l) l_member: (x ∈ l) map: map(f;as) list_accum: list_accum list: List uimplies: supposing a uall: [x:A]. B[x] pi2: snd(t) all: x:A. B[x] and: P ∧ Q apply: a lambda: λx.A[x] function: x:A ⟶ B[x] multiply: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  guard: {T} uimplies: supposing a prop: or: P ∨ Q top: Top cons: [a b] le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) not: ¬A colength: colength(L) nil: [] it: so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) less_than: a < b squash: T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] sq_stable: SqStable(P) subtract: m subtype_rel: A ⊆B iPolynomial: iPolynomial() linearization: linearization(p;L) ipolynomial-term: ipolynomial-term(p) int_term_value: int_term_value(f;t) ifthenelse: if then else fi  btrue: tt itermConstant: "const" int_term_ind: int_term_ind iMonomial: iMonomial() pi2: snd(t) true: True iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) bool: 𝔹 unit: Unit bfalse: ff exists: x:A. B[x] bnot: ¬bb assert: b bor: p ∨bq deq: EqDecider(T) int_nzero: -o istype: istype(T) select: L[n] int_seg: {i..j-} lelt: i ≤ j < k poly-coeff-of: poly-coeff-of(vs;p) so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] nat_plus: + decidable: Dec(P) l_all: (∀x∈L.P[x]) imonomial-less: imonomial-less(m1;m2) imonomial-term: imonomial-term(m) cand: c∧ B nequal: a ≠ b ∈  list_ind: list_ind imonomial-le: imonomial-le(m1;m2) l_member: (x ∈ l)
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf no_repeats_wf list_wf iPolynomial_wf list-cases deq_member_nil_lemma istype-void map_nil_lemma istype-int nil_wf product_subtype_list colength-cons-not-zero nat_wf colength_wf_list istype-false le_wf subtract-1-ge-0 subtype_base_sq set_subtype_base int_subtype_base spread_cons_lemma sq_stable__le add-associates add-commutes add-swap zero-add deq_member_cons_lemma map_cons_lemma cons_wf le_weakening2 filter-bfalse subtype_rel_list iMonomial_wf top_wf null_nil_lemma int_dot_nil_left_lemma int_dot_cons_lemma int_term_value_wf ipolynomial-term_wf filter_wf5 l_member_wf bor_wf list-deq_wf1 int-deq_wf deq-member_wf list-deq_wf poly-coeff-of_wf list_accum_wf integer-dot-product_wf linearization_wf map_wf equal_wf squash_wf true_wf add_functionality_wrt_eq subtype_rel_self iff_weakening_equal no_repeats_cons filter_nil_lemma filter_cons_lemma eqtt_to_assert assert-deq-member eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot testxxx_lemma list_subtype_base assert_wf imonomial-term_wf subtype_rel_product int_nzero_wf sorted_wf ipolynomial-term-cons-value length_of_nil_lemma stuck-spread istype-base int_seg_wf imonomial-less_wf length_of_cons_lemma length_wf select_wf non_neg_length length_wf_nat list_ind_wf intlex_wf mul-commutes less-iff-le add_functionality_wrt_le subtract_wf le_reflexive minus-add minus-one-mul one-mul add-mul-special two-mul mul-distributes-right zero-mul add-zero not-lt-2 omega-shadow mul-distributes mul-associates minus-one-mul-top int_seg_properties decidable__lt list_ind_nil_lemma assert-list-deq iff_weakening_uiff equal-wf-base-T less_than_transitivity2 filter_is_nil add-member-int_seg2 decidable__le not-le-2 condition-implies-le le-add-cancel2 le-add-cancel select_cons_tl add-subtract-cancel list_ind_cons_lemma intlex-reflexive btrue_wf int_nzero_properties itermConstant_wf list_accum_nil_lemma int_term_wf list_accum_cons_lemma itermMultiply_wf itermVar_wf int_term_value_mul_lemma int_term_value_var_lemma mul-swap intlex-antisym not-equal-2 intlex-total l_all_wf_nil l_all_wf add_nat_plus iff_imp_equal_bool select-cons-tl not-equal-implies-less filter_trivial istype-top
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction thin Error :lambdaFormation_alt,  extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination Error :universeIsType,  sqequalRule Error :lambdaEquality_alt,  dependent_functionElimination Error :isect_memberEquality_alt,  axiomEquality Error :functionIsTypeImplies,  Error :inhabitedIsType,  intEquality equalityTransitivity equalitySymmetry unionElimination Error :functionIsType,  because_Cache promote_hyp hypothesis_subsumption productElimination Error :equalityIsType1,  Error :dependent_set_memberEquality_alt,  independent_pairFormation instantiate cumulativity imageElimination imageMemberEquality baseClosed applyLambdaEquality applyEquality minusEquality Error :equalityIsType4,  addEquality functionExtensionality Error :setIsType,  multiplyEquality universeEquality equalityElimination Error :dependent_pairFormation_alt,  independent_pairEquality setEquality sqequalIntensionalEquality Error :productIsType,  hyp_replacement productEquality

\mforall{}[L:\mBbbZ{}  List  List].  \mforall{}[p:iPolynomial()].
    \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
        =  linearization(p;L)  \mcdot{}  map(\mlambda{}vs.accumulate  (with  value  x  and  list  item  v):
                                                                        x  *  (f  v)
                                                                      over  list:
                                                                      with  starting  value:
    supposing  (\mforall{}m\mmember{}p.(snd(m)  \mmember{}  L))  \mwedge{}  no\_repeats(\mBbbZ{}  List;L)

Date html generated: 2019_06_20-PM-00_47_26
Last ObjectModification: 2018_10_04-PM-02_39_59

Theory : omega

Home Index