---

Step * 1 of Lemma fpf-accum_wf


1. A : Type
2. C : Type
3. B : A ─→ Type
4. d : A List
5. x1 : a:{a:A| (a ∈ d)}  ─→ B[a]
6. y : C
7. f : C ─→ a:A ─→ B[a] ─→ C
⊢ accumulate (with value z and list item a):
   f[z;a;x1 a]
  over list:
    d
  with starting value:
   y) ∈ C
BY
{ (AssertBY ⌈d ∈ {a:A| (a ∈ d)}  List⌉   (BLemma `list-subtype` THEN Auto)⋅ THEN Auto) }

---

Latex:



1.  A  :  Type
2.  C  :  Type
3.  B  :  A  {}\mrightarrow{}  Type
4.  d  :  A  List
5.  x1  :  a:\{a:A|  (a  \mmember{}  d)\}    {}\mrightarrow{}  B[a]
6.  y  :  C
7.  f  :  C  {}\mrightarrow{}  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  C
\mvdash{}  accumulate  (with  value  z  and  list  item  a):
      f[z;a;x1  a]
    over  list:
        d
    with  starting  value:
      y)  \mmember{}  C


By

(AssertBY  \mkleeneopen{}d  \mmember{}  \{a:A|  (a  \mmember{}  d)\}    List\mkleeneclose{}      (BLemma  `list-subtype`  THEN  Auto)\mcdot{}  THEN  Auto)

---

Home Index