---

Step * 2 1 1 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. eager-accum(mx,x.if 0 ≤z cmp x mx then mx else x fi ;u;v)
= eager-accum(mx,x.if 0 ≤z cmp x mx then mx else x fi ;u;v)
∈ {mx:T| ((mx = u ∈ T) ∨ (mx ∈ v)) ∧ (0 ≤ (cmp u mx)) ∧ (∀x∈v.0 ≤ (cmp x mx))} 
⊢ {mx:T| ((mx = u ∈ T) ∨ (mx ∈ v)) ∧ (0 ≤ (cmp u mx)) ∧ (∀x∈v.0 ≤ (cmp x mx))}  ⊆r {mx:T| 
                                                                                     (mx ∈ [u / v])
                                                                                     ∧ (∀x∈[u / v].0 ≤ (cmp x mx))} 
BY
{ ((D 0 THENA Auto) THEN D -1 THEN MemTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  cmp  :  comparison(T)
3.  valueall-type(T)
4.  u  :  T
5.  v  :  T  List
6.  eager-accum(mx,x.if  0  \mleq{}z  cmp  x  mx  then  mx  else  x  fi  ;u;v)
=  eager-accum(mx,x.if  0  \mleq{}z  cmp  x  mx  then  mx  else  x  fi  ;u;v)
\mvdash{}  \{mx:T|  ((mx  =  u)  \mvee{}  (mx  \mmember{}  v))  \mwedge{}  (0  \mleq{}  (cmp  u  mx))  \mwedge{}  (\mforall{}x\mmember{}v.0  \mleq{}  (cmp  x  mx))\}    \msubseteq{}r  \{mx:T| 
                                                                                                                                                                  (mx  \mmember{}  [u  /  v])
                                                                                                                                                                  \mwedge{}  (\mforall{}x\mmember{}[u  /  v].
                                                                                                                                                                            0  \mleq{}  (cmp  x 
                                                                                                                                                                                      mx))\} 


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index