law unrev_shown

minebender-game@1.0.0.0 · proof_flood.bend:270

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

270law unrev_shown:
271  for +w: Nat
272  for +h: Nat
273  for +shown: T.Grid(Bool)
274  for +c: T.Pos
275  for e: {G.unrevealed(w, h, shown, c) == False{} : Bool}
276  for on: {B.on_board(w, h, c) == True{} : Bool}
277  {B.at(Bool, False{}, shown, c) == True{} : Bool}