---

Step * 1 of Lemma max-fst-property

.....assertion..... 
∀[Info,A:Type].
  ∀es:EO+(Info). ∀X:EClass(ℤ × A). ∀e:E.
    ((↑e ∈b MaxFst(X))
    ⇒ {(fst(MaxFst(X)(e)) ~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
       ∧ (∃mxe:E(X)
           (mxe ≤loc e 
           ∧ (MaxFst(X)(e) = X(mxe) ∈ (ℤ × A))
           ∧ (∀e':E(X). (e' ≤loc e  ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))})
BY
{ (Unfold `guard` 0
   THEN (UnivCD THENA Auto)
   THEN ((FLemma `max-fst-val` [-1] THENM (RWO "-1" 0 THEN Thin (-1))) THENA Auto)) }

1
1. [Info] : Type
2. [A] : Type
3. es : EO+(Info)@i'
4. X : EClass(ℤ × A)@i'
5. e : E@i
6. ↑e ∈b MaxFst(X)@i
⊢ (fst(accum_list(p1,e.if fst(p1) <z fst(X(e)) then X(e) else p1 fi ;e.X(e);≤(X)(e))) 
~ imax-list(map(λe.(fst(X(e)));≤(X)(e))))
∧ (∃mxe:E(X)
    (mxe ≤loc e 
    ∧ (accum_list(p1,e.if fst(p1) <z fst(X(e)) then X(e) else p1 fi ;e.X(e);≤(X)(e)) = X(mxe) ∈ (ℤ × A))
    ∧ (∀e':E(X). (e' ≤loc e  ⇒ ((fst(X(e'))) ≤ (fst(X(mxe))))))))

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[Info,A:Type].
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(\mBbbZ{}  \mtimes{}  A).  \mforall{}e:E.
        ((\muparrow{}e  \mmember{}\msubb{}  MaxFst(X))
        {}\mRightarrow{}  \{(fst(MaxFst(X)(e))  \msim{}  imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e))))
              \mwedge{}  (\mexists{}mxe:E(X)
                      (mxe  \mleq{}loc  e 
                      \mwedge{}  (MaxFst(X)(e)  =  X(mxe))
                      \mwedge{}  (\mforall{}e':E(X).  (e'  \mleq{}loc  e    {}\mRightarrow{}  ((fst(X(e')))  \mleq{}  (fst(X(mxe))))))))\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  ((FLemma  `max-fst-val`  [-1]  THENM  (RWO  "-1"  0  THEN  Thin  (-1)))  THENA  Auto))

---

Home Index