0 < k-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

sum(L[i] | i < ||L||) = d

(i:||L||. L[i] < k)

i:||L||. 2L[i]

L: List. sum(L[i] | i < ||L||) = d-1 0 < ||L|| (r:. r- > L^k)

i:||L||r:r- > L[i--]^k

R: List. ||R|| = ||L|| & (i:||L||. 0 < L[i] R[i]- > L[i--]^k)

InstConcl [mklist(||L||;i.1of(f(i)))]

1	mklist(||L||;i.1of(f(i))) List	1 step
2	||mklist(||L||;i.1of(f(i)))|| = ||L|| & (i:||L||. 0 < L[i] mklist(||L||;i.1of(f(i)))[i]- > L[i--]^k)	4 steps
3	15. R: List (||R|| = ||L|| & (i:||L||. 0 < L[i] R[i]- > L[i--]^k)) Prop	Auto

About: