def flood_complete.k

minebender-game@1.0.0.0 · proof_laws.bend:937

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/LAWS.bend as L

937def flood_complete.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
938  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, +on: {L.on_board(w, h, p) == True{} : Bool},
939  +q: T.Pos, +path: List<&2, T.Pos>, +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool},
940  c: Canon(w, h, layout, g)) ->
941  {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}:
942  match c:
943    case (eg, facts):
944      match facts:
945        case (sh, f2):
946          match f2:
947            case (won, f3):
948              match f3:
949                case (cm, cl):
950                  +s = shown_of(g)
951                  +f = flags_of(g)
952                  %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
953                    {L.revealed(G.knowledge(G.open(_, p)), q) == True{} : Bool}
954                  %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
955                    {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), q) == True{} : Bool}
956                  flood_complete_c(w, h, layout, s, f, sh, cl, p, on, q, path, wk)