law gsum_cells_go

minebender-game@1.0.0.0 · proof_sums.bend:222

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

222law gsum_cells_go:
223  for ~A: Data
224  for ~f: A -> Nat
225  for +d: A
226  for +w: Nat
227  for +g: T.Grid(A)
228  for +wide: {B.rows_wide(A, w, g) == True{} : Bool}
229  {csum(~A, ~f, d, g, B.cells.go(w, List.range(List.length(&2, List<&2, A>, g)))) == gsum(~A, ~f, g) : Nat}