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