law adc_step

lawful-words@0.1.0.0 · proof_word.bend:365

import Base

365# One bit of the sum, as numbers.
366law adc_step:
367  for +p: Nat
368  for +x: Nat
369  for +y: Nat
370  for +c: Nat
371  for +s: Nat
372  for +k: Nat
373  for +a: Nat
374  for +b: Nat
375  for +r: Nat
376  for +co: Nat
377  for +ih: {Nat.add(r, Nat.mul(co, Nat.pow(2n, p))) == Nat.add(k, Nat.add(a, b)) : Nat}
378  for +bit: {Nat.add(s, Nat.double(k)) == Nat.add(c, Nat.add(x, y)) : Nat}
379  {Nat.add(Nat.add(s, Nat.double(r)), Nat.mul(co, Nat.pow(2n, 1n+p)))
380    == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}