law items_ok_agree

minebender-game@1.0.0.0 · proof_solver.bend:626

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S
import minebender-game@1.0.0.0/proof_cells.bend as PS

626law items_ok_agree:
627  for +w: Nat
628  for +h: Nat
629  for +l1: T.Grid(Bool)
630  for +l2: T.Grid(Bool)
631  for +ag: {agree(w, h, l1, l2) == True{} : Bool}
632  for +its: List<&2, S.Item>
633  for +ion: {items_onb(PS.WH{w, h}, its) == True{} : Bool}
634  {S.items_ok(its, l1) == S.items_ok(its, l2) : Bool}