---

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


1. T : Type
2. L : T List
3. no_repeats(T;L)
⊢ ∀locs:T List. ((∀x:T. (x ↓∈ L ⇒ x ↓∈ locs)) ⇒ (||L|| ≤ ||locs||))
BY
{ (ListInd (-2)
   THEN Reduce 0
   THEN Auto
   THEN GenListD (-3)
   THEN RepD
   THEN (D (-5) THENA Auto)
   THEN (InstHyp [⌜u⌝] (-2)⋅ THENA (Auto THEN BagMemberD 0 THEN D 0 THEN Auto))
   THEN Unfold `bag-member` (-1)
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN ExRepD
   THEN (RevHypSubst' (-2) (-5) THENA Auto)
   THEN Try (Fold `bag-size` 0⋅)
   THEN (RevHypSubst' (-2) 0 THENA (Auto THEN InstLemma `bag-size_wf` [⌜T⌝;⌜v⌝]⋅ THEN Auto))
   THEN Unfold `bag-size` 0
   THEN ThinVar `locs'
   THEN Unfold `l_member` (-1)
   THEN ExRepD) }

1
1. T : Type
2. u : T
3. v : T List
4. no_repeats(T;v)
5. ¬(u ∈ v)
6. ∀locs:T List. ((∀x:T. (x ↓∈ v ⇒ x ↓∈ locs)) ⇒ (||v|| ≤ ||locs||))
7. L : T List
8. ∀x:T. (x ↓∈ [u / v] ⇒ x ↓∈ L)
9. i : ℕ
10. i < ||L||
11. u = L[i] ∈ T
⊢ (||v|| + 1) ≤ ||L||

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  no\_repeats(T;L)
\mvdash{}  \mforall{}locs:T  List.  ((\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  locs))  {}\mRightarrow{}  (||L||  \mleq{}  ||locs||))


By

---

Latex:
(ListInd  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  GenListD  (-3)
  THEN  RepD
  THEN  (D  (-5)  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-2)\mcdot{}  THENA  (Auto  THEN  BagMemberD  0  THEN  D  0  THEN  Auto))
  THEN  Unfold  `bag-member`  (-1)
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD
  THEN  (RevHypSubst'  (-2)  (-5)  THENA  Auto)
  THEN  Try  (Fold  `bag-size`  0\mcdot{})
  THEN  (RevHypSubst'  (-2)  0  THENA  (Auto  THEN  InstLemma  `bag-size\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  Unfold  `bag-size`  0
  THEN  ThinVar  `locs'
  THEN  Unfold  `l\_member`  (-1)
  THEN  ExRepD)

---

Home Index