~/jendhub

law solve_stuck

minebender-game@1.0.0.0 · proof_solver.bend:2848

import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S
import minebender-game@1.0.0.0/LAWS.bend as L

2848# Stuck soundness: when the solver names no cell, no cell is provably safe.
2849law solve_stuck:
2850  for +k: T.Knowledge
2851  for e: {S.solve(k) == None{} : Maybe<&2, T.Pos>}
2852  L.Stuck(k)

Uses (6)

Used by (1)