def assist_stuck.k

minebender-game@1.0.0.0 · proof_assist.bend:245

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/solver.bend as S
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_laws.bend as PW

245def assist_stuck.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
246  +playing: {G.status(g) == T.Playing{} : T.Status}, stuck: L.Stuck(G.knowledge(g)), +k: Nat, c: PW.Canon(w, h, layout, g)) ->
247  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
248    ({L.hidden(G.knowledge(g), p) == True{} : Bool} & {G.step(g, T.Assist{k}) == G.open(g, p) : G.Game})):
249  match c:
250    case (+eg, facts):
251      match facts:
252        case (sh, f2):
253          match f2:
254            case (won, f3):
255              +s = PW.shown_of(g)
256              +f = PW.flags_of(g)
257              +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
258              %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
259                Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
260                  ({L.hidden(G.knowledge(_), p) == True{} : Bool} & {G.step(_, T.Assist{k}) == G.open(_, p) : G.Game}))
261              %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
262                Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
263                  ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, _}), p) == True{} : Bool} &
264                   {G.step(G.Game{w, h, layout, s, f, _}, T.Assist{k}) == G.open(G.Game{w, h, layout, s, f, _}, p) : G.Game}))
265              stuck_pick(w, h, layout, s, f,
266                Equal.sym(Bool, False{}, G.all_safe(w, h, layout, s),
267                  %playing : {L.is_won(_) == G.all_safe(w, h, layout, s) : Bool}; won),
268                {%playing : L.Stuck(G.knowledge(G.Game{w, h, layout, s, f, _}));
269                  %eg : L.Stuck(G.knowledge(_)); stuck : L.Stuck(G.knowledge(gp))},
270                S.solve(G.knowledge(gp)), {==}, k)