def flood_exact.k

minebender-game@1.0.0.0 · proof_laws.bend:976

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
import minebender-game@1.0.0.0/proof_flood.bend as PF

976def flood_exact.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
977  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, +q: T.Pos,
978  before: {L.hidden(G.knowledge(g), q) == True{} : Bool},
979  after: {L.revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool},
980  c: Canon(w, h, layout, g)) -> PF.Walk(w, h, layout, p, q):
981  match c:
982    case (+eg, facts):
983      +s = shown_of(g)
984      +f = flags_of(g)
985      +gp = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
986      flood_exact_c(w, h, layout, s, f, p, q,
987        {%playing : {L.hidden(G.knowledge(G.Game{w, h, layout, s, f, _}), q) == True{} : Bool};
988          %eg : {L.hidden(G.knowledge(_), q) == True{} : Bool};
989          before : {L.hidden(G.knowledge(gp), q) == True{} : Bool}},
990        {%playing : {L.revealed(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), q) == True{} : Bool};
991          %eg : {L.revealed(G.knowledge(G.open(_, p)), q) == True{} : Bool};
992          after : {L.revealed(G.knowledge(G.open(gp, p)), q) == True{} : Bool}})