---

Step * 1 1 of Lemma max-fst-property


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))))))))
BY
{ newAutoStep }

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)))

2
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
7. 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:

1.  [Info]  :  Type
2.  [A]  :  Type
3.  es  :  EO+(Info)@i'
4.  X  :  EClass(\mBbbZ{}  \mtimes{}  A)@i'
5.  e  :  E@i
6.  \muparrow{}e  \mmember{}\msubb{}  MaxFst(X)@i
\mvdash{}  (fst(accum\_list(p1,e.if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi  ;e.X(e);\mleq{}(X)(e))) 
\msim{}  imax-list(map(\mlambda{}e.(fst(X(e)));\mleq{}(X)(e))))
\mwedge{}  (\mexists{}mxe:E(X)
        (mxe  \mleq{}loc  e 
        \mwedge{}  (accum\_list(p1,e.if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi  ;e.X(e);\mleq{}(X)(e))  =  X(mxe))
        \mwedge{}  (\mforall{}e':E(X).  (e'  \mleq{}loc  e    {}\mRightarrow{}  ((fst(X(e')))  \mleq{}  (fst(X(mxe))))))))


By

---

Latex:
newAutoStep

---

Home Index