law count_after

minebender-game@1.0.0.0 · proof_flood.bend:283

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

283law count_after:
284  for +w: Nat
285  for +h: Nat
286  for +shown: T.Grid(Bool)
287  for +c: T.Pos
288  for +m: Nat
289  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
290  for +u: {G.unrevealed(w, h, shown, c) == True{} : Bool}
291  for cnt: {1n+m == B.count_false(shown) : Nat}
292  {m == B.count_false(B.set_at(Bool, shown, c, True{})) : Nat}