---

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


1. Info : Type
2. X : EClass(Top)
3. es : EO+(Info)@i'
4. e : E@i
5. ↑e ∈b X@i
6. ↑e ∈b X@i
⊢ ||≤(X)(e)||
= accumulate (with value b and list item e):
   (λn,x. (n + 1)) b X(e)
  over list:
    ≤(X)(e)
  with starting value:
   0)
∈ ℕ
BY
{ ((GenConclAtAddrType ⌈Top List⌉ [2;1]⋅ THENA Auto) THEN Reduce 0 THEN All Thin) }

1
1. v : Top List@i
⊢ ||v|| = accumulate (with value b and list item e): b + 1over list:  vwith starting value: 0) ∈ ℕ

---

Latex:

---

Latex:

1.  Info  :  Type
2.  X  :  EClass(Top)
3.  es  :  EO+(Info)@i'
4.  e  :  E@i
5.  \muparrow{}e  \mmember{}\msubb{}  X@i
6.  \muparrow{}e  \mmember{}\msubb{}  X@i
\mvdash{}  ||\mleq{}(X)(e)||
=  accumulate  (with  value  b  and  list  item  e):
      (\mlambda{}n,x.  (n  +  1))  b  X(e)
    over  list:
        \mleq{}(X)(e)
    with  starting  value:
      0)


By

---

Latex:
((GenConclAtAddrType  \mkleeneopen{}Top  List\mkleeneclose{}  [2;1]\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  All  Thin)

---

Home Index