law wcon2

lawful-words@0.1.0.0 · proof_word.bend:36

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

36# The same value as t * 2 + b.
37law wcon2:
38  for +p: Nat
39  for +b: Bool
40  for +t: Word(p)
41  {Word.to_nat(1n+p, WCon{b, t}) == Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)) : Nat}