Problem
=======
let there a finite set of mines (positive integers), and
a finite set of jumps (positive integers), and
let size = sum(jumps)
assume that
* there are fever mines than jumps
* every mine is strictly between zero and sum(jumps)
prove that it is possible to arrange the jumps into a list
jumps_l in such a way that no prefix sum of jumps_l
coincide with a mine.
Proof
=====
By induction on the size of jumps.
1) There must be at least one jump to satisfy the condition |jumps| > |mines|
2) If there is just one jump, there is no mine and we are done. For the remaining proof
assume there are at least two jumps.
3) Take the biggest jump from jumps, leaving the remaining set
jumps_rem.
* note: it should be obvious at this point that if we arrange
jumps_rem and add jump to it, we get an arrangement of jumps
4) let mines_sub = map (-jump) mines
5) analyze three cases
A) There is zero in mines_sub
B) There is no non-positive number in mines_sub
C) There are some negative numbers in mines_sub but not zero
A1) Let mines_rem = { x > 0 | x in mines_sub } + { x < jump and x < sum(jumps_rem) | x in mines }
A2) Observe |mines_rem| < |jumps_rem| because we removed the zero jump, and every
other mine just was shifted by jump or not (some mines could be glued but we don't case about that).
A3) Apply the induction hypothesis to mines_rem, jumps_rem, getting an arrangement jumps_rem_l.
A4) let jump2::jumps_rem_l2 = jumps_rem_l
A5) Observe jump2 is not in mines since all mines that could coincide with jump2 were preserved in
jumps_rem.
A5) Observe no jump + sum(any non-empty prefix sum of jumps_rem_l) coincide with a mine from mines since
no non-empty prefix sum of jumps_rem_l coincide with mines_sub
A6) The arrangement jump2::jump::jumps_rem_l2 satisfies the requirement.
B1) Let mine be jump+(the smallest element of mines_sub), and let mines_rem be the rest of mines_sub
note: apparently, mine is also the smallest element of mines
B2) Apply the induction hypothesis to mines_rem, jumps_rem, getting arrangement jumps_rem_l
B3) let jumps_cand = jump::jumps_rem_l
B4) Observe that mine is the only possible prefix sum of jumps_cand coinciding with mines.
B5) If no prefix sum of jumps_cand equals mine, we are done, assume otherwise.
B6) Let jumps_cand = (jump::pref) + (jump2::suff) so that sum(jump::pref) = mine
note that jump is still the biggest jump
B7) Then the following arrangement of jumps is valid: (jump2::pref) + (jump::suff) because
* sum(jump2::pref) < mine, so no prefix of jump2::pref coincides with a mine
* the further prefix sums coincide with the prefix sums of jumps_cand
C1) Let mines_rem = { x > 0 | x in mines_sub }
C2) Apply the induction hypothesis to mines_rem, jumps_rem, getting an arrangement jumps_rem_l.
C3) jump::jumps_rem_l is a valid arrangement of jumps