Nuprl Lemma : fps-compose-single-disjoint
∀[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[v:bag(X)].
((¬x ↓∈ v) ⇒ (∀[f:PowerSeries(X;r)]. (<v>(x:=f) = <v> ∈ PowerSeries(X;r))))
supposing valueall-type(X)
Proof
Definitions occuring in Statement :
fps-compose: g(x:=f),
fps-single: <c>,
power-series: PowerSeries(X;r),
bag-member: x ↓∈ bs,
bag: bag(T),
deq: EqDecider(T),
valueall-type: valueall-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T,
crng: CRng
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
implies: P ⇒ Q,
squash: ↓T,
exists: ∃x:A. B[x],
prop: ℙ,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
so_apply: x[s],
all: ∀x:A. B[x],
true: True,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
empty-bag: {},
uiff: uiff(P;Q),
fps-one: 1,
fps-coeff: f[b],
fps-single: <c>,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
crng: CRng,
rng: Rng,
bfalse: ff,
or: P ∨ Q,
sq_type: SQType(T),
bnot: ¬bb,
assert: ↑b,
false: False,
not: ¬A,
cons-bag: x.b,
top: Top,
fps-atom: atom(x),
rev_uimplies: rev_uimplies(P;Q),
sq_or: a ↓∨ b
Lemmas referenced :
bag_to_squash_list,
not_wf,
bag-member_wf,
list_induction,
list-subtype-bag,
equal_wf,
power-series_wf,
fps-compose_wf,
fps-single_wf,
list_wf,
nil_wf,
cons_wf,
bag_wf,
crng_wf,
deq_wf,
valueall-type_wf,
squash_wf,
true_wf,
fps-compose-one,
fps-one_wf,
iff_weakening_equal,
fps-ext,
empty-bag_wf,
bag-eq_wf,
bool_wf,
eqtt_to_assert,
assert-bag-eq,
bag-null_wf,
assert-bag-null,
rng_one_wf,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
equal-wf-T-base,
rng_zero_wf,
single-bag_wf,
fps-mul_wf,
cons-bag-as-append,
fps-mul-single,
fps-compose-mul,
fps-compose-atom-neq,
bag-member-cons
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
hypothesisEquality,
imageElimination,
productElimination,
promote_hyp,
hypothesis,
equalitySymmetry,
hyp_replacement,
applyLambdaEquality,
cumulativity,
rename,
sqequalRule,
lambdaEquality,
functionEquality,
applyEquality,
independent_isectElimination,
independent_functionElimination,
voidEquality,
voidElimination,
dependent_functionElimination,
isect_memberEquality,
axiomEquality,
equalityTransitivity,
universeEquality,
natural_numberEquality,
imageMemberEquality,
baseClosed,
unionElimination,
equalityElimination,
setElimination,
dependent_pairFormation,
instantiate,
inlFormation,
inrFormation
Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)]. \mforall{}[r:CRng]. \mforall{}[x:X]. \mforall{}[v:bag(X)].
((\mneg{}x \mdownarrow{}\mmember{} v) {}\mRightarrow{} (\mforall{}[f:PowerSeries(X;r)]. (<v>(x:=f) = <v>)))
supposing valueall-type(X)
Date html generated:
2018_05_21-PM-10_10_15
Last ObjectModification:
2017_07_26-PM-06_34_20
Theory : power!series
Home
Index