ProofLaws.monotone.k2: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_laws.bend as ProofLaws
Lines 499-531 of minebender-game@1.0.0.0/proof_laws.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_laws.bend&start_line=499&end_line=531

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

def monotone.k2(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +a: T.Action, +q: T.Pos,
  vis: {L.revealed(G.knowledge(g), q) == True{} : Bool},
  +eg: {g == G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)} : G.Game},
  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}) ->
  {L.seen(G.knowledge(G.step(g, a)), q) == L.seen(G.knowledge(g), q) : T.Seen}:
  +s1 = shown_of(g)
  +f1 = flags_of(g)
  +t1 = G.status(g)
  +g2 = G.step(g, a)
  +s2 = shown_of(g2)
  +f2 = flags_of(g2)
  +t2 = G.status(g2)
  +vis1 = {%eg : {L.revealed(G.knowledge(_), q) == True{} : Bool};
    vis : {L.revealed(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q) == True{} : Bool}}
  +on = vis_parts(w, h, layout, s1, f1, t1, q, vis1)
  +at1 = {%know_revealed(w, h, layout, s1, f1, t1, q, on) : {_ == True{} : Bool};
    vis1 : {B.at(Bool, False{}, s1, q) == True{} : Bool}}
  +at2 = step_mono(g, a, q, at1)
  %Equal.sym(G.Game, g2, G.Game{w, h, layout, s2, f2, t2}, eg2) :
    {L.seen(G.knowledge(_), q) == L.seen(G.knowledge(g), q) : T.Seen}
  %Equal.sym(G.Game, g, G.Game{w, h, layout, s1, f1, t1}, eg) :
    {L.seen(G.knowledge(G.Game{w, h, layout, s2, f2, t2}), q) == L.seen(G.knowledge(_), q) : T.Seen}
  %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),
    know_seen(w, h, layout, s2, f2, t2, q, on)) :
    {_ == L.seen(G.knowledge(G.Game{w, h, layout, s1, f1, t1}), q) : T.Seen}
  %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),
    know_seen(w, h, layout, s1, f1, t1, q, on)) :
    {G.seen_at(w, h, layout, s2, q) == _ : T.Seen}
  %Equal.sym(Bool, B.at(Bool, False{}, s2, q), True{}, at2) :
    {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}
  %Equal.sym(Bool, B.at(Bool, False{}, s1, q), True{}, at1) :
    {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}
  {==}

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=revealed
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=seen
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Game
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=knowledge
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=seen_at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=seen_pick
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=status
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=step
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=flags_of
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=know_revealed
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=know_seen
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=shown_of
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=step_mono
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=vis_parts
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Action
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Seen