何を証明するのか？

証明することは、この関数が最小手数を返していることです。最小手数であるというのはどういうことかというと、

どんな手順でロボットを動かしても、これより短くできない手数

のことです。というのは残念ながらよくある間違いです。

ある手順でロボットを動かせばその手数が達成できて、どんな手順で動かしても、それより短くできない手数

のことです。上の関数が最小手数を返すことを証明するには、実際にその手数でロボットを動かす手順を構成することと、それより短い手順がないことの２つを証明しないといけません。