for x being Integer
for k being Nat st 2 <= k holds
SDSub_Add_Carry (x,k) in k -SD_Sub_S