### Nuprl Lemma : mset_mem_diff

`∀s:DSet. ∀as:FiniteSet{s}. ∀bs:MSet{s}. ∀c:|s|.  c ∈b as - bs = (c ∈b as) ∧b (¬b(c ∈b bs))`

Proof

Definitions occuring in Statement :  mset_diff: `a - b` mset_mem: mset_mem finite_set: `FiniteSet{s}` mset: `MSet{s}` band: `p ∧b q` bnot: `¬bb` bool: `𝔹` all: `∀x:A. B[x]` equal: `s = t ∈ T` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` dset: `DSet` mk_mset: `mk_mset(as)` mset_diff: `a - b` mset_mem: mset_mem so_lambda: `λ2x.t[x]` dislist: `DisList{s}` so_apply: `x[s]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` finite_set: `FiniteSet{s}` prop: `ℙ` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` uimplies: `b supposing a` bfalse: `ff`
Lemmas referenced :  set_car_wf list_wf dislist_wf all_mset_elim all_wf equal_wf bool_wf mset_mem_wf mset_diff_wf mk_mset_wf band_wf bnot_wf mset_wf sq_stable__all sq_stable__equal all_fset_elim finite_set_wf mem_wf diff_wf eqtt_to_assert dset_wf mem_diff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality dependent_functionElimination addLevel sqequalRule allFunctionality lambdaEquality because_Cache independent_functionElimination productElimination levelHypothesis allLevelFunctionality unionElimination equalityElimination independent_isectElimination equalityTransitivity equalitySymmetry

Latex:
\mforall{}s:DSet.  \mforall{}as:FiniteSet\{s\}.  \mforall{}bs:MSet\{s\}.  \mforall{}c:|s|.    c  \mmember{}\msubb{}  as  -  bs  =  (c  \mmember{}\msubb{}  as)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(c  \mmember{}\msubb{}  bs))

Date html generated: 2017_10_01-AM-10_00_09
Last ObjectModification: 2017_03_03-PM-01_01_42

Theory : mset

Home Index