---

Step * 1 1 of Lemma mapfilter-no-rep-fun


1. T : Type
2. U : Type
3. V : Type
4. eq : EqDecider(U)
5. L : T List
6. u : U
7. f : T ⟶ U
8. g : {x:{x:T| (x ∈ L)} | ↑(eq f[x] u)}  ⟶ V
9. no_repeats(U;map(f;L))
10. ||mapfilter(g;λx.(eq f[x] u);L)|| ∈ ℤ
11. L' : T List
12. L' ⊆ L
13. filter(λx.(eq f[x] u);L) = L' ∈ (T List)
14. 2 ≤ ||L'||
15. ∀x:T. ((x ∈ L') ⇒ (f[x] = u ∈ U))
16. f[L'[0]] = f[L'[1]] ∈ U
17. ∀x,y:T.  (x before y ∈ L' ⇒ x before y ∈ L)
18. L'[0] before L'[1] ∈ L
⊢ False
BY
{ (RepUR ``l_before sublist`` (-1) THEN ExRepD) }

1
1. T : Type
2. U : Type
3. V : Type
4. eq : EqDecider(U)
5. L : T List
6. u : U
7. f : T ⟶ U
8. g : {x:{x:T| (x ∈ L)} | ↑(eq f[x] u)}  ⟶ V
9. no_repeats(U;map(f;L))
10. ||mapfilter(g;λx.(eq f[x] u);L)|| ∈ ℤ
11. L' : T List
12. L' ⊆ L
13. filter(λx.(eq f[x] u);L) = L' ∈ (T List)
14. 2 ≤ ||L'||
15. ∀x:T. ((x ∈ L') ⇒ (f[x] = u ∈ U))
16. f[L'[0]] = f[L'[1]] ∈ U
17. ∀x,y:T.  (x before y ∈ L' ⇒ x before y ∈ L)
18. f1 : ℕ2 ⟶ ℕ||L||
19. increasing(f1;2)
20. ∀j:ℕ2. ([L'[0]; L'[1]][j] = L[f1 j] ∈ T)
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  V  :  Type
4.  eq  :  EqDecider(U)
5.  L  :  T  List
6.  u  :  U
7.  f  :  T  {}\mrightarrow{}  U
8.  g  :  \{x:\{x:T|  (x  \mmember{}  L)\}  |  \muparrow{}(eq  f[x]  u)\}    {}\mrightarrow{}  V
9.  no\_repeats(U;map(f;L))
10.  ||mapfilter(g;\mlambda{}x.(eq  f[x]  u);L)||  \mmember{}  \mBbbZ{}
11.  L'  :  T  List
12.  L'  \msubseteq{}  L
13.  filter(\mlambda{}x.(eq  f[x]  u);L)  =  L'
14.  2  \mleq{}  ||L'||
15.  \mforall{}x:T.  ((x  \mmember{}  L')  {}\mRightarrow{}  (f[x]  =  u))
16.  f[L'[0]]  =  f[L'[1]]
17.  \mforall{}x,y:T.    (x  before  y  \mmember{}  L'  {}\mRightarrow{}  x  before  y  \mmember{}  L)
18.  L'[0]  before  L'[1]  \mmember{}  L
\mvdash{}  False


By

---

Latex:
(RepUR  ``l\_before  sublist``  (-1)  THEN  ExRepD)

---

Home Index