ProofInv.all_safe_cell: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_inv.bend as ProofInv
Lines 490-505 of minebender-game@1.0.0.0/proof_inv.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_inv.bend&start_line=490&end_line=505

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/proof_grid.bend as PG
import minebender-game@1.0.0.0/proof_lists.bend as PL

def all_safe_cell(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, +q: T.Pos,
  mp: {B.mine(layout, p) == True{} : Bool}, +b: Bool, be: {B.same(p, q) == b : Bool}) ->
  {Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q))
    == Bool.or(B.mine(layout, q), B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q)) : Bool}:
  match b:
    case True{}:
      +mq = {%PG.same_sound(p, q, be) : {B.mine(layout, _) == True{} : Bool}; mp : {B.mine(layout, q) == True{} : Bool}}
      %Equal.sym(Bool, B.mine(layout, q), True{}, mq) :
        {Bool.or(_, B.at(Bool, False{}, shown, q))
          == Bool.or(_, B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q)) : Bool}
      {==}
    case False{}:
      %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q), B.at(Bool, False{}, shown, q),
        PL.at_set_ne(Bool, shown, p, q, True{}, False{}, be)) :
        {Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) == Bool.or(B.mine(layout, q), _) : Bool}
      {==}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=at
  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=same
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=set_at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_grid.bend&name=same_sound
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=at_set_ne
  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