law csum_shift

minebender-game@1.0.0.0 · proof_sums.bend:146

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

146law csum_shift:
147  for ~A: Data
148  for ~f: A -> Nat
149  for +d: A
150  for +r: List<&2, A>
151  for +rt: T.Grid(A)
152  for +w: Nat
153  for +ys: List<&2, Nat>
154  {csum(~A, ~f, d, r <> rt, B.cells.go(w, smap(ys))) == csum(~A, ~f, d, rt, B.cells.go(w, ys)) : Nat}