law csum_append

minebender-game@1.0.0.0 · proof_sums.bend:86

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

86law csum_append:
87  for ~A: Data
88  for ~f: A -> Nat
89  for +d: A
90  for +g: T.Grid(A)
91  for +xs: List<&2, T.Pos>
92  for +ys: List<&2, T.Pos>
93  {csum(~A, ~f, d, g, List.append(&2, T.Pos, xs, ys)) == Nat.add(csum(~A, ~f, d, g, xs), csum(~A, ~f, d, g, ys)) : Nat}