defpred S1[ Nat] means for k, x, y being Nat st k >= 2 & x is_represented_by $1,k & y is_represented_by $1,k holds
x + y = (SDDec ((DecSD x,$1,k) '+' (DecSD y,$1,k))) + (((Radix k) |^ $1) * (SD_Add_Carry ((DigA (DecSD x,$1,k),$1) + (DigA (DecSD y,$1,k),$1))));
let n be Nat; :: thesis: ( n >= 1 implies for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD x,n,k) '+' (DecSD y,n,k))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (DecSD x,n,k),n) + (DigA (DecSD y,n,k),n)))) )
assume A1: n >= 1 ; :: thesis: for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD x,n,k) '+' (DecSD y,n,k))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (DecSD x,n,k),n) + (DigA (DecSD y,n,k),n))))
A2: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
A3: n >= 1 and
A4: S1[n] ; :: thesis: S1[n + 1]
A5: n in Seg n by A3, FINSEQ_1:5;
let k, x, y be Nat; :: thesis: ( k >= 2 & x is_represented_by n + 1,k & y is_represented_by n + 1,k implies x + y = (SDDec ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),(n + 1)) + (DigA (DecSD y,(n + 1),k),(n + 1))))) )
A6: n + 1 in Seg (n + 1) by FINSEQ_1:5;
set z = (DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k);
set yn = y mod ((Radix k) |^ n);
set xn = x mod ((Radix k) |^ n);
assume that
A7: k >= 2 and
A8: x is_represented_by n + 1,k and
A9: y is_represented_by n + 1,k ; :: thesis: x + y = (SDDec ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),(n + 1)) + (DigA (DecSD y,(n + 1),k),(n + 1)))))
set zn = (DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k);
A10: len (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) = n by FINSEQ_1:def 18;
A11: len (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) = n + 1 by FINSEQ_1:def 18;
A12: for i being Nat st 1 <= i & i <= len (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) holds
(DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) implies (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i )
assume that
A13: 1 <= i and
A14: i <= len (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) ; :: thesis: (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i
A15: i -' 1 = i - 1 by A13, XREAL_1:235;
A16: i <= n + 1 by A14, FINSEQ_1:def 18;
then A17: i in Seg (n + 1) by A13, FINSEQ_1:3;
then A18: i in dom (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) by A11, FINSEQ_1:def 3;
per cases ( i in Seg n or i = n + 1 ) by A17, FINSEQ_2:8;
suppose A19: i in Seg n ; :: thesis: (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i
then A20: i in dom (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) by A10, FINSEQ_1:def 3;
then A21: ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i = (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) . i by FINSEQ_1:def 7
.= (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) /. i by A20, PARTFUN1:def 8
.= SubDigit ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)),i,k by A19, Def6
.= ((Radix k) |^ (i -' 1)) * (Add (DecSD (x mod ((Radix k) |^ n)),n,k),(DecSD (y mod ((Radix k) |^ n)),n,k),i,k) by A19, Def14
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),(i -' 1)) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),(i -' 1))))) by A7, A19, Def13 ;
A22: (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) /. i by A18, PARTFUN1:def 8
.= SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),i,k by A17, Def6
.= ((Radix k) |^ (i -' 1)) * (Add (DecSD x,(n + 1),k),(DecSD y,(n + 1),k),i,k) by A17, Def14
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD x,(n + 1),k),i) + (DigA (DecSD y,(n + 1),k),i)),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),(i -' 1)) + (DigA (DecSD y,(n + 1),k),(i -' 1))))) by A7, A17, Def13 ;
now
per cases ( i = 1 or i > 1 ) by A13, XXREAL_0:1;
suppose A23: i = 1 ; :: thesis: (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i
then A24: ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i = ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),(i -' 1)) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),0 )))) by A21, XREAL_1:234
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),0 ) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),0 )))) by A23, XREAL_1:234
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),0 ) + 0 ))) by Def3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) + 0 ) by Def3, Th21 ;
(DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD x,(n + 1),k),i) + (DigA (DecSD y,(n + 1),k),i)),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),(i -' 1)) + (DigA (DecSD y,(n + 1),k),0 )))) by A22, A23, XREAL_1:234
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD x,(n + 1),k),i) + (DigA (DecSD y,(n + 1),k),i)),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),0 ) + (DigA (DecSD y,(n + 1),k),0 )))) by A23, XREAL_1:234
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD x,(n + 1),k),i) + (DigA (DecSD y,(n + 1),k),i)),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),0 ) + 0 ))) by Def3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD x,(n + 1),k),i) + (DigA (DecSD y,(n + 1),k),i)),k) + 0 ) by Def3, Th21
.= ((Radix k) |^ (i -' 1)) * (SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD y,(n + 1),k),i)),k) by A19, Lm3
.= ((Radix k) |^ (i -' 1)) * (SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) by A19, Lm3 ;
hence (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i by A24; :: thesis: verum
end;
suppose A25: i > 1 ; :: thesis: (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i
A26: i - 1 <= n by A16, XREAL_1:22;
i -' 1 >= 1 by A25, NAT_D:49;
then A27: i -' 1 in Seg n by A15, A26, FINSEQ_1:3;
(DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD y,(n + 1),k),i)),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),(i -' 1)) + (DigA (DecSD y,(n + 1),k),(i -' 1))))) by A19, A22, Lm3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),(i -' 1)) + (DigA (DecSD y,(n + 1),k),(i -' 1))))) by A19, Lm3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),(i -' 1)) + (DigA (DecSD y,(n + 1),k),(i -' 1))))) by A27, Lm3
.= ((Radix k) |^ (i -' 1)) * ((SD_Add_Data ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),i) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),i)),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),(i -' 1)) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),(i -' 1))))) by A27, Lm3 ;
hence (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i by A21; :: thesis: verum
end;
end;
end;
hence (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i ; :: thesis: verum
end;
suppose A28: i = n + 1 ; :: thesis: (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i
then ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . ((len (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) + 1) by FINSEQ_1:def 18
.= SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k by FINSEQ_1:59
.= (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) /. (n + 1) by A6, Def6
.= (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . (n + 1) by A18, A28, PARTFUN1:def 8 ;
hence (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . i = ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) . i by A28; :: thesis: verum
end;
end;
end;
A29: SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k = ((Radix k) |^ n) * (DigB ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1)) by NAT_D:34;
A30: Radix k > 0 by POWER:39;
then A31: x = ((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n)) by NAT_D:2, PREPOWER:13;
set y1 = y div ((Radix k) |^ n);
set x1 = x div ((Radix k) |^ n);
A32: len <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*> = 1 by FINSEQ_1:56;
A33: DigA (DecSD y,(n + 1),k),(n + 1) = y div ((Radix k) |^ n) by A9, Th27;
y mod ((Radix k) |^ n) < (Radix k) |^ n by A30, NAT_D:1, PREPOWER:13;
then A34: y mod ((Radix k) |^ n) is_represented_by n,k by Def12;
x mod ((Radix k) |^ n) < (Radix k) |^ n by A30, NAT_D:1, PREPOWER:13;
then A35: x mod ((Radix k) |^ n) is_represented_by n,k by Def12;
len ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) = (len (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) + (len <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) by FINSEQ_1:35
.= n + 1 by A32, FINSEQ_1:def 18 ;
then len (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) = len ((DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*>) by FINSEQ_1:def 18;
then DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)) = (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) ^ <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*> by A12, FINSEQ_1:18;
then SDDec ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)) = (((Radix k) |^ n) * (DigB ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1))) + (Sum (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) by A29, RVSUM_1:104
.= ((Add (DecSD x,(n + 1),k),(DecSD y,(n + 1),k),(n + 1),k) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) by A6, Def14
.= (((SD_Add_Data ((DigA (DecSD x,(n + 1),k),(n + 1)) + (DigA (DecSD y,(n + 1),k),(n + 1))),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),((n + 1) -' 1)) + (DigA (DecSD y,(n + 1),k),((n + 1) -' 1))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) by A6, A7, Def13
.= (((SD_Add_Data ((DigA (DecSD x,(n + 1),k),(n + 1)) + (DigA (DecSD y,(n + 1),k),(n + 1))),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),((n + 1) -' 1)) + (DigA (DecSD y,(n + 1),k),n)))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) by NAT_D:34
.= (((SD_Add_Data ((DigA (DecSD x,(n + 1),k),(n + 1)) + (DigA (DecSD y,(n + 1),k),(n + 1))),k) + (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),n) + (DigA (DecSD y,(n + 1),k),n)))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) by NAT_D:34
.= (((SD_Add_Data ((DigA (DecSD x,(n + 1),k),(n + 1)) + (DigA (DecSD y,(n + 1),k),(n + 1))),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n) + (DigA (DecSD y,(n + 1),k),n)))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) by A5, Lm3
.= (((SD_Add_Data ((DigA (DecSD x,(n + 1),k),(n + 1)) + (DigA (DecSD y,(n + 1),k),(n + 1))),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),n)))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) by A5, Lm3
.= (((SD_Add_Data ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k) + (SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),n)))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))) by A8, A33, Th27
.= ((SD_Add_Data ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k) * ((Radix k) |^ n)) + (((SD_Add_Carry ((DigA (DecSD (x mod ((Radix k) |^ n)),n,k),n) + (DigA (DecSD (y mod ((Radix k) |^ n)),n,k),n))) * ((Radix k) |^ n)) + (SDDec ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))))
.= ((SD_Add_Data ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k) * ((Radix k) |^ n)) + ((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) by A4, A7, A35, A34
.= (((SD_Add_Data ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n)) ;
then (SDDec ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * ((Radix k) |^ (n + 1))) = ((((SD_Add_Data ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k) * ((Radix k) |^ n)) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * ((Radix k) |^ (n + 1)))) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n))
.= ((((SD_Add_Data ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k) * ((Radix k) |^ n)) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * (((Radix k) |^ n) * (Radix k)))) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n)) by NEWTON:11
.= (((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n))) + (((y div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (y mod ((Radix k) |^ n)))
.= x + y by A30, A31, NAT_D:2, PREPOWER:13 ;
hence x + y = (SDDec ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA (DecSD x,(n + 1),k),(n + 1)) + (DigA (DecSD y,(n + 1),k),(n + 1))))) by A8, A33, Th27; :: thesis: verum
end;
A36: S1[1]
proof
let k, x, y be Nat; :: thesis: ( k >= 2 & x is_represented_by 1,k & y is_represented_by 1,k implies x + y = (SDDec ((DecSD x,1,k) '+' (DecSD y,1,k))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA (DecSD x,1,k),1) + (DigA (DecSD y,1,k),1)))) )
assume ( k >= 2 & x is_represented_by 1,k & y is_represented_by 1,k ) ; :: thesis: x + y = (SDDec ((DecSD x,1,k) '+' (DecSD y,1,k))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA (DecSD x,1,k),1) + (DigA (DecSD y,1,k),1))))
then A37: ( SDDec ((DecSD x,1,k) '+' (DecSD y,1,k)) = SD_Add_Data (x + y),k & SD_Add_Carry ((DigA (DecSD x,1,k),1) + (DigA (DecSD y,1,k),1)) = SD_Add_Carry (x + y) ) by Th26, Th28;
(SD_Add_Data (x + y),k) + ((SD_Add_Carry (x + y)) * (Radix k)) = (x + y) - 0 ;
hence x + y = (SDDec ((DecSD x,1,k) '+' (DecSD y,1,k))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA (DecSD x,1,k),1) + (DigA (DecSD y,1,k),1)))) by A37, NEWTON:10; :: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch 8(A36, A2);
 hence for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD x,n,k) '+' (DecSD y,n,k))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (DecSD x,n,k),n) + (DigA (DecSD y,n,k),n)))) by A1; :: thesis: verum