---

Step * of Lemma list_accum_pair-sq

∀[T,A,B:Type]. ∀[f:A ⟶ T ⟶ A]. ∀[g:B ⟶ T ⟶ B]. ∀[L:T List]. ∀[a0:A]. ∀[b0:B].
  (list_accum_pair(a,x.f[a;x];b,x.g[b;x];a0;b0;L) ~ <accumulate (with value a and list item x):
                                                      f[a;x]
                                                     over list:
                                                       L
                                                     with starting value:
                                                      a0)
                                                    , accumulate (with value b and list item x):
                                                       g[b;x]
                                                      over list:
                                                        L
                                                      with starting value:
                                                       b0)
                                                    >)
BY
{ xxx(Unfold `list_accum_pair` 0
      THEN InductionOnList
      THEN Reduce 0
      THEN (UnivCD THENA Auto)
      THEN Try (RWO "-3" 0⋅)
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T,A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A].  \mforall{}[g:B  {}\mrightarrow{}  T  {}\mrightarrow{}  B].  \mforall{}[L:T  List].  \mforall{}[a0:A].  \mforall{}[b0:B].
    (list\_accum\_pair(a,x.f[a;x];b,x.g[b;x];a0;b0;L)  \msim{}  <accumulate  (with  value  a  and  list  item  x):
                                                                                                            f[a;x]
                                                                                                          over  list:
                                                                                                              L
                                                                                                          with  starting  value:
                                                                                                            a0)
                                                                                                        ,  accumulate  (with  value  b  and  list  item  x):
                                                                                                              g[b;x]
                                                                                                            over  list:
                                                                                                                L
                                                                                                            with  starting  value:
                                                                                                              b0)
                                                                                                        >)


By

---

Latex:
xxx(Unfold  `list\_accum\_pair`  0
        THEN  InductionOnList
        THEN  Reduce  0
        THEN  (UnivCD  THENA  Auto)
        THEN  Try  (RWO  "-3"  0\mcdot{})
        THEN  Auto)xxx

---

Home Index