---

Step * 1 1 of Lemma list_accum_set-equal


1. T : Type
2. A : Type
3. g : T ⟶ A
4. f : A ⟶ A ⟶ A
5. Comm(A;λx,y. f[x;y])
6. Assoc(A;λx,y. f[x;y])
7. u : T
8. v : T List
9. set-equal(T;[];[u / v])
10. no_repeats(T;[])
11. no_repeats(T;[u / v])
12. n : A
⊢ n = accumulate (with value a and list item z): f[a;g[z]]over list:  vwith starting value: f[n;g[u]]) ∈ A
BY
{ (UnfoldTopAb  (-4) THEN (InstHyp [⌜u⌝] (-4)⋅ THENA Auto)) }

1
1. T : Type
2. A : Type
3. g : T ⟶ A
4. f : A ⟶ A ⟶ A
5. Comm(A;λx,y. f[x;y])
6. Assoc(A;λx,y. f[x;y])
7. u : T
8. v : T List
9. ∀t:T. ((t ∈ []) ⇐⇒ (t ∈ [u / v]))
10. no_repeats(T;[])
11. no_repeats(T;[u / v])
12. n : A
13. (u ∈ []) ⇐⇒ (u ∈ [u / v])
⊢ n = accumulate (with value a and list item z): f[a;g[z]]over list:  vwith starting value: f[n;g[u]]) ∈ A

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  g  :  T  {}\mrightarrow{}  A
4.  f  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A
5.  Comm(A;\mlambda{}x,y.  f[x;y])
6.  Assoc(A;\mlambda{}x,y.  f[x;y])
7.  u  :  T
8.  v  :  T  List
9.  set-equal(T;[];[u  /  v])
10.  no\_repeats(T;[])
11.  no\_repeats(T;[u  /  v])
12.  n  :  A
\mvdash{}  n
=  accumulate  (with  value  a  and  list  item  z):
      f[a;g[z]]
    over  list:
        v
    with  starting  value:
      f[n;g[u]])


By

---

Latex:
(UnfoldTopAb    (-4)  THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto))

---

Home Index