law csum_row_shift

minebender-game@1.0.0.0 · proof_sums.bend:126

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B

126law csum_row_shift:
127  for ~A: Data
128  for ~f: A -> Nat
129  for +d: A
130  for +r: List<&2, A>
131  for +rt: T.Grid(A)
132  for +y: Nat
133  for +xs: List<&2, Nat>
134  {csum(~A, ~f, d, r <> rt, B.row_cells(1n+y, xs)) == csum(~A, ~f, d, rt, B.row_cells(y, xs)) : Nat}