law dfs2_some_check

minebender-game@1.0.0.0 · proof_solver.bend:1258

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S

1258# A layout the counting search returns passes the consistency check.
1259law dfs2_some_check:
1260  for +todo: List<&2, S.Todo>
1261  for +part: T.Grid(Maybe<&2, Bool>)
1262  for +t: Nat
1263  for +f: Nat
1264  for +ctx: S.Ctx
1265  for +l: T.Grid(Bool)
1266  for e: {S.dfs2(todo, part, t, f, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>}
1267  {S.check(ctx, l) == True{} : Bool}