def stuck_pick.none

minebender-game@1.0.0.0 · proof_assist.bend:202

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_base.bend as P
import minebender-game@1.0.0.0/proof_grid.bend as PG
import minebender-game@1.0.0.0/proof_copy.bend as PC
import minebender-game@1.0.0.0/proof_cells.bend as PS

202def stuck_pick.none(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +k: Nat,
203  sa: SafeAt(layout, s, G.safe_list(w, h, s, k))) ->
204  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
205    ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p) == True{} : Bool} &
206     {G.assist.safe(G.first_safe(layout, s, G.safe_list(w, h, s, k)), G.Game{w, h, layout, s, f, T.Playing{}})
207       == G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p) : G.Game})):
208  match sa:
209    case (+p, pr):
210      match pr:
211        case (+fe, rest):
212          match rest:
213            case (+sf, m):
214              +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
215              +nm = P.not_true(B.mine(layout, p), P.and_true_l(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, s, p)), sf))
216              +onp = PS.allp_member(~PS.WH, ~PS.onb, PS.WH{w, h}, G.safe_list(w, h, s, k), p, on_list(w, h, s, k), m)
217              (p,
218                (%PC.mine_eq(layout, p) : {_ == False{} : Bool}; nm,
219                 (%Equal.sym(Bool, L.hidden(G.knowledge(g0), p), G.unrevealed(w, h, s, p),
220                    PG.know_hidden(w, h, layout, s, f, T.Playing{}, p)) : {_ == True{} : Bool};
221                    %Equal.sym(Bool, B.on_board(w, h, p), True{}, onp) :
222                      {Bool.and(_, Bool.not(B.at(Bool, False{}, s, p))) == True{} : Bool};
223                    P.and_true_r(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, s, p)), sf),
224                  %Equal.sym(Maybe<&2, T.Pos>, G.first_safe(layout, s, G.safe_list(w, h, s, k)), Some{p}, fe) :
225                    {G.assist.safe(_, g0) == G.open(g0, p) : G.Game};
226                  {==})))