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:12;
then A1: (- 1) + (- 1) <= (SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k)) by XREAL_1:7;
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:13;
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:12;
then (SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k)) <= 1 + 1 by XREAL_1:7;
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:24;
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