law open_ok_sound

minebender-game@1.0.0.0 · proof_solver.bend:383

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/solver.bend as S
import minebender-game@1.0.0.0/proof_cells.bend as PS

383# A partial layout that a consistent layout completes is never pruned.
384law open_ok_sound:
385  for +w: Nat
386  for +h: Nat
387  for +n: Nat
388  for +part: T.Grid(Maybe<&2, Bool>)
389  for +rel: List<&2, S.Item>
390  for +layout: T.Grid(Bool)
391  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
392  for +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool}
393  for +comp: {completes(w, h, part, layout) == True{} : Bool}
394  for tot: {B.total_mines(layout) == n : Nat}
395  for rok: {S.items_ok(rel, layout) == True{} : Bool}
396  for ron: {items_onb(PS.WH{w, h}, rel) == True{} : Bool}
397  {S.open_ok(part, rel, n) == True{} : Bool}