---

Step * of Lemma max-fst-val

∀[Info,A,T:Type].
  ∀[es:EO+(Info)]. ∀[X:EClass(T × A)]. ∀[e:E].
    MaxFst(X)(e) ~ accum_list(p1,e.if fst(p1) <z fst(X(e)) then X(e) else p1 fi ;e.X(e);≤(X)(e)) 
    supposing ↑e ∈b MaxFst(X) 
  supposing T ⊆r ℤ
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `max-fst-class` -1
   THEN Unfold `max-fst-class` 0
   THEN FLemma `max-f-class-val` [-1]
   THEN Auto
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,T:Type].
    \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T  \mtimes{}  A)].  \mforall{}[e:E].
        MaxFst(X)(e)  \msim{}  accum\_list(p1,e.if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi  ;e.X(e);\mleq{}(X)(e)) 
        supposing  \muparrow{}e  \mmember{}\msubb{}  MaxFst(X) 
    supposing  T  \msubseteq{}r  \mBbbZ{}


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `max-fst-class`  -1
  THEN  Unfold  `max-fst-class`  0
  THEN  FLemma  `max-f-class-val`  [-1]
  THEN  Auto
  THEN  Auto)

---

Home Index