law at_set_mono

minebender-game@1.0.0.0 · proof_flood.bend:75

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

75# Revealing a cell keeps every revealed cell revealed.
76law at_set_mono:
77  for +g: T.Grid(Bool)
78  for +p: T.Pos
79  for +q: T.Pos
80  for e: {B.at(Bool, False{}, g, q) == True{} : Bool}
81  {B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q) == True{} : Bool}