:: deftheorem defines IncrementStr TWOSCOMP:def 24 :
for x, b being set holds IncrementStr (x,b) = 1GateCircStr (<*x,b*>,and2a);