law low_high

bend-osdev-u32@0.1.0.0 · LAWS.bend:416

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

416law low_high:
417  for +k: Nat
418  for +x: Nat
419  {Nat.add(U.U32Nat.low(k, x), U.U32Nat.dbl(k, U.U32Nat.high(k, x))) == x : Nat}