law high_unique

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

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

435law high_unique:
436  for +k: Nat
437  for +x: Nat
438  for +r: Nat
439  for +q: Nat
440  for e: {Nat.add(r, U.U32Nat.dbl(k, q)) == x : Nat}
441  for h: {Nat.is_lt(r, U.U32Nat.dbl(k, 1n)) == True{} : Bool}
442  {q == U.U32Nat.high(k, x) : Nat}