Nuprl Lemma : single-valued-bag-is-rep
∀[A:Type]. ∀[as:bag(A)]. ∀a:A. (a ↓∈ as ⇒ (as = bag-rep(#(as);a) ∈ bag(A))) supposing single-valued-bag(as;A)
Proof
Definitions occuring in Statement :
single-valued-bag: single-valued-bag(b;T),
bag-member: x ↓∈ bs,
bag-rep: bag-rep(n;x),
bag-size: #(bs),
bag: bag(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
squash: ↓T,
exists: ∃x:A. B[x],
prop: ℙ,
bag-size: #(bs),
subtype_rel: A ⊆r B,
top: Top,
nat: ℕ,
ge: i ≥ j ,
decidable: Dec(P),
or: P ∨ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
false: False,
not: ¬A,
and: P ∧ Q,
int_seg: {i..j-},
lelt: i ≤ j < k,
le: A ≤ B,
true: True,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
single-valued-list: single-valued-list(L;T)
Lemmas referenced :
bag_to_squash_list,
bag-member_wf,
single-valued-bag_wf,
bag-member-sq-list-member,
single-valued-bag-list,
list_extensionality,
bag-rep_wf,
length_wf_nat,
bag-size-rep,
bag-size_wf,
list-subtype-bag,
nat_wf,
equal_wf,
squash_wf,
true_wf,
select_wf,
nat_properties,
decidable__le,
satisfiable-full-omega-tt,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
select-bag-rep,
lelt_wf,
length_wf,
iff_weakening_equal,
select_member,
less_than_wf,
bag_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
hypothesisEquality,
imageElimination,
productElimination,
promote_hyp,
hypothesis,
equalitySymmetry,
hyp_replacement,
applyLambdaEquality,
cumulativity,
rename,
dependent_functionElimination,
independent_isectElimination,
sqequalRule,
applyEquality,
lambdaEquality,
isect_memberEquality,
voidElimination,
voidEquality,
setElimination,
equalityTransitivity,
natural_numberEquality,
unionElimination,
dependent_pairFormation,
int_eqEquality,
intEquality,
independent_pairFormation,
computeAll,
dependent_set_memberEquality,
imageMemberEquality,
baseClosed,
universeEquality,
independent_functionElimination,
axiomEquality
Latex:
\mforall{}[A:Type]. \mforall{}[as:bag(A)].
\mforall{}a:A. (a \mdownarrow{}\mmember{} as {}\mRightarrow{} (as = bag-rep(\#(as);a))) supposing single-valued-bag(as;A)
Date html generated:
2017_10_01-AM-08_55_35
Last ObjectModification:
2017_07_26-PM-04_37_44
Theory : bags
Home
Index