And with a sense of appalling inevitability, I am obliged to confess that Warren's intuition is once again proved prescient: my optimistically floated proof of Lemma 2 is indeed unfit for purpose, for much the same reason as previously: an implicit inductive assumption that d(x-2, y-1) < d(x, y) . It now seems inevitable that any proof of d = f is going to involve some mildly gruesome grappling with details, overlapping to a large extent existing published attacks on counting the number of cells at distance d . Miller & Farnsworth "Counting the Number of Squares Reachable in k Knight's Moves" http://dx.doi.org/10.4236/ojdm.2013.33027 give a reasonable informal account of the geometrical approach, although I have reservations about how far it qualifies as a copper-fastened proof. Katzman "Counting monomials" http://www.katzman.staff.shef.ac.uk/Articles/CountingMonomials.pdf employs an algebraic approach via Hilbert functions. Er, I might get back later about this ... Warren envisages a CAS-based computation establishing functional equivalence. This ain't on the cards any time soon --- not at least using Maple, as the script attached below illustrates --- two allegedly equal symbolic expressions h, h0 evaluating to incompatible numerical results. Fred Lunnon _______________________________ # Attempted automated proof, after Warren Smith f := proc (x, y) # conjectured counting function local X,Y,p,q,r; X := max(abs(x), abs(y)); Y := min(abs(x), abs(y)); if [X, Y] = [1, 0] then 3 elif [X, Y] = [2, 2] then 4 else p := X-Y; q := p-Y; r := (7 + signum(2*q+1))/2; p - 2*floor(q/r) fi end; h := proc (x, y) # test recursive distance property if [x, y] = [0, 0] then 0 else f(x, y) - 1 - min( f(x-2, y-1), f(x-2, y+1), f(x-1, y-2), f(x-1, y+2), f(x+2, y-1), f(x+2, y+1), f(x+1, y-2), f(x+1, y+2) ) fi end; n := 10; m := 1; # range of numerical verification { seq(seq(h(i, j), j = -n..+n), i = -n..+n) }; # { 0 } ; at all points on n x n board --- OK !! [ seq([ seq(h(i, j), j = -m..+m) ], i = -m..+m) ]; # [ [ 0, 0, 0 ], [ 0, 0, 0 ], [ 0, 0, 0 ] ] assume(x::integer, y::integer); h0 := h(x, y); # output one page long { seq(seq(eval(subs({x = j, y = i}, h0)), j = -n..+n), i = -n..+n) }; # { -2, 0 } ; special value 3 in f() ignored --- BUG ?? [ seq([ seq(eval(subs({x = j, y = i}, h0)), j = -1..+1) ], i = -1..+1) ]; # [ [ 0, -2, 0 ], [ -2, -2, -2 ], [ 0, -2, 0 ] ] _______________________________