let x, y be Integer; :: thesis: for k being Nat st 3 <= k holds
SDSub_Add_Carry ((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)),k = 0
let k be Nat; :: thesis: ( 3 <= k implies SDSub_Add_Carry ((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)),k = 0 )
set CC = (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k);
( - 1 <= SDSub_Add_Carry x,k & - 1 <= SDSub_Add_Carry y,k ) by RADIX_3:13;
then A1: (- 1) + (- 1) <= (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k) by XREAL_1:9;
assume k >= 3 ; :: thesis: SDSub_Add_Carry ((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)),k = 0
then A2: k - 1 >= 3 - 1 by XREAL_1:15;
then k - 1 > 0 by XXREAL_0:2;
then k - 1 = k -' 1 by XREAL_0:def 2;
then A3: Radix (k -' 1) > 2 by A2, Th1;
( SDSub_Add_Carry x,k <= 1 & SDSub_Add_Carry y,k <= 1 ) by RADIX_3:13;
then (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k) <= 1 + 1 by XREAL_1:9;
then A4: (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k) < Radix (k -' 1) by A3, XXREAL_0:2;
- (Radix (k -' 1)) <= - 2 by A3, XREAL_1:26;
then - (Radix (k -' 1)) <= (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k) by A1, XXREAL_0:2;
hence SDSub_Add_Carry ((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)),k = 0 by A4, RADIX_3:def 3; :: thesis: verum