:: deftheorem defines SD_Add_Data RADIX_1:def 11 :
for x being Integer
for k being Nat holds SD_Add_Data (x,k) = x - ((SD_Add_Carry x) * (Radix k));