def all_safe_cell

minebender-game@1.0.0.0 · proof_inv.bend:490

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

490def all_safe_cell(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos, +q: T.Pos,
491  mp: {B.mine(layout, p) == True{} : Bool}, +b: Bool, be: {B.same(p, q) == b : Bool}) ->
492  {Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q))
493    == Bool.or(B.mine(layout, q), B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q)) : Bool}:
494  match b:
495    case True{}:
496      +mq = {%PG.same_sound(p, q, be) : {B.mine(layout, _) == True{} : Bool}; mp : {B.mine(layout, q) == True{} : Bool}}
497      %Equal.sym(Bool, B.mine(layout, q), True{}, mq) :
498        {Bool.or(_, B.at(Bool, False{}, shown, q))
499          == Bool.or(_, B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q)) : Bool}
500      {==}
501    case False{}:
502      %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, shown, p, True{}), q), B.at(Bool, False{}, shown, q),
503        PL.at_set_ne(Bool, shown, p, q, True{}, False{}, be)) :
504        {Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)) == Bool.or(B.mine(layout, q), _) : Bool}
505      {==}