:: Definitions of Radix-2k Signed-Digit number and its adder algorithm
:: by Yoshinori Fujisawa and Yasushi Fuwa
::
:: Received September 7, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem Th1: :: RADIX_1:1

for k, n being Nat st n mod k = k - 1 holds
(n + 1) mod k = 0 by NAT_D:69;

theorem Th2: :: RADIX_1:2

for k, n being Nat st n mod k < k - 1 holds
(n + 1) mod k = (n mod k) + 1 by NAT_D:70;

theorem Th3: :: RADIX_1:3

for k, m, n being Nat st m <> 0 holds
(k mod (m * n)) mod n = k mod n

proof end;

theorem :: RADIX_1:4

for k, n being Nat holds
( not k <> 0 or (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )

proof end;

theorem Th5: :: RADIX_1:5

for i, k, n being Nat st i <> 0 & k <> 0 holds
(n mod (i |^ k)) div (i |^ (k -' 1)) < i

proof end;

theorem :: RADIX_1:6

canceled;

::$CT

theorem :: RADIX_1:7

for i1, i2, i3 being Integer st i2 > 0 & i3 >= 0 holds
(i1 mod (i2 * i3)) mod i3 = i1 mod i3

proof end;

definition

let n be Nat;

func Radix n -> Element of NAT equals :: RADIX_1:def 1
2 to_power n;

correctness
coherence
2 to_power n is Element of NAT ;
by ORDINAL1:def 12;

end;

:: deftheorem defines Radix RADIX_1:def 1 :
for n being Nat holds Radix n = 2 to_power n;

definition

let k be Nat;

func k -SD -> set equals :: RADIX_1:def 2
{ e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } ;

correctness
coherence
{ e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } is set ;
;

end;

:: deftheorem defines -SD RADIX_1:def 2 :
for k being Nat holds k -SD = { e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } ;

Lm1: for k being Nat st k >= 2 holds
Radix k >= 2 + 2

proof end;

theorem Th7: :: RADIX_1:8

for e being object holds
( e in 0 -SD iff e = 0 )

proof end;

theorem :: RADIX_1:9

0 -SD = {0} by Th7, TARSKI:def 1;

theorem Th9: :: RADIX_1:10

for k being Nat holds k -SD c= (k + 1) -SD

proof end;

theorem Th10: :: RADIX_1:11

for e being set
for k being Nat st e in k -SD holds
e is Integer

proof end;

theorem Th11: :: RADIX_1:12

for k being Nat holds k -SD c= INT

proof end;

theorem Th12: :: RADIX_1:13

for i1 being Integer
for k being Nat st i1 in k -SD holds
( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 )

proof end;

theorem Th13: :: RADIX_1:14

for k being Nat holds 0 in k -SD

proof end;

registration

let k be Nat;

cluster k -SD -> non empty ;

coherence
not k -SD is empty by Th13;

end;

definition

let k be Nat;
:: original: -SD
redefine func k -SD -> non empty Subset of INT;
coherence
k -SD is non empty Subset of INT by Th11;

end;

theorem Th14: :: RADIX_1:15

for i, k, n being Nat
for a being Tuple of n,k -SD st i in Seg n holds
a . i is Element of k -SD

proof end;

definition

let i, k, n be Nat;
let x be Tuple of n,k -SD ;

func DigA (x,i) -> Integer equals :Def3: :: RADIX_1:def 3
x . i if i in Seg n
0 if i = 0
;

coherence
( ( i in Seg n implies x . i is Integer ) & ( i = 0 implies 0 is Integer ) ) by INT_1:def 2;
consistency
for b₁ being Integer st i in Seg n & i = 0 holds
( b₁ = x . i iff b₁ = 0 ) by FINSEQ_1:1;

end;

:: deftheorem Def3 defines DigA RADIX_1:def 3 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds
( ( i in Seg n implies DigA (x,i) = x . i ) & ( i = 0 implies DigA (x,i) = 0 ) );

definition

let i, k, n be Nat;
let x be Tuple of n,k -SD ;

func DigB (x,i) -> Element of INT equals :: RADIX_1:def 4
DigA (x,i);

coherence
DigA (x,i) is Element of INT by INT_1:def 2;

end;

:: deftheorem defines DigB RADIX_1:def 4 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds DigB (x,i) = DigA (x,i);

theorem Th15: :: RADIX_1:16

for i, k, n being Nat
for a being Tuple of n,k -SD st i in Seg n holds
DigA (a,i) is Element of k -SD

proof end;

theorem Th16: :: RADIX_1:17

for m being Nat
for x being Tuple of 1, INT st x /. 1 = m holds
x = <*m*>

proof end;

definition

let i, k, n be Nat;
let x be Tuple of n,k -SD ;

func SubDigit (x,i,k) -> Element of INT equals :: RADIX_1:def 5
((Radix k) |^ (i -' 1)) * (DigB (x,i));

coherence
((Radix k) |^ (i -' 1)) * (DigB (x,i)) is Element of INT by INT_1:def 2;

end;

:: deftheorem defines SubDigit RADIX_1:def 5 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds SubDigit (x,i,k) = ((Radix k) |^ (i -' 1)) * (DigB (x,i));

definition

let n, k be Nat;
let x be Tuple of n,k -SD ;

func DigitSD x -> Tuple of n, INT means :Def6: :: RADIX_1:def 6
for i being Nat st i in Seg n holds
it /. i = SubDigit (x,i,k);

existence
ex b₁ being Tuple of n, INT st
for i being Nat st i in Seg n holds
b₁ /. i = SubDigit (x,i,k)

proof end;

uniqueness
for b₁, b₂ being Tuple of n, INT st ( for i being Nat st i in Seg n holds
b₁ /. i = SubDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds
b₂ /. i = SubDigit (x,i,k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines DigitSD RADIX_1:def 6 :
for n, k being Nat
for x being Tuple of n,k -SD
for b₄ being Tuple of n, INT holds
( b₄ = DigitSD x iff for i being Nat st i in Seg n holds
b₄ /. i = SubDigit (x,i,k) );

definition

let n, k be Nat;
let x be Tuple of n,k -SD ;

func SDDec x -> Integer equals :: RADIX_1:def 7
Sum (DigitSD x);

coherence
Sum (DigitSD x) is Integer ;

end;

:: deftheorem defines SDDec RADIX_1:def 7 :
for n, k being Nat
for x being Tuple of n,k -SD holds SDDec x = Sum (DigitSD x);

definition

let i, k, x be Nat;

func DigitDC (x,i,k) -> Element of k -SD equals :: RADIX_1:def 8
(x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));

coherence
(x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) is Element of k -SD

proof end;

end;

:: deftheorem defines DigitDC RADIX_1:def 8 :
for i, k, x being Nat holds DigitDC (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));

definition

let k, n, x be Nat;

func DecSD (x,n,k) -> Tuple of n,k -SD means :Def9: :: RADIX_1:def 9
for i being Nat st i in Seg n holds
DigA (it,i) = DigitDC (x,i,k);

existence
ex b₁ being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA (b₁,i) = DigitDC (x,i,k)

proof end;

uniqueness
for b₁, b₂ being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b₁,i) = DigitDC (x,i,k) ) & ( for i being Nat st i in Seg n holds
DigA (b₂,i) = DigitDC (x,i,k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines DecSD RADIX_1:def 9 :
for k, n, x being Nat
for b₄ being Tuple of n,k -SD holds
( b₄ = DecSD (x,n,k) iff for i being Nat st i in Seg n holds
DigA (b₄,i) = DigitDC (x,i,k) );

definition

let x be Integer;

func SD_Add_Carry x -> Integer equals :Def10: :: RADIX_1:def 10
1 if x > 2
- 1 if x < - 2
otherwise 0 ;

coherence
( ( x > 2 implies 1 is Integer ) & ( x < - 2 implies - 1 is Integer ) & ( not x > 2 & not x < - 2 implies 0 is Integer ) ) ;
consistency
for b₁ being Integer st x > 2 & x < - 2 holds
( b₁ = 1 iff b₁ = - 1 ) ;

end;

:: deftheorem Def10 defines SD_Add_Carry RADIX_1:def 10 :
for x being Integer holds
( ( x > 2 implies SD_Add_Carry x = 1 ) & ( x < - 2 implies SD_Add_Carry x = - 1 ) & ( not x > 2 & not x < - 2 implies SD_Add_Carry x = 0 ) );

theorem Th17: :: RADIX_1:18

SD_Add_Carry 0 = 0 by Def10;

Lm2: for x being Integer holds
( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )

proof end;

definition

let x be Integer;
let k be Nat;

func SD_Add_Data (x,k) -> Integer equals :: RADIX_1:def 11
x - ((SD_Add_Carry x) * (Radix k));

coherence
x - ((SD_Add_Carry x) * (Radix k)) is Integer ;

end;

:: deftheorem defines SD_Add_Data RADIX_1:def 11 :
for x being Integer
for k being Nat holds SD_Add_Data (x,k) = x - ((SD_Add_Carry x) * (Radix k));

theorem :: RADIX_1:19

for k being Nat holds SD_Add_Data (0,k) = 0 by Th17;

theorem Th19: :: RADIX_1:20

for i1, i2 being Integer
for k being Nat st k >= 2 & i1 in k -SD & i2 in k -SD holds
( (- (Radix k)) + 2 <= SD_Add_Data ((i1 + i2),k) & SD_Add_Data ((i1 + i2),k) <= (Radix k) - 2 )

proof end;

:: expressed as n digits Radix-2^k SD number

definition

let n, x, k be Nat;

pred x is_represented_by n,k means :: RADIX_1:def 12
x < (Radix k) |^ n;

end;

:: deftheorem defines is_represented_by RADIX_1:def 12 :
for n, x, k being Nat holds
( x is_represented_by n,k iff x < (Radix k) |^ n );

theorem Th20: :: RADIX_1:21

for k, m being Nat st m is_represented_by 1,k holds
DigA ((DecSD (m,1,k)),1) = m

proof end;

theorem :: RADIX_1:22

for k, n being Nat st n >= 1 holds
for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD (m,n,k))

proof end;

theorem Th22: :: RADIX_1:23

for k, m, n being Nat st m is_represented_by 1,k & n is_represented_by 1,k holds
SD_Add_Carry ((DigA ((DecSD (m,1,k)),1)) + (DigA ((DecSD (n,1,k)),1))) = SD_Add_Carry (m + n)

proof end;

Lm3: for k, m, n, i being Nat st i in Seg n holds
DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i)

proof end;

theorem Th23: :: RADIX_1:24

for k, m, n being Nat st m is_represented_by n + 1,k holds
DigA ((DecSD (m,(n + 1),k)),(n + 1)) = m div ((Radix k) |^ n)

proof end;

:: on Radix-2^k SD number

definition

let k, i, n be Nat;
let 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: :: RADIX_1:def 13
(SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1)))));

coherence
(SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1))))) is Element of k -SD

proof end;

end;

:: deftheorem Def13 defines Add RADIX_1:def 13 :
for k, i, n being Nat
for x, y being Tuple of n,k -SD st i in Seg n & k >= 2 holds
Add (x,y,i,k) = (SD_Add_Data (((DigA (x,i)) + (DigA (y,i))),k)) + (SD_Add_Carry ((DigA (x,(i -' 1))) + (DigA (y,(i -' 1)))));

definition

let n, k be Nat;
let x, y be Tuple of n,k -SD ;

func x '+' y -> Tuple of n,k -SD means :Def14: :: RADIX_1:def 14
for i being Nat st i in Seg n holds
DigA (it,i) = Add (x,y,i,k);

existence
ex b₁ being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA (b₁,i) = Add (x,y,i,k)

proof end;

uniqueness
for b₁, b₂ being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b₁,i) = Add (x,y,i,k) ) & ( for i being Nat st i in Seg n holds
DigA (b₂,i) = Add (x,y,i,k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines '+' RADIX_1:def 14 :
for n, k being Nat
for x, y, b₅ being Tuple of n,k -SD holds
( b₅ = x '+' y iff for i being Nat st i in Seg n holds
DigA (b₅,i) = Add (x,y,i,k) );

theorem Th24: :: RADIX_1:25

for k, m, n being Nat st k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k holds
SDDec ((DecSD (m,1,k)) '+' (DecSD (n,1,k))) = SD_Add_Data ((m + n),k)

proof end;

theorem :: RADIX_1:26

for n being Nat st n >= 1 holds
for k, x, y being Nat 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 end;