~/jendhub

law to_nat_split

lawful-words@0.1.0.0 · proof_u32.bend:1222

import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
import Base

1222law to_nat_split:
1223  for +a: U32
1224  for +m: U32
1225  for +k: Nat
1226  for +h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
1227  {U32.to_nat(a) == Nat.add(Nat.mul(U32.to_nat(U32.shrn(a, k)), Nat.pow(2n, k)), U32.to_nat(U32.and(a, m))) : Nat}

Uses (15)

Used by (1)