---

Step * of Lemma ml-accumulate-sq

∀[A,B:Type].
  (∀[f:B ⟶ A ⟶ B]. ∀[l:A List]. ∀[b:B].
     (ml-accumulate(f;b;l) ~ accumulate (with value v and list item a):
                              f v a
                             over list:
                               l
                             with starting value:
                              b))) supposing 
     ((valueall-type(A) ∧ A) and 
     valueall-type(B))
BY
{ (InductionOnList
   THEN Intro
   THEN All (RepUR ``ml-accumulate spreadcons ml_apply``)
   THEN RW (AddrC [1] (SweepUpC UnrollRecursionC)) 0
   THEN Reduce 0
   THEN (Assert value-type(A ⟶ B) BY
               (Auto THEN D 0 THEN EAuto 1))
   THEN (Assert valueall-type(B ⟶ A ⟶ B) BY
               Auto)
   THEN (All (CallByValueReduceOn ⌜f⌝)⋅ THENA Auto)
   THEN ((CallByValueReduce 0 THENA Auto) THEN Reduce 0)
   THEN (Trivial
   ORELSE ((CallByValueReduce 0 THENA Auto)
           THEN Reduce 0
           THEN RWO "8" 0
           THEN Auto
           THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto)))
   )) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    (\mforall{}[f:B  {}\mrightarrow{}  A  {}\mrightarrow{}  B].  \mforall{}[l:A  List].  \mforall{}[b:B].
          (ml-accumulate(f;b;l)  \msim{}  accumulate  (with  value  v  and  list  item  a):
                                                            f  v  a
                                                          over  list:
                                                              l
                                                          with  starting  value:
                                                            b)))  supposing 
          ((valueall-type(A)  \mwedge{}  A)  and 
          valueall-type(B))


By

---

Latex:
(InductionOnList
  THEN  Intro
  THEN  All  (RepUR  ``ml-accumulate  spreadcons  ml\_apply``)
  THEN  RW  (AddrC  [1]  (SweepUpC  UnrollRecursionC))  0
  THEN  Reduce  0
  THEN  (Assert  value-type(A  {}\mrightarrow{}  B)  BY
                          (Auto  THEN  D  0  THEN  EAuto  1))
  THEN  (Assert  valueall-type(B  {}\mrightarrow{}  A  {}\mrightarrow{}  B)  BY
                          Auto)
  THEN  (All  (CallByValueReduceOn  \mkleeneopen{}f\mkleeneclose{})\mcdot{}  THENA  Auto)
  THEN  ((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0)
  THEN  (Trivial
  ORELSE  ((CallByValueReduce  0  THENA  Auto)
                  THEN  Reduce  0
                  THEN  RWO  "8"  0
                  THEN  Auto
                  THEN  RepeatFor  2  ((CallByValueReduce  0  THEN  Auto)))
  ))

---

Home Index