law dbl_dbl

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

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

40law dbl_dbl:
41  for +m: Nat
42  for +k: Nat
43  for +x: Nat
44  {U.U32Nat.dbl(m, U.U32Nat.dbl(k, x)) == U.U32Nat.dbl(Nat.add(m, k), x) : Nat}