law flood_exact_c

minebender-game@1.0.0.0 · proof_laws.bend:838

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

838law flood_exact_c:
839  for +w: Nat
840  for +h: Nat
841  for +layout: T.Grid(Bool)
842  for +s: T.Grid(Bool)
843  for +f: List<&2, T.Pos>
844  for +p: T.Pos
845  for +q: T.Pos
846  for before: {L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q) == True{} : Bool}
847  for after: {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}
848  PF.Walk(w, h, layout, p, q)