Nope. Upon reconsideration, my "repair of Lunnon's proof" still was inadequate. True situation is more complicated. What you really need, is to prove f(x,y) = min( f(x-1,y-2), f(x+1,y-2), f(x+2,y-1), ... , f(x-1,y+2) ) with 8 arguments inside the min. That is a pretty nasty recurrence. Lunnon thought with his "sorted x,y" trick he could get rid of the nastiness, and that plus his simplified form of my algorithm yielded his proof. But, while I think that thought is largely true, it is not then as trivial as he thought. Thus in the main "case i" besides (x',y') = (x-2, y-1) we really also need to consider (x',y')=(x-2, y+1), for example. [It may actually be that proving this is a good case for a computer symbolic manipulation program to do, not a human prover. Can we just make it verify the full f(x,y) function obeys the full 8-argument recurrence, and be done?] I think it should now be doable even by a mere human, but there are enough cases and enough error-potential that it is a pain.