def item_ok_agree

minebender-game@1.0.0.0 · proof_solver.bend:610

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

610def item_ok_agree(+w: Nat, +h: Nat, +l1: T.Grid(Bool), +l2: T.Grid(Bool), +ag: {agree(w, h, l1, l2) == True{} : Bool},
611  +p: T.Pos, +s: T.Seen, +ns: List<&2, T.Pos>, on: {B.on_board(w, h, p) == True{} : Bool},
612  ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns) == True{} : Bool}) ->
613  {S.item_ok(s, p, ns, l1) == S.item_ok(s, p, ns, l2) : Bool}:
614  match s:
615    case T.Hidden{}:
616      {==}
617    case T.Shown{k}:
618      %Equal.sym(Bool, B.mine(l1, p), B.mine(l2, p), agree_cell(w, h, l1, l2, ag, p, on)) :
619        {Bool.and(Bool.not(_), Nat.is_eq(B.count_mines(l1, ns), k)) == Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(B.count_mines(l2, ns), k)) : Bool}
620      %Equal.sym(Nat, B.count_mines(l1, ns), B.count_mines(l2, ns), count_agree(w, h, l1, l2, ag, ns, ons)) :
621        {Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(_, k)) == Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(B.count_mines(l2, ns), k)) : Bool}
622      {==}
623    case T.Boom{}:
624      agree_cell(w, h, l1, l2, ag, p, on)