:: by Yoshinori Fujisawa and Yasushi Fuwa

::

:: Received September 7, 1999

:: Copyright (c) 1999-2016 Association of Mizar Users

::$CT

definition
end;

definition

let k be Nat;

coherence

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

;

end;
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 { e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } ;

coherence

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

;

:: 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 ) } ;

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 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 )

for k being Nat st i1 in k -SD holds

( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 )

proof 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;
:: original: -SD

redefine func k -SD -> non empty Subset of INT;

coherence

k -SD is non empty Subset of INT by Th11;

definition

let i, k, n be Nat;

let x be Tuple of n,k -SD ;

coherence

( ( i in Seg n implies x . i is Integer ) & ( i = 0 implies 0 is Integer ) ) by INT_1:def 2;

consistency

for b_{1} being Integer st i in Seg n & i = 0 holds

( b_{1} = x . i iff b_{1} = 0 )
by FINSEQ_1:1;

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

coherence

( ( i in Seg n implies x . i is Integer ) & ( i = 0 implies 0 is Integer ) ) by INT_1:def 2;

consistency

for b

( b

:: 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 ) );

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 ;

coherence

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

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

coherence

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

:: 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);

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

for a being Tuple of n,k -SD st i in Seg n holds

DigA (a,i) is Element of k -SD

proof end;

definition

let i, k, n be Nat;

let x be Tuple of n,k -SD ;

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

end;
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));

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

:: 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));

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 ;

ex b_{1} being Tuple of n, INT st

for i being Nat st i in Seg n holds

b_{1} /. i = SubDigit (x,i,k)

for b_{1}, b_{2} being Tuple of n, INT st ( for i being Nat st i in Seg n holds

b_{1} /. i = SubDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds

b_{2} /. i = SubDigit (x,i,k) ) holds

b_{1} = b_{2}

end;
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 for i being Nat st i in Seg n holds

it /. i = SubDigit (x,i,k);

ex b

for i being Nat st i in Seg n holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines DigitSD RADIX_1:def 6 :

for n, k being Nat

for x being Tuple of n,k -SD

for b_{4} being Tuple of n, INT holds

( b_{4} = DigitSD x iff for i being Nat st i in Seg n holds

b_{4} /. i = SubDigit (x,i,k) );

for n, k being Nat

for x being Tuple of n,k -SD

for b

( b

b

:: 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);

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;

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

end;
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));

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

proof 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));

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;

ex b_{1} being Tuple of n,k -SD st

for i being Nat st i in Seg n holds

DigA (b_{1},i) = DigitDC (x,i,k)

for b_{1}, b_{2} being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

DigA (b_{1},i) = DigitDC (x,i,k) ) & ( for i being Nat st i in Seg n holds

DigA (b_{2},i) = DigitDC (x,i,k) ) holds

b_{1} = b_{2}

end;
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 for i being Nat st i in Seg n holds

DigA (it,i) = DigitDC (x,i,k);

ex b

for i being Nat st i in Seg n holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def9 defines DecSD RADIX_1:def 9 :

for k, n, x being Nat

for b_{4} being Tuple of n,k -SD holds

( b_{4} = DecSD (x,n,k) iff for i being Nat st i in Seg n holds

DigA (b_{4},i) = DigitDC (x,i,k) );

for k, n, x being Nat

for b

( b

DigA (b

definition

let x be Integer;

( ( 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_{1} being Integer st x > 2 & x < - 2 holds

( b_{1} = 1 iff b_{1} = - 1 )
;

end;
func SD_Add_Carry x -> Integer equals :Def10: :: RADIX_1:def 10

1 if x > 2

- 1 if x < - 2

otherwise 0 ;

coherence 1 if x > 2

- 1 if x < - 2

otherwise 0 ;

( ( 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

( b

:: 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 ) );

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 ) );

Lm2: for x being Integer holds

( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )

proof end;

definition
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));

for x being Integer

for k being Nat holds SD_Add_Data (x,k) = x - ((SD_Add_Carry x) * (Radix k));

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 )

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
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 );

for n, x, k being Nat holds

( x is_represented_by n,k iff x < (Radix k) |^ n );

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))

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)

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)

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 ;

(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

end;
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)))));

(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;

:: 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)))));

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 ;

ex b_{1} being Tuple of n,k -SD st

for i being Nat st i in Seg n holds

DigA (b_{1},i) = Add (x,y,i,k)

for b_{1}, b_{2} being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

DigA (b_{1},i) = Add (x,y,i,k) ) & ( for i being Nat st i in Seg n holds

DigA (b_{2},i) = Add (x,y,i,k) ) holds

b_{1} = b_{2}

end;
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 for i being Nat st i in Seg n holds

DigA (it,i) = Add (x,y,i,k);

ex b

for i being Nat st i in Seg n holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def14 defines '+' RADIX_1:def 14 :

for n, k being Nat

for x, y, b_{5} being Tuple of n,k -SD holds

( b_{5} = x '+' y iff for i being Nat st i in Seg n holds

DigA (b_{5},i) = Add (x,y,i,k) );

for n, k being Nat

for x, y, b

( b

DigA (b

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)

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)))))

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;