:: by Masaaki Niimura and Yasushi Fuwa

::

:: Received January 3, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

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;

coherence

{ e where e is Element of INT : ( e >= - (Radix (k -' 1)) & e <= (Radix (k -' 1)) - 1 ) } is set ;

;

coherence

{ e where e is Element of INT : ( e >= (- (Radix (k -' 1))) - 1 & e <= Radix (k -' 1) ) } is set ;

;

end;
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 { e where e is Element of INT : ( e >= - (Radix (k -' 1)) & e <= (Radix (k -' 1)) - 1 ) } ;

coherence

{ e where e is Element of INT : ( e >= - (Radix (k -' 1)) & e <= (Radix (k -' 1)) - 1 ) } is set ;

;

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 { e where e is Element of INT : ( e >= (- (Radix (k -' 1))) - 1 & e <= Radix (k -' 1) ) } ;

coherence

{ e where e is Element of INT : ( e >= (- (Radix (k -' 1))) - 1 & e <= Radix (k -' 1) ) } is set ;

;

:: deftheorem defines -SD_Sub_S RADIX_3:def 1 :

for k being Nat holds k -SD_Sub_S = { e where e is Element of INT : ( e >= - (Radix (k -' 1)) & e <= (Radix (k -' 1)) - 1 ) } ;

for k being Nat holds k -SD_Sub_S = { e where e is Element of INT : ( e >= - (Radix (k -' 1)) & e <= (Radix (k -' 1)) - 1 ) } ;

:: deftheorem defines -SD_Sub RADIX_3:def 2 :

for k being Nat holds k -SD_Sub = { e where e is Element of INT : ( e >= (- (Radix (k -' 1))) - 1 & e <= Radix (k -' 1) ) } ;

for k being Nat holds k -SD_Sub = { e where e is Element of INT : ( e >= (- (Radix (k -' 1))) - 1 & e <= Radix (k -' 1) ) } ;

theorem Th1: :: RADIX_3:1

for k being Nat

for i1 being Integer st i1 in k -SD_Sub holds

( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) )

for i1 being Integer st i1 in k -SD_Sub holds

( (- (Radix (k -' 1))) - 1 <= i1 & i1 <= Radix (k -' 1) )

proof end;

registration
end;

definition

let k be Nat;

:: original: -SD_Sub_S

redefine func k -SD_Sub_S -> non empty Subset of INT;

coherence

k -SD_Sub_S is non empty Subset of INT by Th10;

end;
:: original: -SD_Sub_S

redefine func k -SD_Sub_S -> non empty Subset of INT;

coherence

k -SD_Sub_S is non empty Subset of INT by Th10;

definition

let k be Nat;

:: original: -SD_Sub

redefine func k -SD_Sub -> non empty Subset of INT;

coherence

k -SD_Sub is non empty Subset of INT by Th9;

end;
:: original: -SD_Sub

redefine func k -SD_Sub -> non empty Subset of INT;

coherence

k -SD_Sub is non empty Subset of INT by Th9;

theorem Th11: :: RADIX_3:11

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

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;

( ( Radix (k -' 1) <= x implies 1 is Integer ) & ( x < - (Radix (k -' 1)) implies - 1 is Integer ) & ( not Radix (k -' 1) <= x & not x < - (Radix (k -' 1)) implies 0 is Integer ) ) ;

consistency

for b_{1} being Integer st Radix (k -' 1) <= x & x < - (Radix (k -' 1)) holds

( b_{1} = 1 iff b_{1} = - 1 )
;

end;
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 1 if Radix (k -' 1) <= x

- 1 if x < - (Radix (k -' 1))

otherwise 0 ;

( ( Radix (k -' 1) <= x implies 1 is Integer ) & ( x < - (Radix (k -' 1)) implies - 1 is Integer ) & ( not Radix (k -' 1) <= x & not x < - (Radix (k -' 1)) implies 0 is Integer ) ) ;

consistency

for b

( b

:: deftheorem Def3 defines SDSub_Add_Carry RADIX_3:def 3 :

for x being Integer

for k being Nat holds

( ( Radix (k -' 1) <= x implies SDSub_Add_Carry (x,k) = 1 ) & ( x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = - 1 ) & ( not Radix (k -' 1) <= x & not x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = 0 ) );

for x being Integer

for k being Nat holds

( ( Radix (k -' 1) <= x implies SDSub_Add_Carry (x,k) = 1 ) & ( x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = - 1 ) & ( not Radix (k -' 1) <= x & not x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = 0 ) );

definition

let x be Integer;

let k be Nat;

x - ((Radix k) * (SDSub_Add_Carry (x,k))) is Integer ;

end;
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 x - ((Radix k) * (SDSub_Add_Carry (x,k)));

x - ((Radix k) * (SDSub_Add_Carry (x,k))) is Integer ;

:: deftheorem defines SDSub_Add_Data RADIX_3:def 4 :

for x being Integer

for k being Nat holds SDSub_Add_Data (x,k) = x - ((Radix k) * (SDSub_Add_Carry (x,k)));

for x being Integer

for k being Nat holds SDSub_Add_Data (x,k) = x - ((Radix k) * (SDSub_Add_Carry (x,k)));

theorem Th12: :: RADIX_3:12

for x being Integer

for k being Nat holds

( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )

for k being Nat holds

( - 1 <= SDSub_Add_Carry (x,k) & SDSub_Add_Carry (x,k) <= 1 )

proof end;

theorem Th13: :: RADIX_3:13

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 )

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 k being Nat

for i1, i2 being Integer st 2 <= k & i1 in k -SD holds

(SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub

for i1, i2 being Integer st 2 <= k & i1 in k -SD holds

(SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub

proof end;

definition

let i, k, n be Nat;

let x be Tuple of n,k -SD_Sub ;

coherence

( ( i in Seg n implies x . i is Integer ) & ( i = 0 implies 0 is Integer ) ) by INT_1:def 2;

consistency

for b_{1} being Integer st i in Seg n & i = 0 holds

( b_{1} = x . i iff b_{1} = 0 )
by FINSEQ_1:1;

end;
let x be Tuple of n,k -SD_Sub ;

coherence

( ( i in Seg n implies x . i is Integer ) & ( i = 0 implies 0 is Integer ) ) by INT_1:def 2;

consistency

for b

( b

:: deftheorem Def5 defines DigA_SDSub RADIX_3:def 5 :

for i, k, n being Nat

for x being Tuple of n,k -SD_Sub holds

( ( i in Seg n implies DigA_SDSub (x,i) = x . i ) & ( i = 0 implies DigA_SDSub (x,i) = 0 ) );

for i, k, n being Nat

for x being Tuple of n,k -SD_Sub holds

( ( i in Seg n implies DigA_SDSub (x,i) = x . i ) & ( i = 0 implies DigA_SDSub (x,i) = 0 ) );

definition

let i, k, n be Nat;

let x be Tuple of n,k -SD ;

( ( i in Seg n implies (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) is Integer ) & ( i = n + 1 implies SDSub_Add_Carry ((DigA (x,(i -' 1))),k) is Integer ) & ( not i in Seg n & not i = n + 1 implies 0 is Integer ) ) ;

consistency

for b_{1} being Integer st i in Seg n & i = n + 1 holds

( b_{1} = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) iff b_{1} = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) )

end;
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 (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 ;

( ( i in Seg n implies (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) is Integer ) & ( i = n + 1 implies SDSub_Add_Carry ((DigA (x,(i -' 1))),k) is Integer ) & ( not i in Seg n & not i = n + 1 implies 0 is Integer ) ) ;

consistency

for b

( b

proof end;

:: deftheorem Def6 defines SD2SDSubDigit RADIX_3:def 6 :

for i, k, n being Nat

for x being Tuple of n,k -SD holds

( ( i in Seg n implies SD2SDSubDigit (x,i,k) = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) ) & ( i = n + 1 implies SD2SDSubDigit (x,i,k) = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) ) & ( not i in Seg n & not i = n + 1 implies SD2SDSubDigit (x,i,k) = 0 ) );

for i, k, n being Nat

for x being Tuple of n,k -SD holds

( ( i in Seg n implies SD2SDSubDigit (x,i,k) = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) ) & ( i = n + 1 implies SD2SDSubDigit (x,i,k) = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) ) & ( not i in Seg n & not i = n + 1 implies SD2SDSubDigit (x,i,k) = 0 ) );

theorem Th17: :: RADIX_3:17

for i, n, k 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

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) ) ;

SD2SDSubDigit (x,i,k) is Element of k -SD_Sub by A1, Th17;

end;
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 SD2SDSubDigit (x,i,k);

SD2SDSubDigit (x,i,k) is Element of k -SD_Sub by A1, Th17;

:: deftheorem Def7 defines SD2SDSubDigitS RADIX_3:def 7 :

for i, k, n being Nat

for x being Tuple of n,k -SD st 2 <= k & i in Seg (n + 1) holds

SD2SDSubDigitS (x,i,k) = SD2SDSubDigit (x,i,k);

for i, k, n being Nat

for x being Tuple of n,k -SD st 2 <= k & i in Seg (n + 1) holds

SD2SDSubDigitS (x,i,k) = SD2SDSubDigit (x,i,k);

definition

let n, k be Nat;

let x be Tuple of n,k -SD ;

ex b_{1} being Tuple of n + 1,k -SD_Sub st

for i being Nat st i in Seg (n + 1) holds

DigA_SDSub (b_{1},i) = SD2SDSubDigitS (x,i,k)

for b_{1}, b_{2} being Tuple of n + 1,k -SD_Sub st ( for i being Nat st i in Seg (n + 1) holds

DigA_SDSub (b_{1},i) = SD2SDSubDigitS (x,i,k) ) & ( for i being Nat st i in Seg (n + 1) holds

DigA_SDSub (b_{2},i) = SD2SDSubDigitS (x,i,k) ) holds

b_{1} = b_{2}

end;
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 for i being Nat st i in Seg (n + 1) holds

DigA_SDSub (it,i) = SD2SDSubDigitS (x,i,k);

ex b

for i being Nat st i in Seg (n + 1) holds

DigA_SDSub (b

proof end;

uniqueness for b

DigA_SDSub (b

DigA_SDSub (b

b

proof end;

:: deftheorem Def8 defines SD2SDSub RADIX_3:def 8 :

for n, k being Nat

for x being Tuple of n,k -SD

for b_{4} being Tuple of n + 1,k -SD_Sub holds

( b_{4} = SD2SDSub x iff for i being Nat st i in Seg (n + 1) holds

DigA_SDSub (b_{4},i) = SD2SDSubDigitS (x,i,k) );

for n, k being Nat

for x being Tuple of n,k -SD

for b

( b

DigA_SDSub (b

theorem :: RADIX_3:18

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

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:19

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

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 ;

coherence

DigA_SDSub (x,i) is Element of INT by INT_1:def 2;

end;
let x be Tuple of n,k -SD_Sub ;

coherence

DigA_SDSub (x,i) is Element of INT by INT_1:def 2;

:: deftheorem defines DigB_SDSub RADIX_3:def 9 :

for i, k, n being Nat

for x being Tuple of n,k -SD_Sub holds DigB_SDSub (x,i) = DigA_SDSub (x,i);

for i, k, n being Nat

for x being Tuple of n,k -SD_Sub holds DigB_SDSub (x,i) = DigA_SDSub (x,i);

definition

let i, k, n be Nat;

let x be Tuple of n,k -SD_Sub ;

((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i)) is Element of INT by INT_1:def 2;

end;
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 ((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i));

((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i)) is Element of INT by INT_1:def 2;

:: deftheorem defines SDSub2INTDigit RADIX_3:def 10 :

for i, k, n being Nat

for x being Tuple of n,k -SD_Sub holds SDSub2INTDigit (x,i,k) = ((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i));

for i, k, n being Nat

for x being Tuple of n,k -SD_Sub holds SDSub2INTDigit (x,i,k) = ((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i));

definition

let n, k be Nat;

let x be Tuple of n,k -SD_Sub ;

ex b_{1} being Tuple of n, INT st

for i being Nat st i in Seg n holds

b_{1} /. i = SDSub2INTDigit (x,i,k)

for b_{1}, b_{2} being Tuple of n, INT st ( for i being Nat st i in Seg n holds

b_{1} /. i = SDSub2INTDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds

b_{2} /. i = SDSub2INTDigit (x,i,k) ) holds

b_{1} = b_{2}

end;
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 for i being Nat st i in Seg n holds

it /. i = SDSub2INTDigit (x,i,k);

ex b

for i being Nat st i in Seg n holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def11 defines SDSub2INT RADIX_3:def 11 :

for n, k being Nat

for x being Tuple of n,k -SD_Sub

for b_{4} being Tuple of n, INT holds

( b_{4} = SDSub2INT x iff for i being Nat st i in Seg n holds

b_{4} /. i = SDSub2INTDigit (x,i,k) );

for n, k being Nat

for x being Tuple of n,k -SD_Sub

for b

( b

b

definition
end;

:: deftheorem defines SDSub2IntOut RADIX_3:def 12 :

for n, k being Nat

for x being Tuple of n,k -SD_Sub holds SDSub2IntOut x = Sum (SDSub2INT x);

for n, k being Nat

for x being Tuple of n,k -SD_Sub holds SDSub2IntOut x = Sum (SDSub2INT x);

theorem Th20: :: RADIX_3:20

for n, m, k, 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)

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:21

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)))

for k, x being Nat st k >= 2 & x is_represented_by n,k holds

x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))

proof end;