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 :
definition
let n,
k be
Nat;
let x be
Tuple of
n, ;
func DigitSD2 x,
k -> Tuple of
n,
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, 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, 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 :
:: deftheorem defines SDDec2 RADIX_2:def 3 :
:: deftheorem defines DigitDC2 RADIX_2:def 4 :
definition
let k,
n,
x be
Nat;
func DecSD2 x,
n,
k -> Tuple of
n,
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, 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, 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 :
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
:: deftheorem defines Table1 RADIX_2:def 6 :
definition
let q be
Integer;
let k,
f,
n be
Nat;
let c be
Tuple of
n, ;
assume A1:
n >= 1
;
func Mul_mod q,
c,
f,
k -> Tuple of
n,
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, 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, 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, st
n >= 1 holds
for
b6 being
Tuple of
n, 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 :
definition
let k,
f,
m,
n be
Nat;
let e be
Tuple of
n, ;
assume A1:
n >= 1
;
func Pow_mod m,
e,
f,
k -> Tuple of
n,
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, 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, 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, st
n >= 1 holds
for
b6 being
Tuple of
n, 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, st
e = DecSD2 ie,
n,
k holds
(Pow_mod m,e,f,k) . n = (m |^ ie) mod f