law dfs_some_keep

minebender-game@1.0.0.0 · proof_solver.bend:1233

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

1233# A layout the search returns keeps every cell the partial layout fixed.
1234law dfs_some_keep:
1235  for +todo: List<&2, S.Todo>
1236  for +part: T.Grid(Maybe<&2, Bool>)
1237  for +ctx: S.Ctx
1238  for +l: T.Grid(Bool)
1239  for e: {S.dfs(todo, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>}
1240  for +q: T.Pos
1241  for +bq: Bool
1242  for +lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>}
1243  {B.mine(l, q) == bq : Bool}