---

Step * of Lemma list-max-property

∀[T:Type]
  ∀f:T ⟶ ℤ. ∀L:T List.  let n,x = list-max(x.f[x];L) in (x ∈ L) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L.f[y] ≤ n) supposing 0 < ||L||
BY
{ (InstLemma `list-max-aux-property` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN Unfold `list-max` 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:T  List.
        let  n,x  =  list-max(x.f[x];L)  in  (x  \mmember{}  L)  \mwedge{}  (f[x]  =  n)  \mwedge{}  (\mforall{}y\mmember{}L.f[y]  \mleq{}  n)  supposing  0  <  ||L||


By

---

Latex:
(InstLemma  `list-max-aux-property`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  Unfold  `list-max`  0
  THEN  Trivial)

---

Home Index