let n be non zero Nat; for k being Nat st k < 2 to_power n holds
Absval (n -BinarySequence k) = k
defpred S1[ Nat] means ( $1 < 2 to_power n implies Absval (n -BinarySequence $1) = $1 );
A1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
0* n in BOOLEAN *
by Th4;
then
0* n is
FinSequence of
BOOLEAN
by FINSEQ_1:def 11;
then reconsider 0n =
0* n as
Tuple of
n,
BOOLEAN ;
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
(
k < 2
to_power n implies
Absval (n -BinarySequence k) = k )
;
S1[k + 1]
assume A3:
k + 1
< 2
to_power n
;
Absval (n -BinarySequence (k + 1)) = k + 1
then A4:
(k + 1) - 1
< (2 to_power n) - 1
by XREAL_1:9;
k < 2
to_power n
by A3, NAT_1:13;
then
n -BinarySequence k <> 'not' 0n
by A4, Lm4;
then
add_ovfl (
(n -BinarySequence k),
(Bin1 n))
<> TRUE
by Th23;
then
add_ovfl (
(n -BinarySequence k),
(Bin1 n))
= FALSE
by XBOOLEAN:def 3;
then A5:
n -BinarySequence k,
Bin1 n are_summable
by BINARITH:def 7;
thus Absval (n -BinarySequence (k + 1)) =
Absval ((n -BinarySequence k) + (Bin1 n))
by A3, Th33
.=
(Absval (n -BinarySequence k)) + (Absval (Bin1 n))
by A5, BINARITH:22
.=
k + 1
by A2, A3, Th11, NAT_1:13
;
verum
end;
A6:
S1[ 0 ]
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A6, A1); verum