law walk_on

minebender-game@1.0.0.0 · proof_walk.bend:154

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/LAWS.bend as L

154# A walk ends on the board when it starts there.
155law walk_on:
156  for +path: List<&2, T.Pos>
157  for +w: Nat
158  for +h: Nat
159  for +layout: T.Grid(Bool)
160  for +s: T.Pos
161  for +q: T.Pos
162  for +wk: {L.zero_walk(path, w, h, layout, s, q) == True{} : Bool}
163  for +on: {L.on_board(w, h, s) == True{} : Bool}
164  {L.on_board(w, h, q) == True{} : Bool}