---

Step * of Lemma list_accum_invariant

∀[T,A:Type].
  ∀f:A ⟶ T ⟶ A
    ∀[P:A ⟶ ℙ]
      ∀L:T List. ∀a:A.
        (P[a]
        ⇒ (∀a:A. ∀x:T.  (P[a] ⇒ P[f[a;x]]))
        ⇒ P[accumulate (with value a and list item x):
              f[a;x]
             over list:
               L
             with starting value:
              a)])
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN BackThruSomeHyp THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].
    \mforall{}f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A
        \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}]
            \mforall{}L:T  List.  \mforall{}a:A.
                (P[a]
                {}\mRightarrow{}  (\mforall{}a:A.  \mforall{}x:T.    (P[a]  {}\mRightarrow{}  P[f[a;x]]))
                {}\mRightarrow{}  P[accumulate  (with  value  a  and  list  item  x):
                            f[a;x]
                          over  list:
                              L
                          with  starting  value:
                            a)])


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index