ProofLaws.open_mine.k: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_laws.bend as ProofLaws
Lines 859-888 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=859&end_line=888

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_inv.bend as PI

def open_mine.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
  shape: {L.shaped(Bool, w, h, layout) == True{} : Bool},
  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, boom: {L.mine(layout, p) == True{} : Bool},
  c: Canon(w, h, layout, g)) ->
  {G.status(G.open(g, p)) == T.Lost{T.Exploded{p}} : T.Status} &
  {L.seen(G.knowledge(G.open(g, p)), p) == T.Boom{} : T.Seen}:
  match c:
    case (eg, facts):
      match facts:
        case (sh, f2):
          match f2:
            case (won, f3):
              match f3:
                case (cm, cl):
                  +s = shown_of(g)
                  +f = flags_of(g)
                  %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
                    {G.status(G.open(_, p)) == T.Lost{T.Exploded{p}} : T.Status} &
                    {L.seen(G.knowledge(G.open(_, p)), p) == T.Boom{} : T.Seen}
                  %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
                    {G.status(G.open(G.Game{w, h, layout, s, f, _}, p)) == T.Lost{T.Exploded{p}} : T.Status} &
                    {L.seen(G.knowledge(G.open(G.Game{w, h, layout, s, f, _}, p)), p) == T.Boom{} : T.Seen}
                  open_mine_c(w, h, layout, s, f,
                    %Equal.sym(Bool, B.shaped(Bool, w, h, layout), L.shaped(Bool, w, h, layout), PC.shaped_eq(Bool, w, h, layout)) :
                      {_ == True{} : Bool}; shape,
                    sh,
                    %playing : {PI.calm(_, w, h, layout, s) == True{} : Bool}; cm,
                    p,
                    %Equal.sym(Bool, B.mine(layout, p), L.mine(layout, p), PC.mine_eq(layout, p)) :
                      {_ == True{} : Bool}; boom)

Uses (26):
  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=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=mine
  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/LAWS.bend&name=shaped
  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/board.bend&name=shaped
  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=open
  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/proof_copy.bend&name=mine_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=shaped_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=calm
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=Canon
  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=open_mine_c
  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/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Loss
  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
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Status