ProofAssist.assist_stuck.k: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_assist.bend as ProofAssist
Lines 245-270 of minebender-game@1.0.0.0/proof_assist.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_assist.bend&start_line=245&end_line=270

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

def assist_stuck.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
  +playing: {G.status(g) == T.Playing{} : T.Status}, stuck: L.Stuck(G.knowledge(g)), +k: Nat, c: PW.Canon(w, h, layout, g)) ->
  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
    ({L.hidden(G.knowledge(g), p) == True{} : Bool} & {G.step(g, T.Assist{k}) == G.open(g, p) : G.Game})):
  match c:
    case (+eg, facts):
      match facts:
        case (sh, f2):
          match f2:
            case (won, f3):
              +s = PW.shown_of(g)
              +f = PW.flags_of(g)
              +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
              %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
                Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
                  ({L.hidden(G.knowledge(_), p) == True{} : Bool} & {G.step(_, T.Assist{k}) == G.open(_, p) : G.Game}))
              %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
                Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
                  ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, _}), p) == True{} : Bool} &
                   {G.step(G.Game{w, h, layout, s, f, _}, T.Assist{k}) == G.open(G.Game{w, h, layout, s, f, _}, p) : G.Game}))
              stuck_pick(w, h, layout, s, f,
                Equal.sym(Bool, False{}, G.all_safe(w, h, layout, s),
                  %playing : {L.is_won(_) == G.all_safe(w, h, layout, s) : Bool}; won),
                {%playing : L.Stuck(G.knowledge(G.Game{w, h, layout, s, f, _}));
                  %eg : L.Stuck(G.knowledge(_)); stuck : L.Stuck(G.knowledge(gp))},
                S.solve(G.knowledge(gp)), {==}, k)

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Exists
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=Stuck
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=hidden
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_won
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Game
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=all_safe
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=knowledge
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=open
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=status
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_assist.bend&name=stuck_pick
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=Canon
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=flags_of
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=shown_of
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=solve
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Action
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Status