law Word.add_sub.arm

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

import Base

268# one bit: the bit is kept, and e is the law for the rest at the carry k
269law Word.add_sub.arm:
270  for -p: Nat
271  for -h: Bool
272  for -at: Word(p)
273  for -bt: Word(p)
274  for -k: Bool
275  for e: {at == Word.adc(p, Word.adc(p, at, bt, True{}, k), bt, False{}, Bool.not(k)) : Word(p)}
276  {WCon{h, at} == WCon{h, Word.adc(p, Word.adc(p, at, bt, True{}, k), bt, False{}, Bool.not(k))} : Word(1n+p)}