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 )
assume A1: 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;
then A4: - (Radix (k -' 1)) <= - 2 by XREAL_1:26;
set CC = (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k);
A5: k >= 2 by A1, XXREAL_0:2;
then A6: ( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 ) by RADIX_3:13;
A7: ( - 1 <= SDSub_Add_Carry y,k & SDSub_Add_Carry y,k <= 1 ) by A5, RADIX_3:13;
then (- 1) + (- 1) <= (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k) by A6, XREAL_1:9;
then A8: - (Radix (k -' 1)) <= (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k) by A4, XXREAL_0:2;
(SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k) <= 1 + 1 by A6, A7, XREAL_1:9;
then (SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k) < Radix (k -' 1) by A3, XXREAL_0:2;
hence SDSub_Add_Carry ((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)),k = 0 by A8, RADIX_3:def 3; :: thesis: verum