:: deftheorem defines IncrementOutput TWOSCOMP:def 26 :
for x, b being set holds IncrementOutput (x,b) = [<*x,b*>,and2a];