---

Step * 2 1 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 ;u;v) ∈ {mx:T| (mx ∈ [u / v]) ∧ (∀x∈[u / v].0 ≤ (cmp x mx))} 
BY
{ SubsumeC  ⌜{mx:T| ((mx = u ∈ T) ∨ (mx ∈ v)) ∧ (0 ≤ (cmp u mx)) ∧ (∀x∈v.0 ≤ (cmp x mx))} ⌝⋅ }

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 ∈ T) ∨ (mx ∈ v))
                                                               ∧ (0 ≤ (cmp u mx))
                                                               ∧ (∀x∈v.0 ≤ (cmp x mx))} 

2
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))} 

---

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  ;u;v)  \mmember{}  \{mx:T| 
                                                                                                                              (mx  \mmember{}  [u  /  v])
                                                                                                                              \mwedge{}  (\mforall{}x\mmember{}[u  /  v].0  \mleq{}  (cmp  x  mx))\} 


By

---

Latex:
SubsumeC    \mkleeneopen{}\{mx:T|  ((mx  =  u)  \mvee{}  (mx  \mmember{}  v))  \mwedge{}  (0  \mleq{}  (cmp  u  mx))  \mwedge{}  (\mforall{}x\mmember{}v.0  \mleq{}  (cmp  x  mx))\}  \mkleeneclose{}\mcdot{}

---

Home Index