ProofLaws.flood_complete_c.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_laws.bend as ProofLaws
Lines 752-778 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=752&end_line=778

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

def flood_complete_c.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>,
  +shS: {B.shaped(Bool, w, h, s) == True{} : Bool}, +cl: {PI.closed(w, h, layout, s) == True{} : Bool},
  +p: T.Pos, +on: {B.on_board(w, h, p) == True{} : Bool}, +q: T.Pos, +onq: {B.on_board(w, h, q) == True{} : Bool},
  +path: List<&2, T.Pos>, +wk: {L.zero_walk(path, w, h, layout, p, q) == True{} : Bool},
  +c: Bool, ce: {G.unrevealed(w, h, s, p) == c : Bool}, +m: Bool, me: {B.mine(layout, p) == m : Bool}) ->
  {L.revealed(G.knowledge(G.open.go(c, m, G.Game{w, h, layout, s, f, T.Playing{}}, p)), q) == True{} : Bool}:
  match c m:
    case False{} _:
      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), q), B.at(Bool, False{}, s, q),
        know_revealed(w, h, layout, s, f, T.Playing{}, q, onq)) : {_ == True{} : Bool}
      path_closed(path, w, h, layout, s, cl, p, q, PF.unrev_shown(w, h, s, p, ce, on), wk)
    case True{} True{}:
      +s2 = B.set_at(Bool, s, p, True{})
      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, s2, f, T.Lost{T.Exploded{p}}}), q), B.at(Bool, False{}, s2, q),
        know_revealed(w, h, layout, s2, f, T.Lost{T.Exploded{p}}, q, onq)) : {_ == True{} : Bool}
      path_closed(path, w, h, layout, s2, PI.closed_explode(w, h, layout, s, p, me, cl), p, q,
        PF.at_set_on(w, h, s, p, shS, on), wk)
    case True{} False{}:
      +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>}
      +cf = B.count_false(s)
      +hh = G.head_hidden(w, h, s, start)
      +fl = G.flood(cf, start, hh, w, h, layout, s)
      +st = G.won_or_playing(G.all_safe(w, h, layout, fl))
      %Equal.sym(Bool, L.revealed(G.knowledge(G.Game{w, h, layout, fl, f, st}), q), B.at(Bool, False{}, fl, q),
        know_revealed(w, h, layout, fl, f, st, q, onq)) : {_ == True{} : Bool}
      path_closed(path, w, h, layout, fl, PI.closed_flood(cf, start, hh, w, h, layout, s, shS, cl, {==}, {==}), p, q,
        PF.flood_work(cf, start, hh, w, h, layout, s, shS, {==}, {==}, p, on, start_has(p)), wk)

Uses (34):
  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=List
  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=zero_walk
  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=count_false
  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=on_board
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=set_at
  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=Work
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=all_safe
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=flood
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=head_hidden
  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.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=unrevealed
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=won_or_playing
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_flood.bend&name=at_set_on
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_flood.bend&name=flood_work
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_flood.bend&name=unrev_shown
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=closed
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=closed_explode
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=closed_flood
  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=path_closed
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=start_has
  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=Status