law search_none

minebender-game@1.0.0.0 · proof_solver.bend:2660

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/solver.bend as S
import minebender-game@1.0.0.0/LAWS.bend as L

2660# A failed search for c rules out every consistent layout mining c.
2661law search_none:
2662  for +w: Nat
2663  for +h: Nat
2664  for +n: Nat
2665  for +rows: T.Grid(T.Seen)
2666  for +okt: {B.shaped(T.Seen, w, h, rows) == True{} : Bool}
2667  for +c: T.Pos
2668  for +onc: {B.on_board(w, h, c) == True{} : Bool}
2669  for +layout: T.Grid(Bool)
2670  for +cons: {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool}
2671  for +mc: {B.mine(layout, c) == True{} : Bool}
2672  for sn: {S.search(c, S.plan(w, h, S.todos(S.items(w, h, rows, B.cells(w, h)), S.hidden_cells(rows, B.cells(w, h)))),
2673    S.start(rows), S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}) == None{} : Maybe<&2, T.Grid(Bool)>}
2674  Empty