def items_agrees.cell

minebender-game@1.0.0.0 · proof_solver.bend:1355

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/LAWS.bend as L
import minebender-game@1.0.0.0/proof_copy.bend as PC

1355def items_agrees.cell(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +layout: T.Grid(Bool), +p: T.Pos,
1356  +t: List<&2, T.Pos>, +s: T.Seen,
1357  ih: {S.items_ok(S.items(w, h, rows, t), layout) == L.agrees_all(w, h, rows, layout, t) : Bool}) ->
1358  {S.items_ok(S.items.put(s, p, w, h, S.items(w, h, rows, t)), layout)
1359    == Bool.and(L.agrees(w, h, layout, p, s), L.agrees_all(w, h, rows, layout, t)) : Bool}:
1360  match s:
1361    case T.Hidden{}:
1362      ih
1363    case T.Shown{k}:
1364      %PC.mine_eq(layout, p) :
1365        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.count_mines(layout, B.neighbours(w, h, p)), k)),
1366          S.items_ok(S.items(w, h, rows, t), layout))
1367          == Bool.and(Bool.and(Bool.not(_), Nat.is_eq(L.adj_mines(w, h, layout, p), k)), L.agrees_all(w, h, rows, layout, t)) : Bool}
1368      %PC.adj_mines_eq(w, h, layout, p) :
1369        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), k)),
1370          S.items_ok(S.items(w, h, rows, t), layout))
1371          == Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(_, k)), L.agrees_all(w, h, rows, layout, t)) : Bool}
1372      %Equal.sym(Bool, S.items_ok(S.items(w, h, rows, t), layout), L.agrees_all(w, h, rows, layout, t), ih) :
1373        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), k)), _)
1374          == Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), k)), L.agrees_all(w, h, rows, layout, t)) : Bool}
1375      {==}
1376    case T.Boom{}:
1377      %PC.mine_eq(layout, p) :
1378        {Bool.and(B.mine(layout, p), S.items_ok(S.items(w, h, rows, t), layout))
1379          == Bool.and(_, L.agrees_all(w, h, rows, layout, t)) : Bool}
1380      %Equal.sym(Bool, S.items_ok(S.items(w, h, rows, t), layout), L.agrees_all(w, h, rows, layout, t), ih) :
1381        {Bool.and(B.mine(layout, p), _) == Bool.and(B.mine(layout, p), L.agrees_all(w, h, rows, layout, t)) : Bool}
1382      {==}