Nuprl Lemma : member-sub-bags
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs,b:bag(T)]. uiff(b ↓∈ sub-bags(eq;bs);↓sub-bag(T;b;bs)) supposing valueall-type(T)
Proof
Definitions occuring in Statement :
sub-bags: sub-bags(eq;bs),
bag-member: x ↓∈ bs,
sub-bag: sub-bag(T;as;bs),
bag: bag(T),
deq: EqDecider(T),
valueall-type: valueall-type(T),
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
squash: ↓T,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
uiff: uiff(P;Q),
and: P ∧ Q,
squash: ↓T,
prop: ℙ,
bag-member: x ↓∈ bs,
sub-bags: sub-bags(eq;bs),
all: ∀x:A. B[x],
top: Top,
exists: ∃x:A. B[x],
pi1: fst(t),
sub-bag: sub-bag(T;as;bs),
sq_stable: SqStable(P),
implies: P ⇒ Q,
rev_uimplies: rev_uimplies(P;Q),
cand: A c∧ B
Lemmas referenced :
bag-member_wf,
bag_wf,
sub-bags_wf,
squash_wf,
sub-bag_wf,
deq_wf,
valueall-type_wf,
bag-member-map,
pi1_wf_top,
bag-partitions_wf,
bag-member-partitions,
equal_wf,
bag-append_wf,
sq_stable__bag-member
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
independent_pairFormation,
hypothesis,
sqequalHypSubstitution,
imageElimination,
sqequalRule,
imageMemberEquality,
hypothesisEquality,
thin,
baseClosed,
extract_by_obid,
isectElimination,
cumulativity,
independent_isectElimination,
productElimination,
independent_pairEquality,
isect_memberEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry,
universeEquality,
productEquality,
dependent_functionElimination,
lambdaEquality,
voidElimination,
voidEquality,
dependent_pairFormation,
hyp_replacement,
applyLambdaEquality,
independent_functionElimination
Latex:
\mforall{}[T:Type]
\mforall{}[eq:EqDecider(T)]. \mforall{}[bs,b:bag(T)]. uiff(b \mdownarrow{}\mmember{} sub-bags(eq;bs);\mdownarrow{}sub-bag(T;b;bs))
supposing valueall-type(T)
Date html generated:
2018_05_21-PM-09_52_31
Last ObjectModification:
2017_07_26-PM-06_31_52
Theory : bags_2
Home
Index