:: RADIX_5 semantic presentation

begin

theorem Th1: :: RADIX_5:1
for k being Nat st k >= 2 holds
(Radix k) - 1 in k -SD
proof
let k be Nat; ::_thesis: ( k >= 2 implies (Radix k) - 1 in k -SD )
assume  k >= 2 ; ::_thesis: (Radix k) - 1 in k -SD
then  Radix k > 2 by RADIX_4:1;
then  Radix k > 1 by XXREAL_0:2;
then  (Radix k) + (Radix k) > 1 + 1 by XREAL_1:8;
then A1: (Radix k) - 1 > (0 + 1) - (Radix k) by XREAL_1:21;
 ( k -SD =  {  w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 )  }  & (Radix k) - 1 is Element of INT ) by INT_1:def_2, RADIX_1:def_2;
hence  (Radix k) - 1 in k -SD by A1; ::_thesis: verum
end;

theorem Th2: :: RADIX_5:2
for i, n being Nat st i > 1 & i in Seg n holds
i -' 1 in Seg n
proof
let i, n be Nat; ::_thesis: ( i > 1 & i in Seg n implies i -' 1 in Seg n )
assume that
A1: i > 1 and
A2: i in Seg n ; ::_thesis: i -' 1 in Seg n
 i - 1 > 1 - 1 by A1, XREAL_1:9;
then  i -' 1 > 0 by A1, XREAL_1:233;
then A3: i -' 1 >= 0 + 1 by NAT_1:13;
 i <= n by A2, FINSEQ_1:1;
then  i -' 1 <= n by NAT_D:44;
hence  i -' 1 in Seg n by A3, FINSEQ_1:1; ::_thesis: verum
end;

theorem Th3: :: RADIX_5:3
for k being Nat st 2 <= k holds
4 <= Radix k
proof
defpred S1[ Nat] means 4 <= Radix $1;
A1: for kk being Nat st kk >= 2 & S1[kk] holds
S1[kk + 1]
proof
let kk be Nat; ::_thesis: ( kk >= 2 & S1[kk] implies S1[kk + 1] )
assume that
 2 <= kk and
A2: 4 <= Radix kk ; ::_thesis: S1[kk + 1]
Radix (kk + 1) = 2 to_power (kk + 1) by RADIX_1:def_1
.= (2 to_power 1) * (2 to_power kk) by POWER:27
.= 2 * (2 to_power kk) by POWER:25
.= 2 * (Radix kk) by RADIX_1:def_1 ;
then  Radix (kk + 1) >= Radix kk by XREAL_1:151;
hence  S1[kk + 1] by A2, XXREAL_0:2; ::_thesis: verum
end;
Radix 2 = 2 to_power (1 + 1) by RADIX_1:def_1
.= (2 to_power 1) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power 1) by POWER:25
.= 2 * 2 by POWER:25 ;
then A3: S1[2] ;
 for i being Nat st 2 <= i holds
S1[i] from NAT_1:sch_8(A3, A1);
hence  for k being Nat st 2 <= k holds
4 <= Radix k ; ::_thesis: verum
end;

theorem Th4: :: RADIX_5:4
for k being Nat
for tx being Tuple of 1,k -SD holds SDDec tx = DigA (tx,1)
proof
let k be Nat; ::_thesis: for tx being Tuple of 1,k -SD holds SDDec tx = DigA (tx,1)
let tx be Tuple of 1,k -SD ; ::_thesis: SDDec tx = DigA (tx,1)
reconsider w = DigA (tx,1) as Element of INT by INT_1:def_2;
A1: 1 in Seg 1 by FINSEQ_1:1;
then A2: (DigitSD tx) /. 1 = SubDigit (tx,1,k) by RADIX_1:def_6
.= ((Radix k) |^ (1 -' 1)) * (DigB (tx,1)) by RADIX_1:def_5
.= ((Radix k) |^ (1 -' 1)) * (DigA (tx,1)) by RADIX_1:def_4
.= ((Radix k) |^ 0) * (DigA (tx,1)) by XREAL_1:232
.= 1 * (DigA (tx,1)) by NEWTON:4 ;
A3: len (DigitSD tx) = 1 by CARD_1:def_7;
then  1 in dom (DigitSD tx) by A1, FINSEQ_1:def_3;
then A4: (DigitSD tx) . 1 = DigA (tx,1) by A2, PARTFUN1:def_6;
SDDec tx = Sum (DigitSD tx) by RADIX_1:def_7
.= Sum <*w*> by A3, A4, FINSEQ_1:40
.= DigA (tx,1) by RVSUM_1:73 ;
hence  SDDec tx = DigA (tx,1) ; ::_thesis: verum
end;

begin

theorem Th5: :: RADIX_5:5
for i, k, n being Nat st i in Seg n holds
DigA ((DecSD (0,n,k)),i) = 0
proof
let i, k, n be Nat; ::_thesis: ( i in Seg n implies DigA ((DecSD (0,n,k)),i) = 0 )
assume A1: i in Seg n ; ::_thesis: DigA ((DecSD (0,n,k)),i) = 0
then A2: i >= 1 by FINSEQ_1:1;
DigA ((DecSD (0,n,k)),i) = DigitDC (0,i,k) by A1, RADIX_1:def_9
.= (0 mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) by RADIX_1:def_8
.= (0 div ((Radix k) |^ (i -' 1))) mod (Radix k) by A2, RADIX_2:4, RADIX_2:6
.= 0 mod (Radix k) by NAT_2:2 ;
hence  DigA ((DecSD (0,n,k)),i) = 0 by NAT_D:26; ::_thesis: verum
end;

theorem :: RADIX_5:6
for n, k being Nat st n >= 1 holds
SDDec (DecSD (0,n,k)) = 0
proof
let n, k be Nat; ::_thesis: ( n >= 1 implies SDDec (DecSD (0,n,k)) = 0 )
 Radix k >= 0 + 1 by INT_1:7, RADIX_2:6;
then  (Radix k) |^ n >= 1 by PREPOWER:11;
then A1: 0 is_represented_by n,k by RADIX_1:def_12;
assume  n >= 1 ; ::_thesis: SDDec (DecSD (0,n,k)) = 0
hence  SDDec (DecSD (0,n,k)) = 0 by A1, RADIX_1:22; ::_thesis: verum
end;

theorem Th7: :: RADIX_5:7
for k, n being Nat st 1 in Seg n & k >= 2 holds
DigA ((DecSD (1,n,k)),1) = 1
proof
let k, n be Nat; ::_thesis: ( 1 in Seg n & k >= 2 implies DigA ((DecSD (1,n,k)),1) = 1 )
assume that
A1: 1 in Seg n and
A2: k >= 2 ; ::_thesis: DigA ((DecSD (1,n,k)),1) = 1
A3: Radix k > 2 by A2, RADIX_4:1;
then A4: Radix k > 1 by XXREAL_0:2;
DigA ((DecSD (1,n,k)),1) = DigitDC (1,1,k) by A1, RADIX_1:def_9
.= (1 mod ((Radix k) |^ 1)) div ((Radix k) |^ (1 -' 1)) by RADIX_1:def_8
.= (1 div ((Radix k) |^ (1 -' 1))) mod (Radix k) by A3, RADIX_2:4
.= (1 div ((Radix k) |^ 0)) mod (Radix k) by NAT_2:8
.= (1 div 1) mod (Radix k) by NEWTON:4
.= 1 mod (Radix k) by NAT_2:4 ;
hence  DigA ((DecSD (1,n,k)),1) = 1 by A4, NAT_D:14; ::_thesis: verum
end;

theorem Th8: :: RADIX_5:8
for i, k, n being Nat st i in Seg n & i > 1 & k >= 2 holds
DigA ((DecSD (1,n,k)),i) = 0
proof
let i, k, n be Nat; ::_thesis: ( i in Seg n & i > 1 & k >= 2 implies DigA ((DecSD (1,n,k)),i) = 0 )
assume that
A1: i in Seg n and
A2: i > 1 and
A3: k >= 2 ; ::_thesis: DigA ((DecSD (1,n,k)),i) = 0
 i - 1 > 1 - 1 by A2, XREAL_1:14;
then A4: i -' 1 > 0 by XREAL_0:def_2;
A5: Radix k > 2 by A3, RADIX_4:1;
then  Radix k > 1 by XXREAL_0:2;
then A6: 1 div ((Radix k) |^ (i -' 1)) = 0 by A4, NAT_D:27, PEPIN:25;
DigA ((DecSD (1,n,k)),i) = DigitDC (1,i,k) by A1, RADIX_1:def_9
.= (1 mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) by RADIX_1:def_8
.= (1 div ((Radix k) |^ (i -' 1))) mod (Radix k) by A2, A5, RADIX_2:4 ;
hence  DigA ((DecSD (1,n,k)),i) = 0 by A6, NAT_D:26; ::_thesis: verum
end;

theorem :: RADIX_5:9
for n, k being Nat st n >= 1 & k >= 2 holds
SDDec (DecSD (1,n,k)) = 1
proof
let n, k be Nat; ::_thesis: ( n >= 1 & k >= 2 implies SDDec (DecSD (1,n,k)) = 1 )
assume that
A1: n >= 1 and
A2: k >= 2 ; ::_thesis: SDDec (DecSD (1,n,k)) = 1
A3: Radix k > 2 by A2, RADIX_4:1;
 Radix k >= 0 + 1 by INT_1:7, RADIX_2:6;
then  (Radix k) |^ n >= Radix k by A1, PREPOWER:12;
then  (Radix k) |^ n >= 2 by A3, XXREAL_0:2;
then  (Radix k) |^ n > 1 by XXREAL_0:2;
then  1 is_represented_by n,k by RADIX_1:def_12;
hence  SDDec (DecSD (1,n,k)) = 1 by A1, RADIX_1:22; ::_thesis: verum
end;

theorem Th10: :: RADIX_5:10
for k being Nat st k >= 2 holds
SD_Add_Carry (Radix k) = 1
proof
let k be Nat; ::_thesis: ( k >= 2 implies SD_Add_Carry (Radix k) = 1 )
assume  k >= 2 ; ::_thesis: SD_Add_Carry (Radix k) = 1
then  Radix k > 2 by RADIX_4:1;
hence  SD_Add_Carry (Radix k) = 1 by RADIX_1:def_10; ::_thesis: verum
end;

theorem Th11: :: RADIX_5:11
for k being Nat st k >= 2 holds
SD_Add_Data ((Radix k),k) = 0
proof
let k be Nat; ::_thesis: ( k >= 2 implies SD_Add_Data ((Radix k),k) = 0 )
assume  k >= 2 ; ::_thesis: SD_Add_Data ((Radix k),k) = 0
then A1: SD_Add_Carry (Radix k) = 1 by Th10;
SD_Add_Data ((Radix k),k) = (Radix k) - ((SD_Add_Carry (Radix k)) * (Radix k)) by RADIX_1:def_11
.= (Radix k) - (Radix k) by A1 ;
hence  SD_Add_Data ((Radix k),k) = 0 ; ::_thesis: verum
end;

begin

Lm1:  for k being Nat st 2 <= k holds
SD_Add_Carry ((Radix k) - 1) = 1
proof
let k be Nat; ::_thesis: ( 2 <= k implies SD_Add_Carry ((Radix k) - 1) = 1 )
assume  k >= 2 ; ::_thesis: SD_Add_Carry ((Radix k) - 1) = 1
then  Radix k >= 4 by Th3;
then  (Radix k) - 1 >= 4 - 1 by XREAL_1:9;
then  (Radix k) - 1 > 2 by XXREAL_0:2;
hence  SD_Add_Carry ((Radix k) - 1) = 1 by RADIX_1:def_10; ::_thesis: verum
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
let n, k, i be Nat; ::_thesis: ( k >= 2 & i in Seg n implies SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0 )
assume that
A1: k >= 2 and
A2: i in Seg n ; ::_thesis: SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0
A3: i >= 1 by A2, FINSEQ_1:1;
now__::_thesis:_SD_Add_Carry_(DigA_((DecSD_(1,n,k)),i))_=_0
percases ( i = 1 or i > 1 ) by A3, XXREAL_0:1;
suppose i = 1 ; ::_thesis: SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0
then  SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = SD_Add_Carry 1 by A1, A2, Th7;
hence  SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0 by RADIX_1:def_10; ::_thesis: verum
end;
suppose i > 1 ; ::_thesis: SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0
then  SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = SD_Add_Carry 0 by A1, A2, Th8;
hence  SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0 by RADIX_1:def_10; ::_thesis: verum
end;
end;
end;
hence  SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0 ; ::_thesis: verum
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
proof
defpred S1[ Nat] means  for k being Nat
for tx, ty being Tuple of $1,k -SD st ( for i being Nat st i in Seg $1 holds
DigA (tx,i) = DigA (ty,i) ) holds
SDDec tx = SDDec ty;
A1: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A2: S1[n] ; ::_thesis: S1[n + 1]
let k be Nat; ::_thesis: for tx, ty being Tuple of n + 1,k -SD st ( for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) = DigA (ty,i) ) holds
SDDec tx = SDDec ty
let tx, ty be Tuple of n + 1,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) = DigA (ty,i) ) implies SDDec tx = SDDec ty )
assume A3: for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) = DigA (ty,i) ; ::_thesis: SDDec tx = SDDec ty
deffunc H1( Nat) ->  Element of INT = DigB (tx,$1);
consider txn being FinSequence of INT  such that
A4: len txn = n and
A5: for i being Nat st i in dom txn holds
txn . i = H1(i) from FINSEQ_2:sch_1();
A6: dom txn = Seg n by A4, FINSEQ_1:def_3;
 rng txn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng txn or z in k -SD )
assume  z in rng txn ; ::_thesis: z in k -SD
then consider xx being set  such that
A7: xx in dom txn and
A8: z = txn . xx by FUNCT_1:def_3;
reconsider xx = xx as Element of NAT by A7;
 dom txn = Seg n by A4, FINSEQ_1:def_3;
then  xx in Seg (n + 1) by A7, FINSEQ_2:8;
then A9: DigA (tx,xx) is Element of k -SD by RADIX_1:16;
z = DigB (tx,xx) by A5, A7, A8
.= DigA (tx,xx) by RADIX_1:def_4 ;
hence  z in k -SD by A9; ::_thesis: verum
end;
then reconsider txn = txn as FinSequence of k -SD by FINSEQ_1:def_4;
A10: for i being Nat st i in Seg n holds
txn . i = tx . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies txn . i = tx . i )
assume A11: i in Seg n ; ::_thesis: txn . i = tx . i
then A12: i in Seg (n + 1) by FINSEQ_2:8;
txn . i = DigB (tx,i) by A5, A6, A11
.= DigA (tx,i) by RADIX_1:def_4 ;
hence  txn . i = tx . i by A12, RADIX_1:def_3; ::_thesis: verum
end;
deffunc H2( Nat) ->  Element of INT = DigB (ty,$1);
consider tyn being FinSequence of INT  such that
A13: len tyn = n and
A14: for i being Nat st i in dom tyn holds
tyn . i = H2(i) from FINSEQ_2:sch_1();
A15: dom tyn = Seg n by A13, FINSEQ_1:def_3;
 rng tyn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng tyn or z in k -SD )
assume  z in rng tyn ; ::_thesis: z in k -SD
then consider yy being set  such that
A16: yy in dom tyn and
A17: z = tyn . yy by FUNCT_1:def_3;
reconsider yy = yy as Element of NAT by A16;
 dom tyn = Seg n by A13, FINSEQ_1:def_3;
then  yy in Seg (n + 1) by A16, FINSEQ_2:8;
then A18: DigA (ty,yy) is Element of k -SD by RADIX_1:16;
z = DigB (ty,yy) by A14, A16, A17
.= DigA (ty,yy) by RADIX_1:def_4 ;
hence  z in k -SD by A18; ::_thesis: verum
end;
then reconsider tyn = tyn as FinSequence of k -SD by FINSEQ_1:def_4;
A19: for i being Nat st i in Seg n holds
tyn . i = ty . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies tyn . i = ty . i )
assume A20: i in Seg n ; ::_thesis: tyn . i = ty . i
then A21: i in Seg (n + 1) by FINSEQ_2:8;
tyn . i = DigB (ty,i) by A14, A15, A20
.= DigA (ty,i) by RADIX_1:def_4 ;
hence  tyn . i = ty . i by A21, RADIX_1:def_3; ::_thesis: verum
end;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 tyn is Element of n -tuples_on (k -SD) by A13, FINSEQ_2:92;
then reconsider tyn = tyn as Tuple of n,k -SD ;
A22: (SDDec tyn) + (((Radix k) |^ n) * (DigA (ty,(n + 1)))) = SDDec ty by A19, RADIX_2:10;
 txn is Element of n -tuples_on (k -SD) by A4, FINSEQ_2:92;
then reconsider txn = txn as Tuple of n,k -SD ;
 for i being Nat st i in Seg n holds
DigA (txn,i) = DigA (tyn,i)
proof
let i be Nat; ::_thesis: ( i in Seg n implies DigA (txn,i) = DigA (tyn,i) )
assume A23: i in Seg n ; ::_thesis: DigA (txn,i) = DigA (tyn,i)
then A24: DigA (tyn,i) = tyn . i by RADIX_1:def_3
.= DigB (ty,i) by A14, A15, A23
.= DigA (ty,i) by RADIX_1:def_4 ;
DigA (txn,i) = txn . i by A23, RADIX_1:def_3
.= DigB (tx,i) by A5, A6, A23
.= DigA (tx,i) by RADIX_1:def_4 ;
hence  DigA (txn,i) = DigA (tyn,i) by A3, A23, A24, FINSEQ_2:8; ::_thesis: verum
end;
then A25: SDDec txn = SDDec tyn by A2;
 (SDDec txn) + (((Radix k) |^ n) * (DigA (tx,(n + 1)))) = SDDec tx by A10, RADIX_2:10;
hence  SDDec tx = SDDec ty by A3, A22, A25, FINSEQ_1:4; ::_thesis: verum
end;
A26: S1[1]
proof
let k be Nat; ::_thesis: for tx, ty being Tuple of 1,k -SD st ( for i being Nat st i in Seg 1 holds
DigA (tx,i) = DigA (ty,i) ) holds
SDDec tx = SDDec ty
let tx, ty be Tuple of 1,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg 1 holds
DigA (tx,i) = DigA (ty,i) ) implies SDDec tx = SDDec ty )
assume A27: for i being Nat st i in Seg 1 holds
DigA (tx,i) = DigA (ty,i) ; ::_thesis: SDDec tx = SDDec ty
A28: SDDec ty = DigA (ty,1) by Th4;
 ( 1 in Seg 1 & SDDec tx = DigA (tx,1) ) by Th4, FINSEQ_1:1;
hence  SDDec tx = SDDec ty by A27, A28; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A26, A1);
hence  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 ; ::_thesis: verum
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
proof
defpred S1[ Nat] means  for k being Nat
for tx, ty being Tuple of $1,k -SD st ( for i being Nat st i in Seg $1 holds
DigA (tx,i) >= DigA (ty,i) ) holds
SDDec tx >= SDDec ty;
A1: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A2: S1[n] ; ::_thesis: S1[n + 1]
let k be Nat; ::_thesis: for tx, ty being Tuple of n + 1,k -SD st ( for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) >= DigA (ty,i) ) holds
SDDec tx >= SDDec ty
let tx, ty be Tuple of n + 1,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) >= DigA (ty,i) ) implies SDDec tx >= SDDec ty )
assume A3: for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) >= DigA (ty,i) ; ::_thesis: SDDec tx >= SDDec ty
reconsider n = n as Element of NAT by ORDINAL1:def_12;
deffunc H1( Nat) ->  Element of INT = DigB (tx,$1);
consider txn being FinSequence of INT  such that
A4: len txn = n and
A5: for i being Nat st i in dom txn holds
txn . i = H1(i) from FINSEQ_2:sch_1();
deffunc H2( Nat) ->  Element of INT = DigB (ty,$1);
consider tyn being FinSequence of INT  such that
A6: len tyn = n and
A7: for i being Nat st i in dom tyn holds
tyn . i = H2(i) from FINSEQ_2:sch_1();
A8: dom tyn = Seg n by A6, FINSEQ_1:def_3;
 rng tyn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng tyn or z in k -SD )
assume  z in rng tyn ; ::_thesis: z in k -SD
then consider yy being set  such that
A9: yy in dom tyn and
A10: z = tyn . yy by FUNCT_1:def_3;
reconsider yy = yy as Element of NAT by A9;
 dom tyn = Seg n by A6, FINSEQ_1:def_3;
then  yy in Seg (n + 1) by A9, FINSEQ_2:8;
then A11: DigA (ty,yy) is Element of k -SD by RADIX_1:16;
z = DigB (ty,yy) by A7, A9, A10
.= DigA (ty,yy) by RADIX_1:def_4 ;
hence  z in k -SD by A11; ::_thesis: verum
end;
then reconsider tyn = tyn as FinSequence of k -SD by FINSEQ_1:def_4;
A12: for i being Nat st i in Seg n holds
tyn . i = ty . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies tyn . i = ty . i )
assume A13: i in Seg n ; ::_thesis: tyn . i = ty . i
then A14: i in Seg (n + 1) by FINSEQ_2:8;
tyn . i = DigB (ty,i) by A7, A8, A13
.= DigA (ty,i) by RADIX_1:def_4 ;
hence  tyn . i = ty . i by A14, RADIX_1:def_3; ::_thesis: verum
end;
 tyn is Element of n -tuples_on (k -SD) by A6, FINSEQ_2:92;
then reconsider tyn = tyn as Tuple of n,k -SD ;
A15: dom txn = Seg n by A4, FINSEQ_1:def_3;
 rng txn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng txn or z in k -SD )
assume  z in rng txn ; ::_thesis: z in k -SD
then consider xx being set  such that
A16: xx in dom txn and
A17: z = txn . xx by FUNCT_1:def_3;
reconsider xx = xx as Element of NAT by A16;
 dom txn = Seg n by A4, FINSEQ_1:def_3;
then  xx in Seg (n + 1) by A16, FINSEQ_2:8;
then A18: DigA (tx,xx) is Element of k -SD by RADIX_1:16;
z = DigB (tx,xx) by A5, A16, A17
.= DigA (tx,xx) by RADIX_1:def_4 ;
hence  z in k -SD by A18; ::_thesis: verum
end;
then reconsider txn = txn as FinSequence of k -SD by FINSEQ_1:def_4;
A19: for i being Nat st i in Seg n holds
txn . i = tx . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies txn . i = tx . i )
assume A20: i in Seg n ; ::_thesis: txn . i = tx . i
then A21: i in Seg (n + 1) by FINSEQ_2:8;
txn . i = DigB (tx,i) by A5, A15, A20
.= DigA (tx,i) by RADIX_1:def_4 ;
hence  txn . i = tx . i by A21, RADIX_1:def_3; ::_thesis: verum
end;
 txn is Element of n -tuples_on (k -SD) by A4, FINSEQ_2:92;
then reconsider txn = txn as Tuple of n,k -SD ;
 for i being Nat st i in Seg n holds
DigA (txn,i) >= DigA (tyn,i)
proof
let i be Nat; ::_thesis: ( i in Seg n implies DigA (txn,i) >= DigA (tyn,i) )
assume A22: i in Seg n ; ::_thesis: DigA (txn,i) >= DigA (tyn,i)
then A23: DigA (tyn,i) = tyn . i by RADIX_1:def_3
.= DigB (ty,i) by A7, A8, A22
.= DigA (ty,i) by RADIX_1:def_4 ;
DigA (txn,i) = txn . i by A22, RADIX_1:def_3
.= DigB (tx,i) by A5, A15, A22
.= DigA (tx,i) by RADIX_1:def_4 ;
hence  DigA (txn,i) >= DigA (tyn,i) by A3, A22, A23, FINSEQ_2:8; ::_thesis: verum
end;
then A24: SDDec txn >= SDDec tyn by A2;
 n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A25: ((Radix k) |^ n) * (DigA (tx,(n + 1))) >= ((Radix k) |^ n) * (DigA (ty,(n + 1))) by A3, XREAL_1:64;
A26: (SDDec tyn) + (((Radix k) |^ n) * (DigA (ty,(n + 1)))) = SDDec ty by A12, RADIX_2:10;
 (SDDec txn) + (((Radix k) |^ n) * (DigA (tx,(n + 1)))) = SDDec tx by A19, RADIX_2:10;
hence  SDDec tx >= SDDec ty by A26, A24, A25, XREAL_1:7; ::_thesis: verum
end;
A27: S1[1]
proof
let k be Nat; ::_thesis: for tx, ty being Tuple of 1,k -SD st ( for i being Nat st i in Seg 1 holds
DigA (tx,i) >= DigA (ty,i) ) holds
SDDec tx >= SDDec ty
let tx, ty be Tuple of 1,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg 1 holds
DigA (tx,i) >= DigA (ty,i) ) implies SDDec tx >= SDDec ty )
assume A28: for i being Nat st i in Seg 1 holds
DigA (tx,i) >= DigA (ty,i) ; ::_thesis: SDDec tx >= SDDec ty
A29: SDDec ty = DigA (ty,1) by Th4;
 ( 1 in Seg 1 & SDDec tx = DigA (tx,1) ) by Th4, FINSEQ_1:1;
hence  SDDec tx >= SDDec ty by A28, A29; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A27, A1);
hence  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 ; ::_thesis: verum
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)
proof
defpred S1[ Nat] means  for k being Nat st k >= 2 holds
for tx, ty, tz, tw being Tuple of $1,k -SD st ( for i being Nat holds
( not i in Seg $1 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);
A1: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A2: S1[n] ; ::_thesis: S1[n + 1]
let k be Nat; ::_thesis: ( k >= 2 implies for tx, ty, tz, tw being Tuple of n + 1,k -SD st ( for i being Nat holds
( not i in Seg (n + 1) 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) )
assume A3: k >= 2 ; ::_thesis: for tx, ty, tz, tw being Tuple of n + 1,k -SD st ( for i being Nat holds
( not i in Seg (n + 1) 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)
let tx, ty, tz, tw be Tuple of n + 1,k -SD ; ::_thesis: ( ( for i being Nat holds
( not i in Seg (n + 1) 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) ) ) ) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
assume A4: for i being Nat holds
( not i in Seg (n + 1) 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) ) ) ; ::_thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
deffunc H1( Nat) ->  Element of INT = DigB (tx,$1);
consider txn being FinSequence of INT  such that
A5: len txn = n and
A6: for i being Nat st i in dom txn holds
txn . i = H1(i) from FINSEQ_2:sch_1();
A7: dom txn = Seg n by A5, FINSEQ_1:def_3;
 rng txn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng txn or z in k -SD )
assume  z in rng txn ; ::_thesis: z in k -SD
then consider xx being set  such that
A8: xx in dom txn and
A9: z = txn . xx by FUNCT_1:def_3;
reconsider xx = xx as Element of NAT by A8;
 dom txn = Seg n by A5, FINSEQ_1:def_3;
then  xx in Seg (n + 1) by A8, FINSEQ_2:8;
then A10: DigA (tx,xx) is Element of k -SD by RADIX_1:16;
z = DigB (tx,xx) by A6, A8, A9
.= DigA (tx,xx) by RADIX_1:def_4 ;
hence  z in k -SD by A10; ::_thesis: verum
end;
then reconsider txn = txn as FinSequence of k -SD by FINSEQ_1:def_4;
A11: for i being Nat st i in Seg n holds
txn . i = tx . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies txn . i = tx . i )
assume A12: i in Seg n ; ::_thesis: txn . i = tx . i
then A13: i in Seg (n + 1) by FINSEQ_2:8;
txn . i = DigB (tx,i) by A6, A7, A12
.= DigA (tx,i) by RADIX_1:def_4 ;
hence  txn . i = tx . i by A13, RADIX_1:def_3; ::_thesis: verum
end;
deffunc H2( Nat) ->  Element of INT = DigB (ty,$1);
consider tyn being FinSequence of INT  such that
A14: len tyn = n and
A15: for i being Nat st i in dom tyn holds
tyn . i = H2(i) from FINSEQ_2:sch_1();
A16: dom tyn = Seg n by A14, FINSEQ_1:def_3;
 rng tyn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng tyn or z in k -SD )
assume  z in rng tyn ; ::_thesis: z in k -SD
then consider yy being set  such that
A17: yy in dom tyn and
A18: z = tyn . yy by FUNCT_1:def_3;
reconsider yy = yy as Element of NAT by A17;
 dom tyn = Seg n by A14, FINSEQ_1:def_3;
then  yy in Seg (n + 1) by A17, FINSEQ_2:8;
then A19: DigA (ty,yy) is Element of k -SD by RADIX_1:16;
z = DigB (ty,yy) by A15, A17, A18
.= DigA (ty,yy) by RADIX_1:def_4 ;
hence  z in k -SD by A19; ::_thesis: verum
end;
then reconsider tyn = tyn as FinSequence of k -SD by FINSEQ_1:def_4;
A20: for i being Nat st i in Seg n holds
tyn . i = ty . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies tyn . i = ty . i )
assume A21: i in Seg n ; ::_thesis: tyn . i = ty . i
then A22: i in Seg (n + 1) by FINSEQ_2:8;
tyn . i = DigB (ty,i) by A15, A16, A21
.= DigA (ty,i) by RADIX_1:def_4 ;
hence  tyn . i = ty . i by A22, RADIX_1:def_3; ::_thesis: verum
end;
deffunc H3( Nat) ->  Element of INT = DigB (tz,$1);
consider tzn being FinSequence of INT  such that
A23: len tzn = n and
A24: for i being Nat st i in dom tzn holds
tzn . i = H3(i) from FINSEQ_2:sch_1();
A25: dom tzn = Seg n by A23, FINSEQ_1:def_3;
 rng tzn c= k -SD
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng tzn or z in k -SD )
assume  z in rng tzn ; ::_thesis: z in k -SD
then consider zz being set  such that
A26: zz in dom tzn and
A27: z = tzn . zz by FUNCT_1:def_3;
reconsider zz = zz as Element of NAT by A26;
 dom tzn = Seg n by A23, FINSEQ_1:def_3;
then  zz in Seg (n + 1) by A26, FINSEQ_2:8;
then A28: DigA (tz,zz) is Element of k -SD by RADIX_1:16;
z = DigB (tz,zz) by A24, A26, A27
.= DigA (tz,zz) by RADIX_1:def_4 ;
hence  z in k -SD by A28; ::_thesis: verum
end;
then reconsider tzn = tzn as FinSequence of k -SD by FINSEQ_1:def_4;
A29: for i being Nat st i in Seg n holds
tzn . i = tz . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies tzn . i = tz . i )
assume A30: i in Seg n ; ::_thesis: tzn . i = tz . i
then A31: i in Seg (n + 1) by FINSEQ_2:8;
tzn . i = DigB (tz,i) by A24, A25, A30
.= DigA (tz,i) by RADIX_1:def_4 ;
hence  tzn . i = tz . i by A31, RADIX_1:def_3; ::_thesis: verum
end;
deffunc H4( Nat) ->  Element of INT = DigB (tw,$1);
consider twn being FinSequence of INT  such that
A32: len twn = n and
A33: for i being Nat st i in dom twn holds
twn . i = H4(i) from FINSEQ_2:sch_1();
A34: dom twn = Seg n by A32, FINSEQ_1:def_3;
 rng twn c= k -SD
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in rng twn or w in k -SD )
assume  w in rng twn ; ::_thesis: w in k -SD
then consider ww being set  such that
A35: ww in dom twn and
A36: w = twn . ww by FUNCT_1:def_3;
reconsider ww = ww as Element of NAT by A35;
 dom twn = Seg n by A32, FINSEQ_1:def_3;
then  ww in Seg (n + 1) by A35, FINSEQ_2:8;
then A37: DigA (tw,ww) is Element of k -SD by RADIX_1:16;
w = DigB (tw,ww) by A33, A35, A36
.= DigA (tw,ww) by RADIX_1:def_4 ;
hence  w in k -SD by A37; ::_thesis: verum
end;
then reconsider twn = twn as FinSequence of k -SD by FINSEQ_1:def_4;
A38: for i being Nat st i in Seg n holds
twn . i = tw . i
proof
let i be Nat; ::_thesis: ( i in Seg n implies twn . i = tw . i )
assume A39: i in Seg n ; ::_thesis: twn . i = tw . i
then A40: i in Seg (n + 1) by FINSEQ_2:8;
twn . i = DigB (tw,i) by A33, A34, A39
.= DigA (tw,i) by RADIX_1:def_4 ;
hence  twn . i = tw . i by A40, RADIX_1:def_3; ::_thesis: verum
end;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 twn is Element of n -tuples_on (k -SD) by A32, FINSEQ_2:92;
then reconsider twn = twn as Tuple of n,k -SD ;
 tzn is Element of n -tuples_on (k -SD) by A23, FINSEQ_2:92;
then reconsider tzn = tzn as Tuple of n,k -SD ;
 tyn is Element of n -tuples_on (k -SD) by A14, FINSEQ_2:92;
then reconsider tyn = tyn as Tuple of n,k -SD ;
A41: (SDDec tyn) + (((Radix k) |^ n) * (DigA (ty,(n + 1)))) = SDDec ty by A20, RADIX_2:10;
 n + 1 in Seg (n + 1) by FINSEQ_1:3;
then A42: ( ( DigA (tx,(n + 1)) = DigA (tz,(n + 1)) & DigA (ty,(n + 1)) = DigA (tw,(n + 1)) ) or ( DigA (ty,(n + 1)) = DigA (tz,(n + 1)) & DigA (tx,(n + 1)) = DigA (tw,(n + 1)) ) ) by A4;
A43: (SDDec twn) + (((Radix k) |^ n) * (DigA (tw,(n + 1)))) = SDDec tw by A38, RADIX_2:10;
A44: (SDDec tzn) + (((Radix k) |^ n) * (DigA (tz,(n + 1)))) = SDDec tz by A29, RADIX_2:10;
 txn is Element of n -tuples_on (k -SD) by A5, FINSEQ_2:92;
then reconsider txn = txn as Tuple of n,k -SD ;
 for i being Nat holds
( not i in Seg n or ( DigA (txn,i) = DigA (tzn,i) & DigA (tyn,i) = DigA (twn,i) ) or ( DigA (tyn,i) = DigA (tzn,i) & DigA (txn,i) = DigA (twn,i) ) )
proof
let i be Nat; ::_thesis: ( not i in Seg n or ( DigA (txn,i) = DigA (tzn,i) & DigA (tyn,i) = DigA (twn,i) ) or ( DigA (tyn,i) = DigA (tzn,i) & DigA (txn,i) = DigA (twn,i) ) )
assume A45: i in Seg n ; ::_thesis: ( ( DigA (txn,i) = DigA (tzn,i) & DigA (tyn,i) = DigA (twn,i) ) or ( DigA (tyn,i) = DigA (tzn,i) & DigA (txn,i) = DigA (twn,i) ) )
then  i <= n by FINSEQ_1:1;
then A46: i <= n + 1 by NAT_1:12;
 1 <= i by A45, FINSEQ_1:1;
then A47: i in Seg (n + 1) by A46, FINSEQ_1:1;
then A48: DigA (ty,i) = ty . i by RADIX_1:def_3
.= tyn . i by A20, A45
.= DigA (tyn,i) by A45, RADIX_1:def_3 ;
A49: DigA (tw,i) = tw . i by A47, RADIX_1:def_3
.= twn . i by A38, A45
.= DigA (twn,i) by A45, RADIX_1:def_3 ;
A50: DigA (tz,i) = tz . i by A47, RADIX_1:def_3
.= tzn . i by A29, A45
.= DigA (tzn,i) by A45, RADIX_1:def_3 ;
DigA (tx,i) = tx . i by A47, RADIX_1:def_3
.= txn . i by A11, A45
.= DigA (txn,i) by A45, RADIX_1:def_3 ;
hence  ( ( DigA (txn,i) = DigA (tzn,i) & DigA (tyn,i) = DigA (twn,i) ) or ( DigA (tyn,i) = DigA (tzn,i) & DigA (txn,i) = DigA (twn,i) ) ) by A4, A47, A48, A50, A49; ::_thesis: verum
end;
then A51: (SDDec tzn) + (SDDec twn) = (SDDec txn) + (SDDec tyn) by A2, A3;
 (SDDec txn) + (((Radix k) |^ n) * (DigA (tx,(n + 1)))) = SDDec tx by A11, RADIX_2:10;
hence  (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A41, A44, A43, A51, A42; ::_thesis: verum
end;
A52: S1[1]
proof
let k be Nat; ::_thesis: ( k >= 2 implies for tx, ty, tz, tw being Tuple of 1,k -SD st ( for i being Nat holds
( not i in Seg 1 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) )
assume A53: k >= 2 ; ::_thesis: for tx, ty, tz, tw being Tuple of 1,k -SD st ( for i being Nat holds
( not i in Seg 1 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)
let tx, ty, tz, tw be Tuple of 1,k -SD ; ::_thesis: ( ( for i being Nat holds
( not i in Seg 1 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) ) ) ) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
A54: 1 in Seg 1 by FINSEQ_1:1;
A55: SDDec (tx '+' ty) = DigA ((tx '+' ty),1) by Th4
.= Add (tx,ty,1,k) by A54, RADIX_1:def_14
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry ((DigA (tx,(1 -' 1))) + (DigA (ty,(1 -' 1))))) by A53, A54, RADIX_1:def_13
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry ((DigA (tx,0)) + (DigA (ty,(1 -' 1))))) by XREAL_1:232
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry ((DigA (tx,0)) + (DigA (ty,0)))) by XREAL_1:232
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry ((DigA (tx,0)) + 0)) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + (SD_Add_Carry (0 + 0)) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (tx,1)) + (DigA (ty,1))),k)) + 0 by RADIX_1:def_10 ;
A56: SDDec (tz '+' tw) = DigA ((tz '+' tw),1) by Th4
.= Add (tz,tw,1,k) by A54, RADIX_1:def_14
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry ((DigA (tz,(1 -' 1))) + (DigA (tw,(1 -' 1))))) by A53, A54, RADIX_1:def_13
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry ((DigA (tz,0)) + (DigA (tw,(1 -' 1))))) by XREAL_1:232
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry ((DigA (tz,0)) + (DigA (tw,0)))) by XREAL_1:232
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry ((DigA (tz,0)) + 0)) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + (SD_Add_Carry (0 + 0)) by RADIX_1:def_3
.= (SD_Add_Data (((DigA (tz,1)) + (DigA (tw,1))),k)) + 0 by RADIX_1:def_10 ;
A57: ( DigA (tx,1) = DigA (tz,1) & DigA (ty,1) = DigA (tw,1) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
proof
assume  ( DigA (tx,1) = DigA (tz,1) & DigA (ty,1) = DigA (tw,1) ) ; ::_thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
then  (SDDec tz) + (SDDec tw) = (SDDec (tx '+' ty)) + ((SD_Add_Carry ((DigA (tx,1)) + (DigA (ty,1)))) * ((Radix k) |^ 1)) by A53, A56, A55, RADIX_2:11;
hence  (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A53, RADIX_2:11; ::_thesis: verum
end;
assume A58: for j being Nat holds
( not j in Seg 1 or ( DigA (tx,j) = DigA (tz,j) & DigA (ty,j) = DigA (tw,j) ) or ( DigA (ty,j) = DigA (tz,j) & DigA (tx,j) = DigA (tw,j) ) ) ; ::_thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
then A59: ( ( DigA (tx,1) = DigA (tz,1) & DigA (ty,1) = DigA (tw,1) ) or ( DigA (ty,1) = DigA (tz,1) & DigA (tx,1) = DigA (tw,1) ) ) by A54;
 ( DigA (ty,1) = DigA (tz,1) & DigA (tx,1) = DigA (tw,1) implies (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) )
proof
assume that
 DigA (ty,1) = DigA (tz,1) and
 DigA (tx,1) = DigA (tw,1) ; ::_thesis: (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
 (SDDec tz) + (SDDec tw) = (SDDec (tx '+' ty)) + ((SD_Add_Carry ((DigA (tx,1)) + (DigA (ty,1)))) * ((Radix k) |^ 1)) by A53, A56, A55, A59, RADIX_2:11;
hence  (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A53, RADIX_2:11; ::_thesis: verum
end;
hence  (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) by A58, A54, A57; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A52, A1);
hence  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) ; ::_thesis: verum
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)
proof
let n, k be Nat; ::_thesis: ( n >= 1 & k >= 2 implies 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) )
assume A1: ( n >= 1 & k >= 2 ) ; ::_thesis: 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)
let tx, ty, tz be Tuple of n,k -SD ; ::_thesis: ( ( 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 ) ) ) implies (SDDec tz) + (SDDec (DecSD (0,n,k))) = (SDDec tx) + (SDDec ty) )
assume A2: 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 ) ) ; ::_thesis: (SDDec tz) + (SDDec (DecSD (0,n,k))) = (SDDec tx) + (SDDec ty)
 for i being Nat holds
( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA ((DecSD (0,n,k)),i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA ((DecSD (0,n,k)),i) ) )
proof
let i be Nat; ::_thesis: ( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA ((DecSD (0,n,k)),i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA ((DecSD (0,n,k)),i) ) )
assume A3: i in Seg n ; ::_thesis: ( ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA ((DecSD (0,n,k)),i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA ((DecSD (0,n,k)),i) ) )
then  DigA ((DecSD (0,n,k)),i) = 0 by Th5;
hence  ( ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA ((DecSD (0,n,k)),i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA ((DecSD (0,n,k)),i) ) ) by A2, A3; ::_thesis: verum
end;
hence  (SDDec tz) + (SDDec (DecSD (0,n,k))) = (SDDec tx) + (SDDec ty) by A1, Th14; ::_thesis: verum
end;

begin

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
(- (Radix k)) + 1 if ( 1 <= i & i < m )
otherwise  0 ;
coherence
 ( ( 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
 Radix k > 2 by A1, RADIX_4:1;
then  Radix k > 1 by XXREAL_0:2;
then  (Radix k) + (Radix k) > 1 + 1 by XREAL_1:8;
then A2: (Radix k) - 1 > 1 - (Radix k) by XREAL_1:21;
 ( k -SD =  {  w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 )  }  & (- (Radix k)) + 1 is Element of INT ) by INT_1:def_2, RADIX_1:def_2;
then  (- (Radix k)) + 1 in k -SD by A2;
hence  ( ( 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 RADIX_1:14; ::_thesis: verum
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) = (- (Radix k)) + 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
deffunc H1( Nat) ->  Element of k -SD = SDMinDigit (m,k,$1);
consider z being FinSequence of k -SD  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
 z is Element of n -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
DigA (z,i) = SDMinDigit (m,k,i)
let i be Nat; ::_thesis: ( i in Seg n implies DigA (z,i) = SDMinDigit (m,k,i) )
assume A4: i in Seg n ; ::_thesis: DigA (z,i) = SDMinDigit (m,k,i)
then  DigA (z,i) = z . i by RADIX_1:def_3;
hence  DigA (z,i) = SDMinDigit (m,k,i) by A2, A3, A4; ::_thesis: verum
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
let k1, k2 be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
DigA (k1,i) = SDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (k2,i) = SDMinDigit (m,k,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
DigA (k1,i) = SDMinDigit (m,k,i) and
A6: for i being Nat st i in Seg n holds
DigA (k2,i) = SDMinDigit (m,k,i) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= SDMinDigit (m,k,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
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
(Radix k) - 1 if ( 1 <= i & i < m )
otherwise  0 ;
coherence
 ( ( 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 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) = (Radix k) - 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
deffunc H1( Nat) ->  Element of k -SD = SDMaxDigit (m,k,$1);
consider z being FinSequence of k -SD  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
 z is Element of n -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
DigA (z,i) = SDMaxDigit (m,k,i)
let i be Nat; ::_thesis: ( i in Seg n implies DigA (z,i) = SDMaxDigit (m,k,i) )
assume A4: i in Seg n ; ::_thesis: DigA (z,i) = SDMaxDigit (m,k,i)
then  DigA (z,i) = z . i by RADIX_1:def_3;
hence  DigA (z,i) = SDMaxDigit (m,k,i) by A2, A3, A4; ::_thesis: verum
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
let k1, k2 be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
DigA (k1,i) = SDMaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (k2,i) = SDMaxDigit (m,k,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
DigA (k1,i) = SDMaxDigit (m,k,i) and
A6: for i being Nat st i in Seg n holds
DigA (k2,i) = SDMaxDigit (m,k,i) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= SDMaxDigit (m,k,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
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
A2: Radix k > 2 by A1, RADIX_4:1;
then  - (Radix k) < - 2 by XREAL_1:24;
then A3: (- (Radix k)) + 1 < (- 2) + 1 by XREAL_1:6;
A4: ( k -SD =  {  w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 )  }  & 1 is Element of INT ) by INT_1:def_2, RADIX_1:def_2;
 (Radix k) + (- 1) > 2 + (- 1) by A2, XREAL_1:6;
then  1 in k -SD by A3, A4;
hence  ( ( i = m implies 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) ) by RADIX_1:14; ::_thesis: verum
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
deffunc H1( Nat) ->  Element of k -SD = FminDigit (m,k,$1);
consider z being FinSequence of k -SD  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
 z is Element of n -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
DigA (z,i) = FminDigit (m,k,i)
let i be Nat; ::_thesis: ( i in Seg n implies DigA (z,i) = FminDigit (m,k,i) )
assume A4: i in Seg n ; ::_thesis: DigA (z,i) = FminDigit (m,k,i)
hence  DigA (z,i) = z . i by RADIX_1:def_3
.= FminDigit (m,k,i) by A2, A3, A4 ;
::_thesis: verum
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
let k1, k2 be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
DigA (k1,i) = FminDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (k2,i) = FminDigit (m,k,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
DigA (k1,i) = FminDigit (m,k,i) and
A6: for i being Nat st i in Seg n holds
DigA (k2,i) = FminDigit (m,k,i) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= FminDigit (m,k,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
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
(Radix k) - 1 if i = m
otherwise  0 ;
coherence
 ( ( 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 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) = (Radix k) - 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
deffunc H1( Nat) ->  Element of k -SD = FmaxDigit (m,k,$1);
consider z being FinSequence of k -SD  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
 z is Element of n -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
DigA (z,i) = FmaxDigit (m,k,i)
let i be Nat; ::_thesis: ( i in Seg n implies DigA (z,i) = FmaxDigit (m,k,i) )
assume A4: i in Seg n ; ::_thesis: DigA (z,i) = FmaxDigit (m,k,i)
hence  DigA (z,i) = z . i by RADIX_1:def_3
.= FmaxDigit (m,k,i) by A2, A3, A4 ;
::_thesis: verum
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
let k1, k2 be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
DigA (k1,i) = FmaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (k2,i) = FmaxDigit (m,k,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
DigA (k1,i) = FmaxDigit (m,k,i) and
A6: for i being Nat st i in Seg n holds
DigA (k2,i) = FmaxDigit (m,k,i) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= FmaxDigit (m,k,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
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) );

begin

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
proof
let n, m, k be Nat; ::_thesis: ( k >= 2 implies for i being Nat st i in Seg n holds
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 )
assume A1: k >= 2 ; ::_thesis: for i being Nat st i in Seg n holds
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
let i be Nat; ::_thesis: ( i in Seg n implies (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 )
reconsider a = SDMinDigit (m,k,i) as Element of INT ;
reconsider b = SDMaxDigit (m,k,i) as Element of INT ;
assume A2: i in Seg n ; ::_thesis: (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
then A3: i >= 1 by FINSEQ_1:1;
A4: DigA ((SDMin (n,m,k)),i) = SDMinDigit (m,k,i) by A2, Def2;
now__::_thesis:_(DigA_((SDMax_(n,m,k)),i))_+_(DigA_((SDMin_(n,m,k)),i))_=_0
percases ( i < m or i >= m ) ;
supposeA5: i < m ; ::_thesis: (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
then a + b = ((- (Radix k)) + 1) + b by A1, A3, Def1
.= ((- (Radix k)) + 1) + ((Radix k) - 1) by A1, A3, A5, Def3
.= 0 ;
hence  (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 by A2, A4, Def4; ::_thesis: verum
end;
supposeA6: i >= m ; ::_thesis: (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
then a + b = 0 + b by A1, Def1
.= 0 + 0 by A1, A6, Def3 ;
hence  (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 by A2, A4, Def4; ::_thesis: verum
end;
end;
end;
hence  (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 ; ::_thesis: verum
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))
proof
let n be Nat; ::_thesis: ( n >= 1 implies for m, k being Nat st k >= 2 holds
(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k)) )
assume A1: n >= 1 ; ::_thesis: for m, k being Nat st k >= 2 holds
(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k))
then A2: n in Seg n by FINSEQ_1:1;
let m, k be Nat; ::_thesis: ( k >= 2 implies (SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k)) )
assume A3: k >= 2 ; ::_thesis: (SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k))
A4: for i being Nat st i in Seg n holds
DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)
proof
let i be Nat; ::_thesis: ( i in Seg n implies DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) )
assume A5: i in Seg n ; ::_thesis: DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)
then A6: DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) = Add ((SDMax (n,m,k)),(SDMin (n,m,k)),i,k) by RADIX_1:def_14
.= (SD_Add_Data (((DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i))),k)) + (SD_Add_Carry ((DigA ((SDMax (n,m,k)),(i -' 1))) + (DigA ((SDMin (n,m,k)),(i -' 1))))) by A3, A5, RADIX_1:def_13
.= (SD_Add_Data (0,k)) + (SD_Add_Carry ((DigA ((SDMax (n,m,k)),(i -' 1))) + (DigA ((SDMin (n,m,k)),(i -' 1))))) by A3, A5, Th16
.= 0 + (SD_Add_Carry ((DigA ((SDMax (n,m,k)),(i -' 1))) + (DigA ((SDMin (n,m,k)),(i -' 1))))) by RADIX_1:19 ;
A7: DigA ((DecSD (0,n,k)),i) = 0 by A5, Th5;
A8: i >= 1 by A5, FINSEQ_1:1;
now__::_thesis:_DigA_((DecSD_(0,n,k)),i)_=_DigA_(((SDMax_(n,m,k))_'+'_(SDMin_(n,m,k))),i)
percases ( i = 1 or i > 1 ) by A8, XXREAL_0:1;
supposeA9: i = 1 ; ::_thesis: DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)
then  DigA ((SDMin (n,m,k)),(i -' 1)) = 0 by NAT_2:8, RADIX_1:def_3;
then  DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) = SD_Add_Carry (0 + 0) by A6, A9, NAT_2:8, RADIX_1:def_3;
hence  DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) by A7, RADIX_1:def_10; ::_thesis: verum
end;
suppose i > 1 ; ::_thesis: DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i)
then  i -' 1 in Seg n by A5, Th2;
then  DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) = SD_Add_Carry 0 by A3, A6, Th16;
hence  DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) by A7, RADIX_1:def_10; ::_thesis: verum
end;
end;
end;
hence  DigA ((DecSD (0,n,k)),i) = DigA (((SDMax (n,m,k)) '+' (SDMin (n,m,k))),i) ; ::_thesis: verum
end;
(SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = (SDDec ((SDMax (n,m,k)) '+' (SDMin (n,m,k)))) + ((SD_Add_Carry ((DigA ((SDMax (n,m,k)),n)) + (DigA ((SDMin (n,m,k)),n)))) * ((Radix k) |^ n)) by A1, A3, RADIX_2:11
.= (SDDec ((SDMax (n,m,k)) '+' (SDMin (n,m,k)))) + ((SD_Add_Carry 0) * ((Radix k) |^ n)) by A3, A2, Th16
.= (SDDec ((SDMax (n,m,k)) '+' (SDMin (n,m,k)))) + (0 * ((Radix k) |^ n)) by RADIX_1:def_10 ;
hence  (SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k)) by A1, A4, Th12; ::_thesis: verum
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)))
proof
let n be Nat; ::_thesis: ( n >= 1 implies 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))) )
A1: 1 in Seg 1 by FINSEQ_1:1;
assume A2: n >= 1 ; ::_thesis: 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)))
then A3: 1 in Seg n by FINSEQ_1:1;
let m, k be Nat; ::_thesis: ( m in Seg n & k >= 2 implies SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) )
assume that
A4: m in Seg n and
A5: k >= 2 ; ::_thesis: SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))
A6: n >= m by A4, FINSEQ_1:1;
A7: m >= 1 by A4, FINSEQ_1:1;
now__::_thesis:_SDDec_(Fmin_(n,m,k))_=_(SDDec_(SDMax_(n,m,k)))_+_(SDDec_(DecSD_(1,n,k)))
percases ( n = 1 or n > 1 ) by A2, XXREAL_0:1;
supposeA8: n = 1 ; ::_thesis: SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))
then A9: m = 1 by A6, A7, XXREAL_0:1;
A10: SDDec (Fmin (1,m,k)) = DigA ((Fmin (1,m,k)),1) by Th4
.= FminDigit (m,k,1) by A1, Def6
.= 1 by A5, A9, Def5 ;
A11: DigA ((SDMax (1,m,k)),1) = SDMaxDigit (m,k,1) by A1, Def4
.= 0 by A5, A6, A8, Def3 ;
SDDec ((SDMax (1,m,k)) '+' (DecSD (1,1,k))) = DigA (((SDMax (1,m,k)) '+' (DecSD (1,1,k))),1) by Th4
.= Add ((SDMax (1,m,k)),(DecSD (1,1,k)),1,k) by A1, RADIX_1:def_14
.= (SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((SDMax (1,m,k)),(1 -' 1))) + (DigA ((DecSD (1,1,k)),(1 -' 1))))) by A5, A1, RADIX_1:def_13
.= (SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((SDMax (1,m,k)),0)) + (DigA ((DecSD (1,1,k)),(1 -' 1))))) by XREAL_1:232
.= (SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((SDMax (1,m,k)),0)) + (DigA ((DecSD (1,1,k)),0)))) by XREAL_1:232
.= (SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((SDMax (1,m,k)),0)) + 0)) by RADIX_1:def_3
.= (SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry (0 + 0)) by RADIX_1:def_3
.= (SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + 0 by RADIX_1:def_10
.= SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + 1),k) by A5, A1, Th7 ;
then A12: SDDec ((SDMax (1,m,k)) '+' (DecSD (1,1,k))) = 1 - ((SD_Add_Carry 1) * (Radix k)) by A11, RADIX_1:def_11
.= 1 - (0 * (Radix k)) by RADIX_1:def_10
.= 1 ;
(SDDec (SDMax (1,m,k))) + (SDDec (DecSD (1,1,k))) = (SDDec ((SDMax (1,m,k)) '+' (DecSD (1,1,k)))) + ((SD_Add_Carry ((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1)))) * ((Radix k) |^ 1)) by A5, RADIX_2:11
.= 1 + ((SD_Add_Carry (0 + 1)) * ((Radix k) |^ 1)) by A5, A1, A11, A12, Th7
.= 1 + (0 * ((Radix k) |^ 1)) by RADIX_1:def_10 ;
hence  SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) by A8, A10; ::_thesis: verum
end;
supposeA13: n > 1 ; ::_thesis: SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))
A14: n in Seg n by A2, FINSEQ_1:1;
then A15: DigA ((SDMax (n,m,k)),n) = SDMaxDigit (m,k,n) by Def4
.= 0 by A5, A6, Def3 ;
A16: for i being Nat st i in Seg n holds
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
proof
let i be Nat; ::_thesis: ( i in Seg n implies DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) )
assume A17: i in Seg n ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then A18: DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = Add ((SDMax (n,m,k)),(DecSD (1,n,k)),i,k) by RADIX_1:def_14
.= (SD_Add_Data (((DigA ((SDMax (n,m,k)),i)) + (DigA ((DecSD (1,n,k)),i))),k)) + (SD_Add_Carry ((DigA ((SDMax (n,m,k)),(i -' 1))) + (DigA ((DecSD (1,n,k)),(i -' 1))))) by A5, A17, RADIX_1:def_13 ;
A19: DigA ((SDMax (n,m,k)),i) = SDMaxDigit (m,k,i) by A17, Def4;
A20: DigA ((Fmin (n,m,k)),i) = FminDigit (m,k,i) by A17, Def6;
A21: i >= 1 by A17, FINSEQ_1:1;
now__::_thesis:_DigA_((Fmin_(n,m,k)),i)_=_DigA_(((SDMax_(n,m,k))_'+'_(DecSD_(1,n,k))),i)
percases ( i >= m + 1 or i < m + 1 ) ;
supposeA22: i >= m + 1 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then A23: i > m by NAT_1:13;
then A24: DigA ((SDMax (n,m,k)),i) = 0 by A5, A19, Def3;
A25: i > 1 by A7, A23, XXREAL_0:2;
then A26: ( i -' 1 in Seg n & DigA ((DecSD (1,n,k)),i) = 0 ) by A5, A17, Th2, Th8;
now__::_thesis:_DigA_((Fmin_(n,m,k)),i)_=_DigA_(((SDMax_(n,m,k))_'+'_(DecSD_(1,n,k))),i)
percases ( i = m + 1 or i > m + 1 ) by A22, XXREAL_0:1;
suppose i = m + 1 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then  DigA ((SDMax (n,m,k)),(i -' 1)) = DigA ((SDMax (n,m,k)),m) by NAT_D:34
.= SDMaxDigit (m,k,m) by A4, Def4
.= 0 by A5, Def3 ;
then  DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = (SD_Add_Data ((0 + 0),k)) + 0 by A5, A18, A24, A26, Lm2
.= 0 by RADIX_1:19 ;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) by A5, A20, A23, Def5; ::_thesis: verum
end;
suppose i > m + 1 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then  i - 1 > (m + 1) - 1 by XREAL_1:14;
then A27: i -' 1 > m by XREAL_0:def_2;
 i -' 1 in Seg n by A17, A25, Th2;
then  DigA ((SDMax (n,m,k)),(i -' 1)) = SDMaxDigit (m,k,(i -' 1)) by Def4
.= 0 by A5, A27, Def3 ;
then  DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = (SD_Add_Data ((0 + 0),k)) + 0 by A5, A18, A24, A26, Lm2
.= 0 by RADIX_1:19 ;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) by A5, A20, A23, Def5; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) ; ::_thesis: verum
end;
suppose i < m + 1 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then A28: i <= m by NAT_1:13;
A29: i >= 1 by A17, FINSEQ_1:1;
now__::_thesis:_DigA_((Fmin_(n,m,k)),i)_=_DigA_(((SDMax_(n,m,k))_'+'_(DecSD_(1,n,k))),i)
percases ( i > 1 or i = 1 ) by A29, XXREAL_0:1;
supposeA30: i > 1 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then A31: m > 1 by A28, XXREAL_0:2;
then A32: m -' 1 < m by JORDAN5B:1;
A33: m -' 1 in Seg n by A4, A31, Th2;
then A34: m -' 1 >= 1 by FINSEQ_1:1;
now__::_thesis:_DigA_((Fmin_(n,m,k)),i)_=_DigA_(((SDMax_(n,m,k))_'+'_(DecSD_(1,n,k))),i)
percases ( i = m or i < m ) by A28, XXREAL_0:1;
supposeA35: i = m ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then A36: ( DigA ((SDMax (n,m,k)),i) = 0 & DigA ((DecSD (1,n,k)),i) = 0 ) by A4, A5, A19, A30, Def3, Th8;
A37: DigA ((Fmin (n,m,k)),i) = FminDigit (m,k,m) by A4, A35, Def6
.= 1 by A5, Def5 ;
A38: DigA ((SDMax (n,m,k)),(i -' 1)) = SDMaxDigit (m,k,(m -' 1)) by A33, A35, Def4
.= (Radix k) - 1 by A5, A34, A32, Def3 ;
A39: i >= 1 + 1 by A30, INT_1:7;
now__::_thesis:_DigA_((Fmin_(n,m,k)),i)_=_DigA_(((SDMax_(n,m,k))_'+'_(DecSD_(1,n,k))),i)
percases ( i = 2 or i > 2 ) by A39, XXREAL_0:1;
suppose i = 2 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then  i -' 1 = 2 - 1 by XREAL_1:233;
then  DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = (SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 1)) by A5, A3, A18, A36, A38, Th7
.= 0 + (SD_Add_Carry (((Radix k) - 1) + 1)) by RADIX_1:19
.= 1 by A5, Th10 ;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) by A37; ::_thesis: verum
end;
supposeA40: i > 2 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then  i - 1 > 2 - 1 by XREAL_1:14;
then A41: i -' 1 > 1 by XREAL_0:def_2;
 i > 1 by A40, XXREAL_0:2;
then  i -' 1 in Seg n by A17, Th2;
then  DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = (SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 0)) by A5, A18, A36, A38, A41, Th8
.= 0 + (SD_Add_Carry ((Radix k) - 1)) by RADIX_1:19
.= 1 by A5, Lm1 ;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) by A37; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) ; ::_thesis: verum
end;
supposeA42: i < m ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
 i -' 1 < i by A30, JORDAN5B:1;
then A43: i -' 1 < m by A42, XXREAL_0:2;
A44: DigA ((DecSD (1,n,k)),i) = 0 by A5, A17, A30, Th8;
A45: i -' 1 in Seg n by A17, A30, Th2;
A46: i >= 1 + 1 by A30, INT_1:7;
now__::_thesis:_DigA_((Fmin_(n,m,k)),i)_=_DigA_(((SDMax_(n,m,k))_'+'_(DecSD_(1,n,k))),i)
percases ( i = 2 or i > 2 ) by A46, XXREAL_0:1;
suppose i = 2 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then A47: i -' 1 = 2 - 1 by XREAL_1:233;
then A48: DigA ((DecSD (1,n,k)),(i -' 1)) = 1 by A5, A3, Th7;
DigA ((SDMax (n,m,k)),(i -' 1)) = SDMaxDigit (m,k,(i -' 1)) by A45, Def4
.= (Radix k) - 1 by A5, A43, A47, Def3 ;
then  DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = (SD_Add_Data (((Radix k) - 1),k)) + (SD_Add_Carry (((Radix k) + 1) - 1)) by A5, A18, A19, A21, A42, A44, A48, Def3
.= (SD_Add_Data (((Radix k) - 1),k)) + 1 by A5, Th10
.= (((Radix k) - 1) - ((SD_Add_Carry ((Radix k) - 1)) * (Radix k))) + 1 by RADIX_1:def_11
.= (((Radix k) - 1) - (1 * (Radix k))) + 1 by A5, Lm1
.= 0 ;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) by A5, A20, A42, Def5; ::_thesis: verum
end;
supposeA49: i > 2 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then  i - 1 > 2 - 1 by XREAL_1:14;
then A50: i -' 1 > 1 by XREAL_0:def_2;
 i > 1 by A49, XXREAL_0:2;
then  i -' 1 in Seg n by A17, Th2;
then A51: DigA ((DecSD (1,n,k)),(i -' 1)) = 0 by A5, A50, Th8;
DigA ((SDMax (n,m,k)),(i -' 1)) = SDMaxDigit (m,k,(i -' 1)) by A45, Def4
.= (Radix k) - 1 by A5, A43, A50, Def3 ;
then  DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = (SD_Add_Data ((((Radix k) - 1) + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 0)) by A5, A18, A19, A21, A42, A44, A51, Def3
.= (SD_Add_Data (((Radix k) - 1),k)) + 1 by A5, Lm1
.= (((Radix k) - 1) - ((SD_Add_Carry ((Radix k) - 1)) * (Radix k))) + 1 by RADIX_1:def_11
.= (((Radix k) - 1) - (1 * (Radix k))) + 1 by A5, Lm1
.= 0 ;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) by A5, A20, A42, Def5; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) ; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) ; ::_thesis: verum
end;
supposeA52: i = 1 ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then A53: ( DigA ((SDMax (n,m,k)),(i -' 1)) = 0 & DigA ((DecSD (1,n,k)),(i -' 1)) = 0 ) by NAT_2:8, RADIX_1:def_3;
now__::_thesis:_DigA_((Fmin_(n,m,k)),i)_=_DigA_(((SDMax_(n,m,k))_'+'_(DecSD_(1,n,k))),i)
percases ( i < m or i = m ) by A28, XXREAL_0:1;
supposeA54: i < m ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then  DigA ((SDMax (n,m,k)),i) = (Radix k) - 1 by A5, A19, A52, Def3;
then  DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = (SD_Add_Data ((((Radix k) - 1) + 1),k)) + (SD_Add_Carry (0 + 0)) by A5, A3, A18, A52, A53, Th7
.= (Radix k) - ((SD_Add_Carry (Radix k)) * (Radix k)) by RADIX_1:18, RADIX_1:def_11
.= (Radix k) - (1 * (Radix k)) by A5, Th10
.= 0 ;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) by A5, A20, A54, Def5; ::_thesis: verum
end;
supposeA55: i = m ; ::_thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then  DigA ((SDMax (n,m,k)),i) = 0 by A5, A19, Def3;
then  DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) = (SD_Add_Data ((1 + 0),k)) + (SD_Add_Carry (0 + 0)) by A5, A3, A18, A52, A53, Th7
.= 1 - ((SD_Add_Carry 1) * (Radix k)) by RADIX_1:18, RADIX_1:def_11
.= 1 - (0 * (Radix k)) by RADIX_1:def_10
.= 1 ;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) by A5, A20, A55, Def5; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) ; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) ; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) ; ::_thesis: verum
end;
(SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) = (SDDec ((SDMax (n,m,k)) '+' (DecSD (1,n,k)))) + ((SD_Add_Carry ((DigA ((SDMax (n,m,k)),n)) + (DigA ((DecSD (1,n,k)),n)))) * ((Radix k) |^ n)) by A2, A5, RADIX_2:11
.= (SDDec ((SDMax (n,m,k)) '+' (DecSD (1,n,k)))) + (0 * ((Radix k) |^ n)) by A5, A13, A14, A15, Th8, RADIX_1:18 ;
hence  SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) by A2, A16, Th12; ::_thesis: verum
end;
end;
end;
hence  SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) ; ::_thesis: verum
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)))
proof
let n, m, k be Nat; ::_thesis: ( m in Seg n & k >= 2 implies SDDec (Fmin ((n + 1),(m + 1),k)) = (SDDec (Fmin ((n + 1),m,k))) + (SDDec (Fmax ((n + 1),m,k))) )
assume that
A1: m in Seg n and
A2: k >= 2 ; ::_thesis: SDDec (Fmin ((n + 1),(m + 1),k)) = (SDDec (Fmin ((n + 1),m,k))) + (SDDec (Fmax ((n + 1),m,k)))
 n >= m by A1, FINSEQ_1:1;
then A3: n + 1 > m by NAT_1:13;
A4: n + 1 in Seg (n + 1) by FINSEQ_1:3;
then A5: DigA ((Fmin ((n + 1),m,k)),(n + 1)) = FminDigit (m,k,(n + 1)) by Def6
.= 0 by A2, A3, Def5 ;
A6: m in Seg (n + 1) by A1, FINSEQ_2:8;
A7: m >= 1 by A1, FINSEQ_1:1;
A8: for i being Nat st i in Seg (n + 1) holds
DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
proof
let i be Nat; ::_thesis: ( i in Seg (n + 1) implies DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) )
A9: m + 1 > m by NAT_1:13;
assume A10: i in Seg (n + 1) ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then A11: DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) = Add ((Fmin ((n + 1),m,k)),(Fmax ((n + 1),m,k)),i,k) by RADIX_1:def_14
.= (SD_Add_Data (((DigA ((Fmin ((n + 1),m,k)),i)) + (DigA ((Fmax ((n + 1),m,k)),i))),k)) + (SD_Add_Carry ((DigA ((Fmin ((n + 1),m,k)),(i -' 1))) + (DigA ((Fmax ((n + 1),m,k)),(i -' 1))))) by A2, A10, RADIX_1:def_13 ;
A12: DigA ((Fmin ((n + 1),(m + 1),k)),i) = FminDigit ((m + 1),k,i) by A10, Def6;
A13: DigA ((Fmin ((n + 1),m,k)),i) = FminDigit (m,k,i) by A10, Def6;
A14: DigA ((Fmax ((n + 1),m,k)),i) = FmaxDigit (m,k,i) by A10, Def8;
A15: i >= 1 by A10, FINSEQ_1:1;
now__::_thesis:_DigA_((Fmin_((n_+_1),(m_+_1),k)),i)_=_DigA_(((Fmin_((n_+_1),m,k))_'+'_(Fmax_((n_+_1),m,k))),i)
percases ( i >= m + 1 or i < m + 1 ) ;
supposeA16: i >= m + 1 ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
now__::_thesis:_DigA_((Fmin_((n_+_1),(m_+_1),k)),i)_=_DigA_(((Fmin_((n_+_1),m,k))_'+'_(Fmax_((n_+_1),m,k))),i)
percases ( i = m + 1 or i <> m + 1 ) ;
supposeA17: i = m + 1 ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then A18: DigA ((Fmin ((n + 1),(m + 1),k)),i) = FminDigit ((m + 1),k,(m + 1)) by A10, Def6
.= 1 by A2, Def5 ;
A19: DigA ((Fmax ((n + 1),m,k)),(i -' 1)) = DigA ((Fmax ((n + 1),m,k)),m) by A17, NAT_D:34
.= FmaxDigit (m,k,m) by A6, Def8
.= (Radix k) - 1 by A2, Def7 ;
A20: DigA ((Fmax ((n + 1),m,k)),i) = FmaxDigit (m,k,(m + 1)) by A10, A17, Def8
.= 0 by A2, A9, Def7 ;
A21: DigA ((Fmin ((n + 1),m,k)),(i -' 1)) = DigA ((Fmin ((n + 1),m,k)),m) by A17, NAT_D:34
.= FminDigit (m,k,m) by A6, Def6
.= 1 by A2, Def5 ;
DigA ((Fmin ((n + 1),m,k)),i) = FminDigit (m,k,(m + 1)) by A10, A17, Def6
.= 0 by A2, A9, Def5 ;
then  DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) = 0 + (SD_Add_Carry (1 + ((Radix k) - 1))) by A11, A20, A21, A19, RADIX_1:19
.= 1 by A2, Th10 ;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) by A18; ::_thesis: verum
end;
supposeA22: i <> m + 1 ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then  i > m + 1 by A16, XXREAL_0:1;
then  i - 1 > (m + 1) - 1 by XREAL_1:14;
then A23: i -' 1 > m by XREAL_0:def_2;
 i > m by A16, NAT_1:13;
then  i > 1 by A7, XXREAL_0:2;
then A24: i -' 1 in Seg (n + 1) by A10, Th2;
then A25: DigA ((Fmin ((n + 1),m,k)),(i -' 1)) = FminDigit (m,k,(i -' 1)) by Def6
.= 0 by A2, A23, Def5 ;
A26: DigA ((Fmin ((n + 1),(m + 1),k)),i) = 0 by A2, A12, A22, Def5;
A27: DigA ((Fmax ((n + 1),m,k)),(i -' 1)) = FmaxDigit (m,k,(i -' 1)) by A24, Def8
.= 0 by A2, A23, Def7 ;
 ( DigA ((Fmin ((n + 1),m,k)),i) = 0 & DigA ((Fmax ((n + 1),m,k)),i) = 0 ) by A2, A9, A13, A14, A16, Def5, Def7;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) by A11, A25, A27, A26, RADIX_1:18, RADIX_1:19; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) ; ::_thesis: verum
end;
suppose i < m + 1 ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then A28: i <= m by NAT_1:13;
now__::_thesis:_DigA_((Fmin_((n_+_1),(m_+_1),k)),i)_=_DigA_(((Fmin_((n_+_1),m,k))_'+'_(Fmax_((n_+_1),m,k))),i)
percases ( i > 1 or i = 1 ) by A15, XXREAL_0:1;
supposeA29: i > 1 ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then A30: m > 1 by A28, XXREAL_0:2;
then A31: m -' 1 < m by JORDAN5B:1;
A32: m -' 1 in Seg (n + 1) by A6, A30, Th2;
now__::_thesis:_DigA_((Fmin_((n_+_1),(m_+_1),k)),i)_=_DigA_(((Fmin_((n_+_1),m,k))_'+'_(Fmax_((n_+_1),m,k))),i)
percases ( i = m or i < m ) by A28, XXREAL_0:1;
supposeA33: i = m ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then A34: DigA ((Fmax ((n + 1),m,k)),(i -' 1)) = FmaxDigit (m,k,(m -' 1)) by A32, Def8
.= 0 by A2, A31, Def7 ;
A35: DigA ((Fmax ((n + 1),m,k)),i) = (Radix k) - 1 by A2, A14, A33, Def7;
A36: DigA ((Fmin ((n + 1),(m + 1),k)),i) = FminDigit ((m + 1),k,m) by A10, A33, Def6
.= 0 by A2, A9, Def5 ;
DigA ((Fmin ((n + 1),m,k)),(i -' 1)) = FminDigit (m,k,(m -' 1)) by A32, A33, Def6
.= 0 by A2, A31, Def5 ;
then  DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) = (SD_Add_Data ((1 + ((Radix k) - 1)),k)) + 0 by A2, A11, A13, A33, A35, A34, Def5, RADIX_1:18
.= 0 by A2, Th11 ;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) by A36; ::_thesis: verum
end;
supposeA37: i < m ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
A38: i -' 1 >= 1 by A29, NAT_D:49;
A39: i -' 1 < i by A15, JORDAN5B:1;
then  i -' 1 < m by A37, XXREAL_0:2;
then  i -' 1 <= n + 1 by A3, XXREAL_0:2;
then A40: i -' 1 in Seg (n + 1) by A38, FINSEQ_1:1;
then A41: DigA ((Fmax ((n + 1),m,k)),(i -' 1)) = FmaxDigit (m,k,(i -' 1)) by Def8
.= 0 by A2, A37, A39, Def7 ;
A42: DigA ((Fmax ((n + 1),m,k)),i) = 0 by A2, A14, A37, Def7;
A43: i < m + 1 by A37, NAT_1:13;
DigA ((Fmin ((n + 1),m,k)),(i -' 1)) = FminDigit (m,k,(i -' 1)) by A40, Def6
.= 0 by A2, A37, A39, Def5 ;
then  DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) = (SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (0 + 0)) by A2, A11, A13, A37, A42, A41, Def5
.= 0 + 0 by RADIX_1:18, RADIX_1:19 ;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) by A2, A12, A43, Def5; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) ; ::_thesis: verum
end;
supposeA44: i = 1 ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then A45: DigA ((Fmax ((n + 1),m,k)),(i -' 1)) = 0 by NAT_2:8, RADIX_1:def_3;
now__::_thesis:_DigA_((Fmin_((n_+_1),(m_+_1),k)),i)_=_DigA_(((Fmin_((n_+_1),m,k))_'+'_(Fmax_((n_+_1),m,k))),i)
percases ( i < m or i = m ) by A28, XXREAL_0:1;
supposeA46: i < m ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then  ( DigA ((Fmin ((n + 1),m,k)),i) = 0 & DigA ((Fmax ((n + 1),m,k)),i) = 0 ) by A2, A13, A14, Def5, Def7;
then A47: DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) = (SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (0 + 0)) by A11, A44, A45, NAT_2:8, RADIX_1:def_3
.= 0 + 0 by RADIX_1:18, RADIX_1:19 ;
 i < m + 1 by A46, NAT_1:13;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) by A2, A12, A47, Def5; ::_thesis: verum
end;
supposeA48: i = m ; ::_thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
then  ( DigA ((Fmin ((n + 1),m,k)),i) = 1 & DigA ((Fmax ((n + 1),m,k)),i) = (Radix k) - 1 ) by A2, A13, A14, Def5, Def7;
then A49: DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) = (SD_Add_Data ((1 + ((Radix k) - 1)),k)) + 0 by A11, A44, A45, NAT_2:8, RADIX_1:18, RADIX_1:def_3
.= 0 by A2, Th11 ;
 i < m + 1 by A48, NAT_1:13;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) by A2, A12, A49, Def5; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) ; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) ; ::_thesis: verum
end;
end;
end;
hence  DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i) ; ::_thesis: verum
end;
A50: DigA ((Fmax ((n + 1),m,k)),(n + 1)) = FmaxDigit (m,k,(n + 1)) by A4, Def8
.= 0 by A2, A3, Def7 ;
(SDDec (Fmin ((n + 1),m,k))) + (SDDec (Fmax ((n + 1),m,k))) = (SDDec ((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k)))) + ((SD_Add_Carry ((DigA ((Fmin ((n + 1),m,k)),(n + 1))) + (DigA ((Fmax ((n + 1),m,k)),(n + 1))))) * ((Radix k) |^ (n + 1))) by A2, NAT_1:11, RADIX_2:11
.= (SDDec ((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k)))) + (0 * ((Radix k) |^ (n + 1))) by A5, A50, RADIX_1:18 ;
hence  SDDec (Fmin ((n + 1),(m + 1),k)) = (SDDec (Fmin ((n + 1),m,k))) + (SDDec (Fmax ((n + 1),m,k))) by A8, Th12, NAT_1:11; ::_thesis: verum
end;