Nuprl Lemma : bag-member-append
∀[T:Type]. ∀x:T. ∀as,bs:bag(T). (x ↓∈ as + bs ⇐⇒ x ↓∈ as ↓∨ x ↓∈ bs)
Proof
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
bag-append: as + bs,
bag: bag(T),
sq_or: a ↓∨ b,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
universe: Type
Definitions unfolded in proof :
sq_or: a ↓∨ b,
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
squash: ↓T,
exists: ∃x:A. B[x],
prop: ℙ,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
bag-append: as + bs,
rev_implies: P ⇐ Q,
sq_stable: SqStable(P),
or: P ∨ Q,
bag-member: x ↓∈ bs,
bag: bag(T),
quotient: x,y:A//B[x; y],
cand: A c∧ B,
guard: {T}
Lemmas referenced :
bag_to_squash_list,
bag-member_wf,
bag-append_wf,
list-subtype-bag,
squash_wf,
or_wf,
sq_stable__bag-member,
bag_wf,
istype-universe,
member-permutation,
member_append,
l_member_wf,
append_wf,
permutation_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation_alt,
introduction,
cut,
lambdaFormation_alt,
independent_pairFormation,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
imageElimination,
productElimination,
promote_hyp,
hypothesis,
equalitySymmetry,
hyp_replacement,
applyLambdaEquality,
rename,
applyEquality,
because_Cache,
independent_isectElimination,
lambdaEquality_alt,
inhabitedIsType,
imageMemberEquality,
baseClosed,
universeIsType,
independent_functionElimination,
dependent_functionElimination,
independent_pairEquality,
functionIsTypeImplies,
universeEquality,
pertypeElimination,
equalityTransitivity,
unionElimination,
inlFormation_alt,
dependent_pairFormation_alt,
productIsType,
equalityIsType1,
inrFormation_alt
Latex:
\mforall{}[T:Type]. \mforall{}x:T. \mforall{}as,bs:bag(T). (x \mdownarrow{}\mmember{} as + bs \mLeftarrow{}{}\mRightarrow{} x \mdownarrow{}\mmember{} as \mdownarrow{}\mvee{} x \mdownarrow{}\mmember{} bs)
Date html generated:
2019_10_15-AM-11_01_13
Last ObjectModification:
2018_10_10-PM-01_06_41
Theory : bags
Home
Index