:: deftheorem defines BitCompCirc TWOSCOMP:def 28 :
for x, b being set holds BitCompCirc (x,b) = (CompCirc (x,b)) +* (IncrementCirc (x,b));