:: deftheorem defines SDSub_Add_Data RADIX_3:def 4 :
for x being Integer
for k being Nat holds SDSub_Add_Data (x,k) = x - ((Radix k) * (SDSub_Add_Carry (x,k)));