Nuprl Lemma : bag-append-equal-bag-rep
∀[T:Type]. ∀[x:T]. ∀[n:ℕ]. ∀[a,b:bag(T)].
uiff((a + b) = bag-rep(n;x) ∈ bag(T);(n = (#(a) + #(b)) ∈ ℤ)
∧ (a = bag-rep(#(a);x) ∈ bag(T))
∧ (b = bag-rep(#(b);x) ∈ bag(T)))
Proof
Definitions occuring in Statement :
bag-rep: bag-rep(n;x),
bag-size: #(bs),
bag-append: as + bs,
bag: bag(T),
nat: ℕ,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
add: n + m,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
nat: ℕ,
subtype_rel: A ⊆r B,
prop: ℙ,
uimplies: b supposing a,
and: P ∧ Q,
uiff: uiff(P;Q),
member: t ∈ T,
uall: ∀[x:A]. B[x],
exists: ∃x:A. B[x],
sub-bag: sub-bag(T;as;bs),
all: ∀x:A. B[x],
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
guard: {T},
true: True,
squash: ↓T,
sq_type: SQType(T),
top: Top
Lemmas referenced :
nat_wf,
bag-size_wf,
list-subtype-bag,
bag-rep_wf,
bag-append_wf,
bag_wf,
equal_wf,
bag-size-rep,
bag-size-append,
sub-bag-of-bag-rep,
bag-append-comm,
iff_weakening_equal,
true_wf,
squash_wf,
int_subtype_base,
subtype_base_sq,
bag-rep-add
Rules used in proof :
universeEquality,
equalitySymmetry,
equalityTransitivity,
isect_memberEquality,
addEquality,
rename,
setElimination,
intEquality,
productEquality,
lambdaEquality,
independent_isectElimination,
because_Cache,
applyEquality,
hypothesisEquality,
cumulativity,
isectElimination,
extract_by_obid,
axiomEquality,
independent_pairEquality,
thin,
productElimination,
sqequalHypSubstitution,
sqequalRule,
hypothesis,
independent_pairFormation,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
applyLambdaEquality,
Error :memTop,
dependent_pairFormation,
dependent_functionElimination,
independent_functionElimination,
baseClosed,
imageMemberEquality,
natural_numberEquality,
imageElimination,
hyp_replacement,
instantiate,
voidEquality,
voidElimination
Latex:
\mforall{}[T:Type]. \mforall{}[x:T]. \mforall{}[n:\mBbbN{}]. \mforall{}[a,b:bag(T)].
uiff((a + b) = bag-rep(n;x);(n = (\#(a) + \#(b))) \mwedge{} (a = bag-rep(\#(a);x)) \mwedge{} (b = bag-rep(\#(b);x)))
Date html generated:
2020_05_20-AM-08_02_03
Last ObjectModification:
2020_01_07-PM-02_18_08
Theory : bags
Home
Index