:: High Speed Adder Algorithm with Radix-$2^k$ SD_Sub Number
:: by Masaaki Niimura and Yasushi Fuwa
::
:: Received January 3, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, INT_1, XXREAL_0, ARYTM_3, RADIX_1, POWER,
RELAT_1, RADIX_3, ARYTM_1, SUBSET_1, FINSEQ_1, NEWTON, CARD_1, FINSEQ_2,
TARSKI, FUNCT_1, ORDINAL4, PARTFUN1, CARD_3, RADIX_4;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, NAT_D,
FUNCT_1, PARTFUN1, NEWTON, POWER, XXREAL_0, FINSEQ_1, FINSEQ_2, GR_CY_1,
RADIX_1, RADIX_3;
constructors REAL_1, NAT_D, NEWTON, POWER, BINARITH, GR_CY_1, RADIX_3;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON,
VALUED_0, FINSEQ_2, ORDINAL1;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities RADIX_1;
expansions RADIX_1;
theorems RADIX_1, POWER, NAT_1, INT_1, FINSEQ_1, FINSEQ_2, NEWTON, RVSUM_1,
PREPOWER, JORDAN12, EULER_2, RADIX_3, XREAL_1, XXREAL_0, NAT_D, ORDINAL1,
PARTFUN1, XREAL_0, CARD_1;
schemes FINSEQ_2, NAT_1;
begin :: Some Useful Theorems
reserve i,n,m,k,x,y for Nat,
i1 for Integer;
theorem Th1:
2 <= k implies 2 < Radix(k)
proof
defpred P[Nat] means 2 < Radix($1);
A1: for kk be Nat st kk >= 2 & P[kk] holds P[kk + 1]
proof
let kk be Nat;
assume that
2 <= kk and
A2: 2 < Radix(kk);
A3: Radix(kk + 1) = 2 to_power (1) * 2 to_power (kk) by POWER:27
.= 2 * Radix(kk) by POWER:25;
Radix(kk) > 1 by A2,XXREAL_0:2;
hence thesis by A3,XREAL_1:155;
end;
Radix(2) = 2 to_power (1+1) .= 2 to_power 1 * 2 to_power 1 by POWER:27
.= 2 * (2 to_power 1) by POWER:25
.= 2 * 2 by POWER:25
.= 4;
then
A4: P[2];
for k be Nat holds 2 <= k implies P[k] from NAT_1:sch 8(A4,A1);
hence thesis;
end;
Lm1: i1 in k-SD_Sub_S implies i1 >= -Radix(k-'1) & i1 <= Radix(k-'1) - 1
proof
A1: 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;
assume i1 in k-SD_Sub_S;
then
ex i be Element of INT st i = i1 & -Radix(k-'1) <= i & i <= Radix(k-'1) -
1 by A1;
hence thesis;
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 i <= n by FINSEQ_1:1;
then
A2: i <= n+1 by NAT_1:12;
1 <= i by A1,FINSEQ_1:1;
then
A3: i in Seg (n+1) by A2,FINSEQ_1:1;
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 holds DigA(DecSD(x mod (Radix(k) |^ n),n,k),n)
= DigA(DecSD(x,n,k),n)
proof
let k,x,n be Nat;
set xn = x mod (Radix(k) |^ n);
assume n >= 1;
then n <> 0;
then
A1: n in Seg n by FINSEQ_1:3;
then DigA(DecSD(xn,n,k),n) = DigitDC(xn,n,k) by RADIX_1:def 9
.= DigitDC(x,n,k) by NAT_D:73
.= 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;
set CC = SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k);
-1 <= SDSub_Add_Carry(x,k) & -1 <= SDSub_Add_Carry(y,k) by RADIX_3:12;
then
A1: -1 + -1 <= CC by XREAL_1:7;
assume k >= 3;
then
A2: k - 1 >= 3 - 1 by XREAL_1:13;
then k - 1 > 0 by XXREAL_0:2;
then k - 1 = k -' 1 by XREAL_0:def 2;
then
A3: Radix(k-'1) > 2 by A2,Th1;
SDSub_Add_Carry(x,k) <= 1 & SDSub_Add_Carry(y,k) <= 1 by RADIX_3:12;
then CC <= 1 + 1 by XREAL_1:7;
then
A4: CC < Radix(k-'1) by A3,XXREAL_0:2;
-Radix(k-'1) <= -2 by A3,XREAL_1:24;
then -Radix(k-'1) <= CC by A1,XXREAL_0:2;
hence thesis by A4,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 + 1 <= n + 1 by XREAL_1:7;
then
A2: (n+1) in Seg (n+1) by FINSEQ_1:1;
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 NAT_D:34;
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 that
A1: 2 <= k and
A2: m is_represented_by 1,k;
thus DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1+1) = SDSub_Add_Carry( DigA(DecSD(m,
1,k),1), k) by A1,Th3
.= SDSub_Add_Carry(m, k) by A2,RADIX_1:21;
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 that
A1: n >= 1 and
A2: k >= 3;
set xn = x mod (Radix(k) |^ n);
A3: n+1 in Seg (n+1) by FINSEQ_1:3;
then
DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1) = SD2SDSubDigitS(DecSD(xn,n,k),n
+1,k) by RADIX_3:def 8
.= SD2SDSubDigit(DecSD(xn,n,k),n+1,k) by A2,A3,RADIX_3:def 7,XXREAL_0:2
.= 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 NAT_D:34
.= 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 that
A1: 2 <= k and
A2: m is_represented_by 1,k;
A3: 1 in Seg 1 by FINSEQ_1:3;
A4: 1 in Seg (1+1) by FINSEQ_1:1;
then
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,A4,RADIX_3:def 7;
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 XREAL_1:232
.= 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 A2,RADIX_1:21
.= SDSub_Add_Data( m, k ) + 0 by RADIX_3:16
.= m - SDSub_Add_Carry(m,k) * Radix(k) by RADIX_3:def 4;
end;
theorem Th7:
for k,x,n be Nat st k >= 2 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: k >= 2;
A2: n+1 in Seg (n+1) by FINSEQ_1:3;
then
A3: (n+1) in Seg (n+1+1) by FINSEQ_2:8;
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 NAT_D:34
.= (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) |^ 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) )
.= (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 NEWTON:6;
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 that
A1: i in Seg n and
A2: 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
DigA_SDSub(x,i) is Element of k-SD_Sub by A1,RADIX_3:18;
then
A3: DigA_SDSub(x,i) in k-SD_Sub;
set SDAC = SDSub_Add_Carry(DigA_SDSub(x,i -'1)+DigA_SDSub(y,i -'1), k);
set SDAD = SDSub_Add_Data(DigA_SDSub(x,i) + DigA_SDSub(y,i), k );
A4: -1 <= SDAC by RADIX_3:12;
A5: SDAC <= 1 by RADIX_3:12;
k-SD_Sub c= k-SD & DigA_SDSub(y,i) is Element of k-SD_Sub by A1,A2,
RADIX_3:4,18;
then
A6: SDAD in k-SD_Sub_S by A2,A3,RADIX_3:19;
then SDAD >= -Radix(k-'1) by Lm1;
then
A7: -Radix(k-'1) + -1 <= SDAD + SDAC by A4,XREAL_1:7;
SDAD <= Radix(k-'1) - 1 by A6,Lm1;
then
A8: SDAD + SDAC <= Radix(k-'1) -1 + 1 by A5,XREAL_1:7;
SDAD + SDAC is Element of INT & k-SD_Sub = {w where w is Element of
INT: w >= -Radix(k -' 1) - 1 & w <= Radix(k -' 1) } by INT_1:def 2
,RADIX_3:def 2;
then SDAD + SDAC in k-SD_Sub by 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 dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
z is Element of n-tuples_on (k-SD_Sub) by A1,FINSEQ_2:92;
then reconsider z as Tuple of n,(k-SD_Sub);
take z;
let i;
assume
A4: i in Seg n;
hence DigA_SDSub(z,i) = z.i by RADIX_3:def 5
.= SDSubAddDigit(x,y,i,k) by A2,A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,(k-SD_Sub) such that
A5: for i be Nat st i in Seg n holds DigA_SDSub(k1,i) = SDSubAddDigit(
x,y,i,k) and
A6: for i be Nat st i in Seg n holds DigA_SDSub(k2,i) = SDSubAddDigit(
x,y,i,k);
A7: len k1 = n by CARD_1:def 7;
then
A8: dom k1 = Seg n by FINSEQ_1:def 3;
A9: now
let j be Nat;
assume
A10: j in dom k1;
then k1.j = DigA_SDSub(k1,j) by A8,RADIX_3:def 5
.= SDSubAddDigit(x,y,j,k) by A5,A8,A10
.= DigA_SDSub(k2,j) by A6,A8,A10
.= k2.j by A8,A10,RADIX_3:def 5;
hence k1.j = k2.j;
end;
len k2 = n by CARD_1:def 7;
hence thesis by A7,A9,FINSEQ_2:9;
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;
set X = x mod (Radix(k) |^ n);
set Y = y mod (Radix(k) |^ n);
assume
A1: i in Seg n;
then i <= n by FINSEQ_1:1;
then
A2: i <= n + 1 by NAT_1:12;
A3: 1 <= i by A1,FINSEQ_1:1;
then
A4: i in Seg (n+1) by A2,FINSEQ_1:1;
i <= (n+1)+1 by A2,NAT_1:12;
then
A5: i in Seg ((n+1)+1) by A3,FINSEQ_1:1;
reconsider i as Element of NAT by ORDINAL1:def 12;
assume
A6: 2 <= k;
then
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,Def1;
now
per cases;
suppose
A8: i = 1;
then
A9: DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i-'1) = DigA_SDSub(SD2SDSub(DecSD
(Y,n,k)),0) by XREAL_1:232
.= 0 by RADIX_3:def 5;
A10: DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1) = DigA_SDSub(SD2SDSub(DecSD
(X,n,k)),0) by A8,XREAL_1:232
.= 0 by RADIX_3:def 5;
A11: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1) = DigA_SDSub(SD2SDSub(
DecSD(y,n+1,k)),0) by A8,XREAL_1:232
.= 0 by RADIX_3:def 5;
A12: DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1) = DigA_SDSub(SD2SDSub(
DecSD(x,n+1,k)),0) by A8,XREAL_1:232
.= 0 by RADIX_3:def 5;
DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i) = DigA_SDSub(SD2SDSub(DecSD(
X,n,k)),i) & DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i) = DigA_SDSub(SD2SDSub(DecSD
(Y,n,k)), i) by A1,A6,RADIX_3:20;
hence thesis by A4,A6,A7,A12,A11,A10,A9,Def1;
end;
suppose
A13: i <> 1;
i >= 1 by A1,FINSEQ_1:1;
then 1 < i by A13,XXREAL_0:1;
then
A14: 0 + 1 <= i-'1 by INT_1:7,JORDAN12:1;
i <= n by A1,FINSEQ_1:1;
then i -' 1 <= n by NAT_D:44;
then
A15: i -' 1 in Seg n by A14,FINSEQ_1:1;
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:20
.= 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:20
.= 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,A15,RADIX_3:20
.= 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,A15,RADIX_3:20
.= SDSubAddDigit(SD2SDSub(DecSD(X,n,k)),SD2SDSub(DecSD(Y,n,k)),i,k)
by A4,A6,Def1;
hence thesis;
end;
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)) );
let n;
assume
A1: n >= 1;
A2: for n be Nat st n >= 1 & P[n] holds P[n+1]
proof
let n be Nat;
assume that
A3: n >= 1 and
A4: P[n];
let k,x,y be Nat;
assume that
A5: k >= 3 and
A6: x is_represented_by (n+1),k and
A7: y is_represented_by (n+1),k;
reconsider k,x,y as Element of NAT by ORDINAL1:def 12;
A8: (n+1+1) in Seg (n+1+1) by FINSEQ_1:3;
then
A9: DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1) = SD2SDSubDigitS(DecSD(x,
n+1,k),n+1+1,k) by RADIX_3:def 8
.= SD2SDSubDigit(DecSD(x,n+1,k),n+1+1,k) by A5,A8,RADIX_3:def 7
,XXREAL_0:2
.= 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 NAT_D:34;
A10: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1) = SD2SDSubDigitS(DecSD(y,
n+1,k),n+1+1,k) by A8,RADIX_3:def 8
.= SD2SDSubDigit(DecSD(y,n+1,k),n+1+1,k) by A5,A8,RADIX_3:def 7
,XXREAL_0:2
.= 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 NAT_D:34;
set yn = y mod (Radix(k) |^ n);
set xn = x mod (Radix(k) |^ n);
set zn = SD2SDSub(DecSD(xn,n,k)) '+' SD2SDSub(DecSD(yn,n,k));
deffunc GF(Nat)= SDSub2INTDigit(zn,$1,k);
consider znpp being FinSequence of INT such that
A11: len znpp = n and
A12: for i be Nat st i in dom znpp holds znpp.i = GF(i) from FINSEQ_2:
sch 1;
A13: len SDSub2INT(zn) = n+1 by CARD_1:def 7;
A14: dom znpp = Seg n by A11,FINSEQ_1:def 3;
A15: 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
A16: j in Seg (n+1) by A13,FINSEQ_1:1;
then
A17: j in dom SDSub2INT(zn) by A13,FINSEQ_1:def 3;
now
per cases by A16,FINSEQ_2:7;
suppose
A18: j in Seg n;
then j in dom znpp by A11,FINSEQ_1:def 3;
then (znpp^<*SDSub2INTDigit(zn,n+1,k)*>).j = znpp.j by FINSEQ_1:def 7
.= SDSub2INTDigit(zn,j,k) by A12,A14,A18
.= (SDSub2INT(zn))/.j by A16,RADIX_3:def 11
.= SDSub2INT(zn).j by A17,PARTFUN1:def 6;
hence thesis;
end;
suppose
A19: j = n+1;
A20: j in dom SDSub2INT(zn) by A13,A16,FINSEQ_1:def 3;
(znpp^<*SDSub2INTDigit(zn,n+1,k)*>).j = SDSub2INTDigit(zn,n+1,k
) by A11,A19,FINSEQ_1:42
.= (SDSub2INT(zn))/.(n+1) by A16,A19,RADIX_3:def 11
.= SDSub2INT(zn).j by A19,A20,PARTFUN1:def 6;
hence thesis;
end;
end;
hence thesis;
end;
len (znpp^<*SDSub2INTDigit(zn,n+1,k)*>) = n+1 by A11,FINSEQ_2:16;
then
A21: SDSub2INT(zn) = znpp^<* SDSub2INTDigit(zn,n+1,k) *> by A13,A15,FINSEQ_1:14
;
A22: Radix(k) > 0 by POWER:34;
then yn < Radix(k) |^ n by NAT_D:1,PREPOWER:6;
then
A23: yn is_represented_by n,k;
set SDN1 = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1) +DigA_SDSub(SD2SDSub(
DecSD(y,n+1,k)),n+1);
set z = SD2SDSub(DecSD(x,n+1,k)) '+' SD2SDSub(DecSD(y,n+1,k));
deffunc G(Nat)=SDSub2INTDigit(z,$1,k);
consider zpp being FinSequence of INT such that
A24: len zpp = n and
A25: for i be Nat st i in dom zpp holds zpp.i = G(i) from FINSEQ_2:sch
1;
consider zp being FinSequence of INT such that
A26: len zp = n+1 and
A27: for i be Nat st i in dom zp holds zp.i = G(i) from FINSEQ_2:sch 1;
A28: dom zpp = Seg n by A24,FINSEQ_1:def 3;
for j be Nat st 1 <= j & j <= len znpp holds znpp.j = zpp.j
proof
let j be Nat;
assume that
A29: 1 <= j and
A30: j <= len znpp;
A31: j <= n + 1 by A11,A30,NAT_1:12;
then
A32: j in Seg (n+1) by A29,FINSEQ_1:1;
j <= (n+1)+1 by A31,NAT_1:12;
then
A33: j in Seg ((n+1)+1) by A29,FINSEQ_1:1;
A34: j in Seg n by A11,A29,A30,FINSEQ_1:1;
then zpp.j = SDSub2INTDigit(z,j,k) by A25,A28
.= (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 A33,Def2
.= (Radix(k) |^ (j -' 1))* SDSubAddDigit(SD2SDSub(DecSD(xn,n,k)),
SD2SDSub(DecSD(yn,n,k)),j,k) by A5,A34,Th8,XXREAL_0:2
.= (Radix(k) |^ (j -' 1)) * DigA_SDSub(zn,j) by A32,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 A12,A14,A34;
hence thesis;
end;
then
A35: zpp = znpp by A24,A11,FINSEQ_1:14;
set RN1 = (Radix(k) |^ (n+1));
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 RN1SD11 = RN1 * (SDSub_Add_Data(SDN11,k));
set RN = (Radix(k) |^ n);
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;
set SDN = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n) +DigA_SDSub(SD2SDSub(
DecSD(y,n+1,k)),n);
set RNSC = RN * (SDSub_Add_Carry(SDN,k));
A36: 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 NAT_D:34
.= RN1* SDSubAddDigit( SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k
)),n+1+1,k) by A8,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 A5,A8,Def1,XXREAL_0:2
.= 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 NAT_D:34
.= RN1 * ( SDSub_Add_Data(SDN11,k) + SDSub_Add_Carry(SDN1,k) + 0 ) by
NAT_D:34
.= RN1 * ( SDSub_Add_Data(SDN11,k)) + RN1 * ( SDSub_Add_Carry(SDN1,k)
);
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;
then
A37: 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 A5,A9,A10,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 A9,A10;
A38: RN * DigA(DecSD(x,n+1,k),n+1) = RN * (x div (Radix(k) |^ n)) by A6,
RADIX_1:24;
xn < Radix(k) |^ n by A22,NAT_D:1,PREPOWER:6;
then xn is_represented_by n,k;
then xn + yn = SDSub2IntOut(zn) by A4,A5,A23
.= Sum SDSub2INT(zn) by RADIX_3:def 12;
then
A39: (xn + yn) + 0 = Sum (znpp) + SDSub2INTDigit(zn,n+1,k) by A21,RVSUM_1:74;
set SDACy = SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k);
set SDACx = SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k);
A40: 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 A5,Th2;
n <> 0 by A3;
then
A41: n in Seg n by FINSEQ_1:3;
A42: dom zp = Seg(n+1) by A26,FINSEQ_1:def 3;
A43: 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
A44: j in Seg (n+1) by A26,FINSEQ_1:1;
now
per cases by A44,FINSEQ_2:7;
suppose
A45: j in Seg n;
then j in dom zpp by A24,FINSEQ_1:def 3;
then (zpp^<*SDSub2INTDigit(z,n+1,k)*>).j = zpp.j by FINSEQ_1:def 7
.= SDSub2INTDigit(z,j,k) by A25,A28,A45
.= zp.j by A27,A42,A44;
hence thesis;
end;
suppose
A46: j = n+1;
then (zpp^<*SDSub2INTDigit(z,n+1,k)*>).j = SDSub2INTDigit(z,n+1,k)
by A24,FINSEQ_1:42
.= zp.j by A27,A42,A44,A46;
hence thesis;
end;
end;
hence thesis;
end;
A47: len SDSub2INT(z) = n+1+1 by CARD_1:def 7;
A48: 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
A49: j in Seg (n+1+1) by A47,FINSEQ_1:1;
then
A50: j in dom SDSub2INT(z) by A47,FINSEQ_1:def 3;
now
per cases by A49,FINSEQ_2:7;
suppose
A51: 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,A42,A51
.= (SDSub2INT(z))/.j by A49,RADIX_3:def 11
.= SDSub2INT(z).j by A50,PARTFUN1:def 6;
hence thesis;
end;
suppose
A52: j = (n+1)+1;
A53: j in dom SDSub2INT(z) by A47,A49,FINSEQ_1:def 3;
(zp^<*SDSub2INTDigit(z,n+1+1,k)*>).j = SDSub2INTDigit(z,n+1+1,k
) by A26,A52,FINSEQ_1:42
.= (SDSub2INT(z))/.(n+1+1) by A49,A52,RADIX_3:def 11
.= SDSub2INT(z).j by A52,A53,PARTFUN1:def 6;
hence thesis;
end;
end;
hence thesis;
end;
len (zpp^<*SDSub2INTDigit(z,n+1,k)*>) = n+1 by A24,FINSEQ_2:16;
then
A54: zp = zpp^<* SDSub2INTDigit(z,(n+1),k) *> by A26,A43,FINSEQ_1:14;
len (zp^<*SDSub2INTDigit(z,n+1+1,k)*>) = n+1+1 by A26,FINSEQ_2:16;
then SDSub2INT(z) = zp^<* SDSub2INTDigit(z,(n+1)+1,k) *> by A47,A48,
FINSEQ_1:14;
then
A55: Sum SDSub2INT(z) = Sum (zp) + SDSub2INTDigit(z,(n+1)+1,k) by RVSUM_1:74
.= Sum (znpp) + SDSub2INTDigit(z,(n+1),k) + SDSub2INTDigit(z,(n+1)+1,k
) by A54,A35,RVSUM_1:74;
A56: n+1 in Seg (n+1) by FINSEQ_1:3;
then
A57: (n+1) in Seg (n+1+1) by FINSEQ_2:8;
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 NAT_D:34
.= RN* SDSubAddDigit( SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)
),n+1,k) by A57,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
A5,A57,Def1,XXREAL_0:2
.= 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
NAT_D:34
.= RN*(SDSub_Add_Data(SDN1, k)+SDSub_Add_Carry(SDN,k)+0) by NAT_D:34
.= RN * (SDSub_Add_Data(SDN1, k)) + RN * (SDSub_Add_Carry(SDN,k))
.= 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))
.= RN * SDN1 - (Radix(k) |^ (n+1) * SDSub_Add_Carry(SDN1, k)) + RN * (
SDSub_Add_Carry(SDN,k)) by NEWTON:6
.= RN * SDN1 + - (Radix(k) |^ (n+1) * SDSub_Add_Carry(SDN1, k)) + RN *
(SDSub_Add_Carry(SDN,k));
then
A58: Sum SDSub2INT(z) = (xn + yn) + RN*SDN1 + ( - SDSub2INTDigit(zn,n+1,k
) + RNSC ) + RN1SD11 by A55,A39,A36;
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 NAT_D:34
.= RN* SDSubAddDigit( SD2SDSub(DecSD(xn,n,k)),SD2SDSub(DecSD(yn,n,k)),
n+1,k) by A56,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 A56,A5,Def1,XXREAL_0:2
.= 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
NAT_D:34
.= 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
NAT_D:34
.= 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 A3,A5
,A6,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 A3,A5
,A7,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 A41
,A5,RADIX_3:20,XXREAL_0:2
.= 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 A41,A5
,RADIX_3:20,XXREAL_0:2
.= 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));
then
A59: Sum SDSub2INT(z) = (xn + yn) + RNDx11 + RNDy11 + - (RNCx + RNCy) + (
RN1Cx11 + RN1Cy11) by A40,A58,A37
.= (xn + yn) + (RN * DigA(DecSD(x,n+1,k),n+1) - RN1Cx11 + RNCx1) +
RNDy11 + - (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by A5,Th7,XXREAL_0:2
.= (xn + yn) + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + (RNDy11) +
RN1Cy11 - (RNCx + RNCy)
.= (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 A5,Th7,
XXREAL_0:2
.= (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)
.= (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 A41,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 A41,Lm2
.= (xn + yn) + RN * DigA(DecSD(x,n+1,k),n+1) + (0) + RN * DigA(DecSD(y
,n+1,k),n+1);
A60: y = (y div (Radix(k) |^ n))*(Radix(k) |^ n) + (y mod (Radix(k) |^ n)
) by A22,NAT_D:2,PREPOWER:6;
x = (x div (Radix(k) |^ n))*(Radix(k) |^ n) + (x mod (Radix(k) |^ n))
by A22,NAT_D:2,PREPOWER:6;
then Sum SDSub2INT(z) = yn + x + RN * (y div (Radix(k) |^ n)) by A7,A59,A38
,RADIX_1:24;
hence thesis by A60,RADIX_3:def 12;
end;
A61: P[1]
proof
let k,x,y be Nat;
assume that
A62: k >= 3 and
A63: x is_represented_by 1,k and
A64: y is_represented_by 1,k;
reconsider k,x,y as Element of NAT by ORDINAL1:def 12;
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;
reconsider DIG1 = DigA_SDSub((X '+' Y),1) as Element of INT by INT_1:def 2;
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;
A65: 1 in Seg (1+1) by FINSEQ_1:1;
then
A66: (SDSub2INT(X '+' Y))/.1 = SDSub2INTDigit((X '+' Y),1,k) by 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 XREAL_1:232
.= 1 * DigB_SDSub((X '+' Y),1) by NEWTON:4
.= DigA_SDSub((X '+' Y),1) by RADIX_3:def 9;
A67: len (SDSub2INT(X '+' Y)) = 1 + 1 by CARD_1:def 7;
then 1 in dom SDSub2INT(X '+' Y) by A65,FINSEQ_1:def 3;
then
A68: SDSub2INT(X '+' Y).1 = DIG1 by A66,PARTFUN1:def 6;
2 - 1 = 1;
then
A69: 2 -' 1 = 1 by XREAL_0:def 2;
DigA_SDSub(X '+' Y, 1) = SDSubAddDigit(X,Y,1,k) by A65,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 A62,A65,Def1,
XXREAL_0:2
.= 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 XREAL_1:232
.= 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 XREAL_1:232
.= 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
RADIX_3:16
.= DigA_SDSub(X,1) + DigA_SDSub(Y,1) - Radix(k) * CRY1 by RADIX_3:def 4;
then
A70: DIG1 = x - RSDCX + DigA_SDSub(Y,1) - RCRY1 by A62,A63,Th6,XXREAL_0:2
.= x - RSDCX + (y - RSDCY) - RCRY1 by A62,A64,Th6,XXREAL_0:2
.= x + y - RSDCX - RSDCY - RCRY1;
reconsider DIG2 = Radix(k) * DigA_SDSub((X '+' Y),2) as Element of INT by
INT_1:def 2;
A71: 2 in Seg (1+1) by FINSEQ_1:1;
then
A72: (SDSub2INT(X '+' Y))/.2 = SDSub2INTDigit((X '+' Y),2,k) by 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 A69
.= Radix(k) * DigA_SDSub((X '+' Y),2) by RADIX_3:def 9;
2 in dom SDSub2INT(X '+' Y) by A71,A67,FINSEQ_1:def 3;
then SDSub2INT(X '+' Y).2 = DIG2 by A72,PARTFUN1:def 6;
then SDSub2INT(X '+' Y) = <* DIG1, DIG2 *> by A67,A68,FINSEQ_1:44;
then
A73: Sum SDSub2INT(X '+' Y) = DIG1 + DIG2 by RVSUM_1:77;
DigA_SDSub(X '+' Y, 2) = SDSubAddDigit(X,Y,2,k) by A71,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 A62,A71,Def1,
XXREAL_0:2
.= SDSub_Add_Data( SDSub_Add_Carry(x,k) + DigA_SDSub(Y,2), k ) + CRY1
by A62,A63,A69,Th4,XXREAL_0:2
.= SDSub_Add_Data( SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k), k ) +
CRY1 by A62,A64,Th4,XXREAL_0:2
.= 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
A62,Th2
.= SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k) - 0 + CRY1;
hence thesis by A73,A70,RADIX_3:def 12;
end;
for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8(A61,A2);
hence thesis by A1;
end;