---

Step * 2 of Lemma list-max-map


1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. L : A List
6. 0 < ||L||
7. list-max(x.f[x];map(g;L)) = ((λp.<fst(p), g (snd(p))>) list-max(x.f[g x];L)) ∈ (i:ℤ × T)
⊢ list-max(x.f[x];map(g;L)) = ((λp.<fst(p), g (snd(p))>) list-max(x.f[g x];L)) ∈ (i:ℤ × {x:T| f[x] = i ∈ ℤ} )
BY
{ (StrongRevHypSubst (-1) 0 THEN Auto THEN Try (Complete (Auto))) }

1
1. T : Type
2. A : Type
3. g : A ⟶ T
4. f : T ⟶ ℤ
5. L : A List
6. 0 < ||L||
7. list-max(x.f[x];map(g;L)) = ((λp.<fst(p), g (snd(p))>) list-max(x.f[g x];L)) ∈ (i:ℤ × T)
8. i : ℤ
9. z1 : T
10. <i, z1> = list-max(x.f[x];map(g;L)) ∈ (i:ℤ × T)
⊢ z1 ∈ {x:T| f[x] = i ∈ ℤ} 

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  g  :  A  {}\mrightarrow{}  T
4.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
5.  L  :  A  List
6.  0  <  ||L||
7.  list-max(x.f[x];map(g;L))  =  ((\mlambda{}p.<fst(p),  g  (snd(p))>)  list-max(x.f[g  x];L))
\mvdash{}  list-max(x.f[x];map(g;L))  =  ((\mlambda{}p.<fst(p),  g  (snd(p))>)  list-max(x.f[g  x];L))


By

---

Latex:
(StrongRevHypSubst  (-1)  0  THEN  Auto  THEN  Try  (Complete  (Auto)))

---

Home Index