---

Step * 1 1 2 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
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)))
8. u : E(X)@i
9. v : E(X) List@i
10. ∀e:E(X)
      ∃e':E(X)
       (((e' ∈ v) ∨ (e' = e ∈ E(X)))
       ∧ (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(e))
         = X(e')
         ∈ (ℤ × A)))@i
11. e1 : E(X)@i
⊢ ∃e':E(X)
   (((e' ∈ [u / v]) ∨ (e' = e1 ∈ E(X)))
   ∧ (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 fst(X(e1)) <z fst(X(u)) then X(u) else X(e1) fi )
     = X(e')
     ∈ (ℤ × A)))
BY
{ ((Assert X ∈ EClass(ℤ × Top) BY Auto) THEN AutoSplit) }

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. 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)))
8. u : E(X)@i
9. v : E(X) List@i
10. ∀e:E(X)
      ∃e':E(X)
       (((e' ∈ v) ∨ (e' = e ∈ E(X)))
       ∧ (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(e))
         = X(e')
         ∈ (ℤ × A)))@i
11. e1 : E(X)@i
12. X ∈ EClass(ℤ × Top)
13. fst(X(e1)) < fst(X(u))
⊢ ∃e':E(X)
   (((e' ∈ [u / v]) ∨ (e' = e1 ∈ E(X)))
   ∧ (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))
     = X(e')
     ∈ (ℤ × A)))

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)))
8. u : E(X)@i
9. v : E(X) List@i
10. ∀e:E(X)
      ∃e':E(X)
       (((e' ∈ v) ∨ (e' = e ∈ E(X)))
       ∧ (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(e))
         = X(e')
         ∈ (ℤ × A)))@i
11. e1 : E(X)@i
12. ¬fst(X(e1)) < fst(X(u))
13. X ∈ EClass(ℤ × Top)
⊢ ∃e':E(X)
   (((e' ∈ [u / v]) ∨ (e' = e1 ∈ E(X)))
   ∧ (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(e1))
     = X(e')
     ∈ (ℤ × A)))

---

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.  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)))
8.  u  :  E(X)@i
9.  v  :  E(X)  List@i
10.  \mforall{}e:E(X)
            \mexists{}e':E(X)
              (((e'  \mmember{}  v)  \mvee{}  (e'  =  e))
              \mwedge{}  (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(e))
                  =  X(e')))@i
11.  e1  :  E(X)@i
\mvdash{}  \mexists{}e':E(X)
      (((e'  \mmember{}  [u  /  v])  \mvee{}  (e'  =  e1))
      \mwedge{}  (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  fst(X(e1))  <z  fst(X(u))  then  X(u)  else  X(e1)  fi  )
          =  X(e')))


By

---

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

---

Home Index