---

Step * 2 1 1 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)
15. ¬↑null(L)
⊢ P[accumulate (with value a and list item x):
     f[a;x]
    over list:
      L'
    with starting value:
     a);L']
BY
{ (BHyp (-9) 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)
16. a1 : A
17. x : T
18. L1 : T List
19. L1 @ [x] ≤ L'
20. P[a1;L1]
⊢ P[f[a1;x];L1 @ [x]]

2
1. T : Type
2. A : Type
3. f : A ⟶ T ⟶ A
4. P : A ⟶ (T List) ⟶ ℙ
5. n : ℤ
6. 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)
⊢ (n - 1) = ||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)])
15.  \mneg{}\muparrow{}null(L)
\mvdash{}  P[accumulate  (with  value  a  and  list  item  x):
          f[a;x]
        over  list:
            L'
        with  starting  value:
          a);L']


By

---

Latex:
(BHyp  (-9)  THEN  Auto)\mcdot{}

---

Home Index