### Nuprl Lemma : bag-member-union

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

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-union: `bag-union(bbs)` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` squash: `↓T` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` squash: `↓T` prop: `ℙ` exists: `∃x:A. B[x]` and: `P ∧ Q` implies: `P `` Q` sq_stable: `SqStable(P)` uiff: `uiff(P;Q)` uimplies: `b supposing a` bag-member: `x ↓∈ bs` all: `∀x:A. B[x]` nat: `ℕ` 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` empty-bag: `{}` concat: `concat(ll)` bag-union: `bag-union(bbs)` bag-append: `as + bs` sq_or: `a ↓∨ b` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` cand: `A c∧ B` cons-bag: `x.b` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  bag_to_squash_list bag_wf sq_stable__uiff bag-member_wf bag-union_wf squash_wf sq_stable__bag-member sq_stable__squash uiff_wf istype-universe 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-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 istype-nat exists_wf empty-bag_wf bag-member-empty reduce_nil_lemma reduce_cons_lemma sq_or_wf list-subtype-bag cons_wf bag-member-append bag-append_wf bag-member-cons
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis imageElimination sqequalRule productEquality independent_functionElimination productElimination promote_hyp rename hyp_replacement equalitySymmetry applyLambdaEquality imageMemberEquality baseClosed independent_pairEquality isect_memberEquality_alt isectIsTypeImplies inhabitedIsType universeIsType instantiate universeEquality lambdaFormation_alt setElimination intWeakElimination natural_numberEquality independent_isectElimination approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination voidElimination independent_pairFormation functionIsTypeImplies unionElimination hypothesis_subsumption equalityIstype because_Cache dependent_set_memberEquality_alt equalityTransitivity baseApply closedConclusion applyEquality intEquality sqequalBase lambdaEquality cumulativity isect_memberFormation voidEquality isect_memberEquality productIsType inlFormation_alt inrFormation_alt

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

Date html generated: 2019_10_15-AM-11_01_46
Last ObjectModification: 2019_06_25-PM-03_25_58

Theory : bags

Home Index