let m, k be Nat; ( m >= 1 & k >= 2 implies for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k))) )
assume that
A1:
m >= 1
and
A2:
k >= 2
; for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))
let r be Tuple of m + 2,k -SD ; SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))
A3:
m + 2 > 1
by A1, Lm1;
A4: (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k))) =
(SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k)))
by A1, A2, Th12
.=
(SDDec (M0 r)) + 0
by A3, RADIX_5:6
;
A5:
(SDDec (M0 r)) + 1 > (SDDec (M0 r)) + 0
by XREAL_1:8;
m in Seg (m + 2)
by A1, FINSEQ_3:9;
then SDDec (Fmin ((m + 2),m,k)) =
(SDDec (SDMax ((m + 2),m,k))) + (SDDec (DecSD (1,(m + 2),k)))
by A2, A3, RADIX_5:18
.=
(SDDec (SDMax ((m + 2),m,k))) + 1
by A2, A3, RADIX_5:9
;
hence
SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))
by A4, A5; verum