law path_closed

minebender-game@1.0.0.0 · proof_laws.bend:620

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_inv.bend as PI

620# In a closed grid, a zero walk from a revealed cell ends at a revealed cell.
621law path_closed:
622  for +path: List<&2, T.Pos>
623  for +w: Nat
624  for +h: Nat
625  for +layout: T.Grid(Bool)
626  for +g: T.Grid(Bool)
627  for +cl: {PI.closed(w, h, layout, g) == True{} : Bool}
628  for +s: T.Pos
629  for +q: T.Pos
630  for gs: {B.at(Bool, False{}, g, s) == True{} : Bool}
631  for +wk: {L.zero_walk(path, w, h, layout, s, q) == True{} : Bool}
632  {B.at(Bool, False{}, g, q) == True{} : Bool}