---

Step * 1 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)))
BY
{ Assert ⌈∀L:E(X) List. ∀i:ℤ. ∀a:A.
            (fst(accumulate (with value p1 and list item e):
                  if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
                 over list:
                   L
                 with starting value:
                  <i, a>)) ~ accumulate (with value x and list item y):
                              imax(x;y)
                             over list:
                               map(λe.(fst(X(e)));L)
                             with starting value:
                              i))⌉⋅ }

1
.....assertion..... 
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
⊢ ∀L:E(X) List. ∀i:ℤ. ∀a:A.
    (fst(accumulate (with value p1 and list item e):
          if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
         over list:
           L
         with starting value:
          <i, a>)) ~ accumulate (with value x and list item y):
                      imax(x;y)
                     over list:
                       map(λe.(fst(X(e)));L)
                     with starting value:
                      i))

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. ∀L:E(X) List. ∀i:ℤ. ∀a:A.
     (fst(accumulate (with value p1 and list item e):
           if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
          over list:
            L
          with starting value:
           <i, a>)) ~ accumulate (with value x and list item y):
                       imax(x;y)
                      over list:
                        map(λe.(fst(X(e)));L)
                      with starting value:
                       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)))

---

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


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}L:E(X)  List.  \mforall{}i:\mBbbZ{}.  \mforall{}a:A.
                    (fst(accumulate  (with  value  p1  and  list  item  e):
                                if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi 
                              over  list:
                                  L
                              with  starting  value:
                                <i,  a>))  \msim{}  accumulate  (with  value  x  and  list  item  y):
                                                        imax(x;y)
                                                      over  list:
                                                          map(\mlambda{}e.(fst(X(e)));L)
                                                      with  starting  value:
                                                        i))\mkleeneclose{}\mcdot{}

---

Home Index