---

Step * 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
⊢ lastn(n;X(≤(X)(e)))
= 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
{ ((RWO "lastn-as-accum" 0 THENA Auto) THEN Unfold `eclass-vals` 0) }

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

---

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{}  lastn(n;X(\mleq{}(X)(e)))
=  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:
((RWO  "lastn-as-accum"  0  THENA  Auto)  THEN  Unfold  `eclass-vals`  0)

---

Home Index