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)) )
assume A1: 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))
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 A2: ( m in Seg n & k >= 2 ) ; :: thesis: SDDec (Fmin n,m,k) = (SDDec (SDMax n,m,k)) + (SDDec (DecSD 1,n,k))
then A3: ( n >= m & m >= 1 ) by FINSEQ_1:3;
A4: 1 in Seg 1 by FINSEQ_1:3;
A5: 1 in Seg n by A1, FINSEQ_1:3;

now

per cases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;

suppose A6: n = 1 ; :: thesis: SDDec (Fmin n,m,k) = (SDDec (SDMax n,m,k)) + (SDDec (DecSD 1,n,k))

A7: 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 A4, 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 A2, A4, 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:234
.= (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:234
.= (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 A2, A4, Th7 ;
A8: m = 1 by A3, A6, XXREAL_0:1;
A9: DigA (SDMax 1,m,k),1 = SDMaxDigit m,k,1 by A4, Def4
.= 0 by A2, A3, A6, Def3 ;
then A10: SDDec ((SDMax 1,m,k) '+' (DecSD 1,1,k)) = 1 - ((SD_Add_Carry 1) * (Radix k)) by A7, RADIX_1:def 11
.= 1 - (0 * (Radix k)) by RADIX_1:def 10
.= 1 ;
A11: (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 A2, RADIX_2:11
.= 1 + ((SD_Add_Carry (0 + 1)) * ((Radix k) |^ 1)) by A2, A4, A9, A10, Th7
.= 1 + (0 * ((Radix k) |^ 1)) by RADIX_1:def 10 ;
SDDec (Fmin 1,m,k) = DigA (Fmin 1,m,k),1 by Th4
.= FminDigit m,k,1 by A4, Def6
.= 1 by A2, A8, Def5 ;
hence SDDec (Fmin n,m,k) = (SDDec (SDMax n,m,k)) + (SDDec (DecSD 1,n,k)) by A6, A11; :: thesis: verum

end;

suppose A12: n > 1 ; :: thesis: SDDec (Fmin n,m,k) = (SDDec (SDMax n,m,k)) + (SDDec (DecSD 1,n,k))

A13: n in Seg n by A1, FINSEQ_1:3;
then A14: DigA (SDMax n,m,k),n = SDMaxDigit m,k,n by Def4
.= 0 by A2, A3, Def3 ;
A15: (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 A1, A2, RADIX_2:11
.= (SDDec ((SDMax n,m,k) '+' (DecSD 1,n,k))) + (0 * ((Radix k) |^ n)) by A2, A12, A13, A14, Th8, RADIX_1:21 ;
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 A16: i in Seg n ; :: thesis: DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i
then A17: 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 A2, A16, RADIX_1:def 13 ;
A18: DigA (Fmin n,m,k),i = FminDigit m,k,i by A16, Def6;
A19: DigA (SDMax n,m,k),i = SDMaxDigit m,k,i by A16, Def4;
A20: ( i >= 1 & i <= n ) by A16, FINSEQ_1:3;

now

per cases ( i >= m + 1 or i < m + 1 ) ;

suppose A21: i >= m + 1 ; :: thesis: DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i

then A22: i > m by NAT_1:13;
then A23: i > 1 by A3, XXREAL_0:2;
then A24: i -' 1 in Seg n by A16, Th2;
A25: DigA (SDMax n,m,k),i = 0 by A2, A19, A22, Def3;
A26: DigA (DecSD 1,n,k),i = 0 by A2, A16, A23, Th8;

now

per cases ( i = m + 1 or i > m + 1 ) by A21, 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 A2, Def4
.= 0 by A2, Def3 ;
then DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i = (SD_Add_Data (0 + 0 ),k) + 0 by A2, A17, A24, A25, A26, Lm2
.= 0 by RADIX_1:22 ;
hence DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i by A2, A18, A22, 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:16;
then A27: i -' 1 > m by XREAL_0:def 2;
i -' 1 in Seg n by A16, A23, Th2;
then DigA (SDMax n,m,k),(i -' 1) = SDMaxDigit m,k,(i -' 1) by Def4
.= 0 by A2, A27, Def3 ;
then DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i = (SD_Add_Data (0 + 0 ),k) + 0 by A2, A17, A24, A25, A26, Lm2
.= 0 by RADIX_1:22 ;
hence DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i by A2, A18, A22, 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 A16, FINSEQ_1:3;

now

per cases ( i > 1 or i = 1 ) by A29, XXREAL_0:1;

suppose A30: 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 in Seg n by A2, Th2;
then A33: m -' 1 >= 1 by FINSEQ_1:3;
A34: m -' 1 < m by A31, JORDAN5B:1;

now

per cases ( i = m or i < m ) by A28, XXREAL_0:1;

suppose A35: i = m ; :: thesis: DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i

then A36: DigA (Fmin n,m,k),i = FminDigit m,k,m by A2, Def6
.= 1 by A2, Def5 ;
A37: DigA (SDMax n,m,k),i = 0 by A2, A19, A35, Def3;
A38: DigA (DecSD 1,n,k),i = 0 by A2, A30, A35, Th8;
A39: DigA (SDMax n,m,k),(i -' 1) = SDMaxDigit m,k,(m -' 1) by A32, A35, Def4
.= (Radix k) - 1 by A2, A33, A34, Def3 ;
A40: i >= 1 + 1 by A30, INT_1:20;

now

per cases ( i = 2 or i > 2 ) by A40, 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:235;
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 A2, A5, A17, A37, A38, A39, Th7
.= 0 + (SD_Add_Carry (((Radix k) - 1) + 1)) by RADIX_1:22
.= 1 by A2, Th10 ;
hence DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i by A36; :: thesis: verum

end;

suppose A41: 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:16;
then A42: i -' 1 > 1 by XREAL_0:def 2;
i > 1 by A41, XXREAL_0:2;
then i -' 1 in Seg n by A16, 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 A2, A17, A37, A38, A39, A42, Th8
.= 0 + (SD_Add_Carry ((Radix k) - 1)) by RADIX_1:22
.= 1 by A2, Lm1 ;
hence DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i by A36; :: 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 A43: i < m ; :: thesis: DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i

A44: DigA (DecSD 1,n,k),i = 0 by A2, A16, A30, Th8;
A45: i >= 1 + 1 by A30, INT_1:20;
i -' 1 < i by A30, JORDAN5B:1;
then A46: i -' 1 < m by A43, XXREAL_0:2;
A47: i -' 1 in Seg n by A16, A30, Th2;

now

per cases ( i = 2 or i > 2 ) by A45, XXREAL_0:1;

suppose i = 2 ; :: thesis: DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i

then A48: i -' 1 = 2 - 1 by XREAL_1:235;
then A49: DigA (DecSD 1,n,k),(i -' 1) = 1 by A2, A5, Th7;
DigA (SDMax n,m,k),(i -' 1) = SDMaxDigit m,k,(i -' 1) by A47, Def4
.= (Radix k) - 1 by A2, A46, A48, 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 A2, A17, A19, A20, A43, A44, A49, Def3
.= (SD_Add_Data ((Radix k) - 1),k) + 1 by A2, 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 A2, Lm1
.= 0 ;
hence DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i by A2, A18, A43, Def5; :: thesis: verum

end;

suppose A50: 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:16;
then A51: i -' 1 > 1 by XREAL_0:def 2;
i > 1 by A50, XXREAL_0:2;
then i -' 1 in Seg n by A16, Th2;
then A52: DigA (DecSD 1,n,k),(i -' 1) = 0 by A2, A51, Th8;
DigA (SDMax n,m,k),(i -' 1) = SDMaxDigit m,k,(i -' 1) by A47, Def4
.= (Radix k) - 1 by A2, A46, A51, 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 A2, A17, A19, A20, A43, A44, A52, Def3
.= (SD_Add_Data ((Radix k) - 1),k) + 1 by A2, 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 A2, Lm1
.= 0 ;
hence DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i by A2, A18, A43, 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;

suppose A53: i = 1 ; :: thesis: DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i

then A54: i -' 1 = 0 by NAT_2:10;
then A55: DigA (SDMax n,m,k),(i -' 1) = 0 by RADIX_1:def 3;
A56: DigA (DecSD 1,n,k),(i -' 1) = 0 by A54, RADIX_1:def 3;

now

per cases ( i < m or i = m ) by A28, XXREAL_0:1;

suppose A57: 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 A2, A19, A53, 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 A2, A5, A17, A53, A55, A56, Th7
.= (Radix k) - ((SD_Add_Carry (Radix k)) * (Radix k)) by RADIX_1:21, RADIX_1:def 11
.= (Radix k) - (1 * (Radix k)) by A2, Th10
.= 0 ;
hence DigA (Fmin n,m,k),i = DigA ((SDMax n,m,k) '+' (DecSD 1,n,k)),i by A2, A18, A57, Def5; :: thesis: verum

end;

suppose A58: 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 A2, 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 A2, A5, A17, A53, A55, A56, Th7
.= 1 - ((SD_Add_Carry 1) * (Radix k)) by RADIX_1:21, 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 A2, A18, A58, 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;

hence SDDec (Fmin n,m,k) = (SDDec (SDMax n,m,k)) + (SDDec (DecSD 1,n,k)) by A1, A15, Th12; :: thesis: verum

end;

end;

end;

hence SDDec (Fmin n,m,k) = (SDDec (SDMax n,m,k)) + (SDDec (DecSD 1,n,k)) ; :: thesis: verum