law half_cover

bend-ml-tensor-array@0.1.19.0 · main.bend:1565

import Base

1565# LAW (half_cover): the two bands of a node, half(r) rows and r - half(r) rows,
1566# add up to exactly r rows: no row is lost and none is counted twice.
1567law half_cover:
1568  for +n: Nat
1569  {n == Nat.add(half(n), Nat.sub(n, half(n))) : Nat}