---

Step * 1 of Lemma list_accum_invariant3


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]
BY
{ ((Assert ⌜||L|| = 0 ∈ ℤ⌝⋅ THENA Auto)
   THEN (RWO "length_zero" (-1) THENA Auto)
   THEN HypSubst' (-1) 0⋅
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  f  :  A  {}\mrightarrow{}  T  {}\mrightarrow{}  A
4.  [P]  :  A  {}\mrightarrow{}  (T  List)  {}\mrightarrow{}  \mBbbP{}
5.  a  :  A
6.  P[a;[]]
7.  L  :  T  List
8.  \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]])
9.  0  =  ||L||
\mvdash{}  P[accumulate  (with  value  a  and  list  item  x):
          f[a;x]
        over  list:
            L
        with  starting  value:
          a);L]


By

---

Latex:
((Assert  \mkleeneopen{}||L||  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "length\_zero"  (-1)  THENA  Auto)
  THEN  HypSubst'  (-1)  0\mcdot{}
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index