law flood_work

minebender-game@1.0.0.0 · proof_flood.bend:370

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

370# A queued cell of the board ends up revealed (given n counts the
371# unrevealed cells).
372law flood_work:
373  for +n: Nat
374  for +work: List<&2, G.Work>
375  for +hd: Bool
376  for +w: Nat
377  for +h: Nat
378  for +layout: T.Grid(Bool)
379  for +shown: T.Grid(Bool)
380  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
381  for +cnt: {n == B.count_false(shown) : Nat}
382  for +he: {G.head_hidden(w, h, shown, work) == hd : Bool}
383  for +q: T.Pos
384  for +on: {B.on_board(w, h, q) == True{} : Bool}
385  for m: {wcontains(work, q) == True{} : Bool}
386  {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}