law flood_exact_

minebender-game@1.0.0.0 · proof_laws.bend:994

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

994law flood_exact_:
995  for +w: Nat
996  for +h: Nat
997  for +layout: T.Grid(Bool)
998  for shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}
999  for +g: G.Game
1000  for r: L.Reachable(w, h, layout, g)
1001  for +playing: {G.status(g) == T.Playing{} : T.Status}
1002  for +p: T.Pos
1003  for +q: T.Pos
1004  for before: {L.hidden(G.knowledge(g), q) == True{} : Bool}
1005  for after: {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}
1006  PF.Walk(w, h, layout, p, q)