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

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_cells.bend as PS

def won_iff.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, c: Canon(w, h, layout, g)) ->
  {L.is_won(G.status(g)) == L.all_safe_revealed(G.knowledge(g), layout) : Bool}:
  match c:
    case (eg, facts):
      match facts:
        case (sh, f2):
          match f2:
            case (won, f3):
              %Equal.sym(G.Game, g, G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)}, eg) :
                {L.is_won(G.status(_)) == L.all_safe_revealed(G.knowledge(_), layout) : Bool}
              +s = shown_of(g)
              +f = flags_of(g)
              +st = G.status(g)
              %PC.cells_eq(w, h) :
                {L.is_won(st) == L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, s, f, st}), layout, _) : Bool}
              %Equal.sym(Bool, L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, s, f, st}), layout, B.cells(w, h)),
                G.all_safe.go(layout, s, B.cells(w, h)), safe_rev_all(w, h, layout, s, f, st, B.cells(w, h), PS.cells_on(w, h))) :
                {L.is_won(st) == _ : Bool}
              won

Uses (19):
  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=Sigma
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=all_safe_revealed
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=all_safe_revealed.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_won
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=cells
  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=all_safe.go
  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=status
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=cells_on
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=cells_eq
  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=safe_rev_all
  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