~/jendhub

def un.high_half

bend-osdev-u32@0.1.0.0 · PROOF.bend:1272

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

1272# high(k, x / 2) = high(k, x) / 2
1273def un.high_half(k: Nat, +x: Nat) -> {U.U32Nat.high(k, U.U32Nat.half(x)) == U.U32Nat.half(U.U32Nat.high(k, x)) : Nat}:
1274  match k:
1275    case 0n:
1276      {==}
1277    case 1n+ +j:
1278      un.high_half(j, U.U32Nat.half(x))

Uses (3)

Used by (1)