def stuck_wit

minebender-game@1.0.0.0 · proof_solver.bend:2807

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/solver.bend as S
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_copy.bend as PC

2807def stuck_wit(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +p: T.Pos,
2808  H: @layout: T.Grid(Bool) -> {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool} -> {L.mine(layout, p) == False{} : Bool},
2809  wt: Witness(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, p)) -> Empty:
2810  match wt:
2811    case (+l, pr):
2812      match pr:
2813        case (chk, ml):
2814          PF_both(L.mine(l, p),
2815            H(l, Equal.trans(Bool, L.consistent(T.Knowledge{w, h, n, rows}, l),
2816              S.check(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, l), True{},
2817              Equal.sym(Bool, S.check(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, l),
2818                L.consistent(T.Knowledge{w, h, n, rows}, l), check_cons(w, h, n, rows, l)), chk)),
2819            %PC.mine_eq(l, p) : {_ == True{} : Bool}; ml, Empty)