Is there an algorithm which, given a string $s$, generates a sequence of $|s|$ strings, such that it can be proven in some axiomatic system $S$, that the Kolmogorov complexity of each successive term is smaller than the preceeding one?
We further impose a constraint that the terms of the strings themselves, do not decrease in length monotonically.