law dbl_add

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

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

34law dbl_add:
35  for +n: Nat
36  for +x: Nat
37  for +y: Nat
38  {U.U32Nat.dbl(n, Nat.add(x, y)) == Nat.add(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) : Nat}