def monotone.k2

minebender-game@1.0.0.0 · proof_laws.bend:499

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

499def monotone.k2(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +a: T.Action, +q: T.Pos,
500  vis: {L.revealed(G.knowledge(g), q) == True{} : Bool},
501  +eg: {g == G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)} : G.Game},
502  eg2: {G.step(g, a) == G.Game{w, h, layout, shown_of(G.step(g, a)), flags_of(G.step(g, a)), G.status(G.step(g, a))} : G.Game}) ->
503  {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}:
504  +s1 = shown_of(g)
505  +f1 = flags_of(g)
506  +t1 = G.status(g)
507  +g2 = G.step(g, a)
508  +s2 = shown_of(g2)
509  +f2 = flags_of(g2)
510  +t2 = G.status(g2)
511  +vis1 = {%eg : {L.revealed(G.knowledge(_), q) == True{} : Bool};
512    vis : {L.revealed(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q) == True{} : Bool}}
513  +on = vis_parts(w, h, layout, s1, f1, t1, q, vis1)
514  +at1 = {%know_revealed(w, h, layout, s1, f1, t1, q, on) : {_ == True{} : Bool};
515    vis1 : {B.at(Bool, False{}, s1, q) == True{} : Bool}}
516  +at2 = step_mono(g, a, q, at1)
517  %Equal.sym(G.Game, g2, G.Game{w, h, layout, s2, f2, t2}, eg2) :
518    {L.seen(G.knowledge(_), q) == L.seen(G.knowledge(g), q) : T.Seen}
519  %Equal.sym(G.Game, g, G.Game{w, h, layout, s1, f1, t1}, eg) :
520    {L.seen(G.knowledge(G.Game{w, h, layout, s2, f2, t2}), q) == L.seen(G.knowledge(_), q) : T.Seen}
521  %Equal.sym(T.Seen, L.seen(G.knowledge(G.Game{w, h, layout, s2, f2, t2}), q), G.seen_at(w, h, layout, s2, q),
522    know_seen(w, h, layout, s2, f2, t2, q, on)) :
523    {_ == L.seen(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q) : T.Seen}
524  %Equal.sym(T.Seen, L.seen(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q), G.seen_at(w, h, layout, s1, q),
525    know_seen(w, h, layout, s1, f1, t1, q, on)) :
526    {G.seen_at(w, h, layout, s2, q) == _ : T.Seen}
527  %Equal.sym(Bool, B.at(Bool, False{}, s2, q), True{}, at2) :
528    {G.seen_pick(_, B.mine(layout, q), w, h, layout, q) == G.seen_pick(B.at(Bool, False{}, s1, q), B.mine(layout, q), w, h, layout, q) : T.Seen}
529  %Equal.sym(Bool, B.at(Bool, False{}, s1, q), True{}, at1) :
530    {G.seen_pick(True{}, B.mine(layout, q), w, h, layout, q) == G.seen_pick(_, B.mine(layout, q), w, h, layout, q) : T.Seen}
531  {==}