:: by Masaaki Niimura and Yasushi Fuwa

::

:: Received January 3, 2003

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

Lm1: for k being Nat

for i1 being Integer st i1 in k -SD_Sub_S holds

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

proof end;

Lm2: for n, m, k, i being Nat st i in Seg n holds

DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i)

proof end;

Lm3: for k, x, n being Nat st n >= 1 holds

DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n)

proof end;

theorem Th2: :: RADIX_4:2

for x, y being Integer

for k being Nat st 3 <= k holds

SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0

for k being Nat st 3 <= k holds

SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0

proof end;

theorem Th3: :: RADIX_4:3

for n, m, k being Nat st 2 <= k holds

DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k)

DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k)

proof end;

theorem Th4: :: RADIX_4:4

for m, k being Nat st 2 <= k & m is_represented_by 1,k holds

DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),(1 + 1)) = SDSub_Add_Carry (m,k)

DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),(1 + 1)) = SDSub_Add_Carry (m,k)

proof end;

theorem Th5: :: RADIX_4:5

for k, x, n being Nat st n >= 1 & k >= 3 & x is_represented_by n + 1,k holds

DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)

DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)

proof end;

theorem Th6: :: RADIX_4:6

for m, k being Nat st 2 <= k & m is_represented_by 1,k holds

DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k))

DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k))

proof end;

theorem Th7: :: RADIX_4:7

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

((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))

((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))

proof end;

definition

let i, n, k be Nat;

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

assume that

A1: i in Seg n and

A2: k >= 2 ;

(SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k)) is Element of k -SD_Sub

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

assume that

A1: i in Seg n and

A2: k >= 2 ;

func SDSubAddDigit (x,y,i,k) -> Element of k -SD_Sub equals :Def1: :: RADIX_4:def 1

(SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k));

coherence (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k));

(SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k)) is Element of k -SD_Sub

proof end;

:: deftheorem Def1 defines SDSubAddDigit RADIX_4:def 1 :

for i, n, k being Nat

for x, y being Tuple of n,k -SD_Sub st i in Seg n & k >= 2 holds

SDSubAddDigit (x,y,i,k) = (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k));

for i, n, k being Nat

for x, y being Tuple of n,k -SD_Sub st i in Seg n & k >= 2 holds

SDSubAddDigit (x,y,i,k) = (SDSub_Add_Data (((DigA_SDSub (x,i)) + (DigA_SDSub (y,i))),k)) + (SDSub_Add_Carry (((DigA_SDSub (x,(i -' 1))) + (DigA_SDSub (y,(i -' 1)))),k));

definition

let n, k be Nat;

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

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

for i being Nat st i in Seg n holds

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

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

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

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

b_{1} = b_{2}

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

func x '+' y -> Tuple of n,k -SD_Sub means :Def2: :: RADIX_4:def 2

for i being Nat st i in Seg n holds

DigA_SDSub (it,i) = SDSubAddDigit (x,y,i,k);

existence for i being Nat st i in Seg n holds

DigA_SDSub (it,i) = SDSubAddDigit (x,y,i,k);

ex b

for i being Nat st i in Seg n holds

DigA_SDSub (b

proof end;

uniqueness for b

DigA_SDSub (b

DigA_SDSub (b

b

proof end;

:: deftheorem Def2 defines '+' RADIX_4:def 2 :

for n, k being Nat

for x, y, b_{5} being Tuple of n,k -SD_Sub holds

( b_{5} = x '+' y iff for i being Nat st i in Seg n holds

DigA_SDSub (b_{5},i) = SDSubAddDigit (x,y,i,k) );

for n, k being Nat

for x, y, b

( b

DigA_SDSub (b

theorem Th8: :: RADIX_4:8

for n, k, x, y, i being Nat st i in Seg n & 2 <= k holds

SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)

SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)

proof end;

theorem :: RADIX_4:9

for n being Nat st n >= 1 holds

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

x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,n,k))) '+' (SD2SDSub (DecSD (y,n,k))))

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

x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,n,k))) '+' (SD2SDSub (DecSD (y,n,k))))

proof end;