### The Mizar article:

by
Masaaki Niimura, and
Yasushi Fuwa

Copyright (c) 2003 Association of Mizar Users

[ MML identifier index ]

environ

vocabulary INT_1, NAT_1, ARYTM_1, POWER, MIDSP_3, FINSEQ_1, FUNCT_1, RELAT_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,
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);
.= 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
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:
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)
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)
.= ((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
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
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;
A5:  k >= 2 by A1,AXIOMS:22;
;
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;
end;

theorem Th3:
2 <= k implies
DigA_SDSub(SD2SDSub(DecSD(m,n,k)),n+1)
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), k) by BINARITH:39;
end;

theorem Th4:
2 <= k & m is_represented_by 1,k implies
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
end;

theorem Th5:
for k,x,n be Nat st
n >= 1 & k >= 3 & x is_represented_by (n+1),k holds
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)
hence thesis;
end;

theorem Th6:
2 <= k & m is_represented_by 1,k implies
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_Carry( DigA(DecSD(m,1,k),0), k) by GOBOARD9:1
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(DecSD(x,n+1,k),n+1)
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) * (
.= (Radix(k) |^ n) * (
.= (Radix(k) |^ n) * (
DigA(DecSD(x,n+1,k),n+1)
.= (Radix(k) |^ n) * (
( DigA(DecSD(x,n+1,k),n+1)
+ (Radix(k) |^ n) * (
.= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
+ (Radix(k) |^ n) * (
.= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
+ (Radix(k) |^ n) * (
.= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
hence thesis;
end;

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 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;
A5:   -1 <= SDAC & SDAC <= 1 by A1,RADIX_3:13;
then A6:   SDAD + SDAC >= -Radix(k-'1) - 1 by XCMPLX_0:def 8;
then SDAD + SDAC <= Radix(k-'1) + 1 - 1 by XCMPLX_1:29;
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
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
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
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
A5: for i be Nat st i in Seg n holds
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
.= DigA_SDSub(k2,j) by A5,A7
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
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);
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i), k)
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
A10:      DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1)
= DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),0) by A8,GOBOARD9:1
A11:      DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i)
A12: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i)
A13:      DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
= DigA_SDSub(SD2SDSub(DecSD(X,n,k)),0) by A8,GOBOARD9:1
DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i-'1)
= DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),0) by A8,GOBOARD9:1
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;
)
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i), k)
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
+ DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
+ DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i-'1), 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
A4:   1 in Seg (1+1) by FINSEQ_1:3;
then A5:   DigA_SDSub(X '+' Y, 1)
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
by A3,A4,Def1
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,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_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
.= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k ) + 0
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)
.= SDSub_Add_Data( DigA_SDSub(X,2) + DigA_SDSub(Y,2), k )
by A3,A7,Def1
+ CRY1 by A2,A3,A6,Th4
+ CRY1 by A2,A3,Th4
-Radix(k) * 0 + CRY1 by A2,Th2
A9:  (SDSub2INT(X '+' Y))/.1
= SDSub2INTDigit((X '+' Y),1,k) by A4,RADIX_3:def 11
.= (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) * DigB_SDSub((X '+' Y),2) by A6,NEWTON:10
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;
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;
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));
then Radix(k) > 0 by NAT_1:19;
then A21:  (Radix(k) |^ n) > 0 by PREPOWER:13;
+ (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 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).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 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).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))*
by A58,Def2
.= (Radix(k) |^ (j -' 1))*
by A20,A55,Th8
.= (Radix(k) |^ (j -' 1)) * DigA_SDSub(zn,j) by A57,Def2
.= 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))* DigA_SDSub(z,n+1+1) by BINARITH:39
SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),n+1+1,k)
by A25,Def2
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
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
by BINARITH:39
by XCMPLX_1:8;
A62: SDSub2INTDigit(z,n+1,k)
.= RN* DigA_SDSub(z,n+1) by BINARITH:39
SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),n+1,k)
by A24,Def2
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
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1-'1), k)) by BINARITH:39
by BINARITH:39
by XCMPLX_1:8
+ RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_1:40
+ 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 XCMPLX_0:def 8;
A63: SDSub2INTDigit(zn,n+1,k)
.= RN* DigA_SDSub(zn,n+1) by BINARITH:39
SD2SDSub(DecSD(xn,n,k)),SD2SDSub(DecSD(yn,n,k)),n+1,k) by A18,Def2
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
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
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1-'1), k)) by BINARITH:39
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by BINARITH:39
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by A16,A19,Th5
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
+DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by A16,A19,Th5
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n)
+ RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_1:8;
set RNSDACxy = RN*(SDACx + SDACy);
.=(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)
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
A68: DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
A69: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1)
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
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),
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 * DigA(DecSD(y,n+1,k),n+1)