Nuprl Lemma : bag-member-parts

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


Proof




Definitions occuring in Statement :  bag-parts: bag-parts(eq;bs) bag-member: x ↓∈ bs bag-union: bag-union(bbs) empty-bag: {} bag: bag(T) l_all: (∀x∈L.P[x]) listp: List+ deq: EqDecider(T) valueall-type: valueall-type(T) uiff: uiff(P;Q) uimplies: supposing a uall: [x:A]. B[x] not: ¬A and: P ∧ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top and: P ∧ Q prop: guard: {T} uiff: uiff(P;Q) l_all: (∀x∈L.P[x]) listp: List+ int_seg: {i..j-} lelt: i ≤ j < k bag-member: x ↓∈ bs squash: T subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] decidable: Dec(P) or: P ∨ Q sq_type: SQType(T) less_than: a < b bag-parts: bag-parts(eq;bs) callbyvalueall: callbyvalueall has-value: (a)↓ has-valueall: has-valueall(a) pi1: fst(t) pi2: snd(t) cand: c∧ B bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b iff: ⇐⇒ Q rev_implies:  Q bag-union: bag-union(bbs) concat: concat(ll) empty-bag: {} bag-append: as bs true: True cons-bag: x.b le: A ≤ B less_than': less_than'(a;b) length: ||as|| list_ind: list_ind nil: [] cons: [a b] rev_uimplies: rev_uimplies(P;Q) nat_plus: +
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma 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 less_than_wf equal-wf-T-base bag_wf select_wf int_seg_properties length_wf int_seg_wf bag-member_wf listp_wf bag-parts_wf equal_wf bag-union_wf subtype_rel_set list_wf list-subtype-bag l_all_wf2 not_wf l_member_wf le_wf bag-size_wf nat_wf decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma decidable__equal_int subtype_base_sq set_subtype_base lelt_wf int_subtype_base intformeq_wf int_formula_prop_eq_lemma decidable__lt subtype_rel_self itermAdd_wf int_term_value_add_lemma deq_wf valueall-type_wf valueall-type-has-valueall bag-valueall-type product-valueall-type bag-partitions_wf evalall-reduce squash_wf exists_wf bag-null_wf bool_wf eqtt_to_assert assert-bag-null empty-bag_wf eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot not_functionality_wrt_uiff assert_wf single-bag_wf cons_wf_listp nil_wf set-valueall-type list-valueall-type bag-map_wf bag-combine_wf pi1_wf_top pi2_wf iff_transitivity iff_weakening_uiff bag-member-combine exists-pair bag-member-partitions bool_cases uiff_transitivity bnot_wf assert_of_bnot bag-member-empty-iff bag-member-single reduce_cons_lemma reduce_nil_lemma true_wf bag-append_wf iff_weakening_equal bag-member-map bag-union-cons bag-size-append bag-size-zero add-is-int-iff false_wf l_all_iff member_singleton l_all_cons cons_wf and_wf listp_properties list-cases product_subtype_list bag-append-is-empty length_of_nil_lemma length_of_cons_lemma add_nat_plus length_wf_nat nat_plus_wf nat_plus_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut thin lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation productElimination independent_pairEquality axiomEquality cumulativity because_Cache baseClosed equalityTransitivity equalitySymmetry imageElimination imageMemberEquality productEquality applyEquality setEquality unionElimination instantiate applyLambdaEquality dependent_set_memberEquality hypothesis_subsumption addEquality universeIsType universeEquality callbyvalueReduce equalityElimination promote_hyp productIsType hyp_replacement pointwiseFunctionality baseApply closedConclusion

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



Date html generated: 2019_10_16-AM-11_32_10
Last ObjectModification: 2018_09_26-PM-11_46_08

Theory : bags_2


Home Index