### Nuprl Lemma : fps-rng_wf

`∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[r:CRng].  (fps-rng(r) ∈ CRng) supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-rng: `fps-rng(r)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` crng: `CRng` rng: `Rng` prop: `ℙ` fps-rng: `fps-rng(r)` rng_sig: `RngSig` ring_p: `IsRing(T;plus;zero;neg;times;one)` and: `P ∧ Q` group_p: `IsGroup(T;op;id;inv)` cand: `A c∧ B` rng_car: `|r|` pi1: `fst(t)` rng_plus: `+r` pi2: `snd(t)` rng_zero: `0` rng_minus: `-r` infix_ap: `x f y` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` rng_times: `*` rng_one: `1` monoid_p: `IsMonoid(T;op;id)` inverse: `Inverse(T;op;id;inv)` bilinear: `BiLinear(T;pl;tm)` assoc: `Assoc(T;op)` fps-coeff: `f[b]` power-series: `PowerSeries(X;r)` fps-add: `(f+g)` fps-zero: `0` ident: `Ident(T;op;id)` fps-neg: `-(f)` comm: `Comm(T;op)` fps-one: `1` fps-mul: `(f*g)` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` so_apply: `x[s]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` top: `Top` bag-null: `bag-null(bs)` empty-bag: `{}`
Lemmas referenced :  comm_wf rng_car_wf rng_times_wf crng_wf deq_wf valueall-type_wf ring_p_wf rng_plus_wf rng_zero_wf rng_minus_wf rng_one_wf bool_wf unit_wf2 fps-one_wf fps-mul_wf fps-neg_wf fps-zero_wf fps-add_wf btrue_wf power-series_wf crng_properties rng_properties equal_wf squash_wf true_wf istype-universe fps-add-comm subtype_rel_self iff_weakening_equal fps-add-assoc bag_wf fps-mul-assoc rng_plus_comm fps-mul-comm bag-split bag-null_wf bag-partitions_wf bag-summation-append eqtt_to_assert assert-bag-null eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot iff_weakening_uiff assert_wf equal-wf-T-base bag-filter_wf bnot_wf bag-summation_wf crng_all_properties infix_ap_wf bag-append-ident empty-bag_wf bag-partitions-with-one-given subtype_rel_bag iff_wf assert-bag-eq bag-eq_wf pi2_wf iff_imp_equal_bool bag-summation-single pi1_wf_top subtype_rel_product top_wf istype-void null_nil_lemma bag-summation-is-zero null_wf3 bag-subtype-list assert_of_null assert_elim bfalse_wf btrue_neq_bfalse subtype_rel_list bag-member_wf rng_plus_zero fps-coeff_wf rng_times_zero assoc_wf bag-summation-add
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut dependent_set_memberEquality_alt universeIsType extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis because_Cache sqequalRule axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality_alt universeEquality productEquality unionEquality functionEquality inlEquality independent_isectElimination lambdaEquality dependent_pairEquality productElimination independent_pairFormation applyEquality lambdaEquality_alt imageElimination inhabitedIsType natural_numberEquality imageMemberEquality baseClosed instantiate independent_functionElimination independent_pairEquality isect_memberEquality isect_memberFormation functionExtensionality functionExtensionality_alt dependent_functionElimination productIsType lambdaFormation_alt unionElimination equalityElimination dependent_pairFormation_alt equalityIsType1 promote_hyp cumulativity voidElimination equalityIsType3 hyp_replacement applyLambdaEquality setEquality setIsType impliesFunctionality addLevel lambdaFormation dependent_pairFormation voidEquality

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].    (fps-rng(r)  \mmember{}  CRng)  supposing  valueall-type(X)

Date html generated: 2019_10_16-AM-11_34_24
Last ObjectModification: 2018_10_11-PM-02_48_30

Theory : power!series

Home Index