law and_mask

lawful-words@0.1.0.0 · proof_word.bend:1007

import Base

1007# And with a word standing for 2^k - 1 keeps the low k bits.
1008law and_mask:
1009  for +n: Nat
1010  for +a: Word(n)
1011  for +m: Word(n)
1012  for +k: Nat
1013  for +h: {Word.to_nat(n, m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
1014  {Word.to_nat(n, Word.and(n, a, m)) == Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) : Nat}