---

Step * 2 1 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. ∀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))} 
BY
{ ((CallByValueReduce 0 THENA Auto)
   THEN (InstHyp [⌜if 0 ≤z cmp u a then a else u fi ⌝] (-2)⋅ THENA Auto)
   THEN DoSubsume
   THEN Try (Trivial)
   THEN All Thin
   THEN (D 0 THENA Auto)) }

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


By

---

Latex:
((CallByValueReduce  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}if  0  \mleq{}z  cmp  u  a  then  a  else  u  fi  \mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  DoSubsume
  THEN  Try  (Trivial)
  THEN  All  Thin
  THEN  (D  0  THENA  Auto))

---

Home Index