law bit_lt_pow

lawful-words@0.1.0.0 · proof_bytes.bend:85

import Base
import lawful-words@0.1.0.0/defs.bend as D

85law bit_lt_pow:
86  for +b: U32
87  for +n: Nat
88  for +k: Nat
89  for +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, n)) == True{} : Bool}
90  for +hk: {Nat.is_le(n, k) == True{} : Bool}
91  {D.bit(b, k) == False{} : Bool}