---

Step * 1 1 2 of Lemma es-interface-buffer-as-accum


1. Info : Type
2. A1 : Type
3. n : ℕ
4. X : EClass(A1)
5. es : EO+(Info)@i'
6. e : E@i
7. ↑e ∈b X
8. ∀as:A1 List
     (accumulate (with value b and list item x):
       if ||b|| <z n then b @ [x] else tl(b @ [x]) fi 
      over list:
        map(λe.X(e);≤(X)(e))
      with starting value:
       as)
     = accumulate (with value b and list item e):
        (λL,v. if ||L|| <z n then L @ [v] else tl(L @ [v]) fi ) b X(e)
       over list:
         ≤(X)(e)
       with starting value:
        as)
     ∈ (A1 List))
⊢ accumulate (with value b and list item x):
   if ||b|| <z n then b @ [x] else tl(b @ [x]) fi 
  over list:
    map(λe.X(e);≤(X)(e))
  with starting value:
   [])
= accumulate (with value b and list item e):
   (λL,v. if ||L|| <z n then L @ [v] else tl(L @ [v]) fi ) b X(e)
  over list:
    ≤(X)(e)
  with starting value:
   [])
∈ (A1 List)
BY
{ (BHyp (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A1  :  Type
3.  n  :  \mBbbN{}
4.  X  :  EClass(A1)
5.  es  :  EO+(Info)@i'
6.  e  :  E@i
7.  \muparrow{}e  \mmember{}\msubb{}  X
8.  \mforall{}as:A1  List
          (accumulate  (with  value  b  and  list  item  x):
              if  ||b||  <z  n  then  b  @  [x]  else  tl(b  @  [x])  fi 
            over  list:
                map(\mlambda{}e.X(e);\mleq{}(X)(e))
            with  starting  value:
              as)
          =  accumulate  (with  value  b  and  list  item  e):
                (\mlambda{}L,v.  if  ||L||  <z  n  then  L  @  [v]  else  tl(L  @  [v])  fi  )  b  X(e)
              over  list:
                  \mleq{}(X)(e)
              with  starting  value:
                as))
\mvdash{}  accumulate  (with  value  b  and  list  item  x):
      if  ||b||  <z  n  then  b  @  [x]  else  tl(b  @  [x])  fi 
    over  list:
        map(\mlambda{}e.X(e);\mleq{}(X)(e))
    with  starting  value:
      [])
=  accumulate  (with  value  b  and  list  item  e):
      (\mlambda{}L,v.  if  ||L||  <z  n  then  L  @  [v]  else  tl(L  @  [v])  fi  )  b  X(e)
    over  list:
        \mleq{}(X)(e)
    with  starting  value:
      [])


By

---

Latex:
(BHyp  (-1)  THEN  Auto)

---

Home Index