:: RADIX_3 semantic presentation

Lemma1: for b₁ being Nat st 1 <= b₁ holds
Radix b₁ = (Radix (b₁ -' 1)) + (Radix (b₁ -' 1))

proof end;

Lemma2: for b₁ being Nat st 1 <= b₁ holds
(Radix b₁) - (Radix (b₁ -' 1)) = Radix (b₁ -' 1)

proof end;

Lemma3: for b₁ being Nat st 1 <= b₁ holds
(- (Radix b₁)) + (Radix (b₁ -' 1)) = - (Radix (b₁ -' 1))

proof end;

Lemma4: for b₁ being Nat st 1 <= b₁ holds
2 <= Radix b₁

proof end;

Lemma5: for b₁, b₂, b₃, b₄ being Nat st b₄ in Seg b₁ holds
DigA (DecSD b₂,(b₁ + 1),b₃),b₄ = DigA (DecSD (b₂ mod ((Radix b₃) |^ b₁)),b₁,b₃),b₄

proof end;

definition

let c₁ be Nat;
func c₁ -SD_Sub_S -> set equals :: RADIX_3:def 1
{ b₁ where B is Element of INT : ( b₁ >= - (Radix (a₁ -' 1)) & b₁ <= (Radix (a₁ -' 1)) - 1 ) } ;
correctness ;

end;

:: deftheorem Def1 defines -SD_Sub_S RADIX_3:def 1 :

definition

let c₁ be Nat;
func c₁ -SD_Sub -> set equals :: RADIX_3:def 2
{ b₁ where B is Element of INT : ( b₁ >= (- (Radix (a₁ -' 1))) - 1 & b₁ <= Radix (a₁ -' 1) ) } ;
correctness ;

end;

:: deftheorem Def2 defines -SD_Sub RADIX_3:def 2 :

theorem Th1: :: RADIX_3:1

canceled;

theorem Th2: :: RADIX_3:2

for b₁ being Nat
for b₂ being Integer st b₂ in b₁ -SD_Sub holds
( (- (Radix (b₁ -' 1))) - 1 <= b₂ & b₂ <= Radix (b₁ -' 1) )

proof end;

theorem Th3: :: RADIX_3:3

for b₁ being Nat holds b₁ -SD_Sub_S c= b₁ -SD_Sub

proof end;

theorem Th4: :: RADIX_3:4

for b₁ being Nat holds b₁ -SD_Sub_S c= (b₁ + 1) -SD_Sub_S

proof end;

theorem Th5: :: RADIX_3:5

for b₁ being Nat st 2 <= b₁ holds
b₁ -SD_Sub c= b₁ -SD

proof end;

theorem Th6: :: RADIX_3:6

0 in 0 -SD_Sub_S

proof end;

theorem Th7: :: RADIX_3:7

for b₁ being Nat holds 0 in b₁ -SD_Sub_S

proof end;

theorem Th8: :: RADIX_3:8

for b₁ being Nat holds 0 in b₁ -SD_Sub

proof end;

theorem Th9: :: RADIX_3:9

for b₁ being Nat
for b₂ being set st b₂ in b₁ -SD_Sub holds
b₂ is Integer

proof end;

theorem Th10: :: RADIX_3:10

for b₁ being Nat holds b₁ -SD_Sub c= INT

proof end;

theorem Th11: :: RADIX_3:11

for b₁ being Nat holds b₁ -SD_Sub_S c= INT

proof end;

registration

let c₁ be Nat;
cluster a₁ -SD_Sub_S -> non empty ;
coherence by Th7;
cluster a₁ -SD_Sub -> non empty ;
coherence by Th8;

end;

definition

let c₁ be Nat;
redefine func -SD_Sub_S as c₁ -SD_Sub_S -> non empty Subset of INT ;
coherence by Th11;

end;

definition

let c₁ be Nat;
redefine func -SD_Sub as c₁ -SD_Sub -> non empty Subset of INT ;
coherence by Th10;

end;

theorem Th12: :: RADIX_3:12

for b₁, b₂, b₃ being Nat
for b₄ being Tuple of b₂,(b₃ -SD_Sub ) st b₁ in Seg b₂ holds
b₄ . b₁ is Element of b₃ -SD_Sub

proof end;

definition

let c₁ be Integer;
let c₂ be Nat;
func SDSub_Add_Carry c₁,c₂ -> Integer equals :Def3: :: RADIX_3:def 3
1 if Radix (a₂ -' 1) <= a₁
- 1 if a₁ < - (Radix (a₂ -' 1))
otherwise 0;
coherence ;
consistency ;

end;

:: deftheorem Def3 defines SDSub_Add_Carry RADIX_3:def 3 :

definition

let c₁ be Integer;
let c₂ be Nat;
func SDSub_Add_Data c₁,c₂ -> Integer equals :: RADIX_3:def 4
a₁ - ((Radix a₂) * (SDSub_Add_Carry a₁,a₂));
coherence ;

end;

:: deftheorem Def4 defines SDSub_Add_Data RADIX_3:def 4 :

theorem Th13: :: RADIX_3:13

for b₁ being Integer
for b₂ being Nat st 2 <= b₂ holds
( - 1 <= SDSub_Add_Carry b₁,b₂ & SDSub_Add_Carry b₁,b₂ <= 1 )

proof end;

theorem Th14: :: RADIX_3:14

for b₁ being Nat
for b₂ being Integer st 2 <= b₁ & b₂ in b₁ -SD holds
( SDSub_Add_Data b₂,b₁ >= - (Radix (b₁ -' 1)) & SDSub_Add_Data b₂,b₁ <= (Radix (b₁ -' 1)) - 1 )

proof end;

theorem Th15: :: RADIX_3:15

for b₁ being Integer
for b₂ being Nat st 2 <= b₂ holds
SDSub_Add_Carry b₁,b₂ in b₂ -SD_Sub_S

proof end;

theorem Th16: :: RADIX_3:16

for b₁ being Nat
for b₂, b₃ being Integer st 2 <= b₁ & b₂ in b₁ -SD & b₃ in b₁ -SD holds
(SDSub_Add_Data b₂,b₁) + (SDSub_Add_Carry b₃,b₁) in b₁ -SD_Sub

proof end;

theorem Th17: :: RADIX_3:17

for b₁ being Nat st 2 <= b₁ holds
SDSub_Add_Carry 0,b₁ = 0

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,(c₂ -SD_Sub );
func DigA_SDSub c₄,c₁ -> Integer equals :Def5: :: RADIX_3:def 5
a₄ . a₁ if a₁ in Seg a₃
0 if a₁ = 0
;
coherence

proof end;

consistency by FINSEQ_1:3;

end;

:: deftheorem Def5 defines DigA_SDSub RADIX_3:def 5 :

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,(c₂ -SD );
func SD2SDSubDigit c₄,c₁,c₂ -> Integer equals :Def6: :: RADIX_3:def 6
(SDSub_Add_Data (DigA a₄,a₁),a₂) + (SDSub_Add_Carry (DigA a₄,(a₁ -' 1)),a₂) if a₁ in Seg a₃
SDSub_Add_Carry (DigA a₄,(a₁ -' 1)),a₂ if a₁ = a₃ + 1
otherwise 0;
coherence ;
consistency

proof end;

end;

:: deftheorem Def6 defines SD2SDSubDigit RADIX_3:def 6 :

theorem Th18: :: RADIX_3:18

for b₁, b₂, b₃ being Nat
for b₄ being Tuple of b₃,(b₁ -SD ) st 2 <= b₁ & b₂ in Seg (b₃ + 1) holds
SD2SDSubDigit b₄,b₂,b₁ is Element of b₁ -SD_Sub

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,(c₂ -SD );
assume E25: ( 2 <= c₂ & c₁ in Seg (c₃ + 1) ) ;
func SD2SDSubDigitS c₄,c₁,c₂ -> Element of a₂ -SD_Sub equals :Def7: :: RADIX_3:def 7
SD2SDSubDigit a₄,a₁,a₂;
coherence by E25, Th18;

end;

:: deftheorem Def7 defines SD2SDSubDigitS RADIX_3:def 7 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of c₁,(c₂ -SD );
func SD2SDSub c₃ -> Tuple of (a₁ + 1),(a₂ -SD_Sub ) means :Def8: :: RADIX_3:def 8
for b₁ being Nat st b₁ in Seg (a₁ + 1) holds
DigA_SDSub a₄,b₁ = SD2SDSubDigitS a₃,b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines SD2SDSub RADIX_3:def 8 :

theorem Th19: :: RADIX_3:19

for b₁, b₂, b₃ being Nat
for b₄ being Tuple of b₂,(b₃ -SD_Sub ) st b₁ in Seg b₂ holds
DigA_SDSub b₄,b₁ is Element of b₃ -SD_Sub

proof end;

theorem Th20: :: RADIX_3:20

for b₁ being Nat
for b₂, b₃ being Integer st 2 <= b₁ & b₂ in b₁ -SD & b₃ in b₁ -SD_Sub holds
SDSub_Add_Data (b₂ + b₃),b₁ in b₁ -SD_Sub_S

proof end;

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,(c₂ -SD_Sub );
func DigB_SDSub c₄,c₁ -> Element of INT equals :: RADIX_3:def 9
DigA_SDSub a₄,a₁;
coherence by INT_1:def 2;

end;

:: deftheorem Def9 defines DigB_SDSub RADIX_3:def 9 :

definition

let c₁, c₂, c₃ be Nat;
let c₄ be Tuple of c₃,(c₂ -SD_Sub );
func SDSub2INTDigit c₄,c₁,c₂ -> Element of INT equals :: RADIX_3:def 10
((Radix a₂) |^ (a₁ -' 1)) * (DigB_SDSub a₄,a₁);
coherence by INT_1:def 2;

end;

:: deftheorem Def10 defines SDSub2INTDigit RADIX_3:def 10 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of c₁,(c₂ -SD_Sub );
func SDSub2INT c₃ -> Tuple of a₁,INT means :Def11: :: RADIX_3:def 11
for b₁ being Nat st b₁ in Seg a₁ holds
a₄ /. b₁ = SDSub2INTDigit a₃,b₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines SDSub2INT RADIX_3:def 11 :

definition

let c₁, c₂ be Nat;
let c₃ be Tuple of c₁,(c₂ -SD_Sub );
func SDSub2IntOut c₃ -> Integer equals :: RADIX_3:def 12
Sum (SDSub2INT a₃);
coherence ;

end;

:: deftheorem Def12 defines SDSub2IntOut RADIX_3:def 12 :

theorem Th21: :: RADIX_3:21

for b₁, b₂, b₃, b₄ being Nat st b₄ in Seg b₁ & 2 <= b₂ holds
DigA_SDSub (SD2SDSub (DecSD b₃,(b₁ + 1),b₂)),b₄ = DigA_SDSub (SD2SDSub (DecSD (b₃ mod ((Radix b₂) |^ b₁)),b₁,b₂)),b₄

proof end;

theorem Th22: :: RADIX_3:22

for b₁ being Nat st b₁ >= 1 holds
for b₂, b₃ being Nat st b₂ >= 2 & b₃ is_represented_by b₁,b₂ holds
b₃ = SDSub2IntOut (SD2SDSub (DecSD b₃,b₁,b₂))

proof end;