:: RADIX_2 semantic presentation

theorem Th1: :: RADIX_2:1

for b₁ being Nat holds b₁ mod 1 = 0

proof end;

theorem Th2: :: RADIX_2:2

for b₁, b₂ being Integer
for b₃ being Nat st b₃ > 0 holds
((b₁ mod b₃) + (b₂ mod b₃)) mod b₃ = (b₁ + (b₂ mod b₃)) mod b₃

proof end;

theorem Th3: :: RADIX_2:3

for b₁, b₂ being Integer
for b₃ being Nat st b₃ > 0 holds
(b₁ * b₂) mod b₃ = (b₁ * (b₂ mod b₃)) mod b₃

proof end;

theorem Th4: :: RADIX_2:4

for b₁, b₂, b₃ being Nat st 1 <= b₃ & 0 < b₂ holds
(b₁ mod (b₂ |^ b₃)) div (b₂ |^ (b₃ -' 1)) = (b₁ div (b₂ |^ (b₃ -' 1))) mod b₂

proof end;

theorem Th5: :: RADIX_2:5

for b₁, b₂ being Nat st b₁ in Seg b₂ holds
b₁ + 1 in Seg (b₂ + 1)

proof end;

theorem Th6: :: RADIX_2:6

for b₁ being Nat holds Radix b₁ > 0

proof end;

theorem Th7: :: RADIX_2:7

for b₁ being Nat
for b₂ being Tuple of 1,(b₁ -SD ) holds SDDec b₂ = DigA b₂,1

proof end;

theorem Th8: :: RADIX_2:8

for b₁ being Nat
for b₂ being Integer holds (SD_Add_Data b₂,b₁) + ((SD_Add_Carry b₂) * (Radix b₁)) = b₂

proof end;

theorem Th9: :: RADIX_2:9

for b₁, b₂ being Nat
for b₃ being Tuple of (b₂ + 1),(b₁ -SD )
for b₄ being Tuple of b₂,(b₁ -SD ) st ( for b₅ being Nat st b₅ in Seg b₂ holds
b₃ . b₅ = b₄ . b₅ ) holds
Sum (DigitSD b₃) = Sum ((DigitSD b₄) ^ <*(SubDigit b₃,(b₂ + 1),b₁)*>)

proof end;

theorem Th10: :: RADIX_2:10

for b₁, b₂ being Nat
for b₃ being Tuple of (b₂ + 1),(b₁ -SD )
for b₄ being Tuple of b₂,(b₁ -SD ) st ( for b₅ being Nat st b₅ in Seg b₂ holds
b₃ . b₅ = b₄ . b₅ ) holds
(SDDec b₄) + (((Radix b₁) |^ b₂) * (DigA b₃,(b₂ + 1))) = SDDec b₃

proof end;

theorem Th11: :: RADIX_2:11

for b₁, b₂ being Nat st b₂ >= 1 holds
for b₃, b₄ being Tuple of b₂,(b₁ -SD ) st b₁ >= 2 holds
(SDDec (b₃ '+' b₄)) + ((SD_Add_Carry ((DigA b₃,b₂) + (DigA b₄,b₂))) * ((Radix b₁) |^ b₂)) = (SDDec b₃) + (SDDec b₄)

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,NAT ;
func SubDigit2 c₄,c₁,c₂ -> Element of NAT equals :: RADIX_2:def 1
((Radix a₂) |^ (a₁ -' 1)) * (a₄ . a₁);
coherence ;

end;

:: deftheorem Def1 defines SubDigit2 RADIX_2:def 1 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of c₁,NAT ;
func DigitSD2 c₃,c₂ -> Tuple of a₁,NAT means :Def2: :: RADIX_2:def 2
for b₁ being Nat st b₁ in Seg a₁ holds
a₄ /. b₁ = SubDigit2 a₃,b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines DigitSD2 RADIX_2:def 2 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of c₁,NAT ;
func SDDec2 c₃,c₂ -> Nat equals :: RADIX_2:def 3
Sum (DigitSD2 a₃,a₂);
coherence ;

end;

:: deftheorem Def3 defines SDDec2 RADIX_2:def 3 :

definition

let c₁, c₂, c₃ be Nat;
func DigitDC2 c₃,c₁,c₂ -> Nat equals :: RADIX_2:def 4
(a₃ mod ((Radix a₂) |^ a₁)) div ((Radix a₂) |^ (a₁ -' 1));
coherence ;

end;

:: deftheorem Def4 defines DigitDC2 RADIX_2:def 4 :

definition

let c₁, c₂, c₃ be Nat;
func DecSD2 c₃,c₂,c₁ -> Tuple of a₂,NAT means :Def5: :: RADIX_2:def 5
for b₁ being Nat st b₁ in Seg a₂ holds
a₄ . b₁ = DigitDC2 a₃,b₁,a₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines DecSD2 RADIX_2:def 5 :

theorem Th12: :: RADIX_2:12

for b₁, b₂ being Nat
for b₃ being Tuple of b₁,NAT
for b₄ being Tuple of b₁,(b₂ -SD ) st b₃ = b₄ holds
DigitSD2 b₃,b₂ = DigitSD b₄

proof end;

theorem Th13: :: RADIX_2:13

for b₁, b₂ being Nat
for b₃ being Tuple of b₁,NAT
for b₄ being Tuple of b₁,(b₂ -SD ) st b₃ = b₄ holds
SDDec2 b₃,b₂ = SDDec b₄

proof end;

theorem Th14: :: RADIX_2:14

for b₁, b₂, b₃ being Nat holds DecSD2 b₁,b₂,b₃ = DecSD b₁,b₂,b₃

proof end;

theorem Th15: :: RADIX_2:15

for b₁ being Nat st b₁ >= 1 holds
for b₂, b₃ being Nat st b₂ is_represented_by b₁,b₃ holds
b₂ = SDDec2 (DecSD2 b₂,b₁,b₃),b₃

proof end;

definition

let c₁ be Integer;
let c₂, c₃, c₄, c₅ be Nat;
let c₆ be Tuple of c₅,(c₄ -SD );
func Table1 c₁,c₆,c₂,c₃ -> Integer equals :: RADIX_2:def 6
(a₁ * (DigA a₆,a₃)) mod a₂;
correctness ;

end;

:: deftheorem Def6 defines Table1 RADIX_2:def 6 :

definition

let c₁ be Integer;
let c₂, c₃, c₄ be Nat;
let c₅ be Tuple of c₄,(c₂ -SD );
assume E16: c₄ >= 1 ;
func Mul_mod c₁,c₅,c₃,c₂ -> Tuple of a₄,INT means :Def7: :: RADIX_2:def 7
( a₆ . 1 = Table1 a₁,a₅,a₃,a₄ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= a₄ - 1 holds
ex b₂, b₃ being Integer st
( b₂ = a₆ . b₁ & b₃ = a₆ . (b₁ + 1) & b₃ = (((Radix a₂) * b₂) + (Table1 a₁,a₅,a₃,(a₄ -' b₁))) mod a₃ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Mul_mod RADIX_2:def 7 :

theorem Th16: :: RADIX_2:16

for b₁ being Nat st b₁ >= 1 holds
for b₂ being Integer
for b₃, b₄, b₅ being Nat st b₃ is_represented_by b₁,b₅ & b₄ > 0 holds
for b₆ being Tuple of b₁,(b₅ -SD ) st b₆ = DecSD b₃,b₁,b₅ holds
(Mul_mod b₂,b₆,b₄,b₅) . b₁ = (b₂ * b₃) mod b₄

proof end;

definition

let c₁, c₂, c₃, c₄ be Nat;
let c₅ be Tuple of c₁,NAT ;
func Table2 c₄,c₅,c₂,c₃ -> Nat equals :: RADIX_2:def 8
(a₄ |^ (a₅ /. a₃)) mod a₂;
correctness ;

end;

:: deftheorem Def8 defines Table2 RADIX_2:def 8 :

definition

let c₁, c₂, c₃, c₄ be Nat;
let c₅ be Tuple of c₄,NAT ;
assume E17: c₄ >= 1 ;
func Pow_mod c₃,c₅,c₂,c₁ -> Tuple of a₄,NAT means :Def9: :: RADIX_2:def 9
( a₆ . 1 = Table2 a₃,a₅,a₂,a₄ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= a₄ - 1 holds
ex b₂, b₃ being Nat st
( b₂ = a₆ . b₁ & b₃ = a₆ . (b₁ + 1) & b₃ = (((b₂ |^ (Radix a₁)) mod a₂) * (Table2 a₃,a₅,a₂,(a₄ -' b₁))) mod a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Pow_mod RADIX_2:def 9 :

theorem Th17: :: RADIX_2:17

for b₁ being Nat st b₁ >= 1 holds
for b₂, b₃, b₄, b₅ being Nat st b₅ is_represented_by b₁,b₃ & b₄ > 0 holds
for b₆ being Tuple of b₁,NAT st b₆ = DecSD2 b₅,b₁,b₃ holds
(Pow_mod b₂,b₆,b₄,b₃) . b₁ = (b₂ |^ b₅) mod b₄

proof end;