---

Step * 2 1 of Lemma list_accum_invariant3


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|| ∈ ℤ
13. L' : T List
14. L = (L' @ [last(L)]) ∈ (T List)
⊢ P[accumulate (with value a and list item x):
     f[a;x]
    over list:
      L' @ [last(L)]
    with starting value:
     a);L' @ [last(L)]]
BY
{ (Assert ¬↑null(L) BY
         ((D 0 THEN Auto)
          THEN (RWO "assert_of_null" (-1) THENA Auto)
          THEN HypSubst' (-1) (-4)
          THEN Reduce (-4)
          THEN Auto)) }

1
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|| ∈ ℤ
13. L' : T List
14. L = (L' @ [last(L)]) ∈ (T List)
15. ¬↑null(L)
⊢ P[accumulate (with value a and list item x):
     f[a;x]
    over list:
      L' @ [last(L)]
    with starting value:
     a);L' @ [last(L)]]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  f  :  A  {}\mrightarrow{}  T  {}\mrightarrow{}  A
4.  [P]  :  A  {}\mrightarrow{}  (T  List)  {}\mrightarrow{}  \mBbbP{}
5.  n  :  \mBbbZ{}
6.  [\%1]  :  0  <  n
7.  \mforall{}a:A
          (P[a;[]]
          {}\mRightarrow{}  (\mforall{}L:T  List
                      ((\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{}  ((n  -  1)  =  ||L||)
                      {}\mRightarrow{}  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.  \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]])
12.  n  =  ||L||
13.  L'  :  T  List
14.  L  =  (L'  @  [last(L)])
\mvdash{}  P[accumulate  (with  value  a  and  list  item  x):
          f[a;x]
        over  list:
            L'  @  [last(L)]
        with  starting  value:
          a);L'  @  [last(L)]]


By

---

Latex:
(Assert  \mneg{}\muparrow{}null(L)  BY
              ((D  0  THEN  Auto)
                THEN  (RWO  "assert\_of\_null"  (-1)  THENA  Auto)
                THEN  HypSubst'  (-1)  (-4)
                THEN  Reduce  (-4)
                THEN  Auto))

---

Home Index