---

Step * 1 1 1 2 2 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. ∀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))
8. u : E(X)
9. v : E(X) List
10. ≤(X)(e) = [u / v] ∈ (E(X) List)@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:
       X(u))) ~ accumulate (with value x and list item y):
                 imax(x;y)
                over list:
                  map(λe.(fst(X(e)));v)
                with starting value:
                 fst(X(u)))
BY
{ (GenConclAtAddr [1;1;2] THEN D -2 THEN Reduce 0)⋅ }

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. ∀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))
8. u : E(X)
9. v : E(X) List
10. ≤(X)(e) = [u / v] ∈ (E(X) List)@i
11. v2 : ℤ@i
12. v3 : A@i
13. X(u) = <v2, v3> ∈ (ℤ × 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:
       <v2, v3>)) ~ accumulate (with value x and list item y):
                     imax(x;y)
                    over list:
                      map(λe.(fst(X(e)));v)
                    with starting value:
                     v2)

---

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.  \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))
8.  u  :  E(X)
9.  v  :  E(X)  List
10.  \mleq{}(X)(e)  =  [u  /  v]@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:
              X(u)))  \msim{}  accumulate  (with  value  x  and  list  item  y):
                                  imax(x;y)
                                over  list:
                                    map(\mlambda{}e.(fst(X(e)));v)
                                with  starting  value:
                                  fst(X(u)))


By

---

Latex:
(GenConclAtAddr  [1;1;2]  THEN  D  -2  THEN  Reduce  0)\mcdot{}

---

Home Index