Step
*
2
2
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. ∀[bs:T List]
(∀[n:A]
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
v
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs
with starting value:
n)
∈ A)) supposing
(no_repeats(T;bs) and
no_repeats(T;v) and
set-equal(T;v;bs))
10. bs : T List
11. set-equal(T;[u / v];bs)
12. no_repeats(T;[u / v])
13. no_repeats(T;bs)
14. n : A
15. cs : T List
16. ds : T List
17. bs = (cs @ [u / ds]) ∈ (T List)
18. set-equal(T;v;cs @ ds)
19. ∀[as,bs:T List]. ∀[n:A].
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as @ bs
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs @ as
with starting value:
n)
∈ A)
⊢ accumulate (with value a and list item z):
f[a;g[z]]
over list:
v
with starting value:
f[n;g[u]])
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
cs @ [u / ds]
with starting value:
n)
∈ A
BY
{ (((RWO "-1" 0 THENA Auto) THEN Reduce 0) THEN BHyp 9 THEN 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. ∀[bs:T List]
(∀[n:A]
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
v
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs
with starting value:
n)
∈ A)) supposing
(no_repeats(T;bs) and
no_repeats(T;v) and
set-equal(T;v;bs))
10. bs : T List
11. set-equal(T;[u / v];bs)
12. no_repeats(T;[u / v])
13. no_repeats(T;bs)
14. n : A
15. cs : T List
16. ds : T List
17. bs = (cs @ [u / ds]) ∈ (T List)
18. set-equal(T;v;cs @ ds)
19. ∀[as,bs:T List]. ∀[n:A].
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as @ bs
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs @ as
with starting value:
n)
∈ A)
⊢ set-equal(T;v;ds @ cs)
2
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. ∀[bs:T List]
(∀[n:A]
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
v
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs
with starting value:
n)
∈ A)) supposing
(no_repeats(T;bs) and
no_repeats(T;v) and
set-equal(T;v;bs))
10. bs : T List
11. set-equal(T;[u / v];bs)
12. no_repeats(T;[u / v])
13. no_repeats(T;bs)
14. n : A
15. cs : T List
16. ds : T List
17. bs = (cs @ [u / ds]) ∈ (T List)
18. set-equal(T;v;cs @ ds)
19. ∀[as,bs:T List]. ∀[n:A].
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as @ bs
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs @ as
with starting value:
n)
∈ A)
⊢ no_repeats(T;v)
3
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. ∀[bs:T List]
(∀[n:A]
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
v
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs
with starting value:
n)
∈ A)) supposing
(no_repeats(T;bs) and
no_repeats(T;v) and
set-equal(T;v;bs))
10. bs : T List
11. set-equal(T;[u / v];bs)
12. no_repeats(T;[u / v])
13. no_repeats(T;bs)
14. n : A
15. cs : T List
16. ds : T List
17. bs = (cs @ [u / ds]) ∈ (T List)
18. set-equal(T;v;cs @ ds)
19. ∀[as,bs:T List]. ∀[n:A].
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as @ bs
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs @ as
with starting value:
n)
∈ A)
⊢ no_repeats(T;ds @ cs)
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. \mforall{}[bs:T List]
(\mforall{}[n:A]
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
v
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs
with starting value:
n))) supposing
(no\_repeats(T;bs) and
no\_repeats(T;v) and
set-equal(T;v;bs))
10. bs : T List
11. set-equal(T;[u / v];bs)
12. no\_repeats(T;[u / v])
13. no\_repeats(T;bs)
14. n : A
15. cs : T List
16. ds : T List
17. bs = (cs @ [u / ds])
18. set-equal(T;v;cs @ ds)
19. \mforall{}[as,bs:T List]. \mforall{}[n:A].
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as @ bs
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs @ as
with starting value:
n))
\mvdash{} accumulate (with value a and list item z):
f[a;g[z]]
over list:
v
with starting value:
f[n;g[u]])
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
cs @ [u / ds]
with starting value:
n)
By
Latex:
(((RWO "-1" 0 THENA Auto) THEN Reduce 0) THEN BHyp 9 THEN Auto)
Home
Index