:: deftheorem defines BitCompStr TWOSCOMP:def 27 :
for x, b being set holds BitCompStr (x,b) = (CompStr (x,b)) +* (IncrementStr (x,b));