---

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

∀[Info:Type]. ∀[X:EClass(Top)].  (#X = es-interface-accum(λn,x. (n + 1);0;X) ∈ EClass(ℕ))
BY
{ (Auto
   THEN BLemma `es-interface-extensionality`
   THEN Try (Complete (Auto))
   THEN Try ((ProveSV THEN Auto))
   THEN (RepeatFor 2 ((D 0 THENA Auto))
         THEN (RWO "is-interface-count is-interface-accum" 0 THEN Auto)
         THEN RWO "es-interface-count-val es-interface-accum-val" 0
         THEN Auto
         THEN Try (RWO "is-interface-accum" 0)
         THEN Auto)⋅) }

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

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[X:EClass(Top)].    (\#X  =  es-interface-accum(\mlambda{}n,x.  (n  +  1);0;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  (RWO  "is-interface-count  is-interface-accum"  0  THEN  Auto)
              THEN  RWO  "es-interface-count-val  es-interface-accum-val"  0
              THEN  Auto
              THEN  Try  (RWO  "is-interface-accum"  0)
              THEN  Auto)\mcdot{})

---

Home Index