ProofAssist.first_safe.go2: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_assist.bend as ProofAssist
Lines 52-66 of minebender-game@1.0.0.0/proof_assist.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_assist.bend&start_line=52&end_line=66

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/proof_grid.bend as PG
import minebender-game@1.0.0.0/proof_solver.bend as PV

def first_safe.go2(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +t: List<&2, T.Pos>, +hit: Bool,
  he: {Bool.and(Bool.not(B.mine(layout, q)), Bool.not(B.at(Bool, False{}, shown, q))) == hit : Bool},
  e: {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) == False{} : Bool},
  ih: {G.all_safe.go(layout, shown, t) == False{} : Bool} -> SafeAt(layout, shown, t)) ->
  Exists(T.Pos, p => {G.first_safe.go(q <> t, hit, layout, shown) == Some{p} : Maybe<&2, T.Pos>} &
    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
     {B.contains(q <> t, p) == True{} : Bool})):
  match hit:
    case True{}:
      (q, ({==}, (he, PV.or_l(B.same(q, q), B.contains(t, q), PG.same_refl(q)))))
    case False{}:
      first_safe.lift(layout, shown, q, t,
        ih(%not_and_false(B.mine(layout, q), B.at(Bool, False{}, shown, q), he) :
            {Bool.and(_, G.all_safe.go(layout, shown, t)) == False{} : Bool}; e),
        False{}, {==})

Uses (22):
  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.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Exists
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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/board.bend&name=at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=contains
  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=same
  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=first_safe.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_assist.bend&name=SafeAt
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_assist.bend&name=first_safe.lift
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_assist.bend&name=not_and_false
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_grid.bend&name=same_refl
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=or_l
  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