### Nuprl Lemma : fps-moebius-eq

`∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng].  (fps-moebius(eq;r) = (1÷λb.1) ∈ PowerSeries(X;r)) supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-moebius: `fps-moebius(eq;r)` fps-div: `(f÷g)` fps-one: `1` power-series: `PowerSeries(X;r)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` lambda: `λx.A[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng` rng_one: `1`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` fps-div: `(f÷g)` fps-moebius: `fps-moebius(eq;r)` power-series: `PowerSeries(X;r)` has-value: `(a)↓` all: `∀x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` guard: `{T}` le: `A ≤ B` subtype_rel: `A ⊆r B` fps-div-coeff: `fps-div-coeff(eq;r;f;g;x;b)` less_than': `less_than'(a;b)` decidable: `Dec(P)` or: `P ∨ Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uiff: `uiff(P;Q)` crng: `CRng` rng: `Rng` pi1: `fst(t)` pi2: `snd(t)` cand: `A c∧ B` infix_ap: `x f y` true: `True` fps-one: `1` fps-coeff: `f[b]` squash: `↓T` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` bag-filter: `[x∈b|p[x]]` filter: `filter(P;l)` reduce: `reduce(f;k;as)` list_ind: list_ind bag-partitions: `bag-partitions(eq;bs)` callbyvalueall: callbyvalueall evalall: `evalall(t)` bag-splits: `bag-splits(b)` 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` insert: `insert(a;L)` eval_list: `eval_list(t)` deq-member: `x ∈b L` bag-null: `bag-null(bs)` null: `null(as)` assoc: `Assoc(T;op)` comm: `Comm(T;op)` integ_dom: `IntegDom{i}` int_ring: `ℤ-rng` rng_car: `|r|` rng_zero: `0` rng_plus: `+r` less_than: `a < b`
Lemmas referenced :  value-type-has-value int-value-type bag-moebius_wf bag_wf crng_wf deq_wf valueall-type_wf 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 less_than_wf bag-size_wf subtract-1-ge-0 nat_wf add_nat_wf istype-false le_wf decidable__le add-is-int-iff set_subtype_base int_subtype_base intformnot_wf itermAdd_wf intformeq_wf int_formula_prop_not_lemma int_term_value_add_lemma int_formula_prop_eq_lemma false_wf decidable__lt rng_car_wf rng_one_wf fps-coeff_wf fps-one_wf rng_minus_wf bag-summation_wf assert_wf bnot_wf bag-null_wf rng_plus_wf rng_zero_wf pi1_wf_top infix_ap_wf rng_times_wf fps-div-coeff_wf bag-filter_wf bag-partitions_wf crng_all_properties rng_plus_comm2 int-to-ring_wf equal_wf rng_times_over_plus rng_times_over_minus rng_times_one rng_plus_comm iff_weakening_equal bag-moebius-property eqtt_to_assert assert-bag-null eqff_to_assert bool_subtype_base bool_cases_sqequal subtype_base_sq bool_wf assert-bnot iff_weakening_uiff equal-wf-T-base ifthenelse_wf empty-bag_wf int-to-ring-one bag-summation-empty squash_wf true_wf rng_minus_zero subtype_rel_self rng_plus_zero decidable__equal_int subtype_rel_product top_wf pi2_wf int-to-ring-minus assoc_wf comm_wf bag-summation-hom int_ring_wf int-to-ring-hom bag-settype subtract_wf bag-member_wf bag-member-filter bag-member-partitions bag-size-append itermSubtract_wf int_term_value_subtract_lemma null-bag-size eq_int_wf not_wf equal-wf-base iff_transitivity assert_of_bnot assert_of_eq_int set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaEquality_alt sqequalRule callbyvalueReduce extract_by_obid sqequalHypSubstitution isectElimination thin intEquality independent_isectElimination hypothesis hypothesisEquality universeIsType isect_memberEquality_alt axiomEquality isectIsTypeImplies inhabitedIsType universeEquality lambdaFormation_alt setElimination rename intWeakElimination natural_numberEquality approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality dependent_functionElimination voidElimination independent_pairFormation functionIsTypeImplies equalityTransitivity equalitySymmetry applyLambdaEquality productElimination applyEquality because_Cache dependent_set_memberEquality_alt addEquality unionElimination pointwiseFunctionality promote_hyp baseClosed equalityIsType1 setEquality productEquality independent_pairEquality productIsType setIsType imageElimination imageMemberEquality equalityElimination equalityIsType3 baseApply closedConclusion instantiate cumulativity equalityIsType4 hyp_replacement minusEquality functionIsType

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].    (fps-moebius(eq;r)  =  (1\mdiv{}\mlambda{}b.1))  supposing  valueall-type(X)

Date html generated: 2019_10_16-AM-11_34_39
Last ObjectModification: 2018_10_16-AM-09_34_31

Theory : power!series

Home Index