---

Step * of Lemma bag-no-repeats-le-bag-size

No Annotations
∀[T:Type]. ∀[locs,b:bag(T)].  #(b) ≤ #(locs) supposing bag-no-repeats(T;b) ∧ (∀x:T. (x ↓∈ b ⇒ x ↓∈ locs))
BY
{ ((UnivCD THENA Auto)
   THEN SquashConcl
   THEN D (-1)
   THEN Unfold `bag-no-repeats` (-2)
   THEN SquashExRepD
   THEN (RevHypSubst' (-3) (-1) THENA Auto)
   THEN (RevHypSubst' (-3) 0 THENA Auto)
   THEN ThinVar `b'
   THEN (BagToList (-4) THENA (Auto THEN InstLemma `bag-size_wf` [⌜T⌝;⌜L⌝]⋅ THEN Auto))
   THEN Unfold `bag-size` 0
   THEN D 0
   THEN MoveToConcl (-4)) }

1
1. T : Type
2. L : T List
3. no_repeats(T;L)
⊢ ∀locs:T List. ((∀x:T. (x ↓∈ L ⇒ x ↓∈ locs)) ⇒ (||L|| ≤ ||locs||))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[locs,b:bag(T)].
    \#(b)  \mleq{}  \#(locs)  supposing  bag-no-repeats(T;b)  \mwedge{}  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  locs))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SquashConcl
  THEN  D  (-1)
  THEN  Unfold  `bag-no-repeats`  (-2)
  THEN  SquashExRepD
  THEN  (RevHypSubst'  (-3)  (-1)  THENA  Auto)
  THEN  (RevHypSubst'  (-3)  0  THENA  Auto)
  THEN  ThinVar  `b'
  THEN  (BagToList  (-4)  THENA  (Auto  THEN  InstLemma  `bag-size\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  Unfold  `bag-size`  0
  THEN  D  0
  THEN  MoveToConcl  (-4))

---

Home Index