law comp_set

minebender-game@1.0.0.0 · proof_solver.bend:832

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/proof_cells.bend as PS

832law comp_set:
833  for +w: Nat
834  for +h: Nat
835  for +c: T.Pos
836  for +part: T.Grid(Maybe<&2, Bool>)
837  for +layout: T.Grid(Bool)
838  for +bv: Bool
839  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
840  for +mc: {B.mine(layout, c) == bv : Bool}
841  for +ps: List<&2, T.Pos>
842  for +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}
843  for +cm: {PS.allp(~CE, ~cmp_f, CE{part, layout}, ps) == True{} : Bool}
844  {PS.allp(~CE, ~cmp_f, CE{B.set_at(Maybe<&2, Bool>, part, c, Some{bv}), layout}, ps) == True{} : Bool}