law loop_none

minebender-game@1.0.0.0 · proof_solver.bend:2373

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

2373# When the loop names no cell, every one of its cells has a checked layout
2374# that mines it.
2375law loop_none:
2376  for +hs: List<&2, T.Pos>
2377  for +found: List<&2, T.Grid(Bool)>
2378  for +todo: S.Plan
2379  for +part: T.Grid(Maybe<&2, Bool>)
2380  for +w: Nat
2381  for +h: Nat
2382  for +n: Nat
2383  for +rows: T.Grid(T.Seen)
2384  for +its: List<&2, S.Item>
2385  for e: {S.loop(hs, found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>}
2386  for +val: {all_valid(S.Ctx{w, h, n, rows, its}, found) == True{} : Bool}
2387  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
2388  for +hon: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, hs) == True{} : Bool}
2389  for +c: T.Pos
2390  for m: {B.contains(hs, c) == True{} : Bool}
2391  Witness(S.Ctx{w, h, n, rows, its}, c)