:: deftheorem defines DigitDC2 RADIX_2:def 4 :
for i, k, x being Nat holds DigitDC2 (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));