Find n such that p(n) and not p(n-1).
p(n):
exists(f: state -> move) such that solves(f, n)
state: solved | illegal | (k, is_first_move in {T,F}, px in (1,2023), py in (1,2024+1), mapping from x,y to {T,F, ?})
initial_state(n): (n, T, 1, 1, {(x,y) -> ?})
move: U|D|L|R|(x in (1,2023))
power: ((a -> a), integer) -> (a->a)
power(h, 0)(x) = h(x)
power(h, k)(x) = h(power(k-1))(x)
solves(f, n): exists l such that for every board, power(make_move(board, f), l)(initial_state(n)) = solved
board: permutation of (1, 2, 3, ..., 2022+1)
make_move: (board, (state -> move)) -> (state -> state)
make_move(board, f)(solved): solved
make_move(board, f)(illegal): illegal
make_move(board, f)(s = (k, is_first_move, px, py, m))
if is_first_move = T:
if k = 0:
illegal
else if f(s) is a number:
(k, F, f(s), 1, m)
else:
illegal
else:
if f(s) is a number:
illegal
else if py = 2025:
solved
else if board(px) = py and py != 1:
(k - 1, T, px, py, m + {((px, py), T)})
else:
dy = {U:-1,D:1,L:0,R:0}(f(s))
dx = {U:0,D:0,L:-1,R:1}(f(s))
px' = px+dx
py' = py+dy
if px' < 1 or px' > 2023 or py' < 1 or py' > 2025:
illegal
(k, F, px', py', m + {((px, py), F)})