law dbl_le_exp

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

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

684law dbl_le_exp:
685  for +j: Nat
686  for +k: Nat
687  for +x: Nat
688  for h: {Nat.is_le(j, k) == True{} : Bool}
689  {Nat.is_le(U.U32Nat.dbl(j, x), U.U32Nat.dbl(k, x)) == True{} : Bool}