:: deftheorem Def3 defines SDSub_Add_Carry RADIX_3:def 3 :
for x being Integer
for k being Nat holds
( ( Radix (k -' 1) <= x implies SDSub_Add_Carry (x,k) = 1 ) & ( x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = - 1 ) & ( not Radix (k -' 1) <= x & not x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = 0 ) );