law subtract_one

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:78

import Base

78law subtract_one:
79  for +width: Nat
80  for +word: Word(width)
81  {Word.sub(width,word,power(width,0n)) == Word.adc(width,word,Word.zero(width),True{},False{}) : Word(width)}