---

Step * 1 1 of Lemma filter-for-max


1. A : Type
2. l : A List
3. m : ℤ
4. g : A ⟶ ℤ
5. 0 < ||l||
6. imax-list(map(λe.(g e);l)) = m ∈ ℤ
⊢ ¬(filter(λe.(g e =z m);l) = [] ∈ (A List))
BY
{ ((D 0 THENA Auto)
   THEN (Assert (imax-list(map(λe.(g e);l)) ∈ map(λe.(g e);l)) BY
               (BLemma `imax-list-member` THEN Auto THEN RWO "map_length" 0 THEN Auto))
   THEN HypSubst' (-3) (-1)) }

1
1. A : Type
2. l : A List
3. m : ℤ
4. g : A ⟶ ℤ
5. 0 < ||l||
6. imax-list(map(λe.(g e);l)) = m ∈ ℤ
7. filter(λe.(g e =z m);l) = [] ∈ (A List)
8. (m ∈ map(λe.(g e);l))
⊢ False

---

Latex:

---

Latex:

1.  A  :  Type
2.  l  :  A  List
3.  m  :  \mBbbZ{}
4.  g  :  A  {}\mrightarrow{}  \mBbbZ{}
5.  0  <  ||l||
6.  imax-list(map(\mlambda{}e.(g  e);l))  =  m
\mvdash{}  \mneg{}(filter(\mlambda{}e.(g  e  =\msubz{}  m);l)  =  [])


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  (imax-list(map(\mlambda{}e.(g  e);l))  \mmember{}  map(\mlambda{}e.(g  e);l))  BY
                          (BLemma  `imax-list-member`  THEN  Auto  THEN  RWO  "map\_length"  0  THEN  Auto))
  THEN  HypSubst'  (-3)  (-1))

---

Home Index