law wadc

lawful-words@0.1.0.0 · proof_word.bend:411

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

411# The sum with its carry out: r + co * 2^n = c + a + b.
412law wadc:
413  for +n: Nat
414  for +a: Word(n)
415  for +b: Word(n)
416  for +c: Bool
417  {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.mul(N.bn(cout(n, a, b, c)), Nat.pow(2n, n)))
418    == Nat.add(N.bn(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}