### Nuprl Lemma : detach_msubset

`∀s:DSet. ∀a,b:MSet{s}.  ((↑(a ⊆b b)) `` (b = ((b - a) + a) ∈ MSet{s}))`

Proof

Definitions occuring in Statement :  bsubmset: `a ⊆b b` mset_diff: `a - b` mset_sum: `a + b` mset: `MSet{s}` assert: `↑b` all: `∀x:A. B[x]` implies: `P `` Q` equal: `s = t ∈ T` dset: `DSet`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` squash: `↓T` subtype_rel: `A ⊆r B` nat: `ℕ` true: `True` uimplies: `b supposing a` guard: `{T}` dset: `DSet` le: `A ≤ B` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` bfalse: `ff`
Lemmas referenced :  assert_wf bsubmset_wf mset_wf dset_wf eq_mset_iff_eq_counts mset_sum_wf mset_diff_wf equal_wf squash_wf true_wf mset_count_wf nat_wf mset_count_sum add_functionality_wrt_eq ndiff_wf mset_count_diff iff_weakening_equal set_car_wf ndiff_add_eq_imax count_bsubmset imax_unfold le_int_wf bool_wf uiff_transitivity equal-wf-T-base le_wf eqtt_to_assert assert_of_le_int decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf lt_int_wf less_than_wf bnot_wf eqff_to_assert assert_functionality_wrt_uiff bnot_of_le_int assert_of_lt_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality productElimination independent_functionElimination applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality intEquality setElimination rename sqequalRule because_Cache natural_numberEquality imageMemberEquality baseClosed independent_isectElimination unionElimination equalityElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll

Latex:
\mforall{}s:DSet.  \mforall{}a,b:MSet\{s\}.    ((\muparrow{}(a  \msubseteq{}\msubb{}  b))  {}\mRightarrow{}  (b  =  ((b  -  a)  +  a)))

Date html generated: 2017_10_01-AM-10_00_24
Last ObjectModification: 2017_03_03-PM-01_01_49

Theory : mset

Home Index