---

Step * 2 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|| ∈ ℤ
⊢ P[accumulate (with value a and list item x):
     f[a;x]
    over list:
      L
    with starting value:
     a);L]
BY
{ ((InstLemma `last_lemma` [⌜T⌝;⌜L⌝]⋅
    THENA (Auto
           THEN (D 0 THEN Auto)
           THEN (RWO "assert_of_null" (-1) THENA Auto)
           THEN HypSubst' (-1) (-2)
           THEN Reduce (-2)
           THEN Auto)
    )
   THEN ExRepD
   THEN HypSubst' (-1) 0) }

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)
⊢ 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||
\mvdash{}  P[accumulate  (with  value  a  and  list  item  x):
          f[a;x]
        over  list:
            L
        with  starting  value:
          a);L]


By

---

Latex:
((InstLemma  `last\_lemma`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
    THENA  (Auto
                  THEN  (D  0  THEN  Auto)
                  THEN  (RWO  "assert\_of\_null"  (-1)  THENA  Auto)
                  THEN  HypSubst'  (-1)  (-2)
                  THEN  Reduce  (-2)
                  THEN  Auto)
    )
  THEN  ExRepD
  THEN  HypSubst'  (-1)  0)

---

Home Index