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