### Nuprl Lemma : assert-bag-deq-member

`∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[b:bag(A)]. ∀[x:A].  uiff(↑bag-deq-member(eq;x;b);x ↓∈ b)`

Proof

Definitions occuring in Statement :  bag-deq-member: `bag-deq-member(eq;x;b)` bag-member: `x ↓∈ bs` bag: `bag(T)` deq: `EqDecider(T)` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` bag: `bag(T)` implies: `P `` Q` prop: `ℙ` quotient: `x,y:A//B[x; y]` bag-deq-member: `bag-deq-member(eq;x;b)` bag-member: `x ↓∈ bs` squash: `↓T` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` cand: `A c∧ B` subtype_rel: `A ⊆r B` rev_implies: `P `` Q`
Lemmas referenced :  assert_wf bag-deq-member_wf bag-member_wf equal-wf-base list_wf permutation_wf assert_witness bag_wf deq_wf assert-deq-member list-subtype-bag equal_wf l_member_wf deq-member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation thin sqequalHypSubstitution pointwiseFunctionalityForEquality functionEquality extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule hypothesis pertypeElimination productElimination lambdaEquality imageMemberEquality baseClosed because_Cache productEquality independent_functionElimination imageElimination independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry universeEquality dependent_functionElimination dependent_pairFormation applyEquality independent_isectElimination hyp_replacement applyLambdaEquality

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[b:bag(A)].  \mforall{}[x:A].    uiff(\muparrow{}bag-deq-member(eq;x;b);x  \mdownarrow{}\mmember{}  b)

Date html generated: 2018_05_21-PM-09_47_17
Last ObjectModification: 2017_07_26-PM-06_30_09

Theory : bags_2

Home Index