### Nuprl Lemma : fps-exp-linear-coeff

`∀[X:Type]`
`  ∀[eq:EqDecider(X)]. ∀[x,y:X].`
`    ∀[r:CRng]. ∀[k:|r|]. ∀[m,n:ℕ].`
`      ((((k)*atom(x)+atom(y)))^(m)[bag-rep(n;x)] = if (n =z m) then k ↑r m else 0 fi  ∈ |r|) `
`    supposing ¬(x = y ∈ X) `
`  supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-exp: `(f)^(n)` fps-scalar-mul: `(c)*f` fps-add: `(f+g)` fps-atom: `atom(x)` fps-coeff: `f[b]` bag-rep: `bag-rep(n;x)` deq: `EqDecider(T)` nat: `ℕ` valueall-type: `valueall-type(T)` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` universe: `Type` equal: `s = t ∈ T` rng_nexp: `e ↑r n` crng: `CRng` rng_zero: `0` rng_car: `|r|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` crng: `CRng` rng: `Rng` fps-coeff: `f[b]` fps-one: `1` int_upper: `{i...}` assert: `↑b` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` bfalse: `ff` less_than': `less_than'(a;b)` le: `A ≤ B` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` true: `True` subtype_rel: `A ⊆r B` squash: `↓T` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` decidable: `Dec(P)` fps-mul: `(f*g)` bag-partitions: `bag-partitions(eq;bs)` callbyvalueall: callbyvalueall evalall: `evalall(t)` bag-splits: `bag-splits(b)` list_ind: list_ind bag-rep: `bag-rep(n;x)` primrec: `primrec(n;b;c)` empty-bag: `{}` nil: `[]` single-bag: `{x}` cons: `[a / b]` bag-to-set: `bag-to-set(eq;bs)` bag-remove-repeats: `bag-remove-repeats(eq;bs)` list-to-set: `list-to-set(eq;L)` l-union: `as ⋃ bs` reduce: `reduce(f;k;as)` insert: `insert(a;L)` eval_list: `eval_list(t)` deq-member: `x ∈b L` cand: `A c∧ B` so_lambda: `λ2x.t[x]` power-series: `PowerSeries(X;r)` pi1: `fst(t)` pi2: `snd(t)` so_apply: `x[s]` ring_p: `IsRing(T;plus;zero;neg;times;one)` group_p: `IsGroup(T;op;id;inv)` fps-atom: `atom(x)` fps-scalar-mul: `(c)*f` fps-add: `(f+g)` fps-single: `<c>` bag-eq: `bag-eq(eq;as;bs)` bag-count: `(#x in bs)` bag-all: `bag-all(x.p[x];bs)` count: `count(P;L)` bag-map: `bag-map(f;bs)` bag-reduce: `bag-reduce(x,y.f[x; y];zero;bs)` lt_int: `i <z j` band: `p ∧b q` infix_ap: `x f y` respects-equality: `respects-equality(S;T)` bag-size: `#(bs)` length: `||as||` rev_uimplies: `rev_uimplies(P;Q)` nequal: `a ≠ b ∈ T ` nat_plus: `ℕ+` less_than: `a < b`
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than subtract-1-ge-0 istype-nat rng_car_wf crng_wf deq_wf valueall-type_wf istype-universe rng_nexp_zero bag-null-rep rng_zero_wf zero-add nequal-le-implies upper_subtype_nat neg_assert_of_eq_int assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal equal_wf eqff_to_assert le_wf false_wf rng_nexp_wf assert_of_eq_int eqtt_to_assert bool_wf eq_int_wf list-subtype-bag bag-rep_wf fps-atom_wf fps-scalar-mul_wf fps-add_wf squash_wf true_wf fps-coeff_wf bag_wf power-series_wf fps-exp-zero subtype_rel_self iff_weakening_equal subtract-add-cancel subtract_wf decidable__le intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma istype-le istype-false intformeq_wf int_formula_prop_eq_lemma fps-exp_wf fps-exp-add fps-mul_wf fps-exp-one decidable__equal_int int_subtype_base bag-summation-single rng_plus_wf rng_plus_comm2 rng_times_wf empty-bag_wf crng_properties rng_properties reduce_nil_lemma reduce_cons_lemma map_nil_lemma map_cons_lemma nil_wf rng_times_over_plus rng_times_zero rng_plus_zero bag-summation-single-non-zero-no-repeats product-deq_wf bag-deq_wf bag-partitions_wf bag-member_wf bag-member-partitions bag-size_wf bag-append-equal-bag-rep add-is-int-iff itermAdd_wf int_term_value_add_lemma respects-equality-product list_wf subtype-respects-equality bag_qinc bag-eq_wf single-bag_wf assert-bag-eq equal-wf-base set_subtype_base iff_weakening_uiff assert_wf no-repeats-bag-partitions bag-rep-add bag-summation_wf crng_all_properties int_upper_properties rng_nexp_unroll primrec1_lemma cons_bag_empty_lemma member_wf rng_one_wf rng_times_one rng_plus_comm single-valued-bag-single single-valued-bag_wf bag-only_wf2 bag_only_single_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation_alt natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation universeIsType axiomEquality isectIsTypeImplies inhabitedIsType functionIsTypeImplies because_Cache functionIsType equalityIstype instantiate universeEquality voidEquality isect_memberEquality hypothesis_subsumption cumulativity promote_hyp dependent_pairFormation equalitySymmetry equalityTransitivity dependent_set_memberEquality productElimination equalityElimination unionElimination lambdaFormation lambdaEquality applyEquality imageElimination imageMemberEquality baseClosed dependent_set_memberEquality_alt addEquality closedConclusion isectIsType intEquality productEquality productIsType independent_pairEquality inlFormation_alt pointwiseFunctionality baseApply inrFormation_alt sqequalBase hyp_replacement applyLambdaEquality

Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)].  \mforall{}[x,y:X].
\mforall{}[r:CRng].  \mforall{}[k:|r|].  \mforall{}[m,n:\mBbbN{}].
((((k)*atom(x)+atom(y)))\^{}(m)[bag-rep(n;x)]  =  if  (n  =\msubz{}  m)  then  k  \muparrow{}r  m  else  0  fi  )
supposing  \mneg{}(x  =  y)
supposing  valueall-type(X)

Date html generated: 2019_10_16-AM-11_34_54
Last ObjectModification: 2018_11_26-PM-03_09_25

Theory : power!series

Home Index