### Nuprl Lemma : bag-co-restrict-disjoint

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (b|¬x) = b ∈ bag(T) supposing ¬x ↓∈ b`

Proof

Definitions occuring in Statement :  bag-co-restrict: `(b|¬x)` bag-member: `x ↓∈ bs` bag: `bag(T)` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` squash: `↓T` exists: `∃x:A. B[x]` prop: `ℙ` not: `¬A` implies: `P `` Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` bag-co-restrict: `(b|¬x)` bag-filter: `[x∈b|p[x]]` deq: `EqDecider(T)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` uiff: `uiff(P;Q)` eqof: `eqof(d)` subtype_rel: `A ⊆r B` false: `False`
Lemmas referenced :  bag_to_squash_list not_wf bag-member_wf bag-member-list decidable-equal-deq l_member_wf equal_wf bag_wf bag-co-restrict_wf deq_wf filter_trivial bnot_wf l_all_iff assert_wf iff_transitivity eqof_wf iff_weakening_uiff assert_of_bnot safe-assert-deq list-subtype-bag and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality imageElimination productElimination promote_hyp hypothesis equalitySymmetry hyp_replacement applyLambdaEquality cumulativity rename lambdaFormation independent_functionElimination dependent_functionElimination sqequalRule isect_memberEquality axiomEquality equalityTransitivity universeEquality lambdaEquality applyEquality setElimination independent_isectElimination setEquality addLevel independent_pairFormation impliesFunctionality dependent_set_memberEquality voidElimination

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[b:bag(T)].    (b|\mneg{}x)  =  b  supposing  \mneg{}x  \mdownarrow{}\mmember{}  b

Date html generated: 2018_05_21-PM-09_52_52
Last ObjectModification: 2017_07_26-PM-06_32_08

Theory : bags_2

Home Index