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:3;
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 INT = 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 object ; :: 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 object such that
A9: xx in dom xn and
A10: z = xn . xx by FUNCT_1:def 3;
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:8;
then A11: DigA (x,xx) is Element of k -SD by RADIX_1:16;
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:8;
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, CARD_1:def 7;
deffunc H2( Nat) -> Element of INT = 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 object ; :: 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 object such that
A18: yy in dom yn and
A19: z = yn . yy by FUNCT_1:def 3;
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:8;
then A20: DigA (y,yy) is Element of k -SD by RADIX_1:16;
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:8;
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, CARD_1:def 7;
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:8;
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:3;
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:8;
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:8;
(x '+' y) . i = (xn '+' yn) . i
proof
A31: i <= n + 1 by A30, FINSEQ_1:1;
A32: i >= 1 by A29, FINSEQ_1:1;
now :: thesis: (x '+' y) . i = (xn '+' yn) . i
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:9;
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:9;
then A36: i -' 1 in Seg n by A35, A34, FINSEQ_1:1;
(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:232
.= (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,0)) + (DigA (y,0)))) by XREAL_1:232
.= (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:232
.= (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:232
.= 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:74
.= (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:3
.= ((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:6
.= ((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:2, 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:18, 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))
.= (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