let k be Nat; :: thesis: for n being Nat st n >= 1 holds
for x, y being Tuple of n,(k -SD ) st k >= 2 holds
(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,n) + (DigA y,n))) * ((Radix k) |^ n)) = (SDDec x) + (SDDec y)
defpred S1[ Nat] means for x, y being Tuple of $1,(k -SD ) st k >= 2 holds
(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,$1) + (DigA y,$1))) * ((Radix k) |^ $1)) = (SDDec x) + (SDDec y);
A1: S1[1]
proof
let x, y be Tuple of 1,(k -SD ); :: thesis: ( k >= 2 implies (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,1) + (DigA y,1))) * ((Radix k) |^ 1)) = (SDDec x) + (SDDec y) )
assume A2: k >= 2 ; :: thesis: (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,1) + (DigA y,1))) * ((Radix k) |^ 1)) = (SDDec x) + (SDDec y)
A3: 1 in Seg 1 by FINSEQ_1:4, TARSKI:def 1;
1 - 1 = 0 ;
then A4: 1 -' 1 = 0 by XREAL_0:def 2;
A5: DigA (x '+' y),1 = Add x,y,1,k by A3, RADIX_1:def 14
.= (SD_Add_Data ((DigA x,1) + (DigA y,1)),k) + (SD_Add_Carry ((DigA x,0 ) + (DigA y,0 ))) by A2, A3, A4, RADIX_1:def 13
.= (SD_Add_Data ((DigA x,1) + (DigA y,1)),k) + (SD_Add_Carry (0 + (DigA y,0 ))) by RADIX_1:def 3
.= (SD_Add_Data ((DigA x,1) + (DigA y,1)),k) + 0 by RADIX_1:21, RADIX_1:def 3 ;
A6: SDDec y = DigA y,1 by Th7;
A7: SDDec (x '+' y) = SD_Add_Data ((DigA x,1) + (DigA y,1)),k by A5, Th7;
A8: SD_Add_Data ((DigA x,1) + (DigA y,1)),k = ((DigA x,1) + (DigA y,1)) - ((SD_Add_Carry ((DigA x,1) + (DigA y,1))) * (Radix k)) by RADIX_1:def 11;
thus (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,1) + (DigA y,1))) * ((Radix k) |^ 1)) = (SD_Add_Data ((DigA x,1) + (DigA y,1)),k) + ((SD_Add_Carry ((DigA x,1) + (DigA y,1))) * (Radix k)) by A7, NEWTON:10
.= (SDDec x) + (SDDec y) by A6, A8, Th7 ; :: thesis: verum
end;
A9: 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
A10: n >= 1 and
A11: S1[n] ; :: thesis: S1[n + 1]
let x, y be Tuple of (n + 1),(k -SD ); :: thesis: ( k >= 2 implies (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,(n + 1)) + (DigA y,(n + 1)))) * ((Radix k) |^ (n + 1))) = (SDDec x) + (SDDec y) )
assume A12: k >= 2 ; :: thesis: (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,(n + 1)) + (DigA y,(n + 1)))) * ((Radix k) |^ (n + 1))) = (SDDec x) + (SDDec y)
deffunc H1( Nat) -> Element of K485() = DigB x,$1;
consider xn being FinSequence of INT such that
A13: len xn = n and
A14: for i being Nat st i in dom xn holds
xn . i = H1(i) from FINSEQ_2:sch 1();
 A15: dom xn = Seg n by A13, FINSEQ_1:def 3;
rng xn c= k -SD
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng xn or z in k -SD )
assume z in rng xn ; :: thesis: z in k -SD
then consider xx being set such that
A16: xx in dom xn and
A17: z = xn . xx by FUNCT_1:def 5;
reconsider xx = xx as Element of NAT by A16;
A18: dom xn = Seg n by A13, FINSEQ_1:def 3;
A19: z = DigB x,xx by A14, A16, A17
.= DigA x,xx by RADIX_1:def 4 ;
xx in Seg (n + 1) by A16, A18, FINSEQ_2:9;
then DigA x,xx is Element of k -SD by RADIX_1:19;
hence z in k -SD by A19; :: thesis: verum
end;
then reconsider xn = xn as FinSequence of k -SD by FINSEQ_1:def 4;
A20: for i being Nat st i in Seg n holds
xn . i = x . i
proof
let i be Nat; :: thesis: ( i in Seg n implies xn . i = x . i )
assume A21: i in Seg n ; :: thesis: xn . i = x . i
then A22: i in Seg (n + 1) by FINSEQ_2:9;
xn . i = DigB x,i by A14, A21, A15
.= DigA x,i by RADIX_1:def 4 ;
hence xn . i = x . i by A22, RADIX_1:def 3; :: thesis: verum
end;
deffunc H2( Nat) -> Element of K485() = DigB y,$1;
consider yn being FinSequence of INT such that
A23: len yn = n and
A24: for i being Nat st i in dom yn holds
yn . i = H2(i) from FINSEQ_2:sch 1();
 A25: dom yn = Seg n by A23, FINSEQ_1:def 3;
rng yn c= k -SD
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng yn or z in k -SD )
assume z in rng yn ; :: thesis: z in k -SD
then consider yy being set such that
A26: yy in dom yn and
A27: z = yn . yy by FUNCT_1:def 5;
reconsider yy = yy as Element of NAT by A26;
A28: dom yn = Seg n by A23, FINSEQ_1:def 3;
A29: z = DigB y,yy by A24, A26, A27
.= DigA y,yy by RADIX_1:def 4 ;
yy in Seg (n + 1) by A26, A28, FINSEQ_2:9;
then DigA y,yy is Element of k -SD by RADIX_1:19;
hence z in k -SD by A29; :: thesis: verum
end;
then reconsider yn = yn as FinSequence of k -SD by FINSEQ_1:def 4;
A30: for i being Nat st i in Seg n holds
yn . i = y . i
proof
let i be Nat; :: thesis: ( i in Seg n implies yn . i = y . i )
assume A31: i in Seg n ; :: thesis: yn . i = y . i
then A32: i in Seg (n + 1) by FINSEQ_2:9;
yn . i = DigB y,i by A24, A31, A25
.= DigA y,i by RADIX_1:def 4 ;
hence yn . i = y . i by A32, RADIX_1:def 3; :: thesis: verum
end;
reconsider xn = xn as Tuple of n,(k -SD ) by A13, FINSEQ_2:110;
reconsider yn = yn as Tuple of n,(k -SD ) by A23, FINSEQ_2:110;
A33: for i being Element of NAT st i in Seg n holds
DigA x,i = DigA xn,i
proof
let i be Element of NAT ; :: thesis: ( i in Seg n implies DigA x,i = DigA xn,i )
assume A34: i in Seg n ; :: thesis: DigA x,i = DigA xn,i
then i in Seg (n + 1) by FINSEQ_2:9;
then DigA x,i = x . i by RADIX_1:def 3
.= xn . i by A20, A34 ;
hence DigA x,i = DigA xn,i by A34, RADIX_1:def 3; :: thesis: verum
end;
A35: for i being Nat st i in Seg n holds
DigA y,i = DigA yn,i
proof
let i be Nat; :: thesis: ( i in Seg n implies DigA y,i = DigA yn,i )
assume A36: i in Seg n ; :: thesis: DigA y,i = DigA yn,i
then i in Seg (n + 1) by FINSEQ_2:9;
then DigA y,i = y . i by RADIX_1:def 3
.= yn . i by A30, A36 ;
hence DigA y,i = DigA yn,i by A36, RADIX_1:def 3; :: thesis: verum
end;
A37: Sum (DigitSD (x '+' y)) = Sum ((DigitSD (xn '+' yn)) ^ <*(SubDigit (x '+' y),(n + 1),k)*>)
proof
for i being Nat st i in Seg n holds
(x '+' y) . i = (xn '+' yn) . i
proof
let i be Nat; :: thesis: ( i in Seg n implies (x '+' y) . i = (xn '+' yn) . i )
assume A38: i in Seg n ; :: thesis: (x '+' y) . i = (xn '+' yn) . i
then A39: i in Seg (n + 1) by FINSEQ_2:9;
(x '+' y) . i = (xn '+' yn) . i
proof
A40: ( i >= 1 & i <= n + 1 ) by A39, FINSEQ_1:3;
now
per cases ( i > 1 or i = 1 ) by A40, XXREAL_0:1;
suppose A41: i > 1 ; :: thesis: (x '+' y) . i = (xn '+' yn) . i
then i -' 1 > 1 -' 1 by NAT_D:57;
then A42: i -' 1 >= 1 by NAT_1:14;
i - 1 > 1 - 1 by A41, XREAL_1:11;
then A43: i -' 1 = i - 1 by XREAL_0:def 2;
i - 1 <= (n + 1) - 1 by A40, XREAL_1:11;
then A44: i -' 1 in Seg n by A42, A43, FINSEQ_1:3;
(x '+' y) . i = DigA (x '+' y),i by A39, RADIX_1:def 3
.= Add x,y,i,k by A39, RADIX_1:def 14
.= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)))) by A12, A39, RADIX_1:def 13
.= (SD_Add_Data ((DigA xn,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)))) by A33, A38
.= (SD_Add_Data ((DigA xn,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA xn,(i -' 1)) + (DigA y,(i -' 1)))) by A33, A44
.= (SD_Add_Data ((DigA xn,i) + (DigA yn,i)),k) + (SD_Add_Carry ((DigA xn,(i -' 1)) + (DigA y,(i -' 1)))) by A35, A38
.= (SD_Add_Data ((DigA xn,i) + (DigA yn,i)),k) + (SD_Add_Carry ((DigA xn,(i -' 1)) + (DigA yn,(i -' 1)))) by A35, A44
.= Add xn,yn,i,k by A12, A38, RADIX_1:def 13
.= DigA (xn '+' yn),i by A38, RADIX_1:def 14 ;
hence (x '+' y) . i = (xn '+' yn) . i by A38, RADIX_1:def 3; :: thesis: verum
end;
suppose A45: i = 1 ; :: thesis: (x '+' y) . i = (xn '+' yn) . i
(x '+' y) . i = DigA (x '+' y),i by A39, RADIX_1:def 3
.= Add x,y,i,k by A39, RADIX_1:def 14
.= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(1 -' 1)) + (DigA y,(1 -' 1)))) by A12, A39, A45, RADIX_1:def 13
.= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,0 ) + (DigA y,(1 -' 1)))) by XREAL_1:234
.= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,0 ) + (DigA y,0 ))) by XREAL_1:234
.= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry (0 + (DigA y,0 ))) by RADIX_1:def 3
.= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry (0 + 0 )) by RADIX_1:def 3
.= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA xn,0 ) + 0 )) by RADIX_1:def 3
.= (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA xn,0 ) + (DigA yn,0 ))) by RADIX_1:def 3
.= (SD_Add_Data ((DigA xn,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA xn,0 ) + (DigA yn,0 ))) by A33, A38
.= (SD_Add_Data ((DigA xn,i) + (DigA yn,i)),k) + (SD_Add_Carry ((DigA xn,0 ) + (DigA yn,0 ))) by A35, A38
.= (SD_Add_Data ((DigA xn,i) + (DigA yn,i)),k) + (SD_Add_Carry ((DigA xn,(1 -' 1)) + (DigA yn,0 ))) by XREAL_1:234
.= (SD_Add_Data ((DigA xn,i) + (DigA yn,i)),k) + (SD_Add_Carry ((DigA xn,(i -' 1)) + (DigA yn,(i -' 1)))) by A45, XREAL_1:234
.= Add xn,yn,i,k by A12, A38, RADIX_1:def 13
.= DigA (xn '+' yn),i by A38, RADIX_1:def 14 ;
hence (x '+' y) . i = (xn '+' yn) . i by A38, RADIX_1:def 3; :: thesis: verum
end;
end;
end;
hence (x '+' y) . i = (xn '+' yn) . i ; :: thesis: verum
end;
hence (x '+' y) . i = (xn '+' yn) . i ; :: thesis: verum
end;
hence Sum (DigitSD (x '+' y)) = Sum ((DigitSD (xn '+' yn)) ^ <*(SubDigit (x '+' y),(n + 1),k)*>) by Th9; :: thesis: verum
end;
A46: n + 1 in Seg (n + 1) by FINSEQ_1:5;
A47: n in Seg n by A10, FINSEQ_1:5;
SDDec (x '+' y) = Sum ((DigitSD (xn '+' yn)) ^ <*(SubDigit (x '+' y),(n + 1),k)*>) by A37, RADIX_1:def 7
.= (Sum (DigitSD (xn '+' yn))) + (SubDigit (x '+' y),(n + 1),k) by RVSUM_1:104
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ ((n + 1) -' 1)) * (DigB (x '+' y),(n + 1))) by RADIX_1:def 5
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * (DigB (x '+' y),(n + 1))) by NAT_D:34
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * (DigA (x '+' y),(n + 1))) by RADIX_1:def 4
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * (Add x,y,(n + 1),k)) by A46, RADIX_1:def 14
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * ((SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k) + (SD_Add_Carry ((DigA x,((n + 1) -' 1)) + (DigA y,((n + 1) -' 1)))))) by A12, A46, RADIX_1:def 13
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * ((SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k) + (SD_Add_Carry ((DigA x,n) + (DigA y,((n + 1) -' 1)))))) by NAT_D:34
.= (Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * ((SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k) + (SD_Add_Carry ((DigA x,n) + (DigA y,n))))) by NAT_D:34
.= ((Sum (DigitSD (xn '+' yn))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA x,n) + (DigA y,n))))) + (((Radix k) |^ n) * (SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k))
.= ((SDDec (xn '+' yn)) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA x,n) + (DigA y,n))))) + (((Radix k) |^ n) * (SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k)) by RADIX_1:def 7
.= ((SDDec (xn '+' yn)) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA xn,n) + (DigA y,n))))) + (((Radix k) |^ n) * (SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k)) by A33, A47
.= ((SDDec (xn '+' yn)) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA xn,n) + (DigA yn,n))))) + (((Radix k) |^ n) * (SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k)) by A10, A35, FINSEQ_1:5
.= ((SDDec xn) + (SDDec yn)) + (((Radix k) |^ n) * (SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k)) by A11, A12 ;
then (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,(n + 1)) + (DigA y,(n + 1)))) * ((Radix k) |^ (n + 1))) = ((SDDec xn) + (SDDec yn)) + ((((Radix k) |^ n) * (SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k)) + ((SD_Add_Carry ((DigA x,(n + 1)) + (DigA y,(n + 1)))) * ((Radix k) |^ (n + 1))))
.= ((SDDec xn) + (SDDec yn)) + ((((Radix k) |^ n) * (SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k)) + ((SD_Add_Carry ((DigA x,(n + 1)) + (DigA y,(n + 1)))) * (((Radix k) |^ n) * (Radix k)))) by NEWTON:11
.= ((SDDec xn) + (SDDec yn)) + (((Radix k) |^ n) * ((SD_Add_Data ((DigA x,(n + 1)) + (DigA y,(n + 1))),k) + ((SD_Add_Carry ((DigA x,(n + 1)) + (DigA y,(n + 1)))) * (Radix k))))
.= ((SDDec xn) + (SDDec yn)) + (((Radix k) |^ n) * ((DigA x,(n + 1)) + (DigA y,(n + 1)))) by Th8
.= ((SDDec xn) + (((Radix k) |^ n) * (DigA x,(n + 1)))) + ((SDDec yn) + (((Radix k) |^ n) * (DigA y,(n + 1))))
.= (SDDec x) + ((SDDec yn) + (((Radix k) |^ n) * (DigA y,(n + 1)))) by A20, Th10 ;
hence (SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,(n + 1)) + (DigA y,(n + 1)))) * ((Radix k) |^ (n + 1))) = (SDDec x) + (SDDec y) by A30, Th10; :: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch 8(A1, A9);
 hence for n being Nat st n >= 1 holds
for x, y being Tuple of n,(k -SD ) st k >= 2 holds
(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA x,n) + (DigA y,n))) * ((Radix k) |^ n)) = (SDDec x) + (SDDec y) ; :: thesis: verum