law dbl_nowrap

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

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

394law dbl_nowrap:
395  for +n: Nat
396  for +k: Nat
397  for +r: Nat
398  for +p: Nat
399  for +z: Nat
400  for e: {Nat.add(r, U.U32Nat.dbl(n, k)) == p : Nat}
401  for h: {Nat.is_le(p, z) == True{} : Bool}
402  for hz: {Nat.is_lt(z, U.U32Nat.dbl(n, 1n)) == True{} : Bool}
403  {r == p : Nat}