let n be non zero Nat; for k being Nat st k < 2 to_power n holds
for x being Tuple of n, BOOLEAN st x = 0* n holds
( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 )
let k be Nat; ( k < 2 to_power n implies for x being Tuple of n, BOOLEAN st x = 0* n holds
( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 ) )
assume A1:
k < 2 to_power n
; for x being Tuple of n, BOOLEAN st x = 0* n holds
( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 )
let x be Tuple of n, BOOLEAN ; ( x = 0* n implies ( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 ) )
assume A2:
x = 0* n
; ( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 )
thus
( n -BinarySequence k = 'not' x implies k = (2 to_power n) - 1 )
( k = (2 to_power n) - 1 implies n -BinarySequence k = 'not' x )proof
defpred S1[
Nat]
means for
k being
Nat st
k < 2
to_power $1 holds
for
y being
Tuple of $1,
BOOLEAN st
y = 0* $1 & $1
-BinarySequence k = 'not' y holds
k = (2 to_power $1) - 1;
assume A3:
n -BinarySequence k = 'not' x
;
k = (2 to_power n) - 1
A4:
for
m being non
zero Nat st
S1[
m] holds
S1[
m + 1]
proof
let m be non
zero Nat;
( S1[m] implies S1[m + 1] )
assume A5:
S1[
m]
;
S1[m + 1]
A6:
m + 1
in Seg (m + 1)
by FINSEQ_1:4;
A7:
0 + 1
<= m + 1
by XREAL_1:6;
0* m in BOOLEAN *
by Th4;
then
0* m is
FinSequence of
BOOLEAN
by FINSEQ_1:def 11;
then reconsider y1 =
0* m as
Tuple of
m,
BOOLEAN ;
let k be
Nat;
( k < 2 to_power (m + 1) implies for y being Tuple of m + 1, BOOLEAN st y = 0* (m + 1) & (m + 1) -BinarySequence k = 'not' y holds
k = (2 to_power (m + 1)) - 1 )
assume A8:
k < 2
to_power (m + 1)
;
for y being Tuple of m + 1, BOOLEAN st y = 0* (m + 1) & (m + 1) -BinarySequence k = 'not' y holds
k = (2 to_power (m + 1)) - 1
let y be
Tuple of
m + 1,
BOOLEAN ;
( y = 0* (m + 1) & (m + 1) -BinarySequence k = 'not' y implies k = (2 to_power (m + 1)) - 1 )
assume that A9:
y = 0* (m + 1)
and A10:
(m + 1) -BinarySequence k = 'not' y
;
k = (2 to_power (m + 1)) - 1
A11:
y . (m + 1) = FALSE
by A9, FINSEQ_1:4, FUNCOP_1:7;
A12:
y = y1 ^ <*0*>
by A9, FINSEQ_2:60;
A13:
len y = m + 1
by CARD_1:def 7;
len ('not' y) = m + 1
by CARD_1:def 7;
then A14:
((m + 1) -BinarySequence k) . (m + 1) =
('not' y) /. (m + 1)
by A10, A7, FINSEQ_4:15
.=
'not' (y /. (m + 1))
by A6, BINARITH:def 1
.=
'not' FALSE
by A13, A7, A11, FINSEQ_4:15
.=
TRUE
;
then
(m + 1) -BinarySequence k = (m -BinarySequence (k -' (2 to_power m))) ^ <*TRUE*>
by A8, Lm3, Th26;
then
(m -BinarySequence (k -' (2 to_power m))) ^ <*TRUE*> = ('not' y1) ^ <*('not' FALSE)*>
by A10, A12, BINARI_2:9;
then A15:
m -BinarySequence (k -' (2 to_power m)) = 'not' y1
by FINSEQ_2:17;
k < (2 to_power m) * (2 to_power 1)
by A8, POWER:27;
then
k < 2
* (2 to_power m)
by POWER:25;
then
k < (2 to_power m) + (2 to_power m)
;
then
k - (2 to_power m) < 2
to_power m
by XREAL_1:19;
then
k -' (2 to_power m) < 2
to_power m
by A14, Th26, XREAL_1:233;
then
k -' (2 to_power m) = (2 to_power m) - 1
by A5, A15;
then
k - (2 to_power m) = (2 to_power m) - 1
by A14, Th26, XREAL_1:233;
hence k =
((2 to_power m) * 2) - 1
.=
((2 to_power m) * (2 to_power 1)) - 1
by POWER:25
.=
(2 to_power (m + 1)) - 1
by POWER:27
;
verum
end;
A16:
S1[1]
proof
let k be
Nat;
( k < 2 to_power 1 implies for y being Tuple of 1, BOOLEAN st y = 0* 1 & 1 -BinarySequence k = 'not' y holds
k = (2 to_power 1) - 1 )
A17:
1
<= len (1 -BinarySequence k)
by CARD_1:def 7;
assume
k < 2
to_power 1
;
for y being Tuple of 1, BOOLEAN st y = 0* 1 & 1 -BinarySequence k = 'not' y holds
k = (2 to_power 1) - 1
then A18:
k < 2
by POWER:25;
let y be
Tuple of 1,
BOOLEAN ;
( y = 0* 1 & 1 -BinarySequence k = 'not' y implies k = (2 to_power 1) - 1 )
assume
y = 0* 1
;
( not 1 -BinarySequence k = 'not' y or k = (2 to_power 1) - 1 )
then A19:
y = <*FALSE*>
by FINSEQ_2:59;
assume A20:
1
-BinarySequence k = 'not' y
;
k = (2 to_power 1) - 1
A21:
1
in Seg 1
by FINSEQ_1:3;
A22: 1 =
<*1*> . 1
by FINSEQ_1:40
.=
(1 -BinarySequence k) /. 1
by A19, A20, A17, Th14, FINSEQ_4:15
.=
IFEQ (
((k div (2 to_power (1 -' 1))) mod 2),
0,
FALSE,
TRUE)
by A21, Def1
;
k = 1
hence k =
(1 + 1) - 1
.=
(2 to_power 1) - 1
by POWER:25
;
verum
end;
for
m being non
zero Nat holds
S1[
m]
from NAT_1:sch 10(A16, A4);
hence
k = (2 to_power n) - 1
by A1, A2, A3;
verum
end;
assume A23:
k = (2 to_power n) - 1
; n -BinarySequence k = 'not' x
now for i being Nat st i in Seg n holds
(n -BinarySequence k) . i = ('not' x) . ilet i be
Nat;
( i in Seg n implies (n -BinarySequence k) . i = ('not' x) . i )A24:
len x = n
by CARD_1:def 7;
2
to_power (i -' 1) > 0
by POWER:34;
then A25:
2
to_power (i -' 1) >= 0 + 1
by NAT_1:13;
A26:
len ('not' x) = n
by CARD_1:def 7;
A27:
2
to_power (n -' (i -' 1)) > 0
by POWER:34;
then A28:
2
to_power (n -' (i -' 1)) >= 0 + 1
by NAT_1:13;
reconsider z =
i as
Nat ;
assume A29:
i in Seg n
;
(n -BinarySequence k) . i = ('not' x) . ithen A30:
1
<= i
by FINSEQ_1:1;
i <= n
by A29, FINSEQ_1:1;
then
i < n + 1
by NAT_1:13;
then A31:
i - 1
< (n + 1) - 1
by XREAL_1:9;
1
<= i
by A29, FINSEQ_1:1;
then A32:
0 + (i -' 1) < n
by A31, XREAL_1:233;
then
n - (i -' 1) > 0
by XREAL_1:20;
then
n -' (i -' 1) > 0
by A32, XREAL_1:233;
then A33:
(2 to_power (n -' (i -' 1))) mod 2
= 0
by NAT_2:17;
2
to_power n > 0
by POWER:34;
then A34:
2
to_power n >= 0 + 1
by NAT_1:13;
then k div (2 to_power (i -' 1)) =
((2 to_power n) -' 1) div (2 to_power (i -' 1))
by A23, XREAL_1:233
.=
((2 to_power n) div (2 to_power (i -' 1))) - 1
by A25, A32, A34, NAT_2:11, NAT_2:15
.=
(2 to_power (n -' (i -' 1))) - 1
by A32, NAT_2:16
.=
(2 to_power (n -' (i -' 1))) -' 1
by A28, XREAL_1:233
;
then A35:
(k div (2 to_power (i -' 1))) mod 2
= 1
by A33, A27, NAT_2:18;
A36:
x . i = FALSE
by A2, A29, FUNCOP_1:7;
A37:
i <= n
by A29, FINSEQ_1:1;
i in Seg (len (n -BinarySequence k))
by A29, CARD_1:def 7;
then
i in dom (n -BinarySequence k)
by FINSEQ_1:def 3;
hence (n -BinarySequence k) . i =
(n -BinarySequence k) /. i
by PARTFUN1:def 6
.=
IFEQ (
((k div (2 to_power (i -' 1))) mod 2),
0,
FALSE,
TRUE)
by A29, Def1
.=
'not' FALSE
by A35, FUNCOP_1:def 8
.=
'not' (x /. z)
by A24, A30, A37, A36, FINSEQ_4:15
.=
('not' x) /. z
by A29, BINARITH:def 1
.=
('not' x) . i
by A26, A30, A37, FINSEQ_4:15
;
verum end;
hence
n -BinarySequence k = 'not' x
by FINSEQ_2:119; verum