:: deftheorem defines CompStr TWOSCOMP:def 21 :
for x, b being set holds CompStr (x,b) = 1GateCircStr (<*x,b*>,xor2a);