law row_none_set

minebender-game@1.0.0.0 · proof_speed.bend:17

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

17law row_none_set:
18  for +r: List<&2, Maybe<&2, Bool>>
19  for +x: Nat
20  for +b: Bool
21  for e: {List.get(&2, Maybe<&2, Bool>, r, x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}
22  {S.row_none(r) == 1n+S.row_none(List.set(&2, Maybe<&2, Bool>, r, x, Some{b})) : Nat}