### Nuprl Lemma : bag-union-is-single

`∀[T:Type]. ∀[x:T].`
`  ∀bbs:bag(bag(T))`
`    uiff(bag-union(bbs) = {x} ∈ bag(T);↓∃bbs':bag(bag(T))`
`                                         ((bbs = {x}.bbs' ∈ bag(bag(T))) ∧ (bag-union(bbs') = {} ∈ bag(T))))`

Proof

Definitions occuring in Statement :  bag-union: `bag-union(bbs)` cons-bag: `x.b` single-bag: `{x}` empty-bag: `{}` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` squash: `↓T` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` squash: `↓T` prop: `ℙ` exists: `∃x:A. B[x]` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` or: `P ∨ Q` cons: `[a / b]` le: `A ≤ B` less_than': `less_than'(a;b)` colength: `colength(L)` nil: `[]` it: `⋅` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` less_than: `a < b` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` decidable: `Dec(P)` subtype_rel: `A ⊆r B` single-bag: `{x}` bag-union: `bag-union(bbs)` concat: `concat(ll)` bag: `bag(T)` quotient: `x,y:A//B[x; y]` cand: `A c∧ B` true: `True` bag-append: `as + bs` cons-bag: `x.b` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` respects-equality: `respects-equality(S;T)` reduce: `reduce(f;k;as)` list_ind: list_ind append: `as @ bs` empty-bag: `{}` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  bag_wf bag-union_wf single-bag_wf squash_wf equal_wf cons-bag_wf equal-wf-T-base istype-universe bag_to_squash_list nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than list-cases product_subtype_list colength-cons-not-zero colength_wf_list istype-false istype-le list_wf subtract-1-ge-0 subtype_base_sq intformeq_wf int_formula_prop_eq_lemma set_subtype_base int_subtype_base spread_cons_lemma decidable__equal_int subtract_wf intformnot_wf itermSubtract_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_subtract_lemma int_term_value_add_lemma decidable__le le_wf cons_wf list-subtype-bag istype-nat reduce_nil_lemma permutation-length length_of_nil_lemma length_of_cons_lemma permutation_wf concat-cons2 bag-append-is-single-iff true_wf subtype_rel_self iff_weakening_equal subtype-respects-equality list_ind_cons_lemma list_ind_nil_lemma bag-append-assoc-comm bag-append-empty bag-subtype-list bag-append_wf nil_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt independent_pairFormation hypothesis sqequalHypSubstitution imageElimination sqequalRule imageMemberEquality hypothesisEquality thin baseClosed equalityIstype universeIsType extract_by_obid isectElimination dependent_functionElimination productEquality lambdaEquality_alt productElimination independent_pairEquality isect_memberEquality_alt isectIsTypeImplies inhabitedIsType axiomEquality functionIsTypeImplies instantiate universeEquality promote_hyp equalitySymmetry hyp_replacement applyLambdaEquality equalityTransitivity rename setElimination intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality voidElimination unionElimination sqequalBase hypothesis_subsumption because_Cache dependent_set_memberEquality_alt baseApply closedConclusion applyEquality intEquality pertypeElimination cumulativity productIsType

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].
\mforall{}bbs:bag(bag(T))
uiff(bag-union(bbs)  =  \{x\};\mdownarrow{}\mexists{}bbs':bag(bag(T)).  ((bbs  =  \{x\}.bbs')  \mwedge{}  (bag-union(bbs')  =  \{\})))

Date html generated: 2019_10_15-AM-11_00_22
Last ObjectModification: 2018_11_30-AM-09_57_39

Theory : bags

Home Index