law hc_sound

minebender-game@1.0.0.0 · proof_solver.bend:2095

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

2095# A hidden cell is hidden and one of the cells it was taken from.
2096law hc_sound:
2097  for +rows: T.Grid(T.Seen)
2098  for +ps: List<&2, T.Pos>
2099  for +q: T.Pos
2100  for m: {B.contains(S.hidden_cells(rows, ps), q) == True{} : Bool}
2101  {S.is_hidden(B.at(T.Seen, T.Hidden{}, rows, q)) == True{} : Bool} & {B.contains(ps, q) == True{} : Bool}