begin
theorem
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
begin
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
begin
:: 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);
definition
let n,
k be
Nat;
let x be
Tuple of
n,
NAT ;
func DigitSD2 x,
k -> Tuple of
n,
NAT means :
Def2:
for
i being
Nat st
i in Seg n holds
it /. i = SubDigit2 x,
i,
k;
existence
ex b1 being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b1 /. i = SubDigit2 x,i,k
uniqueness
for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b1 /. i = SubDigit2 x,i,k ) & ( for i being Nat st i in Seg n holds
b2 /. i = SubDigit2 x,i,k ) holds
b1 = b2
end;
:: deftheorem Def2 defines DigitSD2 RADIX_2:def 2 :
for n, k being Nat
for x, b4 being Tuple of n, NAT holds
( b4 = DigitSD2 x,k iff for i being Nat st i in Seg n holds
b4 /. i = SubDigit2 x,i,k );
:: 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);
:: 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));
definition
let k,
n,
x be
Nat;
func DecSD2 x,
n,
k -> Tuple of
n,
NAT means :
Def5:
for
i being
Nat st
i in Seg n holds
it . i = DigitDC2 x,
i,
k;
existence
ex b1 being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b1 . i = DigitDC2 x,i,k
uniqueness
for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b1 . i = DigitDC2 x,i,k ) & ( for i being Nat st i in Seg n holds
b2 . i = DigitDC2 x,i,k ) holds
b1 = b2
end;
:: deftheorem Def5 defines DecSD2 RADIX_2:def 5 :
for k, n, x being Nat
for b4 being Tuple of n, NAT holds
( b4 = DecSD2 x,n,k iff for i being Nat st i in Seg n holds
b4 . i = DigitDC2 x,i,k );
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
:: 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;
definition
let q be
Integer;
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:
(
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
ex b1 being Tuple of n, INT st
( b1 . 1 = Table1 q,c,f,n & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b1 . i & I2 = b1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 q,c,f,(n -' i))) mod f ) ) )
uniqueness
for b1, b2 being Tuple of n, INT st b1 . 1 = Table1 q,c,f,n & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b1 . i & I2 = b1 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 q,c,f,(n -' i))) mod f ) ) & b2 . 1 = Table1 q,c,f,n & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b2 . i & I2 = b2 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 q,c,f,(n -' i))) mod f ) ) holds
b1 = b2
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 b6 being Tuple of n, INT holds
( b6 = Mul_mod q,c,f,k iff ( b6 . 1 = Table1 q,c,f,n & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex I1, I2 being Integer st
( I1 = b6 . i & I2 = b6 . (i + 1) & I2 = (((Radix k) * I1) + (Table1 q,c,f,(n -' i))) mod f ) ) ) );
theorem
begin
:: 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;
definition
let k,
f,
m,
n be
Nat;
let e be
Tuple of
n,
NAT ;
assume A1:
n >= 1
;
func Pow_mod m,
e,
f,
k -> Tuple of
n,
NAT means :
Def9:
(
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
ex b1 being Tuple of n, NAT st
( b1 . 1 = Table2 m,e,f,n & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b1 . i & i2 = b1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 m,e,f,(n -' i))) mod f ) ) )
uniqueness
for b1, b2 being Tuple of n, NAT st b1 . 1 = Table2 m,e,f,n & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b1 . i & i2 = b1 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 m,e,f,(n -' i))) mod f ) ) & b2 . 1 = Table2 m,e,f,n & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b2 . i & i2 = b2 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 m,e,f,(n -' i))) mod f ) ) holds
b1 = b2
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 b6 being Tuple of n, NAT holds
( b6 = Pow_mod m,e,f,k iff ( b6 . 1 = Table2 m,e,f,n & ( for i being Nat st 1 <= i & i <= n - 1 holds
ex i1, i2 being Nat st
( i1 = b6 . i & i2 = b6 . (i + 1) & i2 = (((i1 |^ (Radix k)) mod f) * (Table2 m,e,f,(n -' i))) mod f ) ) ) );
theorem
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