Nuprl Lemma : bag-deq-member-bag-diff

[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).  (bag-deq-member(eq;x;bs) isl(bag-diff(eq;bs;{x})))


Proof




Definitions occuring in Statement :  bag-diff: bag-diff(eq;bs;as) bag-deq-member: bag-deq-member(eq;x;b) single-bag: {x} bag: bag(T) deq: EqDecider(T) isl: isl(x) uall: [x:A]. B[x] all: x:A. B[x] universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a iff: ⇐⇒ Q implies:  Q prop: rev_implies:  Q sq_type: SQType(T) guard: {T}
Lemmas referenced :  bag-member-bag-diff subtype_base_sq bool_subtype_base iff_imp_equal_bool bag-deq-member_wf isl_wf bag_wf unit_wf2 bag-diff_wf single-bag_wf bag-member_wf assert_wf assert-bag-deq-member iff_wf deq_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation dependent_functionElimination productElimination instantiate because_Cache independent_isectElimination independent_pairFormation addLevel impliesFunctionality equalityTransitivity equalitySymmetry independent_functionElimination universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}bs:bag(T).    (bag-deq-member(eq;x;bs)  \msim{}  isl(bag-diff(eq;bs;\{x\})))



Date html generated: 2016_05_15-PM-08_05_22
Last ObjectModification: 2015_12_27-PM-04_14_08

Theory : bags_2


Home Index