:: Improvement of Radix-$2^k$ Signed-Digit Number for High Speed Circuit
:: 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, RADIX_1, ARYTM_1, ARYTM_3,
POWER, RELAT_1, CARD_1, FINSEQ_1, NEWTON, SUBSET_1, TARSKI, XBOOLE_0,
FINSEQ_2, FUNCT_1, PARTFUN1, CARD_3, ORDINAL4, RADIX_3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
INT_1, NAT_D, FUNCT_1, PARTFUN1, NEWTON, POWER, FINSEQ_1, FINSEQ_2,
GR_CY_1, RADIX_1;
constructors REAL_1, NAT_D, NEWTON, POWER, BINARITH, GR_CY_1, RADIX_1,
RELSET_1;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED,
NEWTON, VALUED_0, FINSEQ_2, CARD_1, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities RADIX_1;
expansions RADIX_1;
theorems RADIX_1, POWER, NAT_1, INT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, PRE_FF,
NEWTON, RVSUM_1, PREPOWER, JORDAN12, FINSEQ_3, RADIX_2, XREAL_1,
XXREAL_0, NAT_D, ORDINAL1, PARTFUN1, XREAL_0, CARD_1;
schemes NAT_1, FINSEQ_2;
begin :: Definition for Radix-2^k SD_Sub number
reserve i,n,m,k,x for Nat,
i1,i2 for Integer;
Lm1: 1 <= k implies Radix(k) = Radix(k -' 1) + Radix(k -' 1)
proof
assume 1 <= k;
then Radix(k) = 2 to_power ( k -' 1 + 1 ) by XREAL_1:235
.= (2 to_power 1) * (2 to_power (k -' 1)) by POWER:27
.= 2 * Radix(k -' 1) by POWER:25
.= Radix(k -' 1) + Radix(k -' 1);
hence thesis;
end;
Lm2: 1 <= k implies Radix(k) - Radix(k -' 1) = Radix(k -' 1)
proof
assume 1 <= k;
then Radix(k) + 0 = Radix(k-'1) + Radix(k-'1) by Lm1;
hence thesis;
end;
Lm3: 1 <= k implies -Radix(k) + Radix(k -' 1) = -Radix(k -' 1)
proof
assume 1 <= k;
then -(Radix(k) - Radix(k-'1)) = -Radix(k-'1) by Lm2;
hence thesis;
end;
Lm4: for k be Nat st 1 <= k holds 2 <= Radix(k)
proof
defpred P[Nat] means 2<= Radix($1);
let k;
assume
A1: 1 <= k;
A2: for kk be Nat st kk >= 1 & P[kk] holds P[(kk+1)]
proof
let kk be Nat;
assume that
1 <= kk and
A3: 2 <= Radix(kk);
A4: Radix(kk + 1) = 2 to_power (1) * 2 to_power (kk) by POWER:27
.= 2 * Radix(kk) by POWER:25;
Radix(kk) > 1 by A3,XXREAL_0:2;
hence thesis by A4,XREAL_1:155;
end;
A5: P[1] by POWER:25;
for k be Nat holds 1 <= k implies P[k] from NAT_1:sch 8(A5,A2);
hence thesis by A1;
end;
Lm5: 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,RADIX_1:def 9
.= DigitDC(m,i,k) by A5,A6,RADIX_1:3
.= DigA(DecSD(m,n+1,k),i) by A4,RADIX_1:def 9;
hence thesis;
end;
definition
let k;
func k-SD_Sub_S -> set equals
{e where e is Element of INT: e >= -Radix(k -' 1) & e
<= Radix(k -' 1) - 1 };
correctness;
func k-SD_Sub -> set equals
{e where e is Element of INT: e >= -Radix(k -' 1) - 1 &
e <= Radix(k -' 1) };
correctness;
end;
theorem Th1:
i1 in k-SD_Sub implies -Radix(k-'1) - 1 <= i1 & i1 <= Radix(k-'1)
proof
assume i1 in k-SD_Sub;
then
ex i be Element of INT st i = i1 & -Radix(k-'1) - 1 <= i & i <= Radix(k-' 1);
hence thesis;
end;
theorem Th2:
k-SD_Sub_S c= k-SD_Sub
proof
let e be object;
assume e in k-SD_Sub_S;
then consider g being Element of INT such that
A1: e = g and
A2: g >= -Radix(k-'1) and
A3: g <= Radix(k-'1) - 1;
Radix(k-'1) + 1 >= Radix(k-'1) + 0 by XREAL_1:7;
then -Radix(k-'1) >= -(Radix(k-'1) + 1) by XREAL_1:24;
then
A4: g >= -Radix(k-'1) - 1 by A2,XXREAL_0:2;
Radix(k-'1) + 0 >= Radix(k-'1) + -1 by XREAL_1:7;
then Radix(k-'1) >= g by A3,XXREAL_0:2;
hence thesis by A1,A4;
end;
theorem Th3:
k-SD_Sub_S c= (k+1)-SD_Sub_S
proof
let e be object;
assume e in k-SD_Sub_S;
then consider g being Element of INT such that
A1: e = g and
A2: g >= -Radix(k-'1) and
A3: g <= Radix(k-'1) - 1;
k-'1 <= k by NAT_D:44;
then
A4: 2 to_power (k-'1) <= 2 to_power k by PRE_FF:8;
then Radix(k-'1) - 1 <= Radix(k) - 1 by XREAL_1:9;
then Radix(k-'1) - 1 <= Radix(k + 1 -' 1) - 1 by NAT_D:34;
then
A5: g <= Radix(k + 1 -' 1) - 1 by A3,XXREAL_0:2;
-Radix(k-'1) >= -Radix(k) by A4,XREAL_1:24;
then -Radix(k-'1) >= -Radix(k + 1 -' 1) by NAT_D:34;
then g >= -Radix(k + 1 -' 1) by A2,XXREAL_0:2;
hence thesis by A1,A5;
end;
theorem
2 <= k implies k-SD_Sub c= k-SD
proof
assume
A1: 2 <= k;
then 1 + 1 <= k;
then 1 <= k -' 1 by NAT_D:55;
then
A2: Radix(k -' 1) >= 2 by Lm4;
then Radix(k-'1) >= 1 by XXREAL_0:2;
then -Radix(k-'1) <= -1 by XREAL_1:24;
then
A3: Radix(k) + -Radix(k-'1) <= Radix(k) + -1 by XREAL_1:7;
let e be object;
assume e in k-SD_Sub;
then consider g being Element of INT such that
A4: e = g and
A5: g >= -Radix(k-'1) - 1 and
A6: g <= Radix(k-'1);
Radix(k -' 1) + Radix(k -' 1) >= Radix(k -' 1) + 2 by A2,XREAL_1:6;
then Radix(k) + 0 >= (Radix(k -' 1) + 1) + 1 by A1,Lm1,XXREAL_0:2;
then Radix(k) - 1 >= (Radix(k -' 1) + 1) - 0 by XREAL_1:21;
then -(Radix(k -' 1) + 1) >= -(Radix(k) - 1) by XREAL_1:24;
then
A7: g >= -Radix(k) + 1 by A5,XXREAL_0:2;
Radix(k) + 0 = Radix(k-'1) + Radix(k-'1) by A1,Lm1,XXREAL_0:2;
then g <= Radix(k) - 1 by A6,A3,XXREAL_0:2;
hence thesis by A4,A7;
end;
theorem Th5:
0 in 0-SD_Sub_S
proof
reconsider ZERO = 0 as Integer;
0 > 0 - 1;
then 0 -' 1 = 0 by XREAL_0:def 2;
then
A1: Radix(0-'1) = 1 by POWER:24;
ZERO is Element of INT by INT_1:def 2;
hence thesis by A1;
end;
theorem Th6:
0 in k-SD_Sub_S
proof
defpred P[Nat] means 0 in $1-SD_Sub_S;
A1: for k being Nat st P[k] holds P[(k+1)]
proof
let kk be Nat;
assume
A2: 0 in kk-SD_Sub_S;
kk-SD_Sub_S c= (kk+1)-SD_Sub_S by Th3;
hence thesis by A2;
end;
A3: P[0] by Th5;
for k being Nat holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th7:
0 in k-SD_Sub
proof
0 in k-SD_Sub_S & k-SD_Sub_S c= k-SD_Sub by Th2,Th6;
hence thesis;
end;
theorem Th8:
for e being set st e in k-SD_Sub holds e is Integer
proof
let e be set;
assume e in k-SD_Sub;
then
ex t be Element of INT st e = t & t >= -Radix(k-'1)-1 & t <= Radix(k-'1);
hence thesis;
end;
theorem Th9:
k-SD_Sub c= INT
proof
let e be object;
assume e in k-SD_Sub;
then e is Integer by Th8;
hence thesis by INT_1:def 2;
end;
theorem Th10:
k-SD_Sub_S c= INT
proof
let e be object;
assume
A1: e in k-SD_Sub_S;
k-SD_Sub_S c= k-SD_Sub by Th2;
then e is Integer by A1,Th8;
hence thesis by INT_1:def 2;
end;
registration
let k;
cluster k-SD_Sub_S -> non empty;
coherence by Th6;
cluster k-SD_Sub -> non empty;
coherence by Th7;
end;
definition
let k;
redefine func k-SD_Sub_S -> non empty Subset of INT; :: redefines -SD_Sub_S (RADIX_3, definition)
coherence by Th10;
end;
definition
let k;
redefine func k-SD_Sub -> non empty Subset of INT; :: redefines -SD_Sub (RADIX_3, definition)
coherence by Th9;
end;
reserve a for Tuple of n,k-SD;
reserve aSub for Tuple of n,k-SD_Sub;
theorem Th11:
i in Seg n implies aSub.i is Element of k-SD_Sub
proof
A1: len aSub = n by CARD_1:def 7;
assume i in Seg n;
then i in dom aSub by A1,FINSEQ_1:def 3;
then
A2: aSub.i in rng aSub by FUNCT_1:def 3;
rng aSub c= k-SD_Sub by FINSEQ_1:def 4;
hence thesis by A2;
end;
begin :: Definition for new carry calculation method
definition
let x be Integer, k be Nat;
func SDSub_Add_Carry(x,k) -> Integer equals
:Def3:
1 if Radix(k -' 1) <= x,
-1 if x < -Radix(k -' 1) otherwise 0;
coherence;
consistency;
end;
definition
let x be Integer, k be Nat;
func SDSub_Add_Data(x,k) -> Integer equals
x - Radix(k) * SDSub_Add_Carry(x,
k);
coherence;
end;
theorem Th12:
for x be Integer, k be Nat holds -1 <= SDSub_Add_Carry(x,k) &
SDSub_Add_Carry(x,k) <= 1
proof
let x be Integer, k be Nat;
per cases;
suppose
x < -Radix(k-'1);
hence thesis by Def3;
end;
suppose
-Radix(k-'1) <= x & x < Radix(k-'1);
hence thesis by Def3;
end;
suppose
x >= Radix(k-'1);
hence thesis by Def3;
end;
end;
theorem Th13:
2 <= k & i1 in k-SD implies SDSub_Add_Data(i1,k) >= -Radix(k-'1)
& SDSub_Add_Data(i1,k) <= Radix(k-'1) - 1
proof
assume that
A1: 2 <= k and
A2: i1 in k-SD;
A3: -Radix(k) + 1 <= i1 & 1 <= k by A1,A2,RADIX_1:13,XXREAL_0:2;
now
per cases;
case
A4: i1 < -Radix(k -' 1);
then i1 + 1 <= -Radix(k-'1) by INT_1:7;
then i1 <= -Radix(k-'1) - 1 by XREAL_1:19;
then i1 + Radix(k) <= Radix(k) + ( -Radix(k-'1) - 1 ) by XREAL_1:7;
then
A5: i1 + Radix(k) <= Radix(k) - Radix(k-'1) - 1;
SDSub_Add_Carry(i1,k) = -1 by A4,Def3;
hence thesis by A3,A5,Lm2,XREAL_1:19;
end;
case
A6: -Radix(k -' 1) <= i1 & i1 < Radix(k -' 1);
then SDSub_Add_Carry(i1,k) = 0 & i1 + 1 <= Radix(k -' 1) by Def3,INT_1:7;
hence thesis by A6,XREAL_1:19;
end;
case
A7: Radix(k-'1) <= i1;
i1 <= Radix(k) + -1 by A2,RADIX_1:13;
then
A8: 0 - 1 <= Radix(k-'1) - 1 & i1 - Radix(k) <= -1 by XREAL_1:9,20;
SDSub_Add_Carry(i1,k) = 1 & Radix(k-'1) + -Radix(k) <= i1 + -Radix(
k) by A7,Def3,XREAL_1:6;
hence thesis by A1,A8,Lm3,XXREAL_0:2;
end;
end;
hence thesis;
end;
theorem Th14:
for x be Integer, k be Nat st 2 <= k holds SDSub_Add_Carry(x,k) in k-SD_Sub_S
proof
let x be Integer, k be Nat;
A1: SDSub_Add_Carry(x,k) <= 1 by Th12;
assume k >= 2;
then k > 1 by XXREAL_0:2;
then k - 1 > 1 - 1 by XREAL_1:14;
then
A2: k -' 1 > 0 by XREAL_0:def 2;
then 2 to_power (k -' 1) > 1 by POWER:35;
then
A3: -Radix(k-'1) <= -1 by XREAL_1:24;
-1 <= SDSub_Add_Carry(x,k) by Th12;
then
A4: SDSub_Add_Carry(x,k) >= -Radix(k-'1) by A3,XXREAL_0:2;
Radix(k-'1) - 1 >= 1 by A2,INT_1:52,POWER:35;
then
A5: SDSub_Add_Carry(x,k) <= Radix(k-'1) - 1 by A1,XXREAL_0:2;
SDSub_Add_Carry(x,k) is Element of INT by INT_1:def 2;
hence thesis by A5,A4;
end;
theorem Th15:
2 <= k & i1 in k-SD implies SDSub_Add_Data(i1,k) +
SDSub_Add_Carry(i2,k) in k-SD_Sub
proof
A1: SDSub_Add_Carry(i2,k) >= -1 by Th12;
assume
A2: 2 <= k & i1 in k-SD;
then SDSub_Add_Data(i1,k) >= -Radix(k-'1) by Th13;
then
A3: SDSub_Add_Data(i1,k) + SDSub_Add_Carry(i2,k) >= -Radix(k-'1) + - 1 by A1,
XREAL_1:7;
A4: SDSub_Add_Carry(i2,k) <= 1 by Th12;
SDSub_Add_Data(i1,k) <= Radix(k-'1) - 1 by A2,Th13;
then
A5: SDSub_Add_Data(i1,k) + SDSub_Add_Carry(i2,k) <= Radix(k-'1) - 1 + 1 by A4,
XREAL_1:7;
SDSub_Add_Data(i1,k) + SDSub_Add_Carry(i2,k) is Element of INT by INT_1:def 2
;
hence thesis by A3,A5;
end;
theorem Th16:
SDSub_Add_Carry(0,k) = 0
proof
set x = 0;
Radix(k -' 1) <> x & -Radix(k-'1) <= 0 - 0 by POWER:34;
hence thesis by Def3;
end;
begin :: Definition for translation from Radix-2^k SD number
definition
let i,k,n be Nat, x be Tuple of n,(k-SD_Sub);
func DigA_SDSub(x,i) -> Integer equals
:Def5:
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 SD2SDSubDigit(x,i,k) -> Integer equals
:Def6:
SDSub_Add_Data(DigA(x,i),
k)+SDSub_Add_Carry(DigA(x,i-'1),k) if i in Seg n, SDSub_Add_Carry(DigA(x,i-'1),
k) if i = n + 1 otherwise 0;
coherence;
consistency
proof
i in Seg n implies not i = n + 1
proof
assume i in Seg n;
then
A1: i <= n by FINSEQ_1:1;
assume i = n + 1;
hence contradiction by A1,NAT_1:13;
end;
hence thesis;
end;
end;
theorem Th17:
2 <= k & i in Seg (n+1) implies SD2SDSubDigit(a,i,k) is Element of k-SD_Sub
proof
assume that
A1: 2 <= k and
A2: i in Seg (n+1);
set SDD = SDSub_Add_Data(DigA(a,i), k) + SDSub_Add_Carry(DigA(a,i-'1), k);
set SDC = SDSub_Add_Carry(DigA(a,i-'1), k);
now
per cases by A2,FINSEQ_2:7;
suppose
A3: i in Seg n;
SDD in k-SD_Sub
proof
DigA(a,i) is Element of k-SD by A3,RADIX_1:16;
hence thesis by A1,Th15;
end;
hence SD2SDSubDigit(a,i,k) in k-SD_Sub by A3,Def6;
end;
suppose
A4: i = n + 1;
SDSub_Add_Carry(DigA(a,i-'1),k) in k-SD_Sub_S & k-SD_Sub_S c= k
-SD_Sub by A1,Th2,Th14;
then SDC in k-SD_Sub;
hence SD2SDSubDigit(a,i,k) in k-SD_Sub by A4,Def6;
end;
end;
hence thesis;
end;
definition
let i,k,n be Nat, x be Tuple of n,(k-SD);
assume
A1: 2 <= k & i in Seg (n+1);
func SD2SDSubDigitS(x,i,k) -> Element of k-SD_Sub equals
:Def7:
SD2SDSubDigit(x,i,k);
coherence by A1,Th17;
end;
definition
let n,k be Nat, x be Tuple of n,(k-SD);
func SD2SDSub(x) -> Tuple of (n+1),(k-SD_Sub) means
:Def8:
for i be Nat st i
in Seg (n+1) holds DigA_SDSub(it,i) = SD2SDSubDigitS(x,i,k);
existence
proof
deffunc F(Nat)= SD2SDSubDigitS(x,$1,k);
consider z being FinSequence of k-SD_Sub such that
A1: len z = (n+1) 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+1) by A1,FINSEQ_1:def 3;
z is Element of (n+1)-tuples_on (k-SD_Sub) by A1,FINSEQ_2:92;
then reconsider z as Tuple of n+1, k-SD_Sub;
take z;
let i;
assume
A4: i in Seg (n+1);
hence DigA_SDSub(z,i) = z.i by Def5
.= SD2SDSubDigitS(x,i,k) by A2,A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of (n+1),(k-SD_Sub) such that
A5: for i be Nat st i in Seg (n+1) holds DigA_SDSub(k1,i) =
SD2SDSubDigitS(x,i,k) and
A6: for i be Nat st i in Seg (n+1) holds DigA_SDSub(k2,i) =
SD2SDSubDigitS(x,i,k);
A7: len k1 = n+1 by CARD_1:def 7;
then
A8: dom k1 = Seg(n+1) 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,Def5
.= SD2SDSubDigitS(x,j,k) by A5,A8,A10
.= DigA_SDSub(k2,j) by A6,A8,A10
.= k2.j by A8,A10,Def5;
hence k1.j = k2.j;
end;
len k2 = n+1 by CARD_1:def 7;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
theorem
i in Seg n implies DigA_SDSub(aSub,i) is Element of k-SD_Sub
proof
assume
A1: i in Seg n;
then aSub.i = DigA_SDSub(aSub,i) by Def5;
hence thesis by A1,Th11;
end;
theorem
2 <= k & i1 in k-SD & i2 in k-SD_Sub implies SDSub_Add_Data(i1+i2,k)
in k-SD_Sub_S
proof
assume that
A1: 2 <= k and
A2: i1 in k-SD & i2 in k-SD_Sub;
set z = i1+i2;
i1 <= Radix(k) - 1 & i2 <= Radix(k-'1) by A2,Th1,RADIX_1:13;
then
A3: z <= Radix(k) - 1 + Radix(k-'1) by XREAL_1:7;
-Radix(k) + 1 <= i1 & -Radix(k-'1) - 1 <= i2 by A2,Th1,RADIX_1:13;
then
A4: -Radix(k) + 1 + ( -Radix(k-'1) - 1 ) <= z by XREAL_1:7;
A5: SDSub_Add_Data(z,k) >= -Radix(k-'1) & SDSub_Add_Data(z,k) <= Radix(k-'1)
- 1
proof
now
per cases;
case
A6: z < -Radix(k -' 1);
then z + 1 <= -Radix(k-'1) by INT_1:7;
then z <= -Radix(k-'1) - 1 by XREAL_1:19;
then z <= -Radix(k-'1) + -1;
then z <= -Radix(k) + Radix(k-'1) + -1 by A1,Lm3,XXREAL_0:2;
then
A7: z <= -Radix(k) + (Radix(k-'1) + -1);
-Radix(k-'1) + -Radix(k) <= z + 0 by A4;
then
A8: -Radix(k-'1) - 0 <= z - (-Radix(k)) by XREAL_1:21;
SDSub_Add_Carry(z,k) = -1 by A6,Def3;
hence thesis by A8,A7,XREAL_1:20;
end;
case
A9: -Radix(k -' 1) <= z & z < Radix(k -' 1);
then SDSub_Add_Carry(z,k) = 0 & z + 1 <= Radix(k -' 1) by Def3,INT_1:7;
hence thesis by A9,XREAL_1:19;
end;
case
A10: Radix(k -' 1) <= z;
then Radix(k) - Radix(k-'1) <= z by A1,Lm2,XXREAL_0:2;
then
A11: Radix(k) + -Radix(k-'1) <= z;
A12: z <= Radix(k) + (Radix(k-'1) - 1) by A3;
SDSub_Add_Carry(z,k) = 1 by A10,Def3;
hence thesis by A11,A12,XREAL_1:19,20;
end;
end;
hence thesis;
end;
SDSub_Add_Data(z,k) is Element of INT by INT_1:def 2;
hence thesis by A5;
end;
begin :: Definiton for Translation from Radix-2^k SD_Sub number to INT
definition
let i,k,n be Nat, x be Tuple of n,(k-SD_Sub);
func DigB_SDSub(x,i) -> Element of INT equals
DigA_SDSub(x,i);
coherence by INT_1:def 2;
end;
definition
let i,k,n be Nat, x be Tuple of n, k-SD_Sub;
func SDSub2INTDigit(x,i,k) -> Element of INT equals
(Radix(k) |^ (i -'1)) *
DigB_SDSub(x,i);
coherence by INT_1:def 2;
end;
definition
let n,k be Nat, x be Tuple of n, k-SD_Sub;
func SDSub2INT(x) -> Tuple of n,INT means
:Def11:
for i be Nat st i in Seg n holds it/.i = SDSub2INTDigit(x,i,k);
existence
proof
deffunc F(Nat)=SDSub2INTDigit(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;
z is Element of n-tuples_on INT by A1,FINSEQ_2:92;
then reconsider z as Tuple of n, INT;
take z;
let i;
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
.= SDSub2INTDigit(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 = SDSub2INTDigit(x,i,k) and
A6: for i be Nat st i in Seg n holds k2/.i = SDSub2INTDigit(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
.= SDSub2INTDigit(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_Sub);
func SDSub2IntOut(x) -> Integer equals
Sum SDSub2INT(x);
coherence;
end;
theorem Th20:
for i st i in Seg n holds 2 <= k implies DigA_SDSub(SD2SDSub(
DecSD(m,n+1,k)),i) = DigA_SDSub(SD2SDSub(DecSD((m mod (Radix(k) |^ n)),n,k)),i)
proof
let i;
assume
A1: i in Seg n;
reconsider i as Element of NAT by ORDINAL1:def 12;
A2: 1 <= i by A1,FINSEQ_1:1;
i <= n by A1,FINSEQ_1:1;
then
A3: i <= n+1 by NAT_1:12;
then
A4: i in Seg (n+1) by A2,FINSEQ_1:1;
i <= (n+1)+1 by A3,NAT_1:12;
then
A5: i in Seg ((n+1)+1) by A2,FINSEQ_1:1;
set M = m mod (Radix(k) |^ n);
assume
A6: 2 <= k;
A7: DigA_SDSub(SD2SDSub(DecSD(M,n,k)),i) = SD2SDSubDigitS(DecSD(M,n,k),i,k)
by A4,Def8
.= SD2SDSubDigit(DecSD(M,n,k),i,k) by A6,A4,Def7
.= SDSub_Add_Data(DigA(DecSD(M,n,k),i),k) + SDSub_Add_Carry(DigA(DecSD(M
,n,k),i-'1),k) by A1,Def6
.= SDSub_Add_Data(DigA(DecSD(m,n+1,k),i),k) + SDSub_Add_Carry(DigA(DecSD
(M,n,k),i-'1),k) by A1,Lm5;
now
per cases;
suppose
A8: i = 1;
then
A9: DigA_SDSub(SD2SDSub(DecSD(M,n,k)),i) = SDSub_Add_Data(DigA(DecSD(m,
n+1,k),i),k) + SDSub_Add_Carry(DigA(DecSD(M,n,k),0),k) by A7,XREAL_1:232
.= SDSub_Add_Data(DigA(DecSD(m,n+1,k),i),k) + SDSub_Add_Carry(0,k)
by RADIX_1:def 3
.= SDSub_Add_Data(DigA(DecSD(m,n+1,k),i),k) + 0 by Th16;
DigA_SDSub(SD2SDSub(DecSD(m,n+1,k)),i) = SD2SDSubDigitS(DecSD(m,n+1
,k),i,k) by A5,Def8
.= SD2SDSubDigit(DecSD(m,n+1,k),i,k) by A6,A5,Def7
.= SDSub_Add_Data(DigA(DecSD(m,n+1,k),i),k) + SDSub_Add_Carry(DigA(
DecSD(m,n+1,k),i-'1),k) by A4,Def6
.= SDSub_Add_Data(DigA(DecSD(m,n+1,k),i),k) + SDSub_Add_Carry(DigA(
DecSD(m,n+1,k),0),k) by A8,XREAL_1:232
.= SDSub_Add_Data(DigA(DecSD(m,n+1,k),i),k) + SDSub_Add_Carry(0,k)
by RADIX_1:def 3
.= SDSub_Add_Data(DigA(DecSD(m,n+1,k),i),k) + 0 by Th16;
hence thesis by A9;
end;
suppose
A10: i <> 1;
i <= n by A1,FINSEQ_1:1;
then
A11: i -' 1 <= n by NAT_D:44;
1 < i by A2,A10,XXREAL_0:1;
then 0 + 1 <= i-'1 by INT_1:7,JORDAN12:1;
then i -' 1 in Seg n by A11,FINSEQ_1:1;
then
DigA_SDSub(SD2SDSub(DecSD(M,n,k)),i) = SDSub_Add_Data(DigA(DecSD(m,
n+1,k),i),k) + SDSub_Add_Carry(DigA(DecSD(m,n+1,k),i-'1),k) by A7,Lm5
.= SD2SDSubDigit(DecSD(m,n+1,k),i,k) by A4,Def6
.= SD2SDSubDigitS(DecSD(m,n+1,k),i,k) by A6,A5,Def7
.= DigA_SDSub(SD2SDSub(DecSD(m,n+1,k)),i) by A5,Def8;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for n st n >= 1 holds for k,x st k >= 2 & x is_represented_by n,k
holds x = SDSub2IntOut( SD2SDSub(DecSD(x,n,k)) )
proof
defpred P[Nat] means for k,x be Nat st k >= 2 & x is_represented_by $1,k
holds x = SDSub2IntOut( SD2SDSub(DecSD(x,$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];
A5: n in Seg n by A3,FINSEQ_1:3;
let k,x be Nat;
assume that
A6: k >= 2 and
A7: x is_represented_by (n+1),k;
reconsider k as Element of NAT by ORDINAL1:def 12;
set xn = x mod (Radix(k) |^ n);
set RN1 = Radix(k) |^ (n+1);
set RN = Radix(k) |^ n;
A8: (n+1+1) in Seg (n+1+1) by FINSEQ_1:3;
A9: SDSub2INTDigit(SD2SDSub(DecSD(x,n+1,k)),n+1+1,k) = RN1 * DigB_SDSub(
SD2SDSub(DecSD(x,n+1,k)),n+1+1) by NAT_D:34
.= RN1 * SD2SDSubDigitS(DecSD(x,n+1,k),n+1+1,k) by A8,Def8
.= RN1 * SD2SDSubDigit(DecSD(x,n+1,k),n+1+1,k) by A6,A8,Def7
.= RN1 * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1+1-'1),k) by Def6
.= RN1 * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k) by NAT_D:34;
set XN = SD2SDSub(DecSD(xn,n,k));
set X = SD2SDSub(DecSD(x,n+1,k));
deffunc Q(Nat) = SDSub2INTDigit(X,$1,k);
consider xp being FinSequence of INT such that
A10: len xp = n+1 and
A11: for i be Nat st i in dom xp holds xp.i = Q(i) from FINSEQ_2:sch 1;
A12: dom xp = Seg(n+1) by A10,FINSEQ_1:def 3;
A13: len SDSub2INT(X) = n+1+1 by CARD_1:def 7;
A14: for j be Nat st 1 <= j & j <= len SDSub2INT(X) holds SDSub2INT(X).j =
(xp^<* SDSub2INTDigit(X,n+1+1,k) *>).j
proof
let j be Nat;
assume that
A15: 1 <= j and
A16: j <= len SDSub2INT(X);
j <= n+1+1 by A16,CARD_1:def 7;
then
A17: j in Seg (n+1+1) by A15,FINSEQ_1:1;
A18: j in dom SDSub2INT(X) by A15,A16,FINSEQ_3:25;
now
per cases by A17,FINSEQ_2:7;
suppose
A19: j in Seg (n+1);
then j in dom xp by A10,FINSEQ_1:def 3;
then (xp^<*SDSub2INTDigit(X,n+1+1,k)*>).j = xp.j by FINSEQ_1:def 7
.= SDSub2INTDigit(X,j,k) by A11,A12,A19
.= (SDSub2INT(X))/.j by A17,Def11
.= SDSub2INT(X).j by A18,PARTFUN1:def 6;
hence thesis;
end;
suppose
A20: j = (n+1)+1;
A21: j in dom SDSub2INT(X) by A13,A17,FINSEQ_1:def 3;
(xp^<*SDSub2INTDigit(X,n+1+1,k)*>).j = SDSub2INTDigit(X,n+1+1,k
) by A10,A20,FINSEQ_1:42
.= (SDSub2INT(X))/.(n+1+1) by A17,A20,Def11
.= SDSub2INT(X).j by A20,A21,PARTFUN1:def 6;
hence thesis;
end;
end;
hence thesis;
end;
Radix(k) > 0 by RADIX_2:6;
then xn < Radix(k) |^ n by NAT_D:1,PREPOWER:6;
then xn is_represented_by n,k;
then
A22: xn = SDSub2IntOut( SD2SDSub(DecSD(xn,n,k)) ) by A4,A6
.= Sum SDSub2INT( SD2SDSub(DecSD(xn,n,k)) );
A23: n+1 in Seg (n+1) by FINSEQ_1:3;
then
A24: (n+1) in Seg (n+1+1) by FINSEQ_2:8;
consider xpp being FinSequence of INT such that
A25: len xpp = n and
A26: for i be Nat st i in dom xpp holds xpp.i = Q(i) from FINSEQ_2:sch
1;
A27: dom xpp = Seg n by A25,FINSEQ_1:def 3;
A28: for j be Nat st 1 <= j & j <= len xp holds xp.j = (xpp^<*
SDSub2INTDigit(X,n+1,k) *>).j
proof
let j be Nat;
assume 1 <= j & j <= len xp;
then
A29: j in Seg (n+1) by A10,FINSEQ_1:1;
now
per cases by A29,FINSEQ_2:7;
suppose
A30: j in Seg n;
then j in dom xpp by A25,FINSEQ_1:def 3;
then (xpp^<*SDSub2INTDigit(X,n+1,k)*>).j = xpp.j by FINSEQ_1:def 7
.= SDSub2INTDigit(X,j,k) by A26,A27,A30
.= xp.j by A11,A12,A29;
hence thesis;
end;
suppose
A31: j = n+1;
then (xpp^<*SDSub2INTDigit(X,n+1,k)*>).j = SDSub2INTDigit(X,n+1,k)
by A25,FINSEQ_1:42
.= xp.j by A11,A12,A29,A31;
hence thesis;
end;
end;
hence thesis;
end;
deffunc G(Nat) = SDSub2INTDigit(XN,$1,k);
consider xnpp being FinSequence of INT such that
A32: len xnpp = n and
A33: for i be Nat st i in dom xnpp holds xnpp.i = G(i) from FINSEQ_2:
sch 1;
A34: dom xnpp = Seg n by A32,FINSEQ_1:def 3;
for j be Nat st 1 <= j & j <= len xnpp holds xnpp.j = xpp.j
proof
let j be Nat;
assume 1 <= j & j <= len xnpp;
then
A35: j in Seg n by A32,FINSEQ_1:1;
then xpp.j = SDSub2INTDigit(X,j,k) by A26,A27
.= SDSub2INTDigit(XN,j,k) by A6,A35,Th20
.= xnpp.j by A33,A34,A35;
hence thesis;
end;
then
A36: xpp = xnpp by A25,A32,FINSEQ_1:14;
A37: len SDSub2INT(XN) = n+1 by CARD_1:def 7;
A38: for j be Nat st 1 <= j & j <= len SDSub2INT(XN) holds SDSub2INT(XN).j
= (xnpp^<* SDSub2INTDigit(XN,n+1,k) *>).j
proof
let j be Nat;
assume
A39: 1 <= j & j <= len SDSub2INT(XN);
then
A40: j in Seg (n+1) by A37,FINSEQ_1:1;
A41: j in dom SDSub2INT(XN) by A39,FINSEQ_3:25;
now
per cases by A40,FINSEQ_2:7;
suppose
A42: j in Seg n;
then j in dom xnpp by A32,FINSEQ_1:def 3;
then (xnpp^<*SDSub2INTDigit(XN,n+1,k)*>).j = xnpp.j by FINSEQ_1:def 7
.= SDSub2INTDigit(XN,j,k) by A33,A34,A42
.= (SDSub2INT(XN))/.j by A40,Def11
.= SDSub2INT(XN).j by A41,PARTFUN1:def 6;
hence thesis;
end;
suppose
A43: j = n+1;
A44: j in dom SDSub2INT(XN) by A37,A40,FINSEQ_1:def 3;
(xnpp^<*SDSub2INTDigit(XN,n+1,k)*>).j = SDSub2INTDigit(XN,n+1,k
) by A32,A43,FINSEQ_1:42
.= (SDSub2INT(XN))/.(n+1) by A40,A43,Def11
.= SDSub2INT(XN).j by A43,A44,PARTFUN1:def 6;
hence thesis;
end;
end;
hence thesis;
end;
len xp = len (xpp^<*SDSub2INTDigit(X,n+1,k)*>) by A10,A25,FINSEQ_2:16;
then
A45: xp = xpp^<* SDSub2INTDigit(X,(n+1),k) *> by A28,FINSEQ_1:14;
len (xp^<*SDSub2INTDigit(X,n+1+1,k)*>) = n+1+1 by A10,FINSEQ_2:16;
then len SDSub2INT(X) = len (xp^<*SDSub2INTDigit(X,n+1+1,k)*>) by
CARD_1:def 7;
then SDSub2INT(X) = xp^<* SDSub2INTDigit(X,(n+1)+1,k) *> by A14,FINSEQ_1:14
;
then
A46: Sum SDSub2INT(X) = Sum (xp) + SDSub2INTDigit(X,(n+1)+1,k) by RVSUM_1:74
.= Sum (xnpp) + SDSub2INTDigit(X,(n+1),k) + SDSub2INTDigit(X,(n+1)+1,k
) by A45,A36,RVSUM_1:74;
set RNDIG = RN*DigA(DecSD(x,n+1,k),n+1);
set RNSDC = RN*(SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k));
A47: Radix(k) > 0 by RADIX_2:6;
len (xnpp^<*SDSub2INTDigit(XN,n+1,k)*>) = n+1 by A32,FINSEQ_2:16;
then SDSub2INT(XN) = xnpp^<* SDSub2INTDigit(XN,n+1,k) *> by A37,A38,
FINSEQ_1:14;
then
A48: xn + 0 = Sum (xnpp) + SDSub2INTDigit(XN,n+1,k) by A22,RVSUM_1:74;
A49: SDSub2INTDigit(SD2SDSub(DecSD(x,n+1,k)),n+1,k) = (Radix(k) |^ (n))*
DigB_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1) by NAT_D:34
.= RN * SD2SDSubDigitS(DecSD(x,n+1,k),n+1,k) by A24,Def8
.= RN * SD2SDSubDigit(DecSD(x,n+1,k),n+1,k) by A6,A24,Def7
.= RN*( 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 A23,Def6
.= RN*( 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
.= RN * DigA(DecSD(x,n+1,k),n+1) - (RN * Radix(k)) * SDSub_Add_Carry(
DigA(DecSD(x,n+1,k),n+1),k) + RN * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k)
.= RN * DigA(DecSD(x,n+1,k),n+1) - RN1 * SDSub_Add_Carry(DigA(DecSD(x,
n+1,k),n+1),k) + RN * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) by NEWTON:6;
SDSub2INTDigit(SD2SDSub(DecSD(xn,n,k)),n+1,k) = (Radix(k) |^ (n))*
DigB_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1) by NAT_D:34
.= RN * SD2SDSubDigitS(DecSD(xn,n,k),n+1,k) by A23,Def8
.= RN * SD2SDSubDigit(DecSD(xn,n,k),n+1,k) by A23,A6,Def7
.= RN*(SDSub_Add_Carry(DigA(DecSD(xn,n,k),n+1-'1),k)) by Def6
.= RN*(SDSub_Add_Carry(DigA(DecSD(xn,n,k),n),k)) by NAT_D:34
.= RN*(SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k)) by A5,Lm5;
then Sum SDSub2INT(X) = xn + RNDIG - RNSDC + RNSDC by A46,A48,A49,A9
.= xn + RN * ( x div RN ) by A7,RADIX_1:24;
hence thesis by A47,NAT_D:2,PREPOWER:6;
end;
A50: P[1]
proof
A51: 1 in Seg 1 by FINSEQ_1:1;
2 - 1 = 1;
then
A52: 2 -' 1 = 1 by XREAL_0:def 2;
let k,x be Nat;
assume that
A53: k >= 2 and
A54: x is_represented_by 1,k;
set X = DecSD(x,1,k);
reconsider CRY = Radix(k) * SDSub_Add_Carry(DigA(X,1),k) as Integer;
reconsider DIG2 = CRY as Element of INT by INT_1:def 2;
reconsider DIG1 = DigA(X,1) - CRY as Element of INT by INT_1:def 2;
A55: 1 in Seg (1+1) by FINSEQ_1:1;
A56: len(SDSub2INT(SD2SDSub(X))) = 1 + 1 by CARD_1:def 7;
then
A57: 1 in dom SDSub2INT(SD2SDSub(X)) by A55,FINSEQ_1:def 3;
A58: 2 in Seg (1+1) by FINSEQ_1:1;
then
A59: 2 in dom SDSub2INT(SD2SDSub(X)) by A56,FINSEQ_1:def 3;
(SDSub2INT(SD2SDSub(X)))/.2 = SDSub2INTDigit(SD2SDSub(X),2,k) by A58,Def11
.= Radix(k)*DigB_SDSub(SD2SDSub(X),2) by A52
.= Radix(k)*SD2SDSubDigitS(X,2,k) by A58,Def8
.= Radix(k)*SD2SDSubDigit(X,2,k) by A53,A58,Def7
.= Radix(k) * SDSub_Add_Carry(DigA(X,1),k) by A52,A58,Def6;
then
A60: SDSub2INT(SD2SDSub(X)).2 = CRY by A59,PARTFUN1:def 6;
(SDSub2INT(SD2SDSub(X)))/.1 = SDSub2INTDigit(SD2SDSub(X),1,k) by A55,Def11
.= (Radix(k) |^ 0)*DigB_SDSub(SD2SDSub(X),1) by XREAL_1:232
.= 1 * DigB_SDSub(SD2SDSub(X),1) by NEWTON:4
.= SD2SDSubDigitS(X,1,k) by A55,Def8
.= SD2SDSubDigit(X,1,k) by A53,A55,Def7
.= SDSub_Add_Data(DigA(X,1),k) + SDSub_Add_Carry(DigA(X,1-'1),k) by A51
,Def6
.= SDSub_Add_Data(DigA(X,1),k) + SDSub_Add_Carry(DigA(X,0),k) by
XREAL_1:232
.= SDSub_Add_Data(DigA(X,1),k) + SDSub_Add_Carry(0,k) by RADIX_1:def 3
.= SDSub_Add_Data(DigA(X,1),k) + 0 by Th16
.= DigA(X,1) - Radix(k) * SDSub_Add_Carry(DigA(X,1),k);
then SDSub2INT(SD2SDSub(X)).1 = DigA(X,1) - CRY by A57,PARTFUN1:def 6;
then SDSub2INT(SD2SDSub(X)) = <* DIG1, DIG2 *> by A56,A60,FINSEQ_1:44;
then Sum(SDSub2INT(SD2SDSub(X))) = DIG1 + DIG2 by RVSUM_1:77
.= x by A54,RADIX_1:21;
hence thesis;
end;
for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8(A50,A2);
hence thesis by A1;
end;