defpred S1[ Nat] means for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin ((m + $1),m,k)) = SDDec (Fmin (m,m,k));
A1:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1
and A2:
S1[
n]
;
S1[n + 1]
let m,
k be
Nat;
( m >= 1 & k >= 2 implies SDDec (Fmin ((m + (n + 1)),m,k)) = SDDec (Fmin (m,m,k)) )
assume that A3:
m >= 1
and A4:
k >= 2
;
SDDec (Fmin ((m + (n + 1)),m,k)) = SDDec (Fmin (m,m,k))
m + n >= m
by NAT_1:11;
then A5:
(m + n) + 1
> m
by NAT_1:13;
(m + n) + 1
in Seg ((m + n) + 1)
by FINSEQ_1:4;
then A6:
DigA (
(Fmin (((m + n) + 1),m,k)),
((m + n) + 1)) =
FminDigit (
m,
k,
((m + n) + 1))
by RADIX_5:def 6
.=
0
by A4, A5, RADIX_5:def 5
;
for
i being
Nat st
i in Seg (m + n) holds
(Fmin (((m + n) + 1),m,k)) . i = (Fmin ((m + n),m,k)) . i
proof
let i be
Nat;
( i in Seg (m + n) implies (Fmin (((m + n) + 1),m,k)) . i = (Fmin ((m + n),m,k)) . i )
assume A7:
i in Seg (m + n)
;
(Fmin (((m + n) + 1),m,k)) . i = (Fmin ((m + n),m,k)) . i
then A8:
i in Seg ((m + n) + 1)
by FINSEQ_2:8;
then (Fmin (((m + n) + 1),m,k)) . i =
DigA (
(Fmin (((m + n) + 1),m,k)),
i)
by RADIX_1:def 3
.=
FminDigit (
m,
k,
i)
by A8, RADIX_5:def 6
.=
DigA (
(Fmin ((m + n),m,k)),
i)
by A7, RADIX_5:def 6
;
hence
(Fmin (((m + n) + 1),m,k)) . i = (Fmin ((m + n),m,k)) . i
by A7, RADIX_1:def 3;
verum
end;
then SDDec (Fmin ((m + (n + 1)),m,k)) =
(SDDec (Fmin ((m + n),m,k))) + (((Radix k) |^ (m + n)) * (DigA ((Fmin (((m + n) + 1),m,k)),((m + n) + 1))))
by RADIX_2:10
.=
SDDec (Fmin (m,m,k))
by A2, A3, A4, A6
;
hence
SDDec (Fmin ((m + (n + 1)),m,k)) = SDDec (Fmin (m,m,k))
;
verum
end;
A9:
S1[1]
proof
let m,
k be
Nat;
( m >= 1 & k >= 2 implies SDDec (Fmin ((m + 1),m,k)) = SDDec (Fmin (m,m,k)) )
assume that
m >= 1
and A10:
k >= 2
;
SDDec (Fmin ((m + 1),m,k)) = SDDec (Fmin (m,m,k))
A11:
m + 1
> m
by NAT_1:13;
for
i being
Nat st
i in Seg m holds
(Fmin ((m + 1),m,k)) . i = (Fmin (m,m,k)) . i
proof
let i be
Nat;
( i in Seg m implies (Fmin ((m + 1),m,k)) . i = (Fmin (m,m,k)) . i )
assume A12:
i in Seg m
;
(Fmin ((m + 1),m,k)) . i = (Fmin (m,m,k)) . i
then A13:
i in Seg (m + 1)
by FINSEQ_2:8;
then (Fmin ((m + 1),m,k)) . i =
DigA (
(Fmin ((m + 1),m,k)),
i)
by RADIX_1:def 3
.=
FminDigit (
m,
k,
i)
by A13, RADIX_5:def 6
.=
DigA (
(Fmin (m,m,k)),
i)
by A12, RADIX_5:def 6
;
hence
(Fmin ((m + 1),m,k)) . i = (Fmin (m,m,k)) . i
by A12, RADIX_1:def 3;
verum
end;
then A14:
SDDec (Fmin ((m + 1),m,k)) = (SDDec (Fmin (m,m,k))) + (((Radix k) |^ m) * (DigA ((Fmin ((m + 1),m,k)),(m + 1))))
by RADIX_2:10;
m + 1
in Seg (m + 1)
by FINSEQ_1:4;
then DigA (
(Fmin ((m + 1),m,k)),
(m + 1)) =
FminDigit (
m,
k,
(m + 1))
by RADIX_5:def 6
.=
0
by A10, A11, RADIX_5:def 5
;
hence
SDDec (Fmin ((m + 1),m,k)) = SDDec (Fmin (m,m,k))
by A14;
verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A9, A1);
hence
for n being Nat st n >= 1 holds
for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin ((m + n),m,k)) = SDDec (Fmin (m,m,k))
; verum