law Word.add_sub

bend-lawful-stdlib@0.1.0.0 · src/u32.bend:260

import Base

260# (a - b) + b, with carry not(c), is a
261law Word.add_sub:
262  for +n: Nat
263  for a: Word(n)
264  for +b: Word(n)
265  for c: Bool
266  {a == Word.adc(n, Word.adc(n, a, b, True{}, c), b, False{}, Bool.not(c)) : Word(n)}