law nsm_flood

minebender-game@1.0.0.0 · proof_inv.bend:396

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

396# A flood from a safe cell reveals no mine.
397law nsm_flood:
398  for +n: Nat
399  for +work: List<&2, G.Work>
400  for +hd: Bool
401  for +w: Nat
402  for +h: Nat
403  for +layout: T.Grid(Bool)
404  for +shown: T.Grid(Bool)
405  for +p0: T.Pos
406  for +safe: {L.mine(layout, p0) == False{} : Bool}
407  for +ok: {PF.works_ok(work, w, h, layout, p0) == True{} : Bool}
408  for +ns: {nsm(w, h, layout, shown) == True{} : Bool}
409  {nsm(w, h, layout, G.flood(n, work, hd, w, h, layout, shown)) == True{} : Bool}