law mask_n

lawful-arrays@0.1.0.0 · proof_index.bend:391

import Base

391law mask_n:
392  for +d: Nat
393  for +hd: {Nat.is_lt(d, 32n) == True{} : Bool}
394  {U32.to_nat(U32.sub(U32.shln(1, d), 1)) == Nat.sub(Nat.pow(2n, d), 1n) : Nat}