Step
*
of Lemma
list_accum_cons_lemma
∀y,x,z,f:Top.
(accumulate (with value a and list item b):
f[a;b]
over list:
[x / y]
with starting value:
z) ~ accumulate (with value a and list item b):
f[a;b]
over list:
y
with starting value:
f[z;x]))
BY
{ ((UnivCD THENA Auto) THEN Try (RW (AddrC [1] (RecUnfoldC `list_accum` ANDTHENC ReduceC)) 0)⋅) }
1
1. y : Top
2. x : Top
3. z : Top
4. f : Top
⊢ accumulate (with value a and list item b):
f[a;b]
over list:
y
with starting value:
f[z;x]) ~ accumulate (with value a and list item b):
f[a;b]
over list:
y
with starting value:
f[z;x])
Latex:
Latex:
\mforall{}y,x,z,f:Top.
(accumulate (with value a and list item b):
f[a;b]
over list:
[x / y]
with starting value:
z) \msim{} accumulate (with value a and list item b):
f[a;b]
over list:
y
with starting value:
f[z;x]))
By
Latex:
((UnivCD THENA Auto) THEN Try (RW (AddrC [1] (RecUnfoldC `list\_accum` ANDTHENC ReduceC)) 0)\mcdot{})
Home
Index