### Nuprl Lemma : bag-member-remove

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x,z:T].  uiff(z ↓∈ bs - x;z ↓∈ bs ∧ (¬(z = x ∈ T)))`

Proof

Definitions occuring in Statement :  bag-remove: `bs - x` bag-member: `x ↓∈ bs` bag: `bag(T)` deq: `EqDecider(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` not: `¬A` and: `P ∧ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  bag-remove: `bs - x` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` uall: `∀[x:A]. B[x]` bag-member: `x ↓∈ bs` squash: `↓T` deq: `EqDecider(T)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` eqof: `eqof(d)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B`
Lemmas referenced :  equal_wf bag-member_wf assert_wf bnot_wf iff_transitivity eqof_wf not_wf iff_weakening_uiff assert_of_bnot safe-assert-deq assert_witness bag-filter_wf subtype_rel_bag bag-member-filter uiff_wf bag-remove_wf bag_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut independent_pairFormation isect_memberFormation introduction sqequalHypSubstitution productElimination thin hypothesis lambdaFormation independent_functionElimination voidElimination extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule independent_pairEquality imageElimination imageMemberEquality baseClosed lambdaEquality dependent_functionElimination productEquality applyEquality setElimination rename equalitySymmetry addLevel because_Cache impliesFunctionality independent_isectElimination setEquality universeEquality isect_memberEquality equalityTransitivity promote_hyp

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x,z:T].    uiff(z  \mdownarrow{}\mmember{}  bs  -  x;z  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\mneg{}(z  =  x)))

Date html generated: 2018_05_21-PM-09_47_41
Last ObjectModification: 2017_07_26-PM-06_30_23

Theory : bags_2

Home Index