law open_safe_c

minebender-game@1.0.0.0 · proof_laws.bend:736

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
import minebender-game@1.0.0.0/LAWS.bend as L

736law open_safe_c:
737  for +w: Nat
738  for +h: Nat
739  for +layout: T.Grid(Bool)
740  for +s: T.Grid(Bool)
741  for +f: List<&2, T.Pos>
742  for +p: T.Pos
743  for bm: {B.mine(layout, p) == False{} : Bool}
744  {L.is_lost(G.status(G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p))) == False{} : Bool}