:: deftheorem Def1 defines SDSubAddDigit RADIX_4:def 1 :
for i, n, k being Nat
for x, y being Tuple of n,k -SD_Sub st i in Seg n & k >= 2 holds
SDSubAddDigit (x,y,i,k) = (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k));