### Nuprl Lemma : bag-member-parts'

`∀[T:Type]`
`  ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)]. ∀[L:bag(T) List+].`
`    uiff(L ↓∈ bag-parts'(eq;bs;x);(¬x ↓∈ hd(L)) ∧ (∀x∈tl(L).¬(x = {} ∈ bag(T))) ∧ (bag-union(L) = bs ∈ bag(T))) `
`  supposing valueall-type(T)`

Proof

Definitions occuring in Statement :  bag-parts': `bag-parts'(eq;bs;x)` bag-member: `x ↓∈ bs` bag-union: `bag-union(bbs)` empty-bag: `{}` bag: `bag(T)` l_all: `(∀x∈L.P[x])` listp: `A List+` hd: `hd(l)` tl: `tl(l)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uiff: `uiff(P;Q)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bag-parts': `bag-parts'(eq;bs;x)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` listp: `A List+` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` less_than: `a < b` squash: `↓T` bag-member: `x ↓∈ bs` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` ge: `i ≥ j ` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` cons: `[a / b]` cand: `A c∧ B` bag-union: `bag-union(bbs)` concat: `concat(ll)` reduce: `reduce(f;k;as)` list_ind: list_ind append: `as @ bs` empty-bag: `{}` nil: `[]` length: `||as||` bag-append: `as + bs` nat: `ℕ` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` sq_or: `a ↓∨ b` sq_stable: `SqStable(P)` subtract: `n - m` cons-bag: `x.b` rev_uimplies: `rev_uimplies(P;Q)` tl: `tl(l)` pi2: `snd(t)`
Lemmas referenced :  bag-null_wf bool_wf eqtt_to_assert assert-bag-null eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal-wf-T-base bag_wf bag-member_wf hd_wf listp_properties select_wf int_seg_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 decidable__lt length_wf tl_wf intformless_wf int_formula_prop_less_lemma int_seg_wf listp_wf bag-parts'_wf not_wf l_all_wf2 l_member_wf bag-union_wf subtype_rel_set list_wf less_than_wf list-subtype-bag deq_wf valueall-type_wf equal-empty-bag iff_weakening_uiff single-bag_wf cons_wf_listp nil_wf bag-member-single uiff_wf list-cases length_of_nil_lemma product_subtype_list length_of_cons_lemma reduce_hd_cons_lemma ge_wf squash_wf true_wf iff_weakening_equal reduce_tl_cons_lemma bag-member-empty-iff l_all_nil empty-bag_wf reduce_cons_lemma reduce_nil_lemma bag-append-empty bag-subtype-list bag-size_wf bag-size-append subtype_rel_self bag_size_empty_lemma nat_wf non_neg_length itermAdd_wf int_term_value_add_lemma length_wf_nat nat_properties intformeq_wf int_formula_prop_eq_lemma bag-size-zero l_all_cons valueall-type-has-valueall bag-valueall-type set-valueall-type list-valueall-type bag-parts_wf evalall-reduce bag-member-append bag-map_wf bag-filter_wf eq_int_wf bag-count_wf subtype_rel_bag assert_wf bag-append_wf sq_or_wf exists_wf or_wf bag-member-map l_all_iff all_wf sq_stable__and sq_stable__not sq_stable__all sq_stable__equal bag-member-parts bag-member-filter assert_of_eq_int bag-member-count reduce_tl_nil_lemma decidable__assert null_wf3 subtype_rel_list top_wf assert_of_null false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel cons_wf bag_union_cons_lemma empty_bag_append_lemma bag-count-is-zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin cumulativity hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination isectElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination because_Cache sqequalRule dependent_pairFormation promote_hyp instantiate independent_functionElimination voidElimination baseClosed independent_pairEquality isect_memberEquality lambdaEquality setElimination rename natural_numberEquality int_eqEquality intEquality voidEquality independent_pairFormation computeAll imageElimination axiomEquality imageMemberEquality productEquality setEquality applyEquality universeEquality addLevel hypothesis_subsumption applyLambdaEquality dependent_set_memberEquality hyp_replacement addEquality callbyvalueReduce orFunctionality functionEquality inlFormation minusEquality inrFormation

Latex:
\mforall{}[T:Type]
\mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].  \mforall{}[L:bag(T)  List\msupplus{}].
uiff(L  \mdownarrow{}\mmember{}  bag-parts'(eq;bs;x);(\mneg{}x  \mdownarrow{}\mmember{}  hd(L))  \mwedge{}  (\mforall{}x\mmember{}tl(L).\mneg{}(x  =  \{\}))  \mwedge{}  (bag-union(L)  =  bs))
supposing  valueall-type(T)

Date html generated: 2018_05_21-PM-09_51_27
Last ObjectModification: 2017_07_26-PM-06_31_30

Theory : bags_2

Home Index