law dfs2_some_keep

minebender-game@1.0.0.0 · proof_solver.bend:1302

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

1302# A layout the counting search returns keeps every cell the partial layout fixed.
1303law dfs2_some_keep:
1304  for +todo: List<&2, S.Todo>
1305  for +part: T.Grid(Maybe<&2, Bool>)
1306  for +t: Nat
1307  for +f: Nat
1308  for +ctx: S.Ctx
1309  for +l: T.Grid(Bool)
1310  for e: {S.dfs2(todo, part, t, f, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>}
1311  for +q: T.Pos
1312  for +bq: Bool
1313  for +lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>}
1314  {B.mine(l, q) == bq : Bool}