---

Step * of Lemma list_accum_invariant3

∀[T,A:Type].
  ∀f:A ⟶ T ⟶ A
    ∀[P:A ⟶ (T List) ⟶ ℙ]
      ∀L:T List. ∀a:A.
        (P[a;[]]
        ⇒ (∀a:A. ∀x:T. ∀L':T List.  (L' @ [x] ≤ L ⇒ P[a;L'] ⇒ P[f[a;x];L' @ [x]]))
        ⇒ P[accumulate (with value a and list item x):
              f[a;x]
             over list:
               L
             with starting value:
              a);L])
BY
{ (Auto
   THEN (Assert ⌜∃n:ℕ. (n = ||L|| ∈ ℤ)⌝⋅ THENA (InstConcl [⌜||L||⌝]⋅ THEN Auto'))
   THEN ExRepD
   THEN MoveToConcl (-6)
   THEN MoveToConcl (-3)
   THEN NatInd (-1)
   THEN Auto) }

1
1. [T] : Type
2. [A] : Type
3. f : A ⟶ T ⟶ A
4. [P] : A ⟶ (T List) ⟶ ℙ
5. a : A
6. P[a;[]]
7. L : T List
8. ∀a:A. ∀x:T. ∀L':T List.  (L' @ [x] ≤ L ⇒ P[a;L'] ⇒ P[f[a;x];L' @ [x]])
9. 0 = ||L|| ∈ ℤ
⊢ P[accumulate (with value a and list item x):
     f[a;x]
    over list:
      L
    with starting value:
     a);L]

2
1. [T] : Type
2. [A] : Type
3. f : A ⟶ T ⟶ A
4. [P] : A ⟶ (T List) ⟶ ℙ
5. n : ℤ
6. [%1] : 0 < n
7. ∀a:A
     (P[a;[]]
     ⇒ (∀L:T List
           ((∀a:A. ∀x:T. ∀L':T List.  (L' @ [x] ≤ L ⇒ P[a;L'] ⇒ P[f[a;x];L' @ [x]]))
           ⇒ ((n - 1) = ||L|| ∈ ℤ)
           ⇒ P[accumulate (with value a and list item x):
                 f[a;x]
                over list:
                  L
                with starting value:
                 a);L])))
8. a : A
9. P[a;[]]
10. L : T List
11. ∀a:A. ∀x:T. ∀L':T List.  (L' @ [x] ≤ L ⇒ P[a;L'] ⇒ P[f[a;x];L' @ [x]])
12. n = ||L|| ∈ ℤ
⊢ P[accumulate (with value a and list item x):
     f[a;x]
    over list:
      L
    with starting value:
     a);L]

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mexists{}n:\mBbbN{}.  (n  =  ||L||)\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}||L||\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  ExRepD
  THEN  MoveToConcl  (-6)
  THEN  MoveToConcl  (-3)
  THEN  NatInd  (-1)
  THEN  Auto)

---

Home Index