:: deftheorem defines CompCirc TWOSCOMP:def 22 :
for x, b being set holds CompCirc (x,b) = 1GateCircuit (x,b,xor2a);