ゆとり変換

ここまで証明できればあと少しです。初期位置の違いはゆとりポイントの初期値の違いと等価なはずです。

Lemma min_trans_1_0:
  forall (os: list Order) (bp op bp' op' bd:Z),
  Zabs bd = 1 ->
  exists d, Zabs d = 1 /\
    min_trans bp op (bp'+bd) op' os = min_trans (bp+d) op bp' op' os.

青のロボットの初期位置が1だけずれてるのは、ゆとりポイントを１だけ増やすか減らすかしたのと同等である。これくらいのことになってやっと自明といえるレベルです。