---

Step * of Lemma list-max-property2

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

1
1. [T] : Type
2. f : T ⟶ ℤ
3. L : T List
4. 0 < ||L||
5. let n,x = list-max(x.f[x];L) 
   in (x ∈ L) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L.f[y] ≤ n)
⊢ ∀n:ℤ. ∀x:T.  (x ∈ L) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L.f[y] ≤ n) supposing list-max(x.f[x];L) = <n, x> ∈ (ℤ × T)

---

Latex:

---

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


By

---

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

---

Home Index