---

Step * 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. 2 ≤ ||mapfilter(g;λx.(eq f[x] u);L)||
⊢ False
BY
{ (RepUR ``mapfilter`` (-1)
   THEN (RWO "length-map" (-1) THENA Auto)
   THEN (Assert ⌜∃L':T List. (L' ⊆ L ∧ (filter(λx.(eq f[x] u);L) = L' ∈ (T List)))⌝⋅
         THENA (InstConcl [⌜filter(λx.(eq f[x] u);L)⌝]⋅ THEN Auto THEN BLemma `filter_is_sublist` THEN Auto)
         )
   THEN ExRepD
   THEN (RWO "-1" (-4) THENA Auto)
   THEN (Assert ⌜∀x:T. ((x ∈ L') ⇒ (f[x] = u ∈ U))⌝⋅
         THENA (Auto THEN (RWO "-4<" (-1) THENA Auto) THEN GenListD (-1) THEN Auto THEN AllPushDown THEN Auto)
         )
   THEN (Assert ⌜f[L'[0]] = f[L'[1]] ∈ U⌝⋅
         THENA ((InstHyp [⌜L'[0]⌝] (-1)⋅ THENA (Auto THEN GenListD 0))
                THEN (InstHyp [⌜L'[1]⌝] (-2)⋅ THENA (Auto THEN GenListD 0))
                THEN Auto)
         )
   THEN (FLemma `l_before_sublist` [-5] THENA Auto)
   THEN (InstHyp [⌜L'[0]⌝;⌜L'[1]⌝] (-1)⋅ THENA (Auto THEN BLemma `l_before_select` THEN 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. 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

---

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.  2  \mleq{}  ||mapfilter(g;\mlambda{}x.(eq  f[x]  u);L)||
\mvdash{}  False


By

---

Latex:
(RepUR  ``mapfilter``  (-1)
  THEN  (RWO  "length-map"  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}L':T  List.  (L'  \msubseteq{}  L  \mwedge{}  (filter(\mlambda{}x.(eq  f[x]  u);L)  =  L'))\mkleeneclose{}\mcdot{}
              THENA  (InstConcl  [\mkleeneopen{}filter(\mlambda{}x.(eq  f[x]  u);L)\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  BLemma  `filter\_is\_sublist`
                            THEN  Auto)
              )
  THEN  ExRepD
  THEN  (RWO  "-1"  (-4)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mforall{}x:T.  ((x  \mmember{}  L')  {}\mRightarrow{}  (f[x]  =  u))\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (RWO  "-4<"  (-1)  THENA  Auto)
                            THEN  GenListD  (-1)
                            THEN  Auto
                            THEN  AllPushDown
                            THEN  Auto)
              )
  THEN  (Assert  \mkleeneopen{}f[L'[0]]  =  f[L'[1]]\mkleeneclose{}\mcdot{}
              THENA  ((InstHyp  [\mkleeneopen{}L'[0]\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  GenListD  0))
                            THEN  (InstHyp  [\mkleeneopen{}L'[1]\mkleeneclose{}]  (-2)\mcdot{}  THENA  (Auto  THEN  GenListD  0))
                            THEN  Auto)
              )
  THEN  (FLemma  `l\_before\_sublist`  [-5]  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}L'[0]\mkleeneclose{};\mkleeneopen{}L'[1]\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  BLemma  `l\_before\_select`  THEN  Auto)))

---

Home Index