law closed_flood

minebender-game@1.0.0.0 · proof_inv.bend:151

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

151# A flood from a closed grid leaves a closed grid.
152law closed_flood:
153  for +n: Nat
154  for +work: List<&2, G.Work>
155  for +hd: Bool
156  for +w: Nat
157  for +h: Nat
158  for +layout: T.Grid(Bool)
159  for +shown: T.Grid(Bool)
160  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
161  for +cl: {closed(w, h, layout, shown) == True{} : Bool}
162  for +cnt: {n == B.count_false(shown) : Nat}
163  for +he: {G.head_hidden(w, h, shown, work) == hd : Bool}
164  {closed(w, h, layout, G.flood(n, work, hd, w, h, layout, shown)) == True{} : Bool}