:: deftheorem defines IncrementCirc TWOSCOMP:def 25 :
for x, b being set holds IncrementCirc (x,b) = 1GateCircuit (x,b,and2a);