---

Step * of Lemma list-max-imax-list

∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List].  (fst(list-max(x.f[x];L))) = imax-list(map(λx.f[x];L)) ∈ ℤ supposing 0 < ||L||
BY
{ ((InstLemma `list-max-property` [] THEN RepeatFor 4 (ParallelLast') THEN Auto THEN MoveToConcl (-1))
   THEN GenConclAtAddr [1;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

1
1. T : Type
2. f : T ⟶ ℤ
3. L : T List
4. 0 < ||L||
5. i : ℤ
6. v1 : {x:T| f[x] = i ∈ ℤ} 
7. list-max(x.f[x];L) = <i, v1> ∈ (i:ℤ × {x:T| f[x] = i ∈ ℤ} )
8. (v1 ∈ L)
9. f[v1] = i ∈ ℤ
10. (∀y∈L.f[y] ≤ i)
⊢ i = imax-list(map(λx.f[x];L)) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
((InstLemma  `list-max-property`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  Auto  THEN  MoveToConcl  (-1))
  THEN  GenConclAtAddr  [1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index