---

Step * 1 1 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
⊢ 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
{ Assert ⌈∀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))⌉⋅ }

1
.....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))

2
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)

---

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
\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:
Assert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}

---

Home Index