---

Step * of Lemma max-f-class-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[X:EClass(A)]. ∀[e:E].
  (v from X with maximum f[v])(e) ~ accum_list(v,e.if f[v] <z f[X(e)] then X(e) else v fi ;e.X(e);≤(X)(e)) 
  supposing ↑e ∈b (v from X with maximum f[v])
BY
{ (Intros
   THEN Try ((GenConclAtAddr [2;1;2] THEN CompleteAuto))
   THEN UseWitness ⌜Ax⌝⋅
   THEN MemCD
   THEN (Unfold `max-f-class` -1 THEN Unfold `max-f-class` 0 THEN FLemma `accum-class-val` [-1] THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    (v  from  X  with  maximum  f[v])(e)  \msim{}  accum\_list(v,e.if  f[v]  <z  f[X(e)]
    then  X(e)
    else  v
    fi  ;e.X(e);\mleq{}(X)(e)) 
    supposing  \muparrow{}e  \mmember{}\msubb{}  (v  from  X  with  maximum  f[v])


By

---

Latex:
(Intros
  THEN  Try  ((GenConclAtAddr  [2;1;2]  THEN  CompleteAuto))
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  MemCD
  THEN  (Unfold  `max-f-class`  -1
              THEN  Unfold  `max-f-class`  0
              THEN  FLemma  `accum-class-val`  [-1]
              THEN  Auto)\mcdot{})

---

Home Index