law part_none_sum

minebender-game@1.0.0.0 · proof_solver.bend:107

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/proof_sums.bend as PU

107law part_none_sum:
108  for +g: T.Grid(Maybe<&2, Bool>)
109  {S.part_none(g) == PU.gsum(~Maybe<&2, Bool>, ~nf, g) : Nat}