law check_agree

minebender-game@1.0.0.0 · proof_solver.bend:653

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

653law check_agree:
654  for +w: Nat
655  for +h: Nat
656  for +n: Nat
657  for +rows: T.Grid(T.Seen)
658  for +its: List<&2, S.Item>
659  for +l1: T.Grid(Bool)
660  for +l2: T.Grid(Bool)
661  for +sh1: {B.shaped(Bool, w, h, l1) == True{} : Bool}
662  for +sh2: {B.shaped(Bool, w, h, l2) == True{} : Bool}
663  for +ag: {agree(w, h, l1, l2) == True{} : Bool}
664  for +ion: {items_onb(PS.WH{w, h}, its) == True{} : Bool}
665  {S.check(S.Ctx{w, h, n, rows, its}, l1) == S.check(S.Ctx{w, h, n, rows, its}, l2) : Bool}