kikx https://blog.hatena.ne.jp/kikx/ 菊やんの雑記帳 https://kikx.hatenadiary.org/ これより短い手順がないことを証明するには、手順とはなにかを定義しないといけません。 Inductive Move : Set := Left | Right | Push | Stay. Inductive Moves : Set := moves : Move -> Move -> Moves.各ロボットは１ターンに４種類の行動ができて、青のと橙のとの行動のペアが１ターンの手になります。list Movesが手順になります。この手順が命令列を正しく実行するかの述語が必要です。 Definition correct_moves (bp op: Z) (ms: list Moves) (os: … 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fkikx.hatenadiary.org%2Fentry%2F20110509%2F1304947969" title=" とりあえず、これより短い手順がないこと - 菊やんの雑記帳" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2011-05-09 22:32:49 rich https://kikx.hatenadiary.org/entry/20110509/1304947969 1.0 100%