ProofSolver.items_agrees.cell: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 1355-1382 of minebender-game@1.0.0.0/proof_solver.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_solver.bend&start_line=1355&end_line=1382

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

def items_agrees.cell(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +layout: T.Grid(Bool), +p: T.Pos,
  +t: List<&2, T.Pos>, +s: T.Seen,
  ih: {S.items_ok(S.items(w, h, rows, t), layout) == L.agrees_all(w, h, rows, layout, t) : Bool}) ->
  {S.items_ok(S.items.put(s, p, w, h, S.items(w, h, rows, t)), layout)
    == Bool.and(L.agrees(w, h, layout, p, s), L.agrees_all(w, h, rows, layout, t)) : Bool}:
  match s:
    case T.Hidden{}:
      ih
    case T.Shown{k}:
      %PC.mine_eq(layout, p) :
        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.count_mines(layout, B.neighbours(w, h, p)), k)),
          S.items_ok(S.items(w, h, rows, t), layout))
          == 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}
      %PC.adj_mines_eq(w, h, layout, p) :
        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), k)),
          S.items_ok(S.items(w, h, rows, t), layout))
          == Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(_, k)), L.agrees_all(w, h, rows, layout, t)) : Bool}
      %Equal.sym(Bool, S.items_ok(S.items(w, h, rows, t), layout), L.agrees_all(w, h, rows, layout, t), ih) :
        {Bool.and(Bool.and(Bool.not(B.mine(layout, p)), Nat.is_eq(B.adj_mines(w, h, layout, p), k)), _)
          == 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}
      {==}
    case T.Boom{}:
      %PC.mine_eq(layout, p) :
        {Bool.and(B.mine(layout, p), S.items_ok(S.items(w, h, rows, t), layout))
          == Bool.and(_, L.agrees_all(w, h, rows, layout, t)) : Bool}
      %Equal.sym(Bool, S.items_ok(S.items(w, h, rows, t), layout), L.agrees_all(w, h, rows, layout, t), ih) :
        {Bool.and(B.mine(layout, p), _) == Bool.and(B.mine(layout, p), L.agrees_all(w, h, rows, layout, t)) : Bool}
      {==}

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=adj_mines
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=agrees
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=agrees_all
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=adj_mines
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=count_mines
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=neighbours
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=adj_mines_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=mine_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=items
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=items.put
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=items_ok
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Seen