def add_subtract

stelliferous@0.0.2.0 · proofs/word_subtraction.bend:84

import Base

84def add_subtract(+a: U32,+b: U32) -> {U32.add(U32.sub(a,b),b) == a : U32}:
85  match a b:
86    case U32{+x} U32{+y}:
87      %undo(32n,x,y,True{},True{}) : {U32{Word.add(32n,Word.sub(32n,x,y),y)} == U32{_} : U32}
88      {==}