:: by Yasushi Fuwa and Yoshinori Fujisawa

::

:: Received February 1, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

theorem Th4: :: RADIX_2:4

for a, b, i being Nat st 1 <= i & 0 < b holds

(a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b

(a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b

proof end;

theorem Th9: :: RADIX_2:9

for k, n being Nat

for x being Tuple of n + 1,k -SD

for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

x . i = xn . i ) holds

Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>)

for x being Tuple of n + 1,k -SD

for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

x . i = xn . i ) holds

Sum (DigitSD x) = Sum ((DigitSD xn) ^ <*(SubDigit (x,(n + 1),k))*>)

proof end;

theorem Th10: :: RADIX_2:10

for k, n being Nat

for x being Tuple of n + 1,k -SD

for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

x . i = xn . i ) holds

(SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x

for x being Tuple of n + 1,k -SD

for xn being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

x . i = xn . i ) holds

(SDDec xn) + (((Radix k) |^ n) * (DigA (x,(n + 1)))) = SDDec x

proof end;

theorem :: RADIX_2:11

for k, n being Nat st n >= 1 holds

for x, y being Tuple of n,k -SD st k >= 2 holds

(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,n)) + (DigA (y,n)))) * ((Radix k) |^ n)) = (SDDec x) + (SDDec y)

for x, y being Tuple of n,k -SD st k >= 2 holds

(SDDec (x '+' y)) + ((SD_Add_Carry ((DigA (x,n)) + (DigA (y,n)))) * ((Radix k) |^ n)) = (SDDec x) + (SDDec y)

proof end;

:: a FinSequence of NAT and some properties about them

definition

let i, k, n be Nat;

let x be Tuple of n, NAT ;

coherence

((Radix k) |^ (i -' 1)) * (x . i) is Element of NAT ;

end;
let x be Tuple of n, NAT ;

coherence

((Radix k) |^ (i -' 1)) * (x . i) is Element of NAT ;

:: deftheorem defines SubDigit2 RADIX_2:def 1 :

for i, k, n being Nat

for x being Tuple of n, NAT holds SubDigit2 (x,i,k) = ((Radix k) |^ (i -' 1)) * (x . i);

for i, k, n being Nat

for x being Tuple of n, NAT holds SubDigit2 (x,i,k) = ((Radix k) |^ (i -' 1)) * (x . i);

definition

let n, k be Nat;

let x be Tuple of n, NAT ;

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

for i being Nat st i in Seg n holds

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

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

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

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

b_{1} = b_{2}

end;
let x be Tuple of n, NAT ;

func DigitSD2 (x,k) -> Tuple of n, NAT means :Def2: :: RADIX_2:def 2

for i being Nat st i in Seg n holds

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

existence for i being Nat st i in Seg n holds

it /. i = SubDigit2 (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 Def2 defines DigitSD2 RADIX_2:def 2 :

for n, k being Nat

for x, b_{4} being Tuple of n, NAT holds

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

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

for n, k being Nat

for x, b

( b

b

definition
end;

:: deftheorem defines SDDec2 RADIX_2:def 3 :

for n, k being Nat

for x being Tuple of n, NAT holds SDDec2 (x,k) = Sum (DigitSD2 (x,k));

for n, k being Nat

for x being Tuple of n, NAT holds SDDec2 (x,k) = Sum (DigitSD2 (x,k));

definition

let i, k, x be Nat;

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

end;
func DigitDC2 (x,i,k) -> Element of NAT equals :: RADIX_2:def 4

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

:: deftheorem defines DigitDC2 RADIX_2:def 4 :

for i, k, x being Nat holds DigitDC2 (x,i,k) = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));

for i, k, x being Nat holds DigitDC2 (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, NAT st

for i being Nat st i in Seg n holds

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

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

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

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

b_{1} = b_{2}

end;
func DecSD2 (x,n,k) -> Tuple of n, NAT means :Def5: :: RADIX_2:def 5

for i being Nat st i in Seg n holds

it . i = DigitDC2 (x,i,k);

existence for i being Nat st i in Seg n holds

it . i = DigitDC2 (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 Def5 defines DecSD2 RADIX_2:def 5 :

for k, n, x being Nat

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

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

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

for k, n, x being Nat

for b

( b

b

theorem Th12: :: RADIX_2:12

for n, k being Nat

for x being Tuple of n, NAT

for y being Tuple of n,k -SD st x = y holds

DigitSD2 (x,k) = DigitSD y

for x being Tuple of n, NAT

for y being Tuple of n,k -SD st x = y holds

DigitSD2 (x,k) = DigitSD y

proof end;

theorem Th13: :: RADIX_2:13

for n, k being Nat

for x being Tuple of n, NAT

for y being Tuple of n,k -SD st x = y holds

SDDec2 (x,k) = SDDec y

for x being Tuple of n, NAT

for y being Tuple of n,k -SD st x = y holds

SDDec2 (x,k) = SDDec y

proof end;

theorem Th15: :: RADIX_2:15

for n being Nat st n >= 1 holds

for m, k being Nat st m is_represented_by n,k holds

m = SDDec2 ((DecSD2 (m,n,k)),k)

for m, k being Nat st m is_represented_by n,k holds

m = SDDec2 ((DecSD2 (m,n,k)),k)

proof end;

:: radix-2^k SD numbers and its correctness

definition

let q be Integer;

let f, j, k, n be Nat;

let c be Tuple of n,k -SD ;

correctness

coherence

(q * (DigA (c,j))) mod f is Integer;

;

end;
let f, j, k, n be Nat;

let c be Tuple of n,k -SD ;

correctness

coherence

(q * (DigA (c,j))) mod f is Integer;

;

:: deftheorem defines Table1 RADIX_2:def 6 :

for q being Integer

for f, j, k, n being Nat

for c being Tuple of n,k -SD holds Table1 (q,c,f,j) = (q * (DigA (c,j))) mod f;

for q being Integer

for f, j, k, n being Nat

for c being Tuple of n,k -SD holds Table1 (q,c,f,j) = (q * (DigA (c,j))) mod f;

definition

let q be Integer;

let k, f, n be Nat;

let c be Tuple of n,k -SD ;

assume A1: n >= 1 ;

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

( b_{1} . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Integer st

( I1 = b_{1} . i & I2 = b_{1} . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) )

for b_{1}, b_{2} being Tuple of n, INT st b_{1} . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Integer st

( I1 = b_{1} . i & I2 = b_{1} . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) & b_{2} . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Integer st

( I1 = b_{2} . i & I2 = b_{2} . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) holds

b_{1} = b_{2}

end;
let k, f, n be Nat;

let c be Tuple of n,k -SD ;

assume A1: n >= 1 ;

func Mul_mod (q,c,f,k) -> Tuple of n, INT means :Def7: :: RADIX_2:def 7

( it . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Integer st

( I1 = it . i & I2 = it . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) );

existence ( it . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Integer st

( I1 = it . i & I2 = it . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) );

ex b

( b

ex I1, I2 being Integer st

( I1 = b

proof end;

uniqueness for b

ex I1, I2 being Integer st

( I1 = b

ex I1, I2 being Integer st

( I1 = b

b

proof end;

:: deftheorem Def7 defines Mul_mod RADIX_2:def 7 :

for q being Integer

for k, f, n being Nat

for c being Tuple of n,k -SD st n >= 1 holds

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

( b_{6} = Mul_mod (q,c,f,k) iff ( b_{6} . 1 = Table1 (q,c,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex I1, I2 being Integer st

( I1 = b_{6} . i & I2 = b_{6} . (i + 1) & I2 = (((Radix k) * I1) + (Table1 (q,c,f,(n -' i)))) mod f ) ) ) );

for q being Integer

for k, f, n being Nat

for c being Tuple of n,k -SD st n >= 1 holds

for b

( b

ex I1, I2 being Integer st

( I1 = b

theorem :: RADIX_2:16

for n being Nat st n >= 1 holds

for q being Integer

for ic, f, k being Nat st ic is_represented_by n,k & f > 0 holds

for c being Tuple of n,k -SD st c = DecSD (ic,n,k) holds

(Mul_mod (q,c,f,k)) . n = (q * ic) mod f

for q being Integer

for ic, f, k being Nat st ic is_represented_by n,k & f > 0 holds

for c being Tuple of n,k -SD st c = DecSD (ic,n,k) holds

(Mul_mod (q,c,f,k)) . n = (q * ic) mod f

proof end;

:: radix-2^k SD numbers and its correctness

definition

let n, f, j, m be Nat;

let e be Tuple of n, NAT ;

correctness

coherence

(m |^ (e /. j)) mod f is Element of NAT ;

;

end;
let e be Tuple of n, NAT ;

correctness

coherence

(m |^ (e /. j)) mod f is Element of NAT ;

;

:: deftheorem defines Table2 RADIX_2:def 8 :

for n, f, j, m being Nat

for e being Tuple of n, NAT holds Table2 (m,e,f,j) = (m |^ (e /. j)) mod f;

for n, f, j, m being Nat

for e being Tuple of n, NAT holds Table2 (m,e,f,j) = (m |^ (e /. j)) mod f;

definition

let k, f, m, n be Nat;

let e be Tuple of n, NAT ;

assume A1: n >= 1 ;

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

( b_{1} . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = b_{1} . i & i2 = b_{1} . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) )

for b_{1}, b_{2} being Tuple of n, NAT st b_{1} . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = b_{1} . i & i2 = b_{1} . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) & b_{2} . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = b_{2} . i & i2 = b_{2} . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) holds

b_{1} = b_{2}

end;
let e be Tuple of n, NAT ;

assume A1: n >= 1 ;

func Pow_mod (m,e,f,k) -> Tuple of n, NAT means :Def9: :: RADIX_2:def 9

( it . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = it . i & i2 = it . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) );

existence ( it . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = it . i & i2 = it . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) );

ex b

( b

ex i1, i2 being Nat st

( i1 = b

proof end;

uniqueness for b

ex i1, i2 being Nat st

( i1 = b

ex i1, i2 being Nat st

( i1 = b

b

proof end;

:: deftheorem Def9 defines Pow_mod RADIX_2:def 9 :

for k, f, m, n being Nat

for e being Tuple of n, NAT st n >= 1 holds

for b_{6} being Tuple of n, NAT holds

( b_{6} = Pow_mod (m,e,f,k) iff ( b_{6} . 1 = Table2 (m,e,f,n) & ( for i being Nat st 1 <= i & i <= n - 1 holds

ex i1, i2 being Nat st

( i1 = b_{6} . i & i2 = b_{6} . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 (m,e,f,(n -' i)))) mod f ) ) ) );

for k, f, m, n being Nat

for e being Tuple of n, NAT st n >= 1 holds

for b

( b

ex i1, i2 being Nat st

( i1 = b

theorem :: RADIX_2:17

for n being Nat st n >= 1 holds

for m, k, f, ie being Nat st ie is_represented_by n,k & f > 0 holds

for e being Tuple of n, NAT st e = DecSD2 (ie,n,k) holds

(Pow_mod (m,e,f,k)) . n = (m |^ ie) mod f

for m, k, f, ie being Nat st ie is_represented_by n,k & f > 0 holds

for e being Tuple of n, NAT st e = DecSD2 (ie,n,k) holds

(Pow_mod (m,e,f,k)) . n = (m |^ ie) mod f

proof end;