law Word.sub_add.arm

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

import Base

222# one bit: the bit is kept, and e is the law for the rest at the carry k
223law Word.sub_add.arm:
224  for -p: Nat
225  for -h: Bool
226  for -at: Word(p)
227  for -bt: Word(p)
228  for -k: Bool
229  for e: {at == Word.adc(p, Word.adc(p, at, bt, False{}, k), bt, True{}, Bool.not(k)) : Word(p)}
230  {WCon{h, at} == WCon{h, Word.adc(p, Word.adc(p, at, bt, False{}, k), bt, True{}, Bool.not(k))} : Word(1n+p)}