ProofLaws.safe_rev_all: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_laws.bend as ProofLaws
Lines 296-313 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=296&end_line=313

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

def safe_rev_all(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
  +status: T.Status, ps: List<&2, T.Pos>, +ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
  {L.all_safe_revealed.go(G.knowledge(G.Game{w, h, layout, shown, flags, status}), layout, ps)
    == G.all_safe.go(layout, shown, ps) : Bool}:
  match ps:
    case Nil{}:
      {==}
    case +q <> +t:
      +v = G.knowledge(G.Game{w, h, layout, shown, flags, status})
      %Equal.sym(Bool, Bool.or(L.mine(layout, q), L.revealed(v, q)), Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)),
        safe_rev_cell(w, h, layout, shown, flags, status, q, PS.allp_head(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
        {Bool.and(_, L.all_safe_revealed.go(v, layout, t))
          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
      %Equal.sym(Bool, L.all_safe_revealed.go(v, layout, t), G.all_safe.go(layout, shown, t),
        safe_rev_all(w, h, layout, shown, flags, status, t, PS.allp_tail(~PS.WH, ~PS.onb, PS.WH{w, h}, q, t, ons))) :
        {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), _)
          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
      {==}

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=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  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=all_safe_revealed.go
  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=revealed
  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=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/proof_cells.bend&name=WH
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp_head
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp_tail
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=onb
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=safe_rev_cell
  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=Status