:: Magnitude Relation Properties of Radix-$2^k$ SD Number
:: by Masaaki Niimura and Yasushi Fuwa
::
:: Copyright (c) 2003-2018 Association of Mizar Users

for k being Nat st k >= 2 holds
() - 1 in k -SD
proof end;

for i, n being Nat st i > 1 & i in Seg n holds
i -' 1 in Seg n
proof end;

for k being Nat st 2 <= k holds
proof end;

for k being Nat
for tx being Tuple of 1,k -SD holds SDDec tx = DigA (tx,1)
proof end;

for i, k, n being Nat st i in Seg n holds
DigA ((DecSD (0,n,k)),i) = 0
proof end;

for n, k being Nat st n >= 1 holds
SDDec (DecSD (0,n,k)) = 0
proof end;

for k, n being Nat st 1 in Seg n & k >= 2 holds
DigA ((DecSD (1,n,k)),1) = 1
proof end;

for i, k, n being Nat st i in Seg n & i > 1 & k >= 2 holds
DigA ((DecSD (1,n,k)),i) = 0
proof end;

for n, k being Nat st n >= 1 & k >= 2 holds
SDDec (DecSD (1,n,k)) = 1
proof end;

for k being Nat st k >= 2 holds
proof end;

for k being Nat st k >= 2 holds
proof end;

Lm1: for k being Nat st 2 <= k holds
SD_Add_Carry (() - 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;

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

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

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

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

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func SDMinDigit (m,k,i) -> Element of k -SD equals :Def1: :: RADIX_5:def 1
(- ()) + 1 if ( 1 <= i & i < m )
otherwise 0 ;
coherence
( ( 1 <= i & i < m implies (- ()) + 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD holds verum
;
end;

:: 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) = (- ()) + 1 ) & ( ( not 1 <= i or not i < m ) implies SDMinDigit (m,k,i) = 0 ) );

definition
let n, m, k be Nat;
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
ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA (b1,i) = SDMinDigit (m,k,i)
proof end;
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = SDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = SDMinDigit (m,k,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines SDMin RADIX_5:def 2 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = SDMin (n,m,k) iff for i being Nat st i in Seg n holds
DigA (b4,i) = SDMinDigit (m,k,i) );

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func SDMaxDigit (m,k,i) -> Element of k -SD equals :Def3: :: RADIX_5:def 3
() - 1 if ( 1 <= i & i < m )
otherwise 0 ;
coherence
( ( 1 <= i & i < m implies () - 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) )
by ;
consistency
for b1 being Element of k -SD holds verum
;
end;

:: 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) = () - 1 ) & ( ( not 1 <= i or not i < m ) implies SDMaxDigit (m,k,i) = 0 ) );

definition
let n, m, k be Nat;
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
ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA (b1,i) = SDMaxDigit (m,k,i)
proof end;
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = SDMaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = SDMaxDigit (m,k,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines SDMax RADIX_5:def 4 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = SDMax (n,m,k) iff for i being Nat st i in Seg n holds
DigA (b4,i) = SDMaxDigit (m,k,i) );

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func FminDigit (m,k,i) -> Element of k -SD equals :Def5: :: RADIX_5:def 5
1 if i = m
otherwise 0 ;
coherence
( ( i = m implies 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) )
proof end;
consistency
for b1 being Element of k -SD holds verum
;
end;

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

definition
let n, m, k be Nat;
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
ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA (b1,i) = FminDigit (m,k,i)
proof end;
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = FminDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = FminDigit (m,k,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Fmin RADIX_5:def 6 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = Fmin (n,m,k) iff for i being Nat st i in Seg n holds
DigA (b4,i) = FminDigit (m,k,i) );

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func FmaxDigit (m,k,i) -> Element of k -SD equals :Def7: :: RADIX_5:def 7
() - 1 if i = m
otherwise 0 ;
coherence
( ( i = m implies () - 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) )
by ;
consistency
for b1 being Element of k -SD holds verum
;
end;

:: 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) = () - 1 ) & ( not i = m implies FmaxDigit (m,k,i) = 0 ) );

definition
let n, m, k be Nat;
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
ex b1 being Tuple of n,k -SD st
for i being Nat st i in Seg n holds
DigA (b1,i) = FmaxDigit (m,k,i)
proof end;
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = FmaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = FmaxDigit (m,k,i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Fmax RADIX_5:def 8 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = Fmax (n,m,k) iff for i being Nat st i in Seg n holds
DigA (b4,i) = FmaxDigit (m,k,i) );

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

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

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