law flood_complete

minebender-game@1.0.0.0 · LAWS.bend:368

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

368# LAW: "Revealing a cell p reveals every cell reached from p by a path
369# through zeros" (so a 0 opens its whole 0-region and the numbers around it;
370# for a mine, that is p alone).
371law flood_complete:
372  for w: Nat
373  for h: Nat
374  for layout: T.Grid(Bool)
375  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
376  for g: G.Game
377  for r: Reachable(w, h, layout, g)
378  for playing: {G.status(g) == T.Playing{} : T.Status}
379  for p: T.Pos
380  for on: {on_board(w, h, p) == True{} : Bool}
381  for q: T.Pos
382  for path: List<&2, T.Pos>
383  for walk: {zero_walk(path, w, h, layout, p, q) == True{} : Bool}
384  {revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}