law open_safe

minebender-game@1.0.0.0 · LAWS.bend:355

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

355# LAW: "Revealing a safe cell never loses."
356law open_safe:
357  for w: Nat
358  for h: Nat
359  for layout: T.Grid(Bool)
360  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
361  for g: G.Game
362  for r: Reachable(w, h, layout, g)
363  for playing: {G.status(g) == T.Playing{} : T.Status}
364  for p: T.Pos
365  for safe: {mine(layout, p) == False{} : Bool}
366  {is_lost(G.status(G.open(g, p))) == False{} : Bool}