law wbit_num

lawful-words@0.1.0.0 · proof_word.bend:802

import Base

802# The numeric bit (as in D.bit) is the word's bit.
803law wbit_num:
804  for +n: Nat
805  for +w: Word(n)
806  for +k: Nat
807  {Nat.is_eq(Nat.mod(Nat.div(Word.to_nat(n, w), Nat.pow(2n, k)), 2n), 1n) == wbit(n, w, k) : Bool}