---

Step * 2 1 of Lemma comparison-max_wf


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))} 
BY
{ Reduce 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 ;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
\mvdash{}  eager-accum(mx,x.if  0  \mleq{}z  cmp  x  mx  then  mx  else  x  fi  ;hd([u  /  v]);tl([u  /  v]))  \mmember{}  \{mx:T| 
                                                                                                                                                                      (mx  \mmember{}  [u  /  v])
                                                                                                                                                                      \mwedge{}  (\mforall{}x\mmember{}[u  /  v].
                                                                                                                                                                                0  \mleq{}  (cmp  x 
                                                                                                                                                                                          mx))\} 


By

---

Latex:
Reduce  0

---

Home Index