law high_double

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

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

655law high_double:
656  for +k: Nat
657  for +x: Nat
658  {U.U32Nat.high(1n+k, Nat.double(x)) == U.U32Nat.high(k, x) : Nat}