---

Step * of Lemma comparison-max_wf

∀[T:Type]. ∀[cmp:comparison(T)].  ∀L:T List+. (comparison-max(cmp;L) ∈ {mx:T| (mx ∈ L) ∧ (∀x∈L.0 ≤ (cmp x mx))} ) suppos\000Cing valueall-type(T)
BY
{ (Auto THEN D -1 THEN D -2) }

1
1. T : Type
2. cmp : comparison(T)
3. valueall-type(T)
4. ||[]|| ≥ 1 
⊢ comparison-max(cmp;[]) ∈ {mx:T| (mx ∈ []) ∧ (∀x∈[].0 ≤ (cmp x mx))} 

2
1. T : Type
2. cmp : comparison(T)
3. valueall-type(T)
4. u : T
5. v : T List
6. ||[u / v]|| ≥ 1 
⊢ comparison-max(cmp;[u / v]) ∈ {mx:T| (mx ∈ [u / v]) ∧ (∀x∈[u / v].0 ≤ (cmp x mx))} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[cmp:comparison(T)].
    \mforall{}L:T  List\msupplus{}.  (comparison-max(cmp;L)  \mmember{}  \{mx:T|  (mx  \mmember{}  L)  \mwedge{}  (\mforall{}x\mmember{}L.0  \mleq{}  (cmp  x  mx))\}  )  supposing  valueall\000C-type(T)


By

---

Latex:
(Auto  THEN  D  -1  THEN  D  -2)

---

Home Index