law dbl_comm

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

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

314law dbl_comm:
315  for +j: Nat
316  for +k: Nat
317  for +x: Nat
318  {U.U32Nat.dbl(j, U.U32Nat.dbl(k, x)) == U.U32Nat.dbl(k, U.U32Nat.dbl(j, x)) : Nat}