Nuprl Lemma : bag-append-eq-empty
∀[T:Type]. ∀[b1,b2:bag(T)]. uiff((b1 + b2) = {} ∈ bag(T);(b1 = {} ∈ bag(T)) ∧ (b2 = {} ∈ bag(T)))
Proof
Definitions occuring in Statement :
bag-append: as + bs,
empty-bag: {},
bag: bag(T),
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
empty-bag: {},
bag-append: as + bs,
top: Top,
guard: {T},
implies: P ⇒ Q,
prop: ℙ
Lemmas referenced :
bag-append_wf,
bag_wf,
istype-universe,
bag-subtype-list,
append_is_nil,
top_wf,
list-subtype-bag,
istype-void,
istype-top,
equal_functionality_wrt_subtype_rel2,
list_wf,
equal-empty-bag,
equal-wf-T-base,
empty_bag_append_lemma
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
independent_pairFormation,
sqequalRule,
sqequalHypSubstitution,
productElimination,
thin,
independent_pairEquality,
axiomEquality,
hypothesis,
equalityIsType3,
inhabitedIsType,
hypothesisEquality,
extract_by_obid,
isectElimination,
baseClosed,
productIsType,
because_Cache,
isect_memberEquality_alt,
isectIsTypeImplies,
universeIsType,
instantiate,
universeEquality,
applyEquality,
dependent_functionElimination,
independent_isectElimination,
promote_hyp,
lambdaEquality_alt,
voidElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
cumulativity,
applyLambdaEquality,
hyp_replacement,
voidEquality,
isect_memberEquality
Latex:
\mforall{}[T:Type]. \mforall{}[b1,b2:bag(T)]. uiff((b1 + b2) = \{\};(b1 = \{\}) \mwedge{} (b2 = \{\}))
Date html generated:
2019_10_15-AM-10_59_57
Last ObjectModification:
2018_10_16-PM-05_37_36
Theory : bags
Home
Index