law double_carry

stelliferous@0.0.2.0 · proofs/word_arithmetic.bend:77

import Base

77law double_carry:
78  for +n: Nat
79  for +w: Word(n)
80  for +c: Bool
81  {Word.adc(n,w,w,False{},c) == Word.shl.put(n,c,w) : Word(n)}