Nuprl Lemma : bag-val-append
∀[T:Type]. ∀[+:T ⟶ T ⟶ T]. ∀[zero:T].
(Comm(T;+)
⇒ Assoc(T;+)
⇒ Ident(T;+;zero)
⇒ (∀[as,bs:bag(T)]. ((bag-val(zero;+) (as + bs)) = ((bag-val(zero;+) as) + (bag-val(zero;+) bs)) ∈ T)))
Proof
Definitions occuring in Statement :
bag-val: bag-val(zero;+),
bag-append: as + bs,
bag: bag(T),
comm: Comm(T;op),
assoc: Assoc(T;op),
uall: ∀[x:A]. B[x],
infix_ap: x f y,
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T,
ident: Ident(T;op;id)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
bag: bag(T),
quotient: x,y:A//B[x; y],
and: P ∧ Q,
all: ∀x:A. B[x],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
bag-val: bag-val(zero;+),
bag-append: as + bs,
subtype_rel: A ⊆r B,
top: Top,
prop: ℙ,
infix_ap: x f y,
so_lambda: λ2x.t[x],
so_apply: x[s],
ident: Ident(T;op;id),
squash: ↓T,
true: True,
assoc: Assoc(T;op),
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
list_wf,
quotient-member-eq,
permutation_wf,
permutation-equiv,
list_accum_append,
subtype_rel_list,
top_wf,
equal_wf,
bag-val_wf,
bag-append_wf,
equal-wf-base,
bag_wf,
ident_wf,
assoc_wf,
comm_wf,
list_accum_wf,
and_wf,
list_induction,
all_wf,
list_accum_nil_lemma,
list_accum_cons_lemma,
squash_wf,
true_wf,
infix_ap_wf,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
sqequalHypSubstitution,
pointwiseFunctionalityForEquality,
because_Cache,
sqequalRule,
pertypeElimination,
productElimination,
thin,
equalityTransitivity,
hypothesis,
equalitySymmetry,
extract_by_obid,
isectElimination,
cumulativity,
hypothesisEquality,
rename,
lambdaEquality,
independent_isectElimination,
dependent_functionElimination,
independent_functionElimination,
applyEquality,
isect_memberEquality,
voidElimination,
voidEquality,
hyp_replacement,
applyLambdaEquality,
functionExtensionality,
productEquality,
axiomEquality,
functionEquality,
universeEquality,
dependent_set_memberEquality,
independent_pairFormation,
setElimination,
imageElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed
Latex:
\mforall{}[T:Type]. \mforall{}[+:T {}\mrightarrow{} T {}\mrightarrow{} T]. \mforall{}[zero:T].
(Comm(T;+)
{}\mRightarrow{} Assoc(T;+)
{}\mRightarrow{} Ident(T;+;zero)
{}\mRightarrow{} (\mforall{}[as,bs:bag(T)].
((bag-val(zero;+) (as + bs)) = ((bag-val(zero;+) as) + (bag-val(zero;+) bs)))))
Date html generated:
2017_10_01-AM-08_46_21
Last ObjectModification:
2017_07_26-PM-04_31_14
Theory : bags
Home
Index