def won_iff.k

minebender-game@1.0.0.0 · proof_laws.bend:315

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

315def won_iff.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, c: Canon(w, h, layout, g)) ->
316  {L.is_won(G.status(g)) == L.all_safe_revealed(G.knowledge(g), layout) : Bool}:
317  match c:
318    case (eg, facts):
319      match facts:
320        case (sh, f2):
321          match f2:
322            case (won, f3):
323              %Equal.sym(G.Game, g, G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)}, eg) :
324                {L.is_won(G.status(_)) == L.all_safe_revealed(G.knowledge(_), layout) : Bool}
325              +s = shown_of(g)
326              +f = flags_of(g)
327              +st = G.status(g)
328              %PC.cells_eq(w, h) :
329                {L.is_won(st) == L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, s, f, st}), layout, _) : Bool}
330              %Equal.sym(Bool, L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, s, f, st}), layout, B.cells(w, h)),
331                G.all_safe.go(layout, s, B.cells(w, h)), safe_rev_all(w, h, layout, s, f, st, B.cells(w, h), PS.cells_on(w, h))) :
332                {L.is_won(st) == _ : Bool}
333              won