:: RADIX_3 semantic presentation

Lm1: for k being Nat st 1 <= k holds
Radix k = (Radix (k -' 1)) + (Radix (k -' 1))

proof end;

Lm2: for k being Nat st 1 <= k holds
(Radix k) - (Radix (k -' 1)) = Radix (k -' 1)

proof end;

Lm3: for k being Nat st 1 <= k holds
(- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1))

proof end;

Lm4: for k being Nat st 1 <= k holds
2 <= Radix k

proof end;

Lm5: for n, m, k, i being Nat st i in Seg n holds
DigA (DecSD m,(n + 1),k),i = DigA (DecSD (m mod ((Radix k) |^ n)),n,k),i

proof end;

definition

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

end;

:: deftheorem defines -SD_Sub_S RADIX_3:def 1 :

definition

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

end;

:: deftheorem defines -SD_Sub RADIX_3:def 2 :

theorem :: RADIX_3:1

canceled;

theorem Th2: :: RADIX_3:2

for k being Nat
for i1 being Integer st i1 in k -SD_Sub holds
( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) )

proof end;

theorem Th3: :: RADIX_3:3

for k being Nat holds k -SD_Sub_S c= k -SD_Sub

proof end;

theorem Th4: :: RADIX_3:4

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

proof end;

theorem :: RADIX_3:5

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

proof end;

theorem Th6: :: RADIX_3:6

0 in 0 -SD_Sub_S

proof end;

theorem Th7: :: RADIX_3:7

for k being Nat holds 0 in k -SD_Sub_S

proof end;

theorem Th8: :: RADIX_3:8

for k being Nat holds 0 in k -SD_Sub

proof end;

theorem Th9: :: RADIX_3:9

for k being Nat
for e being set st e in k -SD_Sub holds
e is Integer

proof end;

theorem Th10: :: RADIX_3:10

for k being Nat holds k -SD_Sub c= INT

proof end;

theorem Th11: :: RADIX_3:11

for k being Nat holds k -SD_Sub_S c= INT

proof end;

registration

let k be Nat;
cluster k -SD_Sub_S -> non empty ;
coherence by Th7;
cluster k -SD_Sub -> non empty ;
coherence by Th8;

end;

definition

let k be Nat;
:: original: -SD_Sub_S
redefine func k -SD_Sub_S -> non empty Subset of INT ;
coherence by Th11;

end;

definition

let k be Nat;
:: original: -SD_Sub
redefine func k -SD_Sub -> non empty Subset of INT ;
coherence by Th10;

end;

theorem Th12: :: RADIX_3:12

for i, n, k being Nat
for aSub being Tuple of n,(k -SD_Sub ) st i in Seg n holds
aSub . i is Element of k -SD_Sub

proof end;

definition

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

end;

:: deftheorem Def3 defines SDSub_Add_Carry RADIX_3:def 3 :

definition

let x be Integer;
let k be Nat;
func SDSub_Add_Data x,k -> Integer equals :: RADIX_3:def 4
x - ((Radix k) * (SDSub_Add_Carry x,k));
coherence ;

end;

:: deftheorem defines SDSub_Add_Data RADIX_3:def 4 :

theorem Th13: :: RADIX_3:13

for x being Integer
for k being Nat st 2 <= k holds
( - 1 <= SDSub_Add_Carry x,k & SDSub_Add_Carry x,k <= 1 )

proof end;

theorem Th14: :: RADIX_3:14

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

proof end;

theorem Th15: :: RADIX_3:15

for x being Integer
for k being Nat st 2 <= k holds
SDSub_Add_Carry x,k in k -SD_Sub_S

proof end;

theorem Th16: :: RADIX_3:16

for k being Nat
for i1, i2 being Integer st 2 <= k & i1 in k -SD & i2 in k -SD holds
(SDSub_Add_Data i1,k) + (SDSub_Add_Carry i2,k) in k -SD_Sub

proof end;

theorem Th17: :: RADIX_3:17

for k being Nat st 2 <= k holds
SDSub_Add_Carry 0,k = 0

proof end;

definition

let i, k, n be Nat;
let x be Tuple of n,(k -SD_Sub );
func DigA_SDSub x,i -> Integer equals :Def5: :: RADIX_3:def 5
x . i if i in Seg n
0 if i = 0
;
coherence

proof end;

consistency by FINSEQ_1:3;

end;

:: deftheorem Def5 defines DigA_SDSub RADIX_3:def 5 :

definition

let i, k, n be Nat;
let x be Tuple of n,(k -SD );
func SD2SDSubDigit x,i,k -> Integer equals :Def6: :: RADIX_3:def 6
(SDSub_Add_Data (DigA x,i),k) + (SDSub_Add_Carry (DigA x,(i -' 1)),k) if i in Seg n
SDSub_Add_Carry (DigA x,(i -' 1)),k if i = n + 1
otherwise 0;
coherence ;
consistency

proof end;

end;

:: deftheorem Def6 defines SD2SDSubDigit RADIX_3:def 6 :

theorem Th18: :: RADIX_3:18

for k, i, n being Nat
for a being Tuple of n,(k -SD ) st 2 <= k & i in Seg (n + 1) holds
SD2SDSubDigit a,i,k is Element of k -SD_Sub

proof end;

definition

let i, k, n be Nat;
let x be Tuple of n,(k -SD );
assume A1: ( 2 <= k & i in Seg (n + 1) ) ;
func SD2SDSubDigitS x,i,k -> Element of k -SD_Sub equals :Def7: :: RADIX_3:def 7
SD2SDSubDigit x,i,k;
coherence by A1, Th18;

end;

:: deftheorem Def7 defines SD2SDSubDigitS RADIX_3:def 7 :

definition

let n, k be Nat;
let x be Tuple of n,(k -SD );
func SD2SDSub x -> Tuple of (n + 1),(k -SD_Sub ) means :Def8: :: RADIX_3:def 8
for i being Nat st i in Seg (n + 1) holds
DigA_SDSub it,i = SD2SDSubDigitS x,i,k;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines SD2SDSub RADIX_3:def 8 :

theorem :: RADIX_3:19

for i, n, k being Nat
for aSub being Tuple of n,(k -SD_Sub ) st i in Seg n holds
DigA_SDSub aSub,i is Element of k -SD_Sub

proof end;

theorem :: RADIX_3:20

for k being Nat
for i1, i2 being Integer st 2 <= k & i1 in k -SD & i2 in k -SD_Sub holds
SDSub_Add_Data (i1 + i2),k in k -SD_Sub_S

proof end;

definition

let i, k, n be Nat;
let x be Tuple of n,(k -SD_Sub );
func DigB_SDSub x,i -> Element of INT equals :: RADIX_3:def 9
DigA_SDSub x,i;
coherence by INT_1:def 2;

end;

:: deftheorem defines DigB_SDSub RADIX_3:def 9 :

definition

let i, k, n be Nat;
let x be Tuple of n,(k -SD_Sub );
func SDSub2INTDigit x,i,k -> Element of INT equals :: RADIX_3:def 10
((Radix k) |^ (i -' 1)) * (DigB_SDSub x,i);
coherence by INT_1:def 2;

end;

:: deftheorem defines SDSub2INTDigit RADIX_3:def 10 :

definition

let n, k be Nat;
let x be Tuple of n,(k -SD_Sub );
func SDSub2INT x -> Tuple of n,INT means :Def11: :: RADIX_3:def 11
for i being Nat st i in Seg n holds
it /. i = SDSub2INTDigit x,i,k;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines SDSub2INT RADIX_3:def 11 :

definition

let n, k be Nat;
let x be Tuple of n,(k -SD_Sub );
func SDSub2IntOut x -> Integer equals :: RADIX_3:def 12
Sum (SDSub2INT x);
coherence ;

end;

:: deftheorem defines SDSub2IntOut RADIX_3:def 12 :

theorem Th21: :: RADIX_3:21

for n, k, m, i being Nat st i in Seg n & 2 <= k holds
DigA_SDSub (SD2SDSub (DecSD m,(n + 1),k)),i = DigA_SDSub (SD2SDSub (DecSD (m mod ((Radix k) |^ n)),n,k)),i

proof end;

theorem :: RADIX_3:22

for n being Nat st n >= 1 holds
for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD x,n,k))

proof end;