:: RADIX_1 semantic presentation

theorem :: RADIX_1:1

canceled;

theorem Th2: :: RADIX_1:2

for n, k being Nat st n mod k = k - 1 holds
(n + 1) mod k = 0

proof end;

theorem Th3: :: RADIX_1:3

for k, n being Nat st k <> 0 & n mod k < k - 1 holds
(n + 1) mod k = (n mod k) + 1

proof end;

theorem Th4: :: RADIX_1:4

for m, k, n being Nat st m <> 0 holds
(k mod (m * n)) mod n = k mod n

proof end;

theorem :: RADIX_1:5

for k, n being Nat holds
( not k <> 0 or (n + 1) mod k = 0 or (n + 1) mod k = (n mod k) + 1 )

proof end;

theorem Th6: :: RADIX_1:6

for i, k, n being Nat st i <> 0 & k <> 0 holds
(n mod (i |^ k)) div (i |^ (k -' 1)) < i

proof end;

theorem Th7: :: RADIX_1:7

for k, n, m being Nat st k <= n holds
m |^ k divides m |^ n

proof end;

theorem :: RADIX_1:8

for i2, i3, i1 being Integer st i2 > 0 & i3 >= 0 holds
(i1 mod (i2 * i3)) mod i3 = i1 mod i3

proof end;

definition

let n be Nat;
func Radix n -> Nat equals :: RADIX_1:def 1
2 to_power n;
correctness

proof end;

end;

:: deftheorem defines Radix RADIX_1:def 1 :

definition

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

end;

:: deftheorem defines -SD RADIX_1:def 2 :

theorem Th9: :: RADIX_1:9

for n being Nat holds Radix n <> 0 by POWER:39;

Lm1: for k being Nat st k >= 2 holds
Radix k >= 2 + 2

proof end;

theorem Th10: :: RADIX_1:10

for e being set holds
( e in 0 -SD iff e = 0 )

proof end;

theorem :: RADIX_1:11

0 -SD = {0} by Th10, TARSKI:def 1;

theorem Th12: :: RADIX_1:12

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

proof end;

theorem Th13: :: RADIX_1:13

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

proof end;

theorem Th14: :: RADIX_1:14

for k being Nat holds k -SD c= INT

proof end;

theorem Th15: :: RADIX_1:15

for k being Nat
for i1 being Integer st i1 in k -SD holds
( i1 <= (Radix k) - 1 & i1 >= (- (Radix k)) + 1 )

proof end;

theorem Th16: :: RADIX_1:16

for k being Nat holds 0 in k -SD

proof end;

registration

let k be Nat;
cluster k -SD -> non empty ;
coherence by Th16;

end;

definition

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

end;

theorem :: RADIX_1:17

canceled;

theorem Th18: :: RADIX_1:18

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

proof end;

definition

let i, k, n be Nat;
let x be Tuple of n,(k -SD );
func DigA x,i -> Integer equals :Def3: :: RADIX_1:def 3
x . i if i in Seg n
0 if i = 0
;
coherence

proof end;

consistency by FINSEQ_1:3;

end;

:: deftheorem Def3 defines DigA RADIX_1:def 3 :

definition

let i, k, n be Nat;
let x be Tuple of n,(k -SD );
func DigB x,i -> Element of INT equals :: RADIX_1:def 4
DigA x,i;
coherence by INT_1:def 2;

end;

:: deftheorem defines DigB RADIX_1:def 4 :

theorem Th19: :: RADIX_1:19

for i, n, k being Nat
for a being Tuple of n,(k -SD ) st i in Seg n holds
DigA a,i is Element of k -SD

proof end;

theorem Th20: :: RADIX_1:20

for m being Nat
for x being Tuple of 1,INT st x /. 1 = m holds
x = <*m*>

proof end;

definition

let i, k, n be Nat;
let x be Tuple of n,(k -SD );
func SubDigit x,i,k -> Element of INT equals :: RADIX_1:def 5
((Radix k) |^ (i -' 1)) * (DigB x,i);
coherence by INT_1:def 2;

end;

:: deftheorem defines SubDigit RADIX_1:def 5 :

definition

let n, k be Nat;
let x be Tuple of n,(k -SD );
func DigitSD x -> Tuple of n,INT means :Def6: :: RADIX_1:def 6
for i being Nat st i in Seg n holds
it /. i = SubDigit x,i,k;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines DigitSD RADIX_1:def 6 :

definition

let n, k be Nat;
let x be Tuple of n,(k -SD );
func SDDec x -> Integer equals :: RADIX_1:def 7
Sum (DigitSD x);
coherence ;

end;

:: deftheorem defines SDDec RADIX_1:def 7 :

definition

let i, k, x be Nat;
func DigitDC x,i,k -> Element of k -SD equals :: RADIX_1:def 8
(x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));
coherence

proof end;

end;

:: deftheorem defines DigitDC RADIX_1:def 8 :

definition

let k, n, x be Nat;
func DecSD x,n,k -> Tuple of n,(k -SD ) means :Def9: :: RADIX_1:def 9
for i being Nat st i in Seg n holds
DigA it,i = DigitDC x,i,k;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines DecSD RADIX_1:def 9 :

definition

let x be Integer;
func SD_Add_Carry x -> Integer equals :Def10: :: RADIX_1:def 10
1 if x > 2
- 1 if x < - 2
otherwise 0;
coherence ;
consistency ;

end;

:: deftheorem Def10 defines SD_Add_Carry RADIX_1:def 10 :

theorem Th21: :: RADIX_1:21

SD_Add_Carry 0 = 0 by Def10;

Lm2: for x being Integer holds
( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )

proof end;

definition

let x be Integer;
let k be Nat;
func SD_Add_Data x,k -> Integer equals :: RADIX_1:def 11
x - ((SD_Add_Carry x) * (Radix k));
coherence ;

end;

:: deftheorem defines SD_Add_Data RADIX_1:def 11 :

theorem :: RADIX_1:22

for k being Nat holds SD_Add_Data 0,k = 0 by Th21;

theorem Th23: :: RADIX_1:23

for k being Nat
for i1, i2 being Integer st k >= 2 & i1 in k -SD & i2 in k -SD holds
( (- (Radix k)) + 2 <= SD_Add_Data (i1 + i2),k & SD_Add_Data (i1 + i2),k <= (Radix k) - 2 )

proof end;

definition

let n, x, k be Nat;
pred x is_represented_by n,k means :Def12: :: RADIX_1:def 12
x < (Radix k) |^ n;

end;

:: deftheorem Def12 defines is_represented_by RADIX_1:def 12 :

theorem Th24: :: RADIX_1:24

for m, k being Nat st m is_represented_by 1,k holds
DigA (DecSD m,1,k),1 = m

proof end;

theorem :: RADIX_1:25

for k, n being Nat st n >= 1 holds
for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD m,n,k)

proof end;

theorem Th26: :: RADIX_1:26

for k, m, n being Nat st k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k holds
SD_Add_Carry ((DigA (DecSD m,1,k),1) + (DigA (DecSD n,1,k),1)) = SD_Add_Carry (m + n)

proof end;

Lm3: 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;

theorem Th27: :: RADIX_1:27

for m, n, k being Nat st m is_represented_by n + 1,k holds
DigA (DecSD m,(n + 1),k),(n + 1) = m div ((Radix k) |^ n)

proof end;

definition

let k, i, n be Nat;
let x, y be Tuple of n,(k -SD );
assume A1: ( i in Seg n & k >= 2 ) ;
func Add x,y,i,k -> Element of k -SD equals :Def13: :: RADIX_1:def 13
(SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1))));
coherence

proof end;

end;

:: deftheorem Def13 defines Add RADIX_1:def 13 :

definition

let n, k be Nat;
let x, y be Tuple of n,(k -SD );
func x '+' y -> Tuple of n,(k -SD ) means :Def14: :: RADIX_1:def 14
for i being Nat st i in Seg n holds
DigA it,i = Add x,y,i,k;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines '+' RADIX_1:def 14 :

theorem Th28: :: RADIX_1:28

for k, m, n being Nat st k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k holds
SDDec ((DecSD m,1,k) '+' (DecSD n,1,k)) = SD_Add_Data (m + n),k

proof end;

theorem :: RADIX_1:29

for n being Nat st n >= 1 holds
for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD x,n,k) '+' (DecSD y,n,k))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (DecSD x,n,k),n) + (DigA (DecSD y,n,k),n))))

proof end;