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:3;
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:3;
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:3;
A7: m >= 1 by A4, FINSEQ_1:3;

now

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

suppose A8: 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: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 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;

suppose A13: 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:3;
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:3;

now

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

suppose A22: 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

per cases ( 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:22 ;
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:16;
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:22 ;
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: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 < m by JORDAN5B:1;
A33: m -' 1 in Seg n by A4, A31, Th2;
then A34: m -' 1 >= 1 by FINSEQ_1:3;

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 (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:20;

now

per cases ( 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: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 A5, A3, A18, A36, A38, Th7
.= 0 + (SD_Add_Carry (((Radix k) - 1) + 1)) by RADIX_1:22
.= 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;

suppose A40: 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 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:22
.= 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;

suppose A42: 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:20;

now

per cases ( 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:235;
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;

suppose A49: 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 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;

suppose A52: 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:10, RADIX_1:def 3;

now

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

suppose A54: 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:21, 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;

suppose A55: 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: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 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:21 ;
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