law bitw

lawful-words@0.1.0.0 · proof_u32.bend:1255

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

1255law bitw:
1256  for +w: Word(32n)
1257  for +k: Nat
1258  {D.bit(U32{w}, k) == W.wbit(32n, w, k) : Bool}