---

Step * of Lemma list-max-map

∀[T,A:Type]. ∀[g:A ⟶ T]. ∀[f:T ⟶ ℤ]. ∀[L:A List].
  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 ∈ ℤ} ) 
  supposing 0 < ||L||
BY
{ TACTIC:(TACTIC:(UnivCD THENA Auto)
          THEN Assert ⌜list-max(x.f[x];map(g;L)) = ((λp.<fst(p), g (snd(p))>) list-max(x.f[g x];L)) ∈ (i:ℤ × T)⌝⋅
          ) }

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

2
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 ∈ ℤ} )

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[g:A  {}\mrightarrow{}  T].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[L:A  List].
    list-max(x.f[x];map(g;L))  =  ((\mlambda{}p.<fst(p),  g  (snd(p))>)  list-max(x.f[g  x];L))  supposing  0  <  ||L||


By

---

Latex:
TACTIC:(TACTIC:(UnivCD  THENA  Auto)
                THEN  Assert  \mkleeneopen{}list-max(x.f[x];map(g;L))  =  ((\mlambda{}p.<fst(p),  g  (snd(p))>)  list-max(x.f[g  x];L))\mkleeneclose{}\mcdot{}
                )

---

Home Index