Copyright (c) 2003 Association of Mizar Users
environ
vocabulary INT_1, NAT_1, ARYTM_1, POWER, MIDSP_3, FINSEQ_1, FUNCT_1, RELAT_1,
RLVECT_1, RADIX_1, FINSEQ_4, RADIX_3, RADIX_4, GROUP_1;
notation TARSKI, SUBSET_1, XCMPLX_0, XREAL_0, INT_1, NAT_1, FUNCT_1, POWER,
FINSEQ_1, FINSEQ_4, BINARITH, TREES_4, WSIERP_1, MIDSP_3, RADIX_1,
RADIX_3;
constructors REAL_1, POWER, BINARITH, FINSEQ_4, EULER_2, RADIX_3, MEMBERED;
clusters INT_1, RELSET_1, NAT_1, MEMBERED;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
theorems AXIOMS, REAL_1, REAL_2, RADIX_1, POWER, NAT_1, INT_1, BINARITH,
FINSEQ_1, FINSEQ_2, FINSEQ_4, JORDAN3, GOBOARD9, NEWTON, RVSUM_1,
PREPOWER, JORDAN12, EULER_2, RADIX_3, XCMPLX_0, XCMPLX_1;
schemes FINSEQ_2, INT_2, BINOM;
begin :: Some Useful Theorems
reserve i,n,m,k,x,y for Nat,
i1 for Integer;
theorem Th1:
for k be Nat st 2 <= k holds 2 < Radix(k)
proof
defpred P[Nat] means 2 < Radix($1);
Radix(2) = 2 to_power (1+1) by RADIX_1:def 1
.= 2 to_power 1 * 2 to_power 1 by POWER:32
.= 2 * (2 to_power 1) by POWER:30
.= 2 * 2 by POWER:30
.= 4;
then A1: P[2];
A2: for kk be Nat st
kk >= 2 & P[kk] holds P[(kk + 1)]
proof
let kk be Nat;
assume
A3: 2 <= kk & 2 < Radix(kk);
A4: Radix(kk + 1) = 2 to_power (kk + 1) by RADIX_1:def 1
.= 2 to_power (1) * 2 to_power (kk) by POWER:32
.= 2 * 2 to_power (kk) by POWER:30
.= 2 * Radix(kk) by RADIX_1:def 1;
Radix(kk) > 1 by A3,AXIOMS:22;
hence thesis by A4,REAL_2:144;
end;
2 <= k implies P[k] from Ind2(A1,A2);
hence thesis;
end;
Lm1:
i1 in k-SD_Sub_S implies i1 >= -Radix(k-'1) & i1 <= Radix(k-'1) - 1
proof
assume
A1: i1 in k-SD_Sub_S;
k-SD_Sub_S =
{e where e is Element of INT:
-Radix(k-'1) <= e & e <= Radix(k-'1) - 1 } by RADIX_3:def 1;
then consider i be Element of INT such that
A2: i = i1 and
A3: -Radix(k-'1) <= i & i <= Radix(k-'1) - 1 by A1;
thus thesis by A2,A3;
end;
Lm2:
for i st i in Seg n holds
DigA(DecSD(m,n+1,k),i)=DigA(DecSD(m,n,k),i)
proof
let i;
assume
A1: i in Seg n;
then A2: 1 <= i & i <= n by FINSEQ_1:3;
then i <= n+1 by NAT_1:37;
then A3: i in Seg (n+1) by A2,FINSEQ_1:3;
DigA(DecSD(m,n,k),i)
= DigitDC(m,i,k) by A1,RADIX_1:def 9
.= DigA(DecSD(m,n+1,k),i) by A3,RADIX_1:def 9;
hence thesis;
end;
Lm3:
for k,x,n be Nat st
n >= 1 & x is_represented_by (n+1),k holds
DigA(DecSD(x mod (Radix(k) |^ n),n,k),n) = DigA(DecSD(x,n,k),n)
proof
let k,x,n be Nat;
assume n >= 1 & x is_represented_by (n+1),k;
then n <> 0;
then A1: n in Seg n by FINSEQ_1:5;
set xn = x mod (Radix(k) |^ n);
set Rn = (Radix(k) |^ n);
DigA(DecSD(xn,n,k),n)
= DigitDC(xn,n,k) by A1,RADIX_1:def 9
.= ((x mod Rn) mod Rn) div (Radix(k) |^ (n-'1)) by RADIX_1:def 8
.= (x mod Rn) div (Radix(k) |^ (n-'1)) by EULER_2:7
.= DigitDC(x,n,k) by RADIX_1:def 8
.= DigA(DecSD(x,n,k),n) by A1,RADIX_1:def 9;
hence thesis;
end;
begin :: Carry operation at n+1 digits Radix-2^k SD_Sub number
theorem Th2:
for x,y be Integer, k be Nat st 3 <= k holds
SDSub_Add_Carry( SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k), k ) = 0
proof
let x,y be Integer, k be Nat;
assume
A1: k >= 3;
then A2: k - 1 >= 3 - 1 by REAL_1:92;
then k - 1 > 0 by AXIOMS:22;
then k - 1 = k -' 1 by BINARITH:def 3;
then A3: Radix(k-'1) > 2 by A2,Th1;
then A4: -Radix(k-'1) <= -2 by REAL_1:50;
set CC = SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k);
A5: k >= 2 by A1,AXIOMS:22;
then A6: -1 <= SDSub_Add_Carry(x,k) & SDSub_Add_Carry(x,k) <= 1 by RADIX_3:13
;
A7: -1 <= SDSub_Add_Carry(y,k) & SDSub_Add_Carry(y,k) <= 1 by A5,RADIX_3:13;
then -1 + -1 <= CC by A6,REAL_1:55;
then A8: -Radix(k-'1) <= CC by A4,AXIOMS:22;
CC <= 1 + 1 by A6,A7,REAL_1:55;
then CC < Radix(k-'1) by A3,AXIOMS:22;
hence SDSub_Add_Carry(CC,k) = 0 by A8,RADIX_3:def 3;
end;
theorem Th3:
2 <= k implies
DigA_SDSub(SD2SDSub(DecSD(m,n,k)),n+1)
= SDSub_Add_Carry( DigA(DecSD(m,n,k),n), k)
proof
assume
A1: 2 <= k;
0 <= n by NAT_1:18;
then 0 + 1 <= n + 1 by REAL_1:55;
then A2: (n+1) in Seg (n+1) by FINSEQ_1:3;
hence DigA_SDSub(SD2SDSub(DecSD(m,n,k)),n+1)
= SD2SDSubDigitS(DecSD(m,n,k), n+1, k) by RADIX_3:def 8
.= SD2SDSubDigit(DecSD(m,n,k), n+1, k) by A1,A2,RADIX_3:def 7
.= SDSub_Add_Carry( DigA(DecSD(m,n,k),n+1-'1), k)
by RADIX_3:def 6
.= SDSub_Add_Carry( DigA(DecSD(m,n,k),n), k) by BINARITH:39;
end;
theorem Th4:
2 <= k & m is_represented_by 1,k implies
DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1+1) = SDSub_Add_Carry(m, k)
proof
assume
A1: 2 <= k & m is_represented_by 1,k;
hence DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1+1)
= SDSub_Add_Carry( DigA(DecSD(m,1,k),1), k) by Th3
.= SDSub_Add_Carry(m, k) by A1,RADIX_1:24;
end;
theorem Th5:
for k,x,n be Nat st
n >= 1 & k >= 3 & x is_represented_by (n+1),k holds
DigA_SDSub(SD2SDSub(DecSD(x mod (Radix(k) |^ n),n,k)),n+1)
= SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
proof
let k,x,n be Nat;
assume
A1: n >= 1 & k >= 3 & x is_represented_by (n+1),k;
A2: n+1 in Seg (n+1) by FINSEQ_1:5;
A3: k >= 2 by A1,AXIOMS:22;
set xn = x mod (Radix(k) |^ n);
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
= SD2SDSubDigitS(DecSD(xn,n,k),n+1,k) by A2,RADIX_3:def 8
.= SD2SDSubDigit(DecSD(xn,n,k),n+1,k) by A2,A3,RADIX_3:def 7
.= SDSub_Add_Carry(DigA(DecSD(xn,n,k),n+1-'1),k) by RADIX_3:def 6
.= SDSub_Add_Carry(DigA(DecSD(xn,n,k),n+0),k) by BINARITH:39
.= SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k) by A1,Lm3;
hence thesis;
end;
theorem Th6:
2 <= k & m is_represented_by 1,k implies
DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1) = m - SDSub_Add_Carry(m,k)*Radix(k)
proof
assume
A1: 2 <= k & m is_represented_by 1,k;
A2: 1 in Seg (1+1) by FINSEQ_1:3;
then A3: DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1)
= SD2SDSubDigitS(DecSD(m,1,k), 1, k) by RADIX_3:def 8
.= SD2SDSubDigit(DecSD(m,1,k), 1, k) by A1,A2,RADIX_3:def 7;
1 in Seg 1 by FINSEQ_1:5;
hence
DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1)
= SDSub_Add_Data( DigA(DecSD(m,1,k),1), k )
+ SDSub_Add_Carry( DigA(DecSD(m,1,k),1-'1), k)
by A3,RADIX_3:def 6
.= SDSub_Add_Data( DigA(DecSD(m,1,k),1), k )
+ SDSub_Add_Carry( DigA(DecSD(m,1,k),0), k) by GOBOARD9:1
.= SDSub_Add_Data( DigA(DecSD(m,1,k),1), k )
+ SDSub_Add_Carry( 0, k) by RADIX_1:def 3
.= SDSub_Add_Data( m, k ) + SDSub_Add_Carry( 0, k) by A1,RADIX_1:24
.= SDSub_Add_Data( m, k ) + 0 by A1,RADIX_3:17
.= m - SDSub_Add_Carry(m,k) * Radix(k) by RADIX_3:def 4;
end;
theorem Th7:
for k,x,n be Nat st
n >= 1 & k >= 2 & x is_represented_by (n+1),k holds
(Radix(k) |^ n) * DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
- (Radix(k) |^ (n+1)) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
+ (Radix(k) |^ n) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k)
proof
let k,x,n be Nat;
assume
A1: n >= 1 & k >= 2 & x is_represented_by (n+1),k;
A2: n+1 in Seg (n+1) by FINSEQ_1:5;
then A3: (n+1) in Seg (n+1+1) by FINSEQ_2:9;
then (Radix(k) |^ n) * DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
= (Radix(k) |^ n) *
(SD2SDSubDigitS(DecSD(x,n+1,k),n+1,k)) by RADIX_3:def 8
.= (Radix(k) |^ n) *
(SD2SDSubDigit(DecSD(x,n+1,k),n+1,k)) by A1,A3,RADIX_3:def 7
.= (Radix(k) |^ n) * (
SDSub_Add_Data(DigA(DecSD(x,n+1,k),n+1),k)
+ SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1-'1),k))
by A2,RADIX_3:def 6
.= (Radix(k) |^ n) * (
SDSub_Add_Data(DigA(DecSD(x,n+1,k),n+1),k)
+ SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by BINARITH:39
.= (Radix(k) |^ n) * (
DigA(DecSD(x,n+1,k),n+1)
- Radix(k) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
+ SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by RADIX_3:def 4
.= (Radix(k) |^ n) * (
( DigA(DecSD(x,n+1,k),n+1)
- Radix(k) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k) ))
+ (Radix(k) |^ n) * (
SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by XCMPLX_1:8
.= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
- (Radix(k) |^ n) * (Radix(k) *
SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k))
+ (Radix(k) |^ n) * (
SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by XCMPLX_1:40
.= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
- ((Radix(k) |^ n) * Radix(k)) *
SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
+ (Radix(k) |^ n) * (
SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by XCMPLX_1:4
.= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
- (Radix(k) |^ (n+1)) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
+ (Radix(k) |^ n) * ( SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) )
by RADIX_3:1;
hence thesis;
end;
begin :: Definition for adder operation on Radix-2^k SD-Sub number
definition
let i,n,k be Nat,
x be Tuple of n,(k-SD_Sub), y be Tuple of n,(k-SD_Sub);
assume A1:i in Seg n & k >= 2;
func SDSubAddDigit(x,y,i,k) -> Element of k-SD_Sub equals
:Def1:
SDSub_Add_Data( DigA_SDSub(x,i) + DigA_SDSub(y,i), k )
+ SDSub_Add_Carry( DigA_SDSub(x,i -'1) + DigA_SDSub(y,i -'1), k);
coherence
proof
set SDAD = SDSub_Add_Data(DigA_SDSub(x,i) + DigA_SDSub(y,i), k );
set SDAC = SDSub_Add_Carry(DigA_SDSub(x,i -'1)+DigA_SDSub(y,i -'1), k);
DigA_SDSub(x,i) is Element of k-SD_Sub by A1,RADIX_3:19;
then A2: DigA_SDSub(x,i) in k-SD_Sub;
A3: k-SD_Sub c= k-SD by A1,RADIX_3:5;
DigA_SDSub(y,i) is Element of k-SD_Sub by A1,RADIX_3:19;
then SDAD in k-SD_Sub_S by A1,A2,A3,RADIX_3:20;
then A4: SDAD >= -Radix(k-'1) & SDAD <= Radix(k-'1) - 1 by Lm1;
A5: -1 <= SDAC & SDAC <= 1 by A1,RADIX_3:13;
then -Radix(k-'1) + -1 <= SDAD + SDAC by A4,REAL_1:55;
then A6: SDAD + SDAC >= -Radix(k-'1) - 1 by XCMPLX_0:def 8;
SDAD + SDAC <= Radix(k-'1) -1 + 1 by A4,A5,REAL_1:55;
then SDAD + SDAC <= Radix(k-'1) + 1 - 1 by XCMPLX_1:29;
then A7: SDAD + SDAC <= Radix(k-'1) by XCMPLX_1:26;
A8: SDAD + SDAC is Element of INT by INT_1:def 2;
k-SD_Sub = {w where w is Element of INT:
w >= -Radix(k -' 1) - 1 & w <= Radix(k -' 1) } by RADIX_3:def 2;
then SDAD + SDAC in k-SD_Sub by A6,A7,A8;
hence thesis;
end;
end;
definition let n,k be Nat,x,y be Tuple of n,(k-SD_Sub);
func x '+' y -> Tuple of n,(k-SD_Sub) means
:Def2:
for i st i in Seg n holds DigA_SDSub(it,i) = SDSubAddDigit(x,y,i,k);
existence
proof
deffunc F(Nat)=SDSubAddDigit(x,y,$1,k);
consider z being FinSequence of (k-SD_Sub) such that
A1: len z = n and
A2: for j be Nat st j in Seg n holds
z.j = F(j) from SeqLambdaD;
reconsider z as Tuple of n,(k-SD_Sub) by A1,FINSEQ_2:110;
take z;
let i;
assume
A3: i in Seg n;
hence DigA_SDSub(z,i) = z.i by RADIX_3:def 5
.= SDSubAddDigit(x,y,i,k) by A2,A3;
end;
uniqueness
proof
let k1,k2 be Tuple of n,(k-SD_Sub) such that
A4: for i be Nat st i in Seg n holds
DigA_SDSub(k1,i) = SDSubAddDigit(x,y,i,k) and
A5: for i be Nat st i in Seg n holds
DigA_SDSub(k2,i) = SDSubAddDigit(x,y,i,k);
A6:len k1 = n & len k2 = n by FINSEQ_2:109;
now let j be Nat;
assume
A7: j in Seg n;
then k1.j = DigA_SDSub(k1,j) by RADIX_3:def 5
.= SDSubAddDigit(x,y,j,k) by A4,A7
.= DigA_SDSub(k2,j) by A5,A7
.= k2.j by A7,RADIX_3:def 5;
hence k1.j = k2.j;
end;
hence k1 = k2 by A6,FINSEQ_2:10;
end;
end;
theorem Th8:
for i st i in Seg n holds
2 <= k implies
SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),i,k)=
SDSubAddDigit(
SD2SDSub(DecSD((x mod (Radix(k) |^ n)),n,k)),
SD2SDSub(DecSD((y mod (Radix(k) |^ n)),n,k)),i,k)
proof
let i;
assume
A1: i in Seg n;
then A2: 1 <= i & i <= n by FINSEQ_1:3;
then A3: i <= n + 1 by NAT_1:37;
then A4: i in Seg (n+1) by A2,FINSEQ_1:3;
i <= (n+1)+1 by A3,NAT_1:37;
then A5: i in Seg ((n+1)+1) by A2,FINSEQ_1:3;
assume
A6: 2 <= k;
set X = x mod (Radix(k) |^ n);
set Y = y mod (Radix(k) |^ n);
A7: SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),i,k)
= SDSub_Add_Data(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k) by A5,A6,Def1;
now per cases;
suppose
A8: i = 1;
then A9: DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
= DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),0) by GOBOARD9:1
.= 0 by RADIX_3:def 5;
A10: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1)
= DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),0) by A8,GOBOARD9:1
.= 0 by RADIX_3:def 5;
A11: DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i)
= DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i) by A1,A6,RADIX_3:21;
A12: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i)
= DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i) by A1,A6,RADIX_3:21;
A13: DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
= DigA_SDSub(SD2SDSub(DecSD(X,n,k)),0) by A8,GOBOARD9:1
.= 0 by RADIX_3:def 5;
DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i-'1)
= DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),0) by A8,GOBOARD9:1
.= 0 by RADIX_3:def 5;
hence thesis by A4,A6,A7,A9,A10,A11,A12,A13,Def1;
suppose
A14: i <> 1;
i >= 1 by A1,FINSEQ_1:3;
then 1 < i by A14,REAL_1:def 5;
then 0 < i-'1 by JORDAN12:1;
then A15: 0 + 1 <= i-'1 by INT_1:20;
i <= n by A1,FINSEQ_1:3;
then i -' 1 <= n by JORDAN3:7;
then A16: i -' 1 in Seg n by A15,FINSEQ_1:3;
SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),i,k
)
= SDSub_Add_Data(
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
by A1,A6,A7,RADIX_3:21
.= SDSub_Add_Data(
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
by A1,A6,RADIX_3:21
.= SDSub_Add_Data(
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
by A6,A16,RADIX_3:21
.= SDSub_Add_Data(
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i-'1), k)
by A6,A16,RADIX_3:21
.= SDSubAddDigit(SD2SDSub(DecSD(X,n,k)),SD2SDSub(DecSD(Y,n,k)),i,k)
by A4,A6,Def1;
hence thesis;
end;
hence thesis;
end;
theorem
for n st n >= 1 holds
for k,x,y st
k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y =
SDSub2IntOut( SD2SDSub(DecSD(x,n,k)) '+' SD2SDSub(DecSD(y,n,k)) )
proof
defpred P[Nat] means
for k,x,y be Nat st
k >= 3 & x is_represented_by $1,k & y is_represented_by $1,k holds
x + y =
SDSub2IntOut( SD2SDSub(DecSD(x,$1,k)) '+' SD2SDSub(DecSD(y,$1,k)) );
A1: P[1]
proof
let k,x,y be Nat;
assume
A2: k >= 3 & x is_represented_by 1,k & y is_represented_by 1,k;
then A3: k >= 2 by AXIOMS:22;
set X = SD2SDSub(DecSD(x,1,k));
set Y = SD2SDSub(DecSD(y,1,k));
reconsider
CRY1 = SDSub_Add_Carry(DigA_SDSub(X,1)+DigA_SDSub(Y,1),k) as Integer;
A4: 1 in Seg (1+1) by FINSEQ_1:3;
then A5: DigA_SDSub(X '+' Y, 1)
= SDSubAddDigit(X,Y,1,k) by Def2
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
+ SDSub_Add_Carry( DigA_SDSub(X,1-'1)+DigA_SDSub(Y,1 -'1), k)
by A3,A4,Def1
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
+ SDSub_Add_Carry( DigA_SDSub(X,0)+DigA_SDSub(Y,1 -'1), k)
by GOBOARD9:1
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
+ SDSub_Add_Carry( DigA_SDSub(X,0) + DigA_SDSub(Y,0), k)
by GOBOARD9:1
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
+ SDSub_Add_Carry( 0 + DigA_SDSub(Y,0), k) by RADIX_3:def 5
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
+ SDSub_Add_Carry(0 + 0, k) by RADIX_3:def 5
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k ) + 0
by A3,RADIX_3:17
.= DigA_SDSub(X,1) + DigA_SDSub(Y,1) - Radix(k) * CRY1 by RADIX_3:def 4;
2 - 1 = 1;
then A6: 2 -' 1 = 1 by BINARITH:def 3;
A7: 2 in Seg (1+1) by FINSEQ_1:3;
then A8: DigA_SDSub(X '+' Y, 2)
= SDSubAddDigit(X,Y,2,k) by Def2
.= SDSub_Add_Data( DigA_SDSub(X,2) + DigA_SDSub(Y,2), k )
+ SDSub_Add_Carry( DigA_SDSub(X,2-'1)+DigA_SDSub(Y,2 -'1), k)
by A3,A7,Def1
.= SDSub_Add_Data( SDSub_Add_Carry(x,k) + DigA_SDSub(Y,2), k )
+ CRY1 by A2,A3,A6,Th4
.= SDSub_Add_Data( SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k), k )
+ CRY1 by A2,A3,Th4
.= SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k)
- Radix(k)
* SDSub_Add_Carry( SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k), k )
+ CRY1 by RADIX_3:def 4
.= SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k)
-Radix(k) * 0 + CRY1 by A2,Th2
.= SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k) - 0 + CRY1;
A9: (SDSub2INT(X '+' Y))/.1
= SDSub2INTDigit((X '+' Y),1,k) by A4,RADIX_3:def 11
.= (Radix(k) |^ (1-'1)) * DigB_SDSub((X '+' Y),1) by RADIX_3:def 10
.= (Radix(k) |^ (0)) * DigB_SDSub((X '+' Y),1) by GOBOARD9:1
.= 1 * DigB_SDSub((X '+' Y),1) by NEWTON:9
.= DigA_SDSub((X '+' Y),1) by RADIX_3:def 9;
reconsider DIG1 = DigA_SDSub((X '+' Y),1) as Element of INT
by INT_1:def 2;
A10: (SDSub2INT(X '+' Y))/.2
= SDSub2INTDigit((X '+' Y),2,k) by A7,RADIX_3:def 11
.= (Radix(k) |^ (2-'1)) * DigB_SDSub((X '+' Y),2) by RADIX_3:def 10
.= Radix(k) * DigB_SDSub((X '+' Y),2) by A6,NEWTON:10
.= Radix(k) * DigA_SDSub((X '+' Y),2) by RADIX_3:def 9;
reconsider DIG2 = Radix(k) * DigA_SDSub((X '+' Y),2) as Element of INT
by INT_1:def 2;
A11: len (SDSub2INT(X '+' Y)) = 1 + 1 by FINSEQ_2:109;
then 1 in dom SDSub2INT(X '+' Y) by A4,FINSEQ_1:def 3;
then A12: SDSub2INT(X '+' Y).1 = DIG1 by A9,FINSEQ_4:def 4;
2 in dom SDSub2INT(X '+' Y) by A7,A11,FINSEQ_1:def 3;
then SDSub2INT(X '+' Y).2 = DIG2 by A10,FINSEQ_4:def 4;
then SDSub2INT(X '+' Y) = <* DIG1 , DIG2 *> by A11,A12,FINSEQ_1:61;
then A13: Sum SDSub2INT(X '+' Y)
= DIG1 + DIG2 by RVSUM_1:107;
reconsider RSDCX = Radix(k)*SDSub_Add_Carry(x,k),
RSDCY = Radix(k)*SDSub_Add_Carry(y,k) as Integer;
reconsider RCRY1 = Radix(k)*
(SDSub_Add_Carry(DigA_SDSub(X,1)+DigA_SDSub(Y,1),k)) as Integer;
A14: DIG1 = x - RSDCX + DigA_SDSub(Y,1) - RCRY1 by A2,A3,A5,Th6
.= x - RSDCX + (y - RSDCY) - RCRY1 by A2,A3,Th6
.= x - RSDCX + (y - RSDCY)+ -RCRY1 by XCMPLX_0:def 8
.= x - RSDCX + (y + -RSDCY) + -RCRY1 by XCMPLX_0:def 8
.= x - RSDCX + y + -RSDCY + -RCRY1 by XCMPLX_1:1
.= x - RSDCX + y - RSDCY + -RCRY1 by XCMPLX_0:def 8
.= x - RSDCX + y - RSDCY - RCRY1 by XCMPLX_0:def 8
.= x + y - RSDCX - RSDCY - RCRY1 by XCMPLX_1:29;
DIG2 = RSDCX + RSDCY + RCRY1 by A8,XCMPLX_1:9;
then DIG1 + DIG2
= x + y - RSDCX - RSDCY - RCRY1 + (RSDCX + (RSDCY + RCRY1)) by A14,
XCMPLX_1:1
.= x + y - RSDCX - RSDCY - RCRY1 + RSDCX + (RSDCY + RCRY1) by XCMPLX_1:1
.= x + y - RSDCX - RSDCY - RCRY1 + RSDCX + RSDCY + RCRY1 by XCMPLX_1:1
.= x + y - RSDCX - RSDCY + RSDCX - RCRY1 + RSDCY + RCRY1 by XCMPLX_1:29
.= x + y - RSDCX - RSDCY + RSDCX + -RCRY1 + RSDCY + RCRY1 by XCMPLX_0:def
8
.= x + y - RSDCX - RSDCY + RSDCX + (-RCRY1 + RSDCY)+RCRY1 by XCMPLX_1:1
.= x + y - RSDCX - RSDCY + RSDCX + ((-RCRY1 + RSDCY)+RCRY1) by XCMPLX_1:1
.= x + y - RSDCX - RSDCY + RSDCX + RSDCY by XCMPLX_1:139
.= x + y - RSDCX + -RSDCY + RSDCX + RSDCY by XCMPLX_0:def 8
.= x + y - RSDCX + (-RSDCY + RSDCX) + RSDCY by XCMPLX_1:1
.= x + y - RSDCX + ((-RSDCY + RSDCX) + RSDCY) by XCMPLX_1:1
.= x + y - RSDCX + RSDCX by XCMPLX_1:139
.= x + y + -RSDCX + RSDCX by XCMPLX_0:def 8
.= x + y + (-RSDCX + RSDCX) by XCMPLX_1:1
.= x + y + 0 by XCMPLX_0:def 6;
hence thesis by A13,RADIX_3:def 12;
end;
A15: for n be Nat st n >= 1 & P[n] holds P[n+1]
proof
let n be Nat;
assume
A16: n >= 1 & P[n];
then n <> 0;
then A17: n in Seg n by FINSEQ_1:5;
A18: n+1 in Seg (n+1) by FINSEQ_1:5;
let k,x,y be Nat;
assume
A19: k >= 3 & x is_represented_by (n+1),k & y is_represented_by (n+1),k;
then A20: k >= 2 by AXIOMS:22;
set xn = x mod (Radix(k) |^ n);
set yn = y mod (Radix(k) |^ n);
set z = SD2SDSub(DecSD(x,n+1,k)) '+' SD2SDSub(DecSD(y,n+1,k));
set zn = SD2SDSub(DecSD(xn,n,k)) '+' SD2SDSub(DecSD(yn,n,k));
Radix(k) <> 0 by RADIX_1:9;
then Radix(k) > 0 by NAT_1:19;
then A21: (Radix(k) |^ n) > 0 by PREPOWER:13;
then A22: x = (x div (Radix(k) |^ n))*(Radix(k) |^ n)
+ (x mod (Radix(k) |^ n)) by NAT_1:47;
xn < Radix(k) |^ n & yn < Radix(k) |^ n by A21,NAT_1:46;
then xn is_represented_by n,k & yn is_represented_by n,k by RADIX_1:def
12;
then A23: xn + yn
= SDSub2IntOut(zn) by A16,A19
.= Sum SDSub2INT(zn) by RADIX_3:def 12;
A24: (n+1) in Seg (n+1+1) by A18,FINSEQ_2:9;
A25: (n+1+1) in Seg (n+1+1) by FINSEQ_1:5;
deffunc G(Nat)=SDSub2INTDigit(z,$1,k);
consider zp being FinSequence of INT such that
A26: len zp = n+1 and
A27: for i be Nat st i in Seg (n+1) holds zp.i = G(i) from SeqLambdaD;
consider zpp being FinSequence of INT such that
A28: len zpp = n and
A29: for i be Nat st i in Seg n holds zpp.i = G(i) from SeqLambdaD;
deffunc GF(Nat)= SDSub2INTDigit(zn,$1,k);
consider znpp being FinSequence of INT such that
A30: len znpp = n and
A31: for i be Nat st i in Seg n holds znpp.i = GF(i) from SeqLambdaD;
A32: SDSub2INT(z) = zp^<* SDSub2INTDigit(z,(n+1)+1,k) *>
proof
A33: len (zp^<*SDSub2INTDigit(z,n+1+1,k)*>)
= n+1+1 by A26,FINSEQ_2:19;
A34: len SDSub2INT(z) = n+1+1 by FINSEQ_2:109;
for j be Nat st 1 <= j & j <= len SDSub2INT(z) holds
SDSub2INT(z).j = (zp^<* SDSub2INTDigit(z,n+1+1,k) *>).j
proof
let j be Nat;
assume 1 <= j & j <= len SDSub2INT(z);
then A35: j in Seg (n+1+1) by A34,FINSEQ_1:3;
then A36: j in dom SDSub2INT(z) by A34,FINSEQ_1:def 3;
now per cases by A35,FINSEQ_2:8;
suppose
A37: j in Seg (n+1);
then j in dom zp by A26,FINSEQ_1:def 3;
then (zp^<*SDSub2INTDigit(z,n+1+1,k)*>).j
= zp.j by FINSEQ_1:def 7
.= SDSub2INTDigit(z,j,k) by A27,A37
.= (SDSub2INT(z))/.j by A35,RADIX_3:def 11
.= SDSub2INT(z).j by A36,FINSEQ_4:def 4;
hence thesis;
suppose
A38: j = (n+1)+1;
A39: j in dom SDSub2INT(z) by A34,A35,FINSEQ_1:def 3;
(zp^<*SDSub2INTDigit(z,n+1+1,k)*>).j
= SDSub2INTDigit(z,n+1+1,k) by A26,A38,FINSEQ_1:59
.= (SDSub2INT(z))/.(n+1+1) by A35,A38,RADIX_3:def 11
.= SDSub2INT(z).j by A38,A39,FINSEQ_4:def 4;
hence thesis;
end;
hence thesis;
end;
hence thesis by A33,A34,FINSEQ_1:18;
end;
A40: zp = zpp^<* SDSub2INTDigit(z,(n+1),k) *>
proof
A41: len (zpp^<*SDSub2INTDigit(z,n+1,k)*>) = n+1 by A28,FINSEQ_2:19;
for j be Nat st 1 <= j & j <= len zp holds
zp.j = (zpp^<* SDSub2INTDigit(z,n+1,k) *>).j
proof
let j be Nat;
assume 1 <= j & j <= len zp;
then A42: j in Seg (n+1) by A26,FINSEQ_1:3;
now per cases by A42,FINSEQ_2:8;
suppose
A43: j in Seg n;
then j in dom zpp by A28,FINSEQ_1:def 3;
then (zpp^<*SDSub2INTDigit(z,n+1,k)*>).j
= zpp.j by FINSEQ_1:def 7
.= SDSub2INTDigit(z,j,k) by A29,A43
.= zp.j by A27,A42;
hence thesis;
suppose
A44: j = n+1;
then (zpp^<*SDSub2INTDigit(z,n+1,k)*>).j
= SDSub2INTDigit(z,n+1,k) by A28,FINSEQ_1:59
.= zp.j by A27,A42,A44;
hence thesis;
end;
hence thesis;
end;
hence thesis by A26,A41,FINSEQ_1:18;
end;
A45: SDSub2INT(zn) = znpp^<* SDSub2INTDigit(zn,n+1,k) *>
proof
A46: len (znpp^<*SDSub2INTDigit(zn,n+1,k)*>)
= n+1 by A30,FINSEQ_2:19;
A47: len SDSub2INT(zn) = n+1 by FINSEQ_2:109;
for j be Nat st 1 <= j & j <= len SDSub2INT(zn) holds
SDSub2INT(zn).j = (znpp^<* SDSub2INTDigit(zn,n+1,k) *>).j
proof
let j be Nat;
assume 1 <= j & j <= len SDSub2INT(zn);
then A48: j in Seg (n+1) by A47,FINSEQ_1:3;
then A49: j in dom SDSub2INT(zn) by A47,FINSEQ_1:def 3;
now per cases by A48,FINSEQ_2:8;
suppose
A50: j in Seg n;
then j in dom znpp by A30,FINSEQ_1:def 3;
then (znpp^<*SDSub2INTDigit(zn,n+1,k)*>).j
= znpp.j by FINSEQ_1:def 7
.= SDSub2INTDigit(zn,j,k) by A31,A50
.= (SDSub2INT(zn))/.j by A48,RADIX_3:def 11
.= SDSub2INT(zn).j by A49,FINSEQ_4:def 4;
hence thesis;
suppose
A51: j = n+1;
A52: j in dom SDSub2INT(zn) by A47,A48,FINSEQ_1:def 3;
(znpp^<*SDSub2INTDigit(zn,n+1,k)*>).j
= SDSub2INTDigit(zn,n+1,k) by A30,A51,FINSEQ_1:59
.= (SDSub2INT(zn))/.(n+1) by A48,A51,RADIX_3:def 11
.= SDSub2INT(zn).j by A51,A52,FINSEQ_4:def 4;
hence thesis;
end;
hence thesis;
end;
hence thesis by A46,A47,FINSEQ_1:18;
end;
A53: zpp = znpp
proof
for j be Nat st 1 <= j & j <= len znpp holds znpp.j = zpp.j
proof
let j be Nat;
assume A54: 1 <= j & j <= len znpp;
then A55: j in Seg n by A30,FINSEQ_1:3;
A56: j <= n + 1 by A30,A54,NAT_1:37;
then A57: j in Seg (n+1) by A54,FINSEQ_1:3;
j <= (n+1)+1 by A56,NAT_1:37;
then A58: j in Seg ((n+1)+1) by A54,FINSEQ_1:3;
zpp.j
= SDSub2INTDigit(z,j,k) by A29,A55
.= (Radix(k) |^ (j -' 1))* DigB_SDSub(z,j) by RADIX_3:def 10
.= (Radix(k) |^ (j -' 1))* DigA_SDSub(z,j) by RADIX_3:def 9
.= (Radix(k) |^ (j -' 1))*
SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),j,k)
by A58,Def2
.= (Radix(k) |^ (j -' 1))*
SDSubAddDigit(SD2SDSub(DecSD(xn,n,k)),SD2SDSub(DecSD(yn,n,k)),j,k)
by A20,A55,Th8
.= (Radix(k) |^ (j -' 1)) * DigA_SDSub(zn,j) by A57,Def2
.= (Radix(k) |^ (j -' 1)) * DigB_SDSub(zn,j) by RADIX_3:def 9
.= SDSub2INTDigit(zn,j,k) by RADIX_3:def 10
.= znpp.j by A31,A55;
hence thesis;
end;
hence thesis by A28,A30,FINSEQ_1:18;
end;
A59: Sum SDSub2INT(z)
= Sum (zp) + SDSub2INTDigit(z,(n+1)+1,k) by A32,RVSUM_1:104
.= Sum (znpp) + SDSub2INTDigit(z,(n+1),k)
+ SDSub2INTDigit(z,(n+1)+1,k) by A40,A53,RVSUM_1:104;
(xn + yn) + 0 = Sum (znpp) + SDSub2INTDigit(zn,n+1,k) by A23,A45,
RVSUM_1:104;
then A60: Sum (znpp) - 0 = (xn + yn) - SDSub2INTDigit(zn,n+1,k) by
XCMPLX_1:33;
set SDN11 = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1);
set SDN1 = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1);
set SDN = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n);
set RN1 = (Radix(k) |^ (n+1));
set RN = (Radix(k) |^ n);
A61: SDSub2INTDigit(z,n+1+1,k)
= (Radix(k) |^ (n+1+1-'1)) * DigB_SDSub(z,n+1+1) by RADIX_3:def 10
.= (Radix(k) |^ (n+1+1-'1)) * DigA_SDSub(z,n+1+1) by RADIX_3:def 9
.= (Radix(k) |^ (n+1))* DigA_SDSub(z,n+1+1) by BINARITH:39
.= RN1* SDSubAddDigit(
SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),n+1+1,k)
by A25,Def2
.= RN1* (SDSub_Add_Data(SDN11, k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1-'1)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1-'1), k))
by A20,A25,Def1
.= RN1* (SDSub_Add_Data(SDN11, k) + SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1-'1), k))
by BINARITH:39
.= RN1 * ( SDSub_Add_Data(SDN11,k) + SDSub_Add_Carry(SDN1,k) + 0 )
by BINARITH:39
.= RN1 * ( SDSub_Add_Data(SDN11,k)) + RN1 * ( SDSub_Add_Carry(SDN1,k) )
by XCMPLX_1:8;
A62: SDSub2INTDigit(z,n+1,k)
= (Radix(k) |^ (n+1-'1)) * DigB_SDSub(z,n+1) by RADIX_3:def 10
.= (Radix(k) |^ (n+1-'1)) * DigA_SDSub(z,n+1) by RADIX_3:def 9
.= RN* DigA_SDSub(z,n+1) by BINARITH:39
.= RN* SDSubAddDigit(
SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),n+1,k)
by A24,Def2
.= RN* (SDSub_Add_Data(SDN1, k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1-'1)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1-'1), k)) by A20,A24,Def1
.= RN* (SDSub_Add_Data(SDN1, k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1-'1), k)) by BINARITH:39
.= RN*(SDSub_Add_Data(SDN1, k)+SDSub_Add_Carry(SDN,k)+0)
by BINARITH:39
.= RN * (SDSub_Add_Data(SDN1, k)) + RN * (SDSub_Add_Carry(SDN,k))
by XCMPLX_1:8
.= RN * (SDN1 - Radix(k) * SDSub_Add_Carry(SDN1, k))
+ RN * (SDSub_Add_Carry(SDN,k)) by RADIX_3:def 4
.= RN * SDN1 - RN * (Radix(k) * SDSub_Add_Carry(SDN1, k))
+ RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_1:40
.= RN * SDN1 - (RN * (Radix(k))) * SDSub_Add_Carry(SDN1, k)
+ RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_1:4
.= RN * SDN1 - (Radix(k) |^ (n+1) * SDSub_Add_Carry(SDN1, k))
+ RN * (SDSub_Add_Carry(SDN,k)) by RADIX_3:1
.= RN * SDN1 + - (Radix(k) |^ (n+1) * SDSub_Add_Carry(SDN1, k))
+ RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_0:def 8;
A63: SDSub2INTDigit(zn,n+1,k)
= (Radix(k) |^ (n+1-'1)) * DigB_SDSub(zn,n+1) by RADIX_3:def 10
.= (Radix(k) |^ (n+1-'1)) * DigA_SDSub(zn,n+1) by RADIX_3:def 9
.= RN* DigA_SDSub(zn,n+1) by BINARITH:39
.= RN* SDSubAddDigit(
SD2SDSub(DecSD(xn,n,k)),SD2SDSub(DecSD(yn,n,k)),n+1,k) by A18,Def2
.= RN * (SDSub_Add_Data(
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1-'1)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1-'1), k)) by A18,A20,Def1
.= RN * (SDSub_Add_Data(
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1-'1), k)) by BINARITH:39
.= RN * (SDSub_Add_Data(
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by BINARITH:39
.= RN * (SDSub_Add_Data(
SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by A16,A19,Th5
.= RN * (SDSub_Add_Data(
SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
+SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by A16,A19,Th5
.= RN * (SDSub_Add_Data(
SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
+SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k), k)
+ SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by A17,A20,RADIX_3:21
.= RN * (SDSub_Add_Data(
SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
+SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k), k)
+ SDSub_Add_Carry(SDN,k)) by A17,A20,RADIX_3:21
.= RN * (SDSub_Add_Data(
SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
+SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k), k))
+ RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_1:8;
set SDACx = SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k);
set SDACy = SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k);
set RNSDACxy = RN*(SDACx + SDACy);
A64: SDSub_Add_Data(SDACx + SDACy, k)
=(SDACx + SDACy) - Radix(k) * SDSub_Add_Carry(SDACx+SDACy,k)
by RADIX_3:def 4
.=(SDACx + SDACy) - Radix(k) * 0 by A19,Th2;
set RN1SD11 = RN1 * (SDSub_Add_Data(SDN11,k));
set RN1SC1 = RN1 * (SDSub_Add_Carry(SDN1,k));
set RNSC = RN * (SDSub_Add_Carry(SDN,k));
A65: Sum SDSub2INT(z)
= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + ((RN*SDN1 + -RN1SC1) + RNSC)
+ RN1SD11 + RN1SC1 by A59,A60,A61,A62,XCMPLX_1:1
.= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + (RN*SDN1 + -RN1SC1) + RNSC
+ RN1SD11 + RN1SC1 by XCMPLX_1:1
.= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + -RN1SC1 + RNSC
+ RN1SD11 + RN1SC1 by XCMPLX_1:1
.= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 - RN1SC1 + RNSC
+ RN1SD11 + RN1SC1 by XCMPLX_0:def 8
.= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + RNSC - RN1SC1
+ RN1SD11 + RN1SC1 by XCMPLX_1:29
.= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + RNSC
+ RN1SD11 - RN1SC1 + RN1SC1 by XCMPLX_1:29
.= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + RNSC
+ RN1SD11 + RN1SC1 - RN1SC1 by XCMPLX_1:29
.= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + RNSC
+ RN1SD11 by XCMPLX_1:26
.= (xn + yn) + RN*SDN1 - SDSub2INTDigit(zn,n+1,k) + RNSC
+ RN1SD11 by XCMPLX_1:29
.= (xn + yn) + RN*SDN1 + - SDSub2INTDigit(zn,n+1,k) + RNSC
+ RN1SD11 by XCMPLX_0:def 8
.= (xn + yn) + RN*SDN1 + ( - SDSub2INTDigit(zn,n+1,k) + RNSC )
+ RN1SD11 by XCMPLX_1:1;
A66: - SDSub2INTDigit(zn,n+1,k) + RNSC
= - RNSDACxy - RNSC + RNSC by A63,A64,XCMPLX_1:161
.= - RNSDACxy + RNSC - RNSC by XCMPLX_1:29
.= - RNSDACxy by XCMPLX_1:26;
A67: RN1SD11 = RN1 * ( DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1)
- Radix(k) * SDSub_Add_Carry(
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1), k)) by RADIX_3:def 4;
A68: DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
= SD2SDSubDigitS(DecSD(x,n+1,k),n+1+1,k) by A25,RADIX_3:def 8
.= SD2SDSubDigit(DecSD(x,n+1,k),n+1+1,k) by A20,A25,RADIX_3:def 7
.= SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1+1-'1),k)
by RADIX_3:def 6
.= SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k) by BINARITH:39;
A69: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1)
= SD2SDSubDigitS(DecSD(y,n+1,k),n+1+1,k) by A25,RADIX_3:def 8
.= SD2SDSubDigit(DecSD(y,n+1,k),n+1+1,k) by A20,A25,RADIX_3:def 7
.= SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n+1+1-'1),k)
by RADIX_3:def 6
.= SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n+1),k) by BINARITH:39;
then A70: RN1SD11 = RN1 * (DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1)
- Radix(k) * 0) by A19,A67,A68,Th2
.= RN1 * (SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
+ SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n+1),k) ) by A68,A69;
reconsider RNDx11 = RN * DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1),
RNDy11 = RN * DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1),
RN1Cx11 = RN1*SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k),
RN1Cy11 = RN1*SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n+1),k),
RNCx1 = RN * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k),
RNCy1 = RN * SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n),k),
RNCx = RN*SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k),
RNCy = RN*SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k)
as Integer;
A71: Sum SDSub2INT(z)
= (xn + yn) + (RNDx11 + RNDy11)
+ (- RNSDACxy) + RN1SD11 by A65,A66,XCMPLX_1:8
.= (xn + yn) + (RNDx11 + RNDy11)
+ - (RNCx + RNCy) + RN1SD11 by XCMPLX_1:8
.= (xn + yn) + (RNDx11 + RNDy11)
+ - (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by A70,XCMPLX_1:8
.= (xn + yn) + RNDx11 + RNDy11
+ - (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by XCMPLX_1:1
.= (xn + yn)
+ (RN * DigA(DecSD(x,n+1,k),n+1) - RN1Cx11 + RNCx1)
+ RNDy11
+ - (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by A16,A19,A20,Th7
.= (xn + yn)
+ (RN * DigA(DecSD(x,n+1,k),n+1) - RN1Cx11 + RNCx1)
+ RNDy11
- (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by XCMPLX_0:def 8
.= (xn + yn)
+ (RN * DigA(DecSD(x,n+1,k),n+1) - RN1Cx11 + RNCx1) + RNDy11
+ (RN1Cx11 + RN1Cy11) - (RNCx + RNCy) by XCMPLX_1:29
.= (xn + yn)
+ (RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 - RN1Cx11) + RNDy11
+ (RN1Cx11 + RN1Cy11) - (RNCx + RNCy) by XCMPLX_1:29
.= (xn + yn)
+ ((RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1) + -RN1Cx11) + RNDy11
+ (RN1Cx11 + RN1Cy11) - (RNCx + RNCy) by XCMPLX_0:def 8
.= (xn + yn)
+ (RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1) + -RN1Cx11 + RNDy11
+ (RN1Cx11 + RN1Cy11) - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ (RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1) + -RN1Cx11 + RNDy11
+ RN1Cx11 + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + -RN1Cx11 + RNDy11
+ RN1Cx11 + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + (-RN1Cx11 + RNDy11)
+ RN1Cx11 + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + ((-RN1Cx11 + RNDy11)
+ RN1Cx11) + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + (RNDy11)
+ RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:139
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ (RN * DigA(DecSD(y,n+1,k),n+1) - RN1Cy11 + RNCy1)
+ RN1Cy11 - (RNCx + RNCy) by A16,A19,A20,Th7
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ (RN * DigA(DecSD(y,n+1,k),n+1) - RN1Cy11 + RNCy1)
+ RN1Cy11 + - (RNCx + RNCy) by XCMPLX_0:def 8
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ ((RN * DigA(DecSD(y,n+1,k),n+1) + -RN1Cy11) + RNCy1)
+ RN1Cy11 + - (RNCx + RNCy) by XCMPLX_0:def 8
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ (RN * DigA(DecSD(y,n+1,k),n+1) + -RN1Cy11) + RNCy1
+ RN1Cy11 + - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + - RN1Cy11 + RNCy1
+ RN1Cy11 + - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + (- RN1Cy11 + RNCy1)
+ RN1Cy11 + - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + ((- RN1Cy11 + RNCy1)
+ RN1Cy11) + - (RNCx + RNCy) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + (RNCy1) + - (RNCx + RNCy)
by XCMPLX_1:139
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + (RNCy1) + - (RNCx1 + RNCy)
by A17,Lm2
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + (RNCy1) + - (RNCx1 + RNCy1)
by A17,Lm2
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + RNCy1 - (RNCx1 + RNCy1)
by XCMPLX_0:def 8
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + RNCy1 - RNCx1 - RNCy1
by XCMPLX_1:36
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) + RNCy1 - RNCx1 + - RNCy1
by XCMPLX_0:def 8
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) - RNCx1 + RNCy1 + - RNCy1
by XCMPLX_1:29
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) - RNCx1 + (RNCy1 + - RNCy1)
by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) - RNCx1 + 0 by XCMPLX_0:def 6
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 - RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) by XCMPLX_1:29
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + - RNCx1
+ RN * DigA(DecSD(y,n+1,k),n+1) by XCMPLX_0:def 8
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + (RNCx1 + - RNCx1)
+ RN * DigA(DecSD(y,n+1,k),n+1) by XCMPLX_1:1
.= (xn + yn)
+ RN * DigA(DecSD(x,n+1,k),n+1) + (0)
+ RN * DigA(DecSD(y,n+1,k),n+1) by XCMPLX_0:def 6;
A72: RN * DigA(DecSD(x,n+1,k),n+1)
= RN * (x div (Radix(k) |^ n)) by A19,RADIX_1:27;
RN * DigA(DecSD(y,n+1,k),n+1)
= RN * (y div (Radix(k) |^ n)) by A19,RADIX_1:27;
then A73: Sum SDSub2INT(z)
= yn + x + RN * (y div (Radix(k) |^ n)) by A22,A71,A72,XCMPLX_1:1;
y = (y div (Radix(k) |^ n))*(Radix(k) |^ n)
+ (y mod (Radix(k) |^ n)) by A21,NAT_1:47;
then Sum SDSub2INT(z) = x + y by A73,XCMPLX_1:1;
hence thesis by RADIX_3:def 12;
end;
for n be Nat st n >= 1 holds P[n] from Ind1(A1,A15);
hence thesis;
end;