:: deftheorem defines CompOutput TWOSCOMP:def 23 :
for x, b being set holds CompOutput (x,b) = [<*x,b*>,xor2a];