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

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

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

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 :: thesis: DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)

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

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

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

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

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

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

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

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

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

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

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

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:8, RADIX_1:def 3;

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

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

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