---

Step * of Lemma mapfilter-no-rep-fun

∀[T,U,V:Type]. ∀[eq:EqDecider(U)]. ∀[L:T List]. ∀[u:U]. ∀[f:T ⟶ U]. ∀[g:{x:{x:T| (x ∈ L)} | ↑(eq f[x] u)}  ⟶ V].
  ||mapfilter(g;λx.(eq f[x] u);L)|| ≤ 1 supposing no_repeats(U;map(f;L))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌜||mapfilter(g;λx.(eq f[x] u);L)|| ∈ ℤ⌝⋅
         THENA (Using [`A',⌜V⌝] (BLemma `length_wf`)⋅
                THEN Try (Complete (Auto))
                THEN BLemma `mapfilter-wf`
                THEN Auto
                THEN DoSubsume
                THEN Auto)
         )
   THEN Auto
   THEN (SupposeNot THEN Auto)
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN Assert ⌜2 ≤ ||mapfilter(g;λx.(eq f[x] u);L)||⌝⋅
   THEN Auto
   THEN Thin (-2)) }

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. 2 ≤ ||mapfilter(g;λx.(eq f[x] u);L)||
⊢ False

---

Latex:

---

Latex:
\mforall{}[T,U,V:Type].  \mforall{}[eq:EqDecider(U)].  \mforall{}[L:T  List].  \mforall{}[u:U].  \mforall{}[f:T  {}\mrightarrow{}  U].  \mforall{}[g:\{x:\{x:T|  (x  \mmember{}  L)\}  | 
                                                                                                                                                    \muparrow{}(eq  f[x]  u)\}    {}\mrightarrow{}  V].
    ||mapfilter(g;\mlambda{}x.(eq  f[x]  u);L)||  \mleq{}  1  supposing  no\_repeats(U;map(f;L))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}||mapfilter(g;\mlambda{}x.(eq  f[x]  u);L)||  \mmember{}  \mBbbZ{}\mkleeneclose{}\mcdot{}
              THENA  (Using  [`A',\mkleeneopen{}V\mkleeneclose{}]  (BLemma  `length\_wf`)\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  BLemma  `mapfilter-wf`
                            THEN  Auto
                            THEN  DoSubsume
                            THEN  Auto)
              )
  THEN  Auto
  THEN  (SupposeNot  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Assert  \mkleeneopen{}2  \mleq{}  ||mapfilter(g;\mlambda{}x.(eq  f[x]  u);L)||\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Thin  (-2))

---

Home Index