:: Definitions of Radix-2k Signed-Digit number and its adder algorithm
:: by Yoshinori Fujisawa and Yasushi Fuwa
::
:: Received September 7, 1999
:: Copyright (c) 1999-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, ARYTM_1, ARYTM_3, CARD_1, XXREAL_0,
SUBSET_1, RELAT_1, NEWTON, POWER, TARSKI, XBOOLE_0, FINSEQ_2, FINSEQ_1,
FUNCT_1, PARTFUN1, CARD_3, ORDINAL4, RADIX_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1,
NAT_D, FUNCT_1, PARTFUN1, NEWTON, POWER, FINSEQ_1, RVSUM_1, FINSEQ_2,
GR_CY_1, XXREAL_0;
constructors REAL_1, NAT_D, FINSOP_1, NEWTON, POWER, GR_CY_1, BINOP_2;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED,
NEWTON, VALUED_0, POWER, CARD_1, FINSEQ_1, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities RVSUM_1;
theorems NAT_1, NAT_2, INT_1, FINSEQ_1, EULER_1, PREPOWER, POWER, RVSUM_1,
FINSEQ_2, FINSEQ_4, TARSKI, FUNCT_1, PEPIN, FINSEQ_5, NEWTON, XCMPLX_1,
XREAL_1, XXREAL_0, FINSOP_1, ORDINAL1, NAT_D, PARTFUN1, CARD_1, XREAL_0;
schemes NAT_1, FINSEQ_2;
begin :: Some Useful Theorems
reserve k,m,n for Nat,
i1,i2,i3 for Integer,
e for set;
Th1:
n mod k = k - 1 implies (n+1) mod k = 0 by NAT_D:69;
Th2:
n mod k < k - 1 implies (n+1) mod k = (n mod k) + 1 by NAT_D:70;
::$CT 2
theorem Th3:
for k,m,n being Integer holds
m <> 0 implies (k mod (m*n)) mod n = k mod n
proof
let k,m,n be Integer;
assume
A1: m <> 0;
per cases;
suppose
A2: n <> 0;
reconsider k9 = k, m9 = m, n9 = n as Integer;
m9*n9 <> 0 by A1,A2,XCMPLX_1:6;
hence (k mod (m*n)) mod n = (k9 - (k9 div (m9*n9))*(m9*n9)) mod n9
by INT_1:def 10
.= (k9 + (-(m9*(k9 div m9*n9)))*n9) mod n9
.= k mod n by NAT_D:61;
end;
suppose
A3: n = 0;
hence (k mod (m*n)) mod n = 0
.= k mod n by A3;
end;
end;
theorem
k <> 0 implies (n+1) mod k = 0 or (n+1) mod k = (n mod k) + 1
proof
assume
A1: k <> 0;
then k >= 1 by NAT_1:14;
then reconsider K = k - 1 as Element of NAT by INT_1:3,XREAL_1:48;
n mod k < k - 1 + 1 by A1,NAT_D:1;
then
A2: n mod k <= K by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
n mod k < k - 1;
hence thesis by Th2;
end;
suppose
n mod k = k - 1;
hence thesis by Th1;
end;
end;
reserve i,k,m,n,p,x,y for Nat;
theorem Th5:
i <> 0 & k <> 0 implies (n mod (i |^ k)) div (i |^ (k -'1)) < i
proof
assume that
A1: i <> 0 and
A2: k <> 0;
A3: n mod (i |^ k) < (i |^ k) by A1,NAT_D:1,PREPOWER:6;
reconsider n,i,k as Element of NAT by ORDINAL1:def 12;
set I1 = i |^ (k -'1);
set T = n mod (i |^ k);
i |^ k = i*(i |^ (k -'1)) by A1,A2,PEPIN:26;
then T mod I1 = n mod I1 by A1,Th3
.= n - I1*(n div I1) by A1,NEWTON:63,PREPOWER:6;
then T = I1*(T div I1) + (n - I1*(n div I1)) by A1,NAT_D:2,PREPOWER:6;
then
A4: I1*(T div I1) + (n - I1*(n div I1)) < i*I1 by A1,A2,A3,PEPIN:26;
A5: I1 <> 0 by A1,PREPOWER:6;
[\n/I1/] <= n/I1 by INT_1:def 6;
then n div I1 = [\n/I1/] & (T div I1) + [\n/I1/] <= (T div I1) + n/I1 by
INT_1:def 9,XREAL_1:6;
then
A6: (T div I1) + [\n/I1/] - [\n/I1/] <= (T div I1) + n/I1 - (n div I1) by
XREAL_1:9;
I1 > 0 by A1,PREPOWER:6;
then (I1*(T div I1) + n - I1*(n div I1))/I1 < i*I1/I1 by A4,XREAL_1:74;
then I1*(T div I1)/I1 + n/I1 - I1*(n div I1)/I1 < i*I1/I1 by XCMPLX_1:124;
then (T div I1) + n/I1 - I1*(n div I1)/I1 < i*I1/I1 by A5,XCMPLX_1:89;
then (T div I1) + n/I1 - (n div I1) < i*I1/I1 by A5,XCMPLX_1:89;
then (T div I1) + n/I1 - (n div I1) < i by A5,XCMPLX_1:89;
hence thesis by A6,XXREAL_0:2;
end;
::$CT
theorem
i2 > 0 & i3 >= 0 implies (i1 mod (i2*i3)) mod i3 = i1 mod i3
proof
assume that
A1: i2 > 0 and
A2: i3 >= 0;
per cases by A2;
suppose
i3 > 0;
then i2*i3 <> 0 by A1,XCMPLX_1:6;
then (i1 mod (i2*i3)) mod i3 = (i1 - (i1 div (i2*i3))*(i2*i3)) mod i3 by
INT_1:def 10
.= (i1 + (-(i2*(i1 div i2*i3)))*i3) mod i3;
hence thesis by NAT_D:61;
end;
suppose
A3: i3 = 0;
then (i1 mod (i2*i3)) mod i3 = 0;
hence thesis by A3;
end;
end;
begin :: Definition for Radix-2^k, k-SD
definition
let n be Nat;
func Radix(n) -> Element of NAT equals
2 to_power n;
correctness by ORDINAL1:def 12;
end;
definition
let k be Nat;
func k-SD -> set equals
{e where e is Element of INT:e <= Radix(k)-1 & e >=
-Radix(k)+1};
correctness;
end;
Lm1: for k be Nat st k >= 2 holds Radix(k) >= 2 + 2
proof
defpred P[Nat] means Radix($1) >= 2+2;
let k;
A1: for kk be Nat st kk >= 2 & P[kk] holds P[kk+1]
proof
let kk be Nat;
assume kk >= 2;
Radix(kk+1) = 2 to_power kk * 2 to_power 1 by POWER:27
.= Radix(kk) * 2;
then
A2: Radix(kk+1) >= Radix(kk) by XREAL_1:155;
assume Radix(kk) >= 2 + 2;
hence thesis by A2,XXREAL_0:2;
end;
Radix(2) = 2 to_power (1+1) .= 2 to_power 1 * 2 to_power 1 by POWER:27
.= 2 * 2 to_power 1
.= 2 * 2;
then
A3: P[2];
for k be Nat st k >= 2 holds P[k] from NAT_1:sch 8(A3,A1);
hence thesis;
end;
theorem Th7:
for e be object holds e in 0-SD iff e = 0
proof
let e be object;
A1: Radix(0) = 1 by POWER:24;
hereby
assume e in 0-SD;
then ex b be Element of INT st e = b & b <= 0 & b >= 0 by A1;
hence e = 0;
end;
assume
A2: e = 0;
then e is Element of INT by INT_1:def 2;
hence thesis by A1,A2;
end;
theorem
0-SD = {0} by Th7,TARSKI:def 1;
theorem Th9:
k-SD c= (k+1)-SD
proof
let e be object;
assume e in k-SD;
then consider g being Element of INT such that
A1: e = g and
A2: g <= Radix(k)-1 and
A3: g >= -Radix(k)+1;
k < k+1 by NAT_1:13;
then
A4: 2 to_power k < 2 to_power (k+1) by POWER:39;
then -Radix(k) > -Radix(k+1) by XREAL_1:24;
then -Radix(k)+1 > -Radix(k+1)+1 by XREAL_1:6;
then
A5: g >= -Radix(k+1)+1 by A3,XXREAL_0:2;
Radix(k)-1 < Radix(k+1)-1 by A4,XREAL_1:9;
then g <= Radix(k+1)-1 by A2,XXREAL_0:2;
hence thesis by A1,A5;
end;
theorem Th10:
e in k-SD implies e is Integer
proof
assume e in k-SD;
then ex t be Element of INT st e = t & t <= Radix(k)-1 & t >= -Radix(k)+1;
hence thesis;
end;
theorem Th11:
k-SD c= INT
proof
let e be object;
assume e in k-SD;
then e is Integer by Th10;
hence thesis by INT_1:def 2;
end;
theorem Th12:
i1 in k-SD implies i1 <= Radix(k)-1 & i1 >= -Radix(k)+1
proof
assume i1 in k-SD;
then
ex i be Element of INT st i = i1 & i <= Radix(k)-1 & i >= -Radix(k)+1;
hence thesis;
end;
theorem Th13:
0 in k-SD
proof
defpred P[Nat] means 0 in $1-SD;
A1: for k being Nat st P[k] holds P[k+1]
proof
let kk be Nat;
assume
A2: 0 in kk-SD;
kk-SD c= (kk+1)-SD by Th9;
hence thesis by A2;
end;
A3: P[0] by Th7;
for k being Nat holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
registration
let k be Nat;
cluster k-SD -> non empty;
coherence by Th13;
end;
definition
let k be Nat;
redefine func k-SD -> non empty Subset of INT; :: redefines -SD (RADIX_1, definition)
coherence by Th11;
end;
begin :: Functions for generating Radix-2^k SD numbers from Nats
:: and Nats from Radix-2^k SD numbers
reserve a for Tuple of n,(k-SD);
theorem Th14:
i in Seg n implies a.i is Element of k-SD
proof
A1: len a = n by CARD_1:def 7;
assume i in Seg n;
then i in dom a by A1,FINSEQ_1:def 3;
then
A2: a.i in rng a by FUNCT_1:def 3;
rng a c= k-SD by FINSEQ_1:def 4;
hence thesis by A2;
end;
definition
let i,k,n be Nat, x be Tuple of n,(k-SD);
func DigA(x,i) -> Integer equals
:Def3:
x.i if i in Seg n, 0 if i = 0;
coherence;
consistency by FINSEQ_1:1;
end;
definition
let i,k,n be Nat, x be Tuple of n,(k-SD);
func DigB(x,i) -> Element of INT equals
DigA(x,i);
coherence by INT_1:def 2;
end;
theorem Th15:
i in Seg n implies DigA(a,i) is Element of k-SD
proof
assume
A1: i in Seg n;
then a.i = DigA(a,i) by Def3;
hence thesis by A1,Th14;
end;
theorem Th16:
for x be Tuple of 1,INT st x/.1 = m holds x = <*m*>
proof
let x be Tuple of 1,INT;
assume
A1: x/.1 = m;
A2: len x = 1 by CARD_1:def 7;
then x/.1 = x.1 by FINSEQ_4:15;
hence thesis by A1,A2,FINSEQ_1:40;
end;
definition
let i,k,n be Nat, x be Tuple of n,(k-SD);
func SubDigit(x,i,k) -> Element of INT equals
(Radix(k) |^ (i -'1))*DigB(x,i
);
coherence by INT_1:def 2;
end;
definition
let n,k be Nat, x be Tuple of n,(k-SD);
func DigitSD(x) -> Tuple of n,INT means
:Def6:
for i be Nat st i in Seg n holds it/.i = SubDigit(x,i,k);
existence
proof
deffunc F(Nat)=SubDigit(x,$1,k);
consider z being FinSequence of INT 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;
reconsider z as Tuple of n,INT by A1,CARD_1:def 7;
take z;
let i be Nat;
assume
A4: i in Seg n;
then i in dom z by A1,FINSEQ_1:def 3;
hence z/.i = z.i by PARTFUN1:def 6
.= SubDigit(x,i,k) by A2,A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,INT such that
A5: for i be Nat st i in Seg n holds k1/.i = SubDigit(x,i,k) and
A6: for i be Nat st i in Seg n holds k2/.i = SubDigit(x,i,k);
A7: len k1 = n by CARD_1:def 7;
then
A8: dom k1 = Seg n by FINSEQ_1:def 3;
A9: len k2 = n by CARD_1:def 7;
now
let j be Nat;
assume
A10: j in dom k1;
then
A11: j in dom k2 by A9,A8,FINSEQ_1:def 3;
k1.j = k1/.j by A10,PARTFUN1:def 6
.= SubDigit(x,j,k) by A5,A8,A10
.= k2/.j by A6,A8,A10
.= k2.j by A11,PARTFUN1:def 6;
hence k1.j = k2.j;
end;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
definition
let n,k be Nat, x be Tuple of n,(k-SD);
func SDDec(x) -> Integer equals
Sum DigitSD(x);
coherence;
end;
definition
let i,k,x be Nat;
func DigitDC(x,i,k) -> Element of k-SD equals
(x mod (Radix(k) |^ i)) div (Radix(k) |^ (i -'1));
coherence
proof
reconsider i,k as Element of NAT by ORDINAL1:def 12;
set T = Radix(k) |^ i;
set S = Radix(k) |^ (i -'1);
defpred P[Nat] means ($1 mod T) div S is Element of k-SD;
A1: 0 in k-SD by Th13;
A2: Radix(k) <> 0 by POWER:34;
A4: 0 div S = 0;
A5: Radix(k) >= 1 by A2,NAT_1:14;
A6: for x being Nat st P[x] holds P[(x+1)]
proof
reconsider R = Radix(k)-1 as Element of NAT by A5,INT_1:3,XREAL_1:48;
let xx be Nat;
assume (xx mod T) div S is Element of k-SD;
set X = ((xx+1) mod T) div S;
per cases;
suppose
A7: i = 0;
Radix(k) |^ i = Radix(k) to_power i .= 1 by A7,POWER:24;
then ((xx+1) mod T) = (((xx+1)*1) mod 1) .= 0;
then X = 0;
hence thesis by Th13;
end;
suppose
A8: i > 0;
-1 >= -Radix(k) by A5,XREAL_1:24;
then
A9: X is Element of INT & 0 >= -Radix(k)+1 by INT_1:def 2,XREAL_1:59;
X < Radix(k) - 1 + 1 by A2,A8,Th5;
then X <= R by NAT_1:13;
then X in k-SD by A9;
hence thesis;
end;
end;
T > 0 by A2,NAT_1:14,PREPOWER:11;
then
A10: P[0] by A4,A1,NAT_D:24;
for x being Nat holds P[x] from NAT_1:sch 2(A10,A6);
hence thesis;
end;
end;
definition
let k,n,x be Nat;
func DecSD(x,n,k) -> Tuple of n,(k-SD) means
:Def9:
for i be Nat st i in Seg n holds DigA(it,i) = DigitDC(x,i,k);
existence
proof
deffunc F(Nat)=DigitDC(x,$1,k);
consider z being FinSequence of k-SD 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;
reconsider z as Tuple of n,(k-SD) by A1,CARD_1:def 7;
take z;
let i;
assume
A4: i in Seg n;
hence DigA(z,i) = z.i by Def3
.= DigitDC(x,i,k) by A2,A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,(k-SD) such that
A5: for i be Nat st i in Seg n holds DigA(k1,i) = DigitDC(x,i,k) and
A6: for i be Nat st i in Seg n holds DigA(k2,i) = DigitDC(x,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(k1,j) by A8,Def3
.= DigitDC(x,j,k) by A5,A8,A10
.= DigA(k2,j) by A6,A8,A10
.= k2.j by A8,A10,Def3;
hence k1.j = k2.j;
end;
len k2 = n by CARD_1:def 7;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
begin :: Definition for carry & data components of Addition
definition
let x be Integer;
func SD_Add_Carry(x) -> Integer equals
:Def10:
1 if x > 2, -1 if x < -2
otherwise 0;
coherence;
consistency;
end;
theorem Th17:
SD_Add_Carry(0) = 0 by Def10;
Lm2: for x be Integer holds -1 <= SD_Add_Carry(x) & SD_Add_Carry(x) <= 1
proof
let x be Integer;
per cases;
suppose
x < -2;
hence thesis by Def10;
end;
suppose
-2 <= x & x <= 2;
hence thesis by Def10;
end;
suppose
x > 2;
hence thesis by Def10;
end;
end;
definition
let x be Integer, k be Nat;
func SD_Add_Data(x,k) -> Integer equals
x - SD_Add_Carry(x)*Radix(k);
coherence;
end;
theorem
SD_Add_Data(0,k) = 0 by Th17;
theorem Th19:
k >= 2 & i1 in k-SD & i2 in k-SD implies -Radix(k)+2 <=
SD_Add_Data(i1+i2,k) & SD_Add_Data(i1+i2,k) <= Radix(k)-2
proof
assume that
A1: k >= 2 and
A2: i1 in k-SD & i2 in k-SD;
A3: -Radix(k)+1 <= i1 & -Radix(k)+1 <= i2 by A2,Th12;
set z = i1+i2;
i1 <= Radix(k)-1 & i2 <= Radix(k)-1 by A2,Th12;
then
A4: z <= Radix(k)-1 + (Radix(k)-1) by XREAL_1:7;
per cases;
suppose
A5: z < -2;
-Radix(k)+1 + (1 + -Radix(k)) <= z by A3,XREAL_1:7;
then
A6: (-Radix(k)+(1+1))-Radix(k) <= z;
SD_Add_Carry(z) = -1 & z + Radix(k) < -2 + Radix(k) by A5,Def10,XREAL_1:6;
hence thesis by A6,XREAL_1:20;
end;
suppose
A7: -2 <= z & z <= 2;
A8: Radix(k) >= 2+2 by A1,Lm1;
then
A9: Radix(k)-2 >= 2 by XREAL_1:19;
-Radix(k) <= -(2+2) by A8,XREAL_1:24;
then -Radix(k) <= -2 + -2;
then
A10: -Radix(k) - -2 <= -2 by XREAL_1:20;
SD_Add_Carry(z) = 0 by A7,Def10;
hence thesis by A7,A9,A10,XXREAL_0:2;
end;
suppose
A11: z > 2;
A12: z <= Radix(k)-1 -1 + Radix(k) by A4;
SD_Add_Carry(z) = 1 & z - Radix(k) > 2 - Radix(k) by A11,Def10,XREAL_1:9;
hence thesis by A12,XREAL_1:20;
end;
end;
begin :: Definition for checking whether or not a Nat can be
:: expressed as n digits Radix-2^k SD number
definition
let n,x,k be Nat;
pred x is_represented_by n,k means
x < (Radix(k) |^ n);
end;
theorem Th20:
m is_represented_by 1,k implies DigA(DecSD(m,1,k),1) = m
proof
assume m is_represented_by 1,k;
then
A1: m < Radix(k) |^ 1;
1 in Seg 1 by FINSEQ_1:1;
hence DigA(DecSD(m,1,k),1) = DigitDC(m,1,k) by Def9
.= (m mod (Radix(k) |^ 1)) div (Radix(k) |^ 0) by XREAL_1:232
.= (m mod (Radix(k) |^ 1)) div 1 by NEWTON:4
.= m mod (Radix(k) |^ 1)
.= m by A1,NAT_D:24;
end;
theorem
for n st n >= 1
for m st m is_represented_by n,k holds m = SDDec(DecSD(m,n,k))
proof
let n;
defpred P[Nat] means for m st m is_represented_by $1,k holds m = SDDec(DecSD
(m,$1,k));
A1: for u be Nat st u >= 1 & P[u] holds P[u+1]
proof
let u be Nat;
assume that
u >= 1 and
A2: P[u];
p is_represented_by (u+1),k implies p = SDDec(DecSD(p,(u+1),k))
proof
set I = u + 1;
set R = Radix(k) |^ u;
set M = p mod R;
set N = R*(p div R);
A3: I -' 1 = u by NAT_D:34;
A4: u+1 <= len (DigitSD(DecSD(p,(u+1),k))) by CARD_1:def 7;
A5: 1 <= u+1 by NAT_1:12;
then
A6: u+1 in Seg (u+1) by FINSEQ_1:1;
assume p is_represented_by (u+1),k;
then p < Radix(k) |^ (u+1);
then p div R = DigitDC(p,(u+1),k) by A3,NAT_D:24;
then
A7: N = SubDigit(DecSD(p,(u+1),k),(u+1),k) by A3,A6,Def9
.= (DigitSD(DecSD(p,(u+1),k)))/.(u+1) by A6,Def6
.= DigitSD(DecSD(p,(u+1),k)).(u+1) by A4,FINSEQ_4:15,NAT_1:12;
A8: DigitSD(DecSD(M,u,k))^<*N*> = DigitSD(DecSD(p,(u+1),k))
proof
N is Element of INT by INT_1:def 2;
then reconsider z1 = <*N*> as FinSequence of INT by FINSEQ_1:74;
reconsider DD = DigitSD(DecSD(p,(u+1),k)) as FinSequence of INT;
set z0 = DigitSD(DecSD(M,u,k));
reconsider z = z0^z1 as FinSequence of INT;
A9: len z = len (DigitSD(DecSD(M,u,k))) + len <*N*> by FINSEQ_1:22
.= u + len <*N*> by CARD_1:def 7
.= u + 1 by FINSEQ_1:39;
A10: for i be Nat st 1 <= i & i <= len z holds z/.i = DD/.i
proof
let i be Nat;
assume 1 <= i & i <= len z;
then
A11: i in Seg (u+1) by A9,FINSEQ_1:1;
per cases by A11,FINSEQ_2:7;
suppose
A12: i in Seg u;
A13: M mod (Radix(k) |^ i) = p mod (Radix(k) |^ i)
proof
i <= u by A12,FINSEQ_1:1;
then Radix(k) |^ i divides Radix(k) |^ u by NEWTON:89;
then consider t being Nat such that
A14: Radix(k) |^ u = (Radix(k) |^ i)*t by NAT_D:def 3;
Radix(k) <> 0 by POWER:34;
then t <> 0 by A14,PREPOWER:5;
hence thesis by A14,Th3;
end;
A15: i in dom (z0^z1) by A9,A11,FINSEQ_1:def 3;
len DD = u+1 by CARD_1:def 7;
then
A16: i in dom DD by A11,FINSEQ_1:def 3;
then
A17: DD.i = DD/.i by PARTFUN1:def 6;
A18: DD.i = (DigitSD(DecSD(p,(u+1),k)))/.i by A16,PARTFUN1:def 6
.= SubDigit(DecSD(p,(u+1),k),i,k) by A11,Def6
.= (Radix(k) |^ (i -'1))*DigitDC(p,i,k) by A11,Def9
.= (Radix(k) |^ (i -'1))*((p mod (Radix(k) |^ i)) div (Radix(k
) |^ (i -'1)));
len z0 = u by CARD_1:def 7;
then
A19: i in dom z0 by A12,FINSEQ_1:def 3;
then (z0^z1).i = DigitSD(DecSD(M,u,k)).i by FINSEQ_1:def 7
.= (DigitSD(DecSD(M,u,k)))/.i by A19,PARTFUN1:def 6
.= SubDigit(DecSD(M,u,k),i,k) by A12,Def6
.= (Radix(k) |^ (i -'1))*DigitDC(M,i,k) by A12,Def9
.= (Radix(k) |^ (i -'1))*((p mod (Radix(k) |^ i)) div (Radix(k
) |^ (i -'1))) by A13;
hence thesis by A18,A17,A15,PARTFUN1:def 6;
end;
suppose
A20: i = u+1;
hence z/.i = z.(u+1) by A5,A9,FINSEQ_4:15
.= (z0^z1).(len z0 + 1) by CARD_1:def 7
.= DigitSD(DecSD(p,(u+1),k)).(u+1) by A7,FINSEQ_1:42
.= DD/.i by A4,A20,FINSEQ_4:15,NAT_1:12;
end;
end;
len DD = u+1 by CARD_1:def 7;
hence thesis by A9,A10,FINSEQ_5:13;
end;
Radix(k) <> 0 by POWER:34;
then
A21: R <> 0 by PREPOWER:5;
then M < R by NAT_D:1;
then
A22: M is_represented_by u,k;
p = R*(p div R) + (p mod R) by A21,NAT_D:2;
then p = SDDec(DecSD(M,u,k)) + N by A2,A22;
hence thesis by A8,RVSUM_1:74;
end;
hence thesis;
end;
A23: P[1]
proof
let m;
assume
A24: m is_represented_by 1,k;
reconsider i = m as Element of REAL by XREAL_0:def 1;
reconsider M = <*i*> as FinSequence of REAL;
A25: 1 in Seg 1 by FINSEQ_1:1;
SubDigit(DecSD(m,1,k),1,k) = (Radix(k) |^ 0)*DigB(DecSD(m,1,k),1) by
XREAL_1:232
.= 1*DigB(DecSD(m,1,k),1) by NEWTON:4
.= m by A24,Th20;
then (DigitSD(DecSD(m,1,k)))/.1 = m by A25,Def6;
hence SDDec(DecSD(m,1,k)) = Sum M by Th16
.= m by FINSOP_1:11;
end;
for u be Nat st u >= 1 holds P[u] from NAT_1:sch 8(A23,A1);
hence thesis;
end;
theorem Th22:
m is_represented_by 1,k & n is_represented_by 1,k implies
SD_Add_Carry(DigA(DecSD(m,1,k),1)+DigA(DecSD(n,1,k),1)) = SD_Add_Carry(m+n)
proof
assume that
A1: m is_represented_by 1,k and
A2: n is_represented_by 1,k;
SD_Add_Carry(DigA(DecSD(m,1,k),1)+DigA(DecSD(n,1,k),1)) = SD_Add_Carry(m
+ DigA(DecSD(n,1,k),1)) by A1,Th20
.= SD_Add_Carry(m + n) by A2,Th20;
hence thesis;
end;
Lm3: for i st i in Seg n holds DigA(DecSD(m,n+1,k),i)=DigA(DecSD((m mod (Radix
(k) |^ n)),n,k),i)
proof
let i;
assume
A1: i in Seg n;
then
A2: i <= n by FINSEQ_1:1;
then
A3: i <= n+1 by NAT_1:12;
1 <= i by A1,FINSEQ_1:1;
then
A4: i in Seg (n+1) by A3,FINSEQ_1:1;
Radix(k) |^ i divides Radix(k) |^ n by A2,NEWTON:89;
then consider t be Nat such that
A5: Radix(k) |^ n = (Radix(k) |^ i)*t by NAT_D:def 3;
Radix(k) <> 0 by POWER:34;
then
A6: t <> 0 by A5,PREPOWER:5;
DigA(DecSD((m mod (Radix(k) |^ n)),n,k),i) = DigitDC((m mod (Radix(k)
|^ n)),i,k) by A1,Def9
.= DigitDC(m,i,k) by A5,A6,Th3
.= DigA(DecSD(m,n+1,k),i) by A4,Def9;
hence thesis;
end;
theorem Th23:
m is_represented_by (n+1),k implies DigA(DecSD(m,(n+1),k),n+1) =
m div (Radix(k) |^ n)
proof
assume m is_represented_by (n+1),k;
then
A1: m < Radix(k) |^ (n+1);
n+1 in Seg (n+1) by FINSEQ_1:3;
then DigA(DecSD(m,(n+1),k),n+1) = DigitDC(m,n+1,k) by Def9
.= m div (Radix(k) |^ ((n+1) -'1)) by A1,NAT_D:24
.= m div (Radix(k) |^ n) by NAT_D:34;
hence thesis;
end;
begin :: Definition for Addition operation for a high-speed adder algorithm
:: on Radix-2^k SD number
definition
let k,i,n be Nat, x,y be Tuple of n,(k-SD);
assume that
A1: i in Seg n and
A2: k >= 2;
func Add(x,y,i,k) -> Element of k-SD equals
:Def13:
SD_Add_Data(DigA(x,i)+
DigA(y,i),k) + SD_Add_Carry(DigA(x,i -'1)+DigA(y,i -'1));
coherence
proof
set SDC = SD_Add_Carry(DigA(x,i -'1)+DigA(y,i -'1));
set SDD = SD_Add_Data(DigA(x,i)+DigA(y,i),k);
A3: -1 <= SDC by Lm2;
A4: SDC <= 1 by Lm2;
A5: DigA(x,i) is Element of k-SD & DigA(y,i) is Element of k-SD by A1,Th15;
then SDD <= Radix(k)-2 by A2,Th19;
then
A6: SDD + SDC <= Radix(k)-2 + 1 by A4,XREAL_1:7;
-Radix(k)+2 <= SDD by A2,A5,Th19;
then SDD + SDC is Element of INT & -Radix(k)+2 +(-1) <= SDD + SDC by A3,
INT_1:def 2,XREAL_1:7;
then SDD + SDC in k-SD by A6;
hence thesis;
end;
end;
definition
let n,k be Nat,x,y be Tuple of n,(k-SD);
func x '+' y -> Tuple of n,(k-SD) means
:Def14:
for i st i in Seg n holds DigA(it,i) = Add(x,y,i,k);
existence
proof
deffunc F(Nat)= Add(x,y,$1,k);
consider z being FinSequence of (k-SD) 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;
reconsider z as Tuple of n,(k-SD) by A1,CARD_1:def 7;
take z;
let i;
assume
A4: i in Seg n;
hence DigA(z,i) = z.i by Def3
.= Add(x,y,i,k) by A2,A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,(k-SD) such that
A5: for i st i in Seg n holds DigA(k1,i) = Add(x,y,i,k) and
A6: for i st i in Seg n holds DigA(k2,i) = Add(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(k1,j) by A8,Def3
.= Add(x,y,j,k) by A5,A8,A10
.= DigA(k2,j) by A6,A8,A10
.= k2.j by A8,A10,Def3;
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 Th24:
k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k
implies SDDec(DecSD(m,1,k)'+'DecSD(n,1,k)) = SD_Add_Data(m+n,k)
proof
assume that
A1: k >= 2 and
A2: m is_represented_by 1,k and
A3: n is_represented_by 1,k;
set N = DecSD(n,1,k);
set M = DecSD(m,1,k);
A4: 1 in Seg 1 by FINSEQ_1:1;
then
A5: DigA((M '+' N),1) = Add(M,N,1,k) by Def14
.= SD_Add_Data(DigA(M,1)+DigA(N,1),k) + SD_Add_Carry(DigA(M,1 -'1)+DigA(
N,1 -'1)) by A1,A4,Def13
.= SD_Add_Data(DigA(M,1)+DigA(N,1),k) + SD_Add_Carry(DigA(M,0)+DigA(N,1
-'1)) by XREAL_1:232
.= SD_Add_Data(DigA(M,1)+DigA(N,1),k) + SD_Add_Carry(DigA(M,0)+DigA(N,0)
) by XREAL_1:232
.= SD_Add_Data(DigA(M,1)+DigA(N,1),k) + SD_Add_Carry(0+DigA(N,0)) by Def3
.= SD_Add_Data(DigA(M,1)+DigA(N,1),k) + 0 by Def3,Th17
.= SD_Add_Data(m+DigA(N,1),k) by A2,Th20
.= SD_Add_Data(m+n,k) by A3,Th20;
A6: (DigitSD(M '+' N))/.1 = SubDigit((M '+' N),1,k) by A4,Def6
.= (Radix(k) |^ 0)*DigA((M '+' N),1) by XREAL_1:232
.= 1*DigA((M '+' N),1) by NEWTON:4
.= SD_Add_Data(m+n,k) by A5;
reconsider w = SD_Add_Data(m+n,k) as Element of INT by INT_1:def 2;
A7: len (DigitSD(M '+' N)) = 1 by CARD_1:def 7;
1 in Seg 1 by FINSEQ_1:1;
then 1 in dom DigitSD(M '+' N) by A7,FINSEQ_1:def 3;
then DigitSD(M '+' N).1 = SD_Add_Data(m+n,k) by A6,PARTFUN1:def 6;
then SDDec(M '+' N) = Sum <*w*> by A7,FINSEQ_1:40
.= SD_Add_Data(m+n,k) by RVSUM_1:73;
hence thesis;
end;
theorem
for n st n >= 1 holds for k,x,y st k >= 2 & x is_represented_by n,k &
y is_represented_by n,k holds x + y = (SDDec(DecSD(x,n,k) '+' DecSD(y,n,k))) +
(Radix(k) |^ n)* SD_Add_Carry(DigA(DecSD(x,n,k),n)+DigA(DecSD(y,n,k),n))
proof
defpred P[Nat] means for k,x,y be Nat st k >= 2 & x is_represented_by $1,k &
y is_represented_by $1,k holds x + y = (SDDec(DecSD(x,$1,k) '+' DecSD(y,$1,k)))
+(Radix(k) |^ $1)* SD_Add_Carry(DigA(DecSD(x,$1,k),$1)+DigA(DecSD(y,$1,k),$1));
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];
A5: n in Seg n by A3,FINSEQ_1:3;
let k,x,y be Nat;
A6: n+1 in Seg (n+1) by FINSEQ_1:3;
set z = DecSD(x,(n+1),k) '+' DecSD(y,(n+1),k);
set yn = y mod (Radix(k) |^ n);
set xn = x mod (Radix(k) |^ n);
assume that
A7: k >= 2 and
A8: x is_represented_by (n+1),k and
A9: y is_represented_by (n+1),k;
set zn = DecSD(xn,n,k) '+' DecSD(yn,n,k);
A10: len DigitSD(zn) = n by CARD_1:def 7;
A11: len DigitSD(z) = n+1 by CARD_1:def 7;
A12: for i be Nat st 1 <= i & i <= len DigitSD(z) holds (DigitSD(z)).i = (
(DigitSD(zn))^<*SubDigit(z,n+1,k)*>).i
proof
let i be Nat;
assume that
A13: 1 <= i and
A14: i <= len DigitSD(z);
A15: i -'1 = i - 1 by A13,XREAL_1:233;
A16: i <= n+1 by A14,CARD_1:def 7;
then
A17: i in Seg (n+1) by A13,FINSEQ_1:1;
then
A18: i in dom DigitSD(z) by A11,FINSEQ_1:def 3;
per cases by A17,FINSEQ_2:7;
suppose
A19: i in Seg n;
then
A20: i in dom DigitSD(zn) by A10,FINSEQ_1:def 3;
then
A21: ((DigitSD(zn))^<*SubDigit(z,n+1,k)*>).i = DigitSD(zn).i by
FINSEQ_1:def 7
.= (DigitSD(zn))/.i by A20,PARTFUN1:def 6
.= SubDigit(zn,i,k) by A19,Def6
.= (Radix(k) |^ (i -'1)) *Add(DecSD(xn,n,k),DecSD(yn,n,k),i,k) by A19
,Def14
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(yn,n,k),i),k) + SD_Add_Carry(DigA(DecSD(xn,n,k),i -'1) + DigA(DecSD(
yn,n,k),i -'1))) by A7,A19,Def13;
A22: DigitSD(z).i = (DigitSD(z))/.i by A18,PARTFUN1:def 6
.= SubDigit(z,i,k) by A17,Def6
.= (Radix(k) |^ (i -'1)) *Add(DecSD(x,(n+1),k),DecSD(y,(n+1),k),i,
k) by A17,Def14
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(x,(n+1),k),i) +
DigA(DecSD(y,(n+1),k),i),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),k),i -'1) + DigA(
DecSD(y,(n+1),k),i -'1))) by A7,A17,Def13;
now
per cases by A13,XXREAL_0:1;
suppose
A23: i = 1;
then
A24: ((DigitSD(zn))^<*SubDigit(z,n+1,k)*>).i = ( Radix(k) |^ (i -'
1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) + DigA(DecSD(yn,n,k),i),k) +
SD_Add_Carry(DigA(DecSD(xn,n,k),i -'1) + DigA(DecSD(yn,n,k),0))) by A21,
XREAL_1:232
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(yn,n,k),i),k) + SD_Add_Carry(DigA(DecSD(xn,n,k),0) + DigA(DecSD(yn,n
,k),0))) by A23,XREAL_1:232
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(yn,n,k),i),k) + SD_Add_Carry(DigA(DecSD(xn,n,k),0) + 0)) by Def3
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(yn,n,k),i),k)+0) by Def3,Th17;
DigitSD(z).i = (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD
(x,(n+1),k),i) + DigA(DecSD(y,(n+1),k),i),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),
k),i -'1) + DigA(DecSD(y,(n+1),k),0))) by A22,A23,XREAL_1:232
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(x,(n+1),k),i
) + DigA(DecSD(y,(n+1),k),i),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),k),0) + DigA(
DecSD(y,(n+1),k),0))) by A23,XREAL_1:232
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(x,(n+1),k),i
) + DigA(DecSD(y,(n+1),k),i),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),k),0) + 0))
by Def3
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(x,(n+1),k),i
) + DigA(DecSD(y,(n+1),k),i),k)+0) by Def3,Th17
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(y,(n+1),k),i),k)) by A19,Lm3
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(yn,n,k),i),k)) by A19,Lm3;
hence thesis by A24;
end;
suppose
A25: i > 1;
A26: i - 1 <= n by A16,XREAL_1:20;
i -'1 >= 1 by A25,NAT_D:49;
then
A27: i -'1 in Seg n by A15,A26,FINSEQ_1:1;
DigitSD(z).i = (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD
(xn,n,k),i) + DigA(DecSD(y,(n+1),k),i),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),k),
i -'1) + DigA(DecSD(y,(n+1),k),i -'1))) by A19,A22,Lm3
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(yn,n,k),i),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),k),i -'1) + DigA(
DecSD(y,(n+1),k),i -'1))) by A19,Lm3
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(yn,n,k),i),k) + SD_Add_Carry(DigA(DecSD(xn,n,k),i -'1) + DigA(DecSD(
y,(n+1),k),i -'1))) by A27,Lm3
.= (Radix(k) |^ (i -'1)) *(SD_Add_Data(DigA(DecSD(xn,n,k),i) +
DigA(DecSD(yn,n,k),i),k) + SD_Add_Carry(DigA(DecSD(xn,n,k),i -'1) + DigA(DecSD(
yn,n,k),i -'1))) by A27,Lm3;
hence thesis by A21;
end;
end;
hence thesis;
end;
suppose
A28: i = n+1;
then ((DigitSD(zn))^<*SubDigit(z,n+1,k)*>).i = ((DigitSD(zn))^<*
SubDigit(z,n+1,k)*>).((len (DigitSD(zn)))+1) by CARD_1:def 7
.= SubDigit(z,n+1,k) by FINSEQ_1:42
.= (DigitSD(z))/.(n+1) by A6,Def6
.= DigitSD(z).(n+1) by A18,A28,PARTFUN1:def 6;
hence thesis by A28;
end;
end;
A29: SubDigit(z,n+1,k) = (Radix(k) |^ n)*DigB(z,(n+1)) by NAT_D:34;
A30: Radix(k) > 0 by POWER:34;
then
A31: x = (x div (Radix(k) |^ n))*(Radix(k) |^ n) + (x mod (Radix(k) |^ n))
by NAT_D:2,PREPOWER:6;
set y1 = y div (Radix(k) |^ n);
set x1 = x div (Radix(k) |^ n);
A32: len <*SubDigit(z,n+1,k)*> = 1 by FINSEQ_1:39;
A33: DigA(DecSD(y,(n+1),k),n+1) = y1 by A9,Th23;
yn < Radix(k) |^ n by A30,NAT_D:1,PREPOWER:6;
then
A34: yn is_represented_by n,k;
xn < Radix(k) |^ n by A30,NAT_D:1,PREPOWER:6;
then
A35: xn is_represented_by n,k;
len (DigitSD(zn)^<*SubDigit(z,n+1,k)*>) = len DigitSD(zn) + len <*
SubDigit(z,n+1,k)*> by FINSEQ_1:22
.= n+1 by A32,CARD_1:def 7;
then len DigitSD(z) = len (DigitSD(zn)^<*SubDigit(z,n+1,k)*>) by
CARD_1:def 7;
then DigitSD(z) = DigitSD(zn)^<*SubDigit(z,n+1,k)*> by A12,FINSEQ_1:14;
then SDDec(z) = (Radix(k) |^ n)*DigB(z,(n+1)) + Sum DigitSD(zn) by A29,
RVSUM_1:74
.= Add(DecSD(x,(n+1),k),DecSD(y,(n+1),k),(n+1),k)*(Radix(k) |^ n) +
Sum DigitSD(zn) by A6,Def14
.= (SD_Add_Data(DigA(DecSD(x,(n+1),k),(n+1)) + DigA(DecSD(y,(n+1),k),(
n+1)),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),k),(n+1)-'1) + DigA(DecSD(y,(n+1),k)
,(n+1)-'1)))*(Radix(k) |^ n) + Sum DigitSD(zn) by A6,A7,Def13
.= (SD_Add_Data(DigA(DecSD(x,(n+1),k),(n+1)) + DigA(DecSD(y,(n+1),k),(
n+1)),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),k),(n+1)-'1) + DigA(DecSD(y,(n+1),k)
,n)))*(Radix(k) |^ n) + Sum DigitSD(zn) by NAT_D:34
.= (SD_Add_Data(DigA(DecSD(x,(n+1),k),(n+1)) + DigA(DecSD(y,(n+1),k),(
n+1)),k) + SD_Add_Carry(DigA(DecSD(x,(n+1),k),n) + DigA(DecSD(y,(n+1),k),n)))*(
Radix(k) |^ n) + Sum DigitSD(zn) by NAT_D:34
.= (SD_Add_Data(DigA(DecSD(x,(n+1),k),(n+1)) + DigA(DecSD(y,(n+1),k),(
n+1)),k) + SD_Add_Carry(DigA(DecSD(xn,n,k),n) + DigA(DecSD(y,(n+1),k),n)))*(
Radix(k) |^ n) + Sum DigitSD(zn) by A5,Lm3
.= (SD_Add_Data(DigA(DecSD(x,(n+1),k),(n+1)) + DigA(DecSD(y,(n+1),k),(
n+1)),k) + SD_Add_Carry(DigA(DecSD(xn,n,k),n) + DigA(DecSD(yn,n,k),n)))*(Radix(
k) |^ n) + Sum DigitSD(zn) by A5,Lm3
.= (SD_Add_Data(x1+y1,k)+ SD_Add_Carry(DigA(DecSD(xn,n,k),n) + DigA(
DecSD(yn,n,k),n)))*(Radix(k) |^ n) + Sum DigitSD(zn) by A8,A33,Th23
.= SD_Add_Data(x1+y1,k)*(Radix(k) |^ n) + (SD_Add_Carry(DigA(DecSD(xn,
n,k),n)+DigA(DecSD(yn,n,k),n)) *(Radix(k) |^ n)+(SDDec(DecSD(xn,n,k)'+'DecSD(yn
,n,k))))
.= SD_Add_Data(x1+y1,k)*(Radix(k) |^ n) + (xn + yn) by A4,A7,A35,A34
.= SD_Add_Data(x1+y1,k)*(Radix(k) |^ n) + xn + yn;
then SDDec(z) + SD_Add_Carry(x1+y1)*(Radix(k) |^ (n+1)) = SD_Add_Data(x1+
y1,k)*(Radix(k) |^ n) + SD_Add_Carry(x1+y1)*(Radix(k) |^ (n+1))+ xn + yn
.= SD_Add_Data(x1+y1,k)*(Radix(k) |^ n) + SD_Add_Carry(x1+y1)*((Radix(
k) |^ n)*Radix(k)) + xn + yn by NEWTON:6
.= (x1*(Radix(k) |^ n) + xn) + (y1*(Radix(k) |^ n) + yn)
.= x + y by A30,A31,NAT_D:2,PREPOWER:6;
hence thesis by A8,A33,Th23;
end;
A36: P[1]
proof
let k,x,y be Nat;
assume k >= 2 & x is_represented_by 1,k & y is_represented_by 1,k;
then
A37: SDDec(DecSD(x,1,k)'+'DecSD(y,1,k)) = SD_Add_Data(x + y,k) &
SD_Add_Carry( DigA(DecSD(x,1,k),1)+DigA(DecSD(y,1,k),1)) = SD_Add_Carry(x+y)
by Th22,Th24;
thus thesis by A37;
end;
for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8(A36,A2);
hence thesis by A1;
end;