let n be non zero Nat; for k being Nat st 2 to_power n <= k & k < 2 to_power (n + 1) holds
(n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>
let k be Nat; ( 2 to_power n <= k & k < 2 to_power (n + 1) implies (n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*> )
assume that
A1:
2 to_power n <= k
and
A2:
k < 2 to_power (n + 1)
; (n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>
now for i being Nat st i in Seg (n + 1) holds
((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . ilet i be
Nat;
( i in Seg (n + 1) implies ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i )reconsider z =
i as
Nat ;
assume A3:
i in Seg (n + 1)
;
((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . ithen
i in Seg (len ((n + 1) -BinarySequence k))
by CARD_1:def 7;
then A4:
i in dom ((n + 1) -BinarySequence k)
by FINSEQ_1:def 3;
now ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . iper cases
( i in Seg n or i = n + 1 )
by A3, FINSEQ_2:7;
suppose A5:
i in Seg n
;
((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . ithen A6:
1
<= i
by FINSEQ_1:1;
A7: 2
* (2 to_power (i -' 1)) =
(2 to_power (i -' 1)) * (2 to_power 1)
by POWER:25
.=
2
to_power ((i -' 1) + 1)
by POWER:27
.=
2
to_power ((i - 1) + 1)
by A6, XREAL_1:233
.=
2
to_power i
;
2
to_power (i -' 1) > 0
by POWER:34;
then A8:
0 + 1
<= 2
to_power (i -' 1)
by NAT_1:13;
i <= n
by A5, FINSEQ_1:1;
then A9:
2
* (2 to_power (z -' 1)) divides 2
to_power n
by A7, NAT_2:11;
i in Seg (len (n -BinarySequence (k -' (2 to_power n))))
by A5, CARD_1:def 7;
then A15:
i in dom (n -BinarySequence (k -' (2 to_power n)))
by FINSEQ_1:def 3;
thus ((n + 1) -BinarySequence k) . i =
((n + 1) -BinarySequence k) /. i
by A4, PARTFUN1:def 6
.=
IFEQ (
((k div (2 to_power (i -' 1))) mod 2),
0,
FALSE,
TRUE)
by A3, Def1
.=
(n -BinarySequence (k -' (2 to_power n))) /. i
by A5, A10, Def1
.=
(n -BinarySequence (k -' (2 to_power n))) . i
by A15, PARTFUN1:def 6
.=
((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i
by A15, FINSEQ_1:def 7
;
verum end; end; end; hence
((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i
;
verum end;
hence
(n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>
by FINSEQ_2:119; verum