:: by Masaaki Niimura and Yasushi Fuwa

::

:: Received November 7, 2003

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

Lm1: for k being Nat st 2 <= k holds

SD_Add_Carry ((Radix k) - 1) = 1

proof end;

Lm2: for n, k, i being Nat st k >= 2 & i in Seg n holds

SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0

proof end;

theorem Th12: :: RADIX_5:12

for n being Nat st n >= 1 holds

for k being Nat

for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

DigA (tx,i) = DigA (ty,i) ) holds

SDDec tx = SDDec ty

for k being Nat

for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

DigA (tx,i) = DigA (ty,i) ) holds

SDDec tx = SDDec ty

proof end;

theorem :: RADIX_5:13

for n being Nat st n >= 1 holds

for k being Nat

for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

DigA (tx,i) >= DigA (ty,i) ) holds

SDDec tx >= SDDec ty

for k being Nat

for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds

DigA (tx,i) >= DigA (ty,i) ) holds

SDDec tx >= SDDec ty

proof end;

theorem Th14: :: RADIX_5:14

for n being Nat st n >= 1 holds

for k being Nat st k >= 2 holds

for tx, ty, tz, tw being Tuple of n,k -SD st ( for i being Nat holds

( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds

(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)

for k being Nat st k >= 2 holds

for tx, ty, tz, tw being Tuple of n,k -SD st ( for i being Nat holds

( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds

(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)

proof end;

theorem :: RADIX_5:15

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

for tx, ty, tz being Tuple of n,k -SD st ( for i being Nat holds

( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = 0 ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = 0 ) ) ) holds

(SDDec tz) + (SDDec (DecSD (0,n,k))) = (SDDec tx) + (SDDec ty)

for tx, ty, tz being Tuple of n,k -SD st ( for i being Nat holds

( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = 0 ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = 0 ) ) ) holds

(SDDec tz) + (SDDec (DecSD (0,n,k))) = (SDDec tx) + (SDDec ty)

proof end;

definition

let i, m, k be Nat;

assume A1: k >= 2 ;

( ( 1 <= i & i < m implies (- (Radix k)) + 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) )

for b_{1} being Element of k -SD holds verum
;

end;
assume A1: k >= 2 ;

func SDMinDigit (m,k,i) -> Element of k -SD equals :Def1: :: RADIX_5:def 1

(- (Radix k)) + 1 if ( 1 <= i & i < m )

otherwise 0 ;

coherence (- (Radix k)) + 1 if ( 1 <= i & i < m )

otherwise 0 ;

( ( 1 <= i & i < m implies (- (Radix k)) + 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) )

proof end;

consistency for b

:: deftheorem Def1 defines SDMinDigit RADIX_5:def 1 :

for i, m, k being Nat st k >= 2 holds

( ( 1 <= i & i < m implies SDMinDigit (m,k,i) = (- (Radix k)) + 1 ) & ( ( not 1 <= i or not i < m ) implies SDMinDigit (m,k,i) = 0 ) );

for i, m, k being Nat st k >= 2 holds

( ( 1 <= i & i < m implies SDMinDigit (m,k,i) = (- (Radix k)) + 1 ) & ( ( not 1 <= i or not i < m ) implies SDMinDigit (m,k,i) = 0 ) );

definition

let n, m, k be Nat;

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

for i being Nat st i in Seg n holds

DigA (b_{1},i) = SDMinDigit (m,k,i)

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

DigA (b_{1},i) = SDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds

DigA (b_{2},i) = SDMinDigit (m,k,i) ) holds

b_{1} = b_{2}

end;
func SDMin (n,m,k) -> Tuple of n,k -SD means :Def2: :: RADIX_5:def 2

for i being Nat st i in Seg n holds

DigA (it,i) = SDMinDigit (m,k,i);

existence for i being Nat st i in Seg n holds

DigA (it,i) = SDMinDigit (m,k,i);

ex b

for i being Nat st i in Seg n holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def2 defines SDMin RADIX_5:def 2 :

for n, m, k being Nat

for b_{4} being Tuple of n,k -SD holds

( b_{4} = SDMin (n,m,k) iff for i being Nat st i in Seg n holds

DigA (b_{4},i) = SDMinDigit (m,k,i) );

for n, m, k being Nat

for b

( b

DigA (b

definition

let i, m, k be Nat;

assume A1: k >= 2 ;

( ( 1 <= i & i < m implies (Radix k) - 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) ) by A1, Th1, RADIX_1:14;

consistency

for b_{1} being Element of k -SD holds verum
;

end;
assume A1: k >= 2 ;

func SDMaxDigit (m,k,i) -> Element of k -SD equals :Def3: :: RADIX_5:def 3

(Radix k) - 1 if ( 1 <= i & i < m )

otherwise 0 ;

coherence (Radix k) - 1 if ( 1 <= i & i < m )

otherwise 0 ;

( ( 1 <= i & i < m implies (Radix k) - 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) ) by A1, Th1, RADIX_1:14;

consistency

for b

:: deftheorem Def3 defines SDMaxDigit RADIX_5:def 3 :

for i, m, k being Nat st k >= 2 holds

( ( 1 <= i & i < m implies SDMaxDigit (m,k,i) = (Radix k) - 1 ) & ( ( not 1 <= i or not i < m ) implies SDMaxDigit (m,k,i) = 0 ) );

for i, m, k being Nat st k >= 2 holds

( ( 1 <= i & i < m implies SDMaxDigit (m,k,i) = (Radix k) - 1 ) & ( ( not 1 <= i or not i < m ) implies SDMaxDigit (m,k,i) = 0 ) );

definition

let n, m, k be Nat;

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

for i being Nat st i in Seg n holds

DigA (b_{1},i) = SDMaxDigit (m,k,i)

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

DigA (b_{1},i) = SDMaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds

DigA (b_{2},i) = SDMaxDigit (m,k,i) ) holds

b_{1} = b_{2}

end;
func SDMax (n,m,k) -> Tuple of n,k -SD means :Def4: :: RADIX_5:def 4

for i being Nat st i in Seg n holds

DigA (it,i) = SDMaxDigit (m,k,i);

existence for i being Nat st i in Seg n holds

DigA (it,i) = SDMaxDigit (m,k,i);

ex b

for i being Nat st i in Seg n holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def4 defines SDMax RADIX_5:def 4 :

for n, m, k being Nat

for b_{4} being Tuple of n,k -SD holds

( b_{4} = SDMax (n,m,k) iff for i being Nat st i in Seg n holds

DigA (b_{4},i) = SDMaxDigit (m,k,i) );

for n, m, k being Nat

for b

( b

DigA (b

definition

let i, m, k be Nat;

assume A1: k >= 2 ;

coherence

( ( i = m implies 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) )

for b_{1} being Element of k -SD holds verum
;

end;
assume A1: k >= 2 ;

coherence

( ( i = m implies 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) )

proof end;

consistency for b

:: deftheorem Def5 defines FminDigit RADIX_5:def 5 :

for i, m, k being Nat st k >= 2 holds

( ( i = m implies FminDigit (m,k,i) = 1 ) & ( not i = m implies FminDigit (m,k,i) = 0 ) );

for i, m, k being Nat st k >= 2 holds

( ( i = m implies FminDigit (m,k,i) = 1 ) & ( not i = m implies FminDigit (m,k,i) = 0 ) );

definition

let n, m, k be Nat;

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

for i being Nat st i in Seg n holds

DigA (b_{1},i) = FminDigit (m,k,i)

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

DigA (b_{1},i) = FminDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds

DigA (b_{2},i) = FminDigit (m,k,i) ) holds

b_{1} = b_{2}

end;
func Fmin (n,m,k) -> Tuple of n,k -SD means :Def6: :: RADIX_5:def 6

for i being Nat st i in Seg n holds

DigA (it,i) = FminDigit (m,k,i);

existence for i being Nat st i in Seg n holds

DigA (it,i) = FminDigit (m,k,i);

ex b

for i being Nat st i in Seg n holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def6 defines Fmin RADIX_5:def 6 :

for n, m, k being Nat

for b_{4} being Tuple of n,k -SD holds

( b_{4} = Fmin (n,m,k) iff for i being Nat st i in Seg n holds

DigA (b_{4},i) = FminDigit (m,k,i) );

for n, m, k being Nat

for b

( b

DigA (b

definition

let i, m, k be Nat;

assume A1: k >= 2 ;

( ( i = m implies (Radix k) - 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) ) by A1, Th1, RADIX_1:14;

consistency

for b_{1} being Element of k -SD holds verum
;

end;
assume A1: k >= 2 ;

func FmaxDigit (m,k,i) -> Element of k -SD equals :Def7: :: RADIX_5:def 7

(Radix k) - 1 if i = m

otherwise 0 ;

coherence (Radix k) - 1 if i = m

otherwise 0 ;

( ( i = m implies (Radix k) - 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) ) by A1, Th1, RADIX_1:14;

consistency

for b

:: deftheorem Def7 defines FmaxDigit RADIX_5:def 7 :

for i, m, k being Nat st k >= 2 holds

( ( i = m implies FmaxDigit (m,k,i) = (Radix k) - 1 ) & ( not i = m implies FmaxDigit (m,k,i) = 0 ) );

for i, m, k being Nat st k >= 2 holds

( ( i = m implies FmaxDigit (m,k,i) = (Radix k) - 1 ) & ( not i = m implies FmaxDigit (m,k,i) = 0 ) );

definition

let n, m, k be Nat;

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

for i being Nat st i in Seg n holds

DigA (b_{1},i) = FmaxDigit (m,k,i)

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

DigA (b_{1},i) = FmaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds

DigA (b_{2},i) = FmaxDigit (m,k,i) ) holds

b_{1} = b_{2}

end;
func Fmax (n,m,k) -> Tuple of n,k -SD means :Def8: :: RADIX_5:def 8

for i being Nat st i in Seg n holds

DigA (it,i) = FmaxDigit (m,k,i);

existence for i being Nat st i in Seg n holds

DigA (it,i) = FmaxDigit (m,k,i);

ex b

for i being Nat st i in Seg n holds

DigA (b

proof end;

uniqueness for b

DigA (b

DigA (b

b

proof end;

:: deftheorem Def8 defines Fmax RADIX_5:def 8 :

for n, m, k being Nat

for b_{4} being Tuple of n,k -SD holds

( b_{4} = Fmax (n,m,k) iff for i being Nat st i in Seg n holds

DigA (b_{4},i) = FmaxDigit (m,k,i) );

for n, m, k being Nat

for b

( b

DigA (b

theorem Th16: :: RADIX_5:16

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

for i being Nat st i in Seg n holds

(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0

for i being Nat st i in Seg n holds

(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0

proof end;

theorem :: RADIX_5:17

for n being Nat st n >= 1 holds

for m, k being Nat st k >= 2 holds

(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k))

for m, k being Nat st k >= 2 holds

(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k))

proof end;

theorem :: RADIX_5:18

for n being Nat st n >= 1 holds

for m, k being Nat st m in Seg n & k >= 2 holds

SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))

for m, k being Nat st m in Seg n & k >= 2 holds

SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))

proof end;

theorem :: RADIX_5:19

for n, m, k being Nat st m in Seg n & k >= 2 holds

SDDec (Fmin ((n + 1),(m + 1),k)) = (SDDec (Fmin ((n + 1),m,k))) + (SDDec (Fmax ((n + 1),m,k)))

SDDec (Fmin ((n + 1),(m + 1),k)) = (SDDec (Fmin ((n + 1),m,k))) + (SDDec (Fmax ((n + 1),m,k)))

proof end;