---

Step * 2 1 1 2 of Lemma no-repeats-iff-count


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
5. i : ℕ
6. j : ℕ
7. i < ||L||
8. j < ||L||
9. ¬(i = j ∈ ℕ)
10. L[i] = L[j] ∈ T
11. ¬i < j
⊢ 2 ≤ ||filter(eq L[i];L)||
BY
{ ((InstLemma `sublist_filter` [⌜T⌝;⌜L⌝;⌜[L[j]; L[i]]⌝;⌜eq L[i]⌝]⋅ THEN Auto)
   THEN (D -1 THENM (FLemma `length_sublist` [-1] THEN Auto))
   THEN Auto
   THEN Try ((RW assert_pushdownC 0 THEN Auto))
   THEN Thin (-1))⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. ∀[x:T]. uiff(1 ≤ ||filter(eq x;L)||;||filter(eq x;L)|| = 1 ∈ ℤ)
5. i : ℕ
6. j : ℕ
7. i < ||L||
8. j < ||L||
9. ¬(i = j ∈ ℕ)
10. L[i] = L[j] ∈ T
11. ¬i < j
⊢ [L[j]; L[i]] ⊆ L

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  \mforall{}[x:T].  uiff(1  \mleq{}  ||filter(eq  x;L)||;||filter(eq  x;L)||  =  1)
5.  i  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  i  <  ||L||
8.  j  <  ||L||
9.  \mneg{}(i  =  j)
10.  L[i]  =  L[j]
11.  \mneg{}i  <  j
\mvdash{}  2  \mleq{}  ||filter(eq  L[i];L)||


By

---

Latex:
((InstLemma  `sublist\_filter`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}[L[j];  L[i]]\mkleeneclose{};\mkleeneopen{}eq  L[i]\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (D  -1  THENM  (FLemma  `length\_sublist`  [-1]  THEN  Auto))
  THEN  Auto
  THEN  Try  ((RW  assert\_pushdownC  0  THEN  Auto))
  THEN  Thin  (-1))\mcdot{}

---

Home Index