law adc_step

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

import Base

325# One bit of the adder: s + 2k is the sum c + x + y of the three input bits.
326law adc_step:
327  for +s: Nat
328  for +x: Nat
329  for +y: Nat
330  for +c: Nat
331  for +k: Nat
332  for +r: Nat
333  for +q: Bool
334  for +m: Nat
335  for +a: Nat
336  for +b: Nat
337  for ih: {Nat.add(r, scale(q, m)) == Nat.add(k, Nat.add(a, b)) : Nat}
338  for fa: {Nat.add(c, Nat.add(x, y)) == Nat.add(s, Nat.double(k)) : Nat}
339  {Nat.add(Nat.add(s, Nat.double(r)), scale(q, Nat.double(m))) == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}