def all_safe_set_mine.go

minebender-game@1.0.0.0 · proof_inv.bend:507

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/game.bend as G

507def all_safe_set_mine.go(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
508  +mp: {B.mine(layout, p) == True{} : Bool}, ps: List<&2, T.Pos>) ->
509  {G.all_safe.go(layout, B.set_at(Bool, shown, p, True{}), ps) == G.all_safe.go(layout, shown, ps) : Bool}:
510  match ps:
511    case Nil{}:
512      {==}
513    case +q <> t:
514      +s2 = B.set_at(Bool, shown, p, True{})
515      %Equal.sym(Bool, G.all_safe.go(layout, s2, t), G.all_safe.go(layout, shown, t),
516        all_safe_set_mine.go(layout, shown, p, mp, t)) :
517        {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, s2, q)), _)
518          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
519      %all_safe_cell(layout, shown, p, q, mp, B.same(p, q), {==}) :
520        {Bool.and(_, G.all_safe.go(layout, shown, t))
521          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
522      {==}