law to_nat_con

bend-kit-lemmas@0.1.1.0 · lemmas.bend:21

import Base

21law to_nat_con:
22  for -p: Nat
23  for x: Bool
24  for -t: Word(p)
25  {bit(x, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{x, t}) : Nat}