---

Step * of Lemma list_accum_invariant2

∀[T,A:Type].
  ∀f:A ⟶ T ⟶ A
    ∀[P:A ⟶ ℙ]
      ∀L:T List. ∀a:A.
        (P[a]
        ⇒ (∀a:A. ∀x:T.  ((x ∈ L) ⇒ 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 RepeatFor 2 ((BackThruSomeHyp THEN Auto))
   THEN GenListD 0⋅
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN Try (Complete ((OrRight 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.    ((x  \mmember{}  L)  {}\mRightarrow{}  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  RepeatFor  2  ((BackThruSomeHyp  THEN  Auto))
  THEN  GenListD  0\mcdot{}
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  Try  (Complete  ((OrRight  THEN  Auto))))

---

Home Index