### Nuprl Lemma : count_diff

`∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  ((c #∈ (as - bs)) = ((c #∈ as) -- (c #∈ bs)) ∈ ℤ)`

Proof

Definitions occuring in Statement :  diff: `as - bs` count: `a #∈ as` ndiff: `a -- b` list: `T List` all: `∀x:A. B[x]` int: `ℤ` equal: `s = t ∈ T` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` dset: `DSet` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` prop: `ℙ` top: `Top` nat: `ℕ` and: `P ∧ Q` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` infix_ap: `x f y`
Lemmas referenced :  list_induction set_car_wf all_wf list_wf equal_wf count_wf diff_wf ndiff_wf dset_wf diff_nil_lemma count_nil_lemma count_bounds le_wf squash_wf true_wf ndiff_id_r iff_weakening_equal diff_cons_lemma count_cons_lemma remove1_wf b2i_wf infix_ap_wf bool_wf set_eq_wf ndiff_ndiff count_remove1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination setElimination rename because_Cache hypothesis sqequalRule lambdaEquality intEquality dependent_functionElimination hypothesisEquality independent_functionElimination isect_memberEquality voidElimination voidEquality dependent_set_memberEquality productElimination natural_numberEquality applyEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed independent_isectElimination addEquality

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:|s|  List.  \mforall{}c:|s|.    ((c  \#\mmember{}  (as  -  bs))  =  ((c  \#\mmember{}  as)  --  (c  \#\mmember{}  bs)))

Date html generated: 2017_10_01-AM-09_56_39
Last ObjectModification: 2017_03_03-PM-00_57_44

Theory : list_2

Home Index