---

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

∀[Info,A1:Type]. ∀[n:ℕ]. ∀[X:EClass(A1)].
  (Buffer(n;X) = es-interface-accum(λL,v. if ||L|| <z n then L @ [v] else tl(L @ [v]) fi ;[];X) ∈ EClass(A1 List))
BY
{ (Auto
   THEN BLemma `es-interface-extensionality`
   THEN Try (Complete (Auto))
   THEN Try ((ProveSV THEN Auto))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN Try (((RWO "is-interface-accum" 0 THENM RWO "is-interface-buffer" 0)⋅ THEN Complete (Auto)))
   THEN Auto
   THEN (RWO "es-interface-accum-val interface-buffer-val" 0 THENA Auto)
   THEN Thin (-1)
   THEN (RWO "is-interface-buffer" (-1) THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[Info,A1:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:EClass(A1)].
    (Buffer(n;X)  =  es-interface-accum(\mlambda{}L,v.  if  ||L||  <z  n  then  L  @  [v]  else  tl(L  @  [v])  fi  ;[];X))


By

---

Latex:
(Auto
  THEN  BLemma  `es-interface-extensionality`
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((ProveSV  THEN  Auto))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Try  (((RWO  "is-interface-accum"  0  THENM  RWO  "is-interface-buffer"  0)\mcdot{}  THEN  Complete  (Auto)))
  THEN  Auto
  THEN  (RWO  "es-interface-accum-val  interface-buffer-val"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (RWO  "is-interface-buffer"  (-1)  THENA  Auto))

---

Home Index