---

Step * 1 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. f1 : ℕ2 ⟶ ℕ||L||
19. increasing(f1;2)
20. ∀j:ℕ2. ([L'[0]; L'[1]][j] = L[f1 j] ∈ T)
⊢ False
BY
{ ((InstHyp [⌜0⌝] (-1)⋅ THENA Auto)
   THEN (InstHyp [⌜1⌝] (-2)⋅ THENA Auto)
   THEN All Reduce
   THEN (HypSubst' (-1) (-7) THENA Auto)
   THEN (HypSubst' (-3) (-1) THENA Auto)) }

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. ∀x,y:T.  (x before y ∈ L' ⇒ x before y ∈ L)
17. f1 : ℕ2 ⟶ ℕ||L||
18. increasing(f1;2)
19. ∀j:ℕ2. ([L'[0]; L'[1]][j] = L[f1 j] ∈ T)
20. L'[0] = L[f1 0] ∈ T
21. L'[1] = L[f1 1] ∈ T
22. f[L[f1 0]] = f[L[f1 1]] ∈ U
⊢ 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.  f1  :  \mBbbN{}2  {}\mrightarrow{}  \mBbbN{}||L||
19.  increasing(f1;2)
20.  \mforall{}j:\mBbbN{}2.  ([L'[0];  L'[1]][j]  =  L[f1  j])
\mvdash{}  False


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  All  Reduce
  THEN  (HypSubst'  (-1)  (-7)  THENA  Auto)
  THEN  (HypSubst'  (-3)  (-1)  THENA  Auto))

---

Home Index