---

Step * 2 1 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 ∈ T) ∨ (mx ∈ v))
                                                               ∧ (0 ≤ (cmp u mx))
                                                               ∧ (∀x∈v.0 ≤ (cmp x mx))} 
BY
{ ((RenameVar `a' (-2) THEN RenameVar `L' (-1))
   THEN MoveToConcl (-2)
   THEN ListInd (-1)
   THEN (D 0 THENA Auto)
   THEN RecUnfold `eager-accum` 0
   THEN Reduce 0) }

1
1. T : Type
2. cmp : comparison(T)
3. valueall-type(T)
4. a : T
⊢ a ∈ {mx:T| ((mx = a ∈ T) ∨ (mx ∈ [])) ∧ (0 ≤ (cmp a 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. ∀a:T
     (eager-accum(mx,x.if 0 ≤z cmp x mx then mx else x fi ;a;v) ∈ {mx:T| 
                                                                   ((mx = a ∈ T) ∨ (mx ∈ v))
                                                                   ∧ (0 ≤ (cmp a mx))
                                                                   ∧ (∀x∈v.0 ≤ (cmp x mx))} )
7. a : T
⊢ let y' ⟵ if 0 ≤z cmp u a then a else u fi 
  in eager-accum(mx,x.if 0 ≤z cmp x mx then mx else x fi ;y';v) ∈ {mx:T| 
                                                                   ((mx = a ∈ T) ∨ (mx ∈ [u / v]))
                                                                   ∧ (0 ≤ (cmp a mx))
                                                                   ∧ (∀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  =  u)  \mvee{}  (mx  \mmember{}  v))
                                                                                                                              \mwedge{}  (0  \mleq{}  (cmp  u  mx))
                                                                                                                              \mwedge{}  (\mforall{}x\mmember{}v.0  \mleq{}  (cmp  x  mx))\} 


By

---

Latex:
((RenameVar  `a'  (-2)  THEN  RenameVar  `L'  (-1))
  THEN  MoveToConcl  (-2)
  THEN  ListInd  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  RecUnfold  `eager-accum`  0
  THEN  Reduce  0)

---

Home Index