law start_comp

minebender-game@1.0.0.0 · proof_solver.bend:1593

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

1593# A consistent layout completes the starting partial layout.
1594law start_comp:
1595  for +w: Nat
1596  for +h: Nat
1597  for +n: Nat
1598  for +rows: T.Grid(T.Seen)
1599  for +layout: T.Grid(Bool)
1600  for cons: {L.consistent(T.Knowledge{w, h, n, rows}, layout) == True{} : Bool}
1601  {completes(w, h, S.start(rows), layout) == True{} : Bool}