---

Step * 1 1 1 1 2 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
7. u : E(X)
8. v : E(X) List
9. ∀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:
            v
          with starting value:
           <i, a>)) ~ accumulate (with value x and list item y):
                       imax(x;y)
                      over list:
                        map(λe.(fst(X(e)));v)
                      with starting value:
                       i))
10. i : ℤ@i
11. a : A@i
⊢ (fst(accumulate (with value p1 and list item e):
        if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
       over list:
         v
       with starting value:
        if i <z fst(X(u)) then X(u) else <i, a> fi )))
= accumulate (with value x and list item y):
   imax(x;y)
  over list:
    map(λe.(fst(X(e)));v)
  with starting value:
   imax(i;fst(X(u))))
∈ ℤ
BY
{ (Assert X ∈ EClass(ℤ × Top) BY
         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
7. u : E(X)
8. v : E(X) List
9. ∀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:
            v
          with starting value:
           <i, a>)) ~ accumulate (with value x and list item y):
                       imax(x;y)
                      over list:
                        map(λe.(fst(X(e)));v)
                      with starting value:
                       i))
10. i : ℤ@i
11. a : A@i
12. X ∈ EClass(ℤ × Top)
⊢ (fst(accumulate (with value p1 and list item e):
        if fst(p1) <z fst(X(e)) then X(e) else p1 fi 
       over list:
         v
       with starting value:
        if i <z fst(X(u)) then X(u) else <i, a> fi )))
= accumulate (with value x and list item y):
   imax(x;y)
  over list:
    map(λe.(fst(X(e)));v)
  with starting value:
   imax(i;fst(X(u))))
∈ ℤ

---

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
7.  u  :  E(X)
8.  v  :  E(X)  List
9.  \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:
                        v
                    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)));v)
                                            with  starting  value:
                                              i))
10.  i  :  \mBbbZ{}@i
11.  a  :  A@i
\mvdash{}  (fst(accumulate  (with  value  p1  and  list  item  e):
                if  fst(p1)  <z  fst(X(e))  then  X(e)  else  p1  fi 
              over  list:
                  v
              with  starting  value:
                if  i  <z  fst(X(u))  then  X(u)  else  <i,  a>  fi  )))
=  accumulate  (with  value  x  and  list  item  y):
      imax(x;y)
    over  list:
        map(\mlambda{}e.(fst(X(e)));v)
    with  starting  value:
      imax(i;fst(X(u))))


By

---

Latex:
(Assert  X  \mmember{}  EClass(\mBbbZ{}  \mtimes{}  Top)  BY
              Auto)

---

Home Index