d:
. sum(L[x]-L[i--][x] | x < ||L||) = d 
sum(L[x] | x < ||L||) = sum(L[i--][x] | x < ||L||)+d
sum(L[i--][i@0] | i@0 < ||L||) = d-1 
(L: List. 0 < ||L|| (
r:
. r- > L^k-1))
k = 1
d1:. d1 < d (L: List. sum(L[i] | i < ||L||) = d1 0 < ||L|| (r:. r- > L^k))
List
(i:||L||. L[i] < k)
i:||L||. 2
L[i]
L: List. sum(L[i] | i < ||L||) = d-1 0 < ||L|| (r:. r- > L^k)
||L||
sum(L[i--][i@0] | i@0 < ||L||) = d-1
n:, f,g:(n
), d:. sum(f(x)-g(x) | x < n) = d sum(f(x) | x < n) = sum(g(x) | x < n)+d
[||L||;
j. L[j];j. L[i--][j]])
THENA
(Auto THEN (AutoInst [i])
THEN
(RWO
Thm* L: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L||
0)
THEN
(AutoInst [i]))
| 1 | 15. d:. sum(L[x]-L[i--][x] | x < ||L||) = d sum(L[x] | x < ||L||) = sum(L[i--][x] | x < ||L||)+d sum(L[i--][i@0] | i@0 < ||L||) = d-1 | 7 steps |
About:
 |  |  |  |  |  |
 |  |  |  |
 |