def safe_rev_all

minebender-game@1.0.0.0 · proof_laws.bend:296

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

296def safe_rev_all(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
297  +status: T.Status, ps: List<&2, T.Pos>, +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
298  {L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, shown, flags, status}), layout, ps)
299    == G.all_safe.go(layout, shown, ps) : Bool}:
300  match ps:
301    case Nil{}:
302      {==}
303    case +q <> +t:
304      +v = G.knowledge(G.Game{w, h, layout, shown, flags, status})
305      %Equal.sym(Bool, Bool.or(L.mine(layout, q), L.revealed(v, q)), Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)),
306        safe_rev_cell(w, h, layout, shown, flags, status, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
307        {Bool.and(_, L.all_safe_revealed.go(v, layout, t))
308          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
309      %Equal.sym(Bool, L.all_safe_revealed.go(v, layout, t), G.all_safe.go(layout, shown, t),
310        safe_rev_all(w, h, layout, shown, flags, status, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
311        {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), _)
312          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
313      {==}