---

Step * 2 of Lemma comparison-max_wf


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))} 
BY
{ (Thin (-1) THEN Unfold `comparison-max` 0) }

1
1. T : Type
2. cmp : comparison(T)
3. valueall-type(T)
4. u : T
5. v : T List
⊢ eager-accum(mx,x.if 0 ≤z cmp x mx then mx else x fi ;hd([u / v]);tl([u / v])) ∈ {mx:T| 
                                                                                   (mx ∈ [u / v])
                                                                                   ∧ (∀x∈[u / v].0 ≤ (cmp x mx))} 

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  valueall-type(T)
4.  u  :  T
5.  v  :  T  List
6.  ||[u  /  v]||  \mgeq{}  1 
\mvdash{}  comparison-max(cmp;[u  /  v])  \mmember{}  \{mx:T|  (mx  \mmember{}  [u  /  v])  \mwedge{}  (\mforall{}x\mmember{}[u  /  v].0  \mleq{}  (cmp  x  mx))\} 


By

---

Latex:
(Thin  (-1)  THEN  Unfold  `comparison-max`  0)

---

Home Index