law monotone

minebender-game@1.0.0.0 · LAWS.bend:315

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

315# LAW: "A revealed cell stays revealed, showing the same thing."
316# With bridge, this makes every action that changes the knowledge reveal at least
317# one more cell, so a game has at most w*h such actions.
318law monotone:
319  for w: Nat
320  for h: Nat
321  for layout: T.Grid(Bool)
322  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
323  for g: G.Game
324  for r: Reachable(w, h, layout, g)
325  for a: T.Action
326  for q: T.Pos
327  for vis: {revealed(G.knowledge(g), q) == True{} : Bool}
328  {seen(G.knowledge(G.step(g, a)), q) == seen(G.knowledge(g), q) : T.Seen}