law dfs2_eq

minebender-game@1.0.0.0 · proof_speed.bend:506

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/proof_cells.bend as PS

506# With the counts right and every cell on the board, the counting search
507# answers exactly as the plain one.
508law dfs2_eq:
509  for +todo: List<&2, S.Todo>
510  for +part: T.Grid(Maybe<&2, Bool>)
511  for +w: Nat
512  for +h: Nat
513  for +n: Nat
514  for +rows: T.Grid(T.Seen)
515  for +its: List<&2, S.Item>
516  for +t: Nat
517  for +f: Nat
518  for +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
519  for +con: {tall(~PS.WH, ~con_f, PS.WH{w, h}, todo) == True{} : Bool}
520  for +et: {S.part_true(part) == t : Nat}
521  for +ef: {S.part_none(part) == f : Nat}
522  {S.dfs2(todo, part, t, f, S.Ctx{w, h, n, rows, its}) == S.dfs(todo, part, S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>}