Nuprl Lemma : not-list-member-not-bag-member
∀[T:Type]. ∀[L:T List]. ∀[x:T]. ((¬(x ∈ L)) ⇒ (¬x ↓∈ L))
Proof
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
l_member: (x ∈ l),
list: T List,
uall: ∀[x:A]. B[x],
not: ¬A,
implies: P ⇒ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
implies: P ⇒ Q,
prop: ℙ,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
so_apply: x[s],
not: ¬A,
false: False,
empty-bag: {},
uiff: uiff(P;Q),
and: P ∧ Q,
all: ∀x:A. B[x],
cons-bag: x.b,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
or: P ∨ Q,
sq_or: a ↓∨ b,
squash: ↓T
Lemmas referenced :
list_induction,
not_wf,
l_member_wf,
bag-member_wf,
list-subtype-bag,
list_wf,
bag-member-empty-iff,
nil_wf,
bag-member-cons,
cons_member,
or_wf,
equal_wf,
not_over_or,
cons_wf
Rules used in proof :
cut,
thin,
lemma_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
hypothesisEquality,
sqequalRule,
lambdaEquality,
functionEquality,
hypothesis,
applyEquality,
because_Cache,
independent_isectElimination,
independent_functionElimination,
lambdaFormation,
productElimination,
voidElimination,
cumulativity,
voidEquality,
rename,
addLevel,
impliesFunctionality,
dependent_functionElimination,
levelHypothesis,
promote_hyp,
imageElimination,
unionElimination,
impliesLevelFunctionality,
universeEquality,
isect_memberFormation,
introduction,
isect_memberEquality
Latex:
\mforall{}[T:Type]. \mforall{}[L:T List]. \mforall{}[x:T]. ((\mneg{}(x \mmember{} L)) {}\mRightarrow{} (\mneg{}x \mdownarrow{}\mmember{} L))
Date html generated:
2016_05_15-PM-02_40_01
Last ObjectModification:
2015_12_27-AM-09_42_17
Theory : bags
Home
Index