law flood_mono

minebender-game@1.0.0.0 · proof_flood.bend:118

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

118law flood_mono:
119  for +n: Nat
120  for +work: List<&2, G.Work>
121  for +hd: Bool
122  for +w: Nat
123  for +h: Nat
124  for +layout: T.Grid(Bool)
125  for +shown: T.Grid(Bool)
126  for +q: T.Pos
127  for +s: {B.at(Bool, False{}, shown, q) == True{} : Bool}
128  {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}