Nuprl Lemma : sub-bag-remove-repeats-if-no-repeats

[T:Type]
  ∀eq:EqDecider(T). ∀b1,b2:bag(T).
    (bag-no-repeats(T;b1)  sub-bag(T;b1;b2)  sub-bag(T;b1;bag-remove-repeats(eq;b2)))


Proof




Definitions occuring in Statement :  bag-remove-repeats: bag-remove-repeats(eq;bs) sub-bag: sub-bag(T;as;bs) bag-no-repeats: bag-no-repeats(T;bs) bag: bag(T) deq: EqDecider(T) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) uimplies: supposing a bag-member: x ↓∈ bs squash: T prop: iff: ⇐⇒ Q
Lemmas referenced :  deq_wf bag-no-repeats_wf sub-bag_wf bag-remove-repeats_wf sub-bag-no-repeats-iff bag-member_wf sub-bag-member bag-member-remove-repeats
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality hypothesis productElimination independent_pairFormation independent_isectElimination sqequalRule imageElimination imageMemberEquality baseClosed dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}b1,b2:bag(T).
        (bag-no-repeats(T;b1)  {}\mRightarrow{}  sub-bag(T;b1;b2)  {}\mRightarrow{}  sub-bag(T;b1;bag-remove-repeats(eq;b2)))



Date html generated: 2016_05_15-PM-08_08_53
Last ObjectModification: 2016_01_16-PM-01_27_36

Theory : bags_2


Home Index