---

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

.....assertion..... 
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
⊢ ∀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))
BY
{ ((GenConclAtAddr [2;3;3] THEN Thin (-1) THEN ListInd (-1))
   THEN Reduce 0
   THEN Auto
   THEN (RWO "-2" 0 THENM Reduce 0)
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  \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))


By

---

Latex:
((GenConclAtAddr  [2;3;3]  THEN  Thin  (-1)  THEN  ListInd  (-1))
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "-2"  0  THENM  Reduce  0)
  THEN  Auto)

---

Home Index