law undo

stelliferous@0.0.2.0 · proofs/word_subtraction.bend:6

import Base

6law undo:
7  for +n: Nat
8  for +a: Word(n)
9  for +b: Word(n)
10  for +f: Bool
11  for +c: Bool
12  {Word.adc(n,Word.adc(n,a,b,f,c),b,Bool.not(f),Bool.not(c)) == a : Word(n)}