let n be non empty Nat; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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 ; :: thesis: ( x = 0* n implies ( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 ) )
assume A2:
x = 0* n
; :: thesis: ( 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 )
:: thesis: ( k = (2 to_power n) - 1 implies n -BinarySequence k = 'not' x )proof
assume A3:
n -BinarySequence k = 'not' x
;
:: thesis: k = (2 to_power n) - 1
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;
A4:
S1[1]
proof
let k be
Nat;
:: thesis: ( 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 )
assume A5:
k < 2
to_power 1
;
:: thesis: for y being Tuple of 1,BOOLEAN st y = 0* 1 & 1 -BinarySequence k = 'not' y holds
k = (2 to_power 1) - 1
let y be
Tuple of 1,
BOOLEAN ;
:: thesis: ( y = 0* 1 & 1 -BinarySequence k = 'not' y implies k = (2 to_power 1) - 1 )
assume
y = 0* 1
;
:: thesis: ( not 1 -BinarySequence k = 'not' y or k = (2 to_power 1) - 1 )
then A6:
y = <*FALSE *>
by FINSEQ_2:73;
assume A7:
1
-BinarySequence k = 'not' y
;
:: thesis: k = (2 to_power 1) - 1
A8:
1
<= len (1 -BinarySequence k)
by FINSEQ_1:def 18;
A9:
1
in Seg 1
by FINSEQ_1:5;
A10:
k < 2
by A5, POWER:30;
A11: 1 =
<*1*> . 1
by FINSEQ_1:57
.=
(1 -BinarySequence k) /. 1
by A6, A7, A8, Th15, FINSEQ_4:24
.=
IFEQ ((k div (2 to_power (1 -' 1))) mod 2),
0 ,
FALSE ,
TRUE
by A9, Def1
;
k = 1
hence k =
(1 + 1) - 1
.=
(2 to_power 1) - 1
by POWER:30
;
:: thesis: verum
end;
A12:
for
m being non
empty Nat st
S1[
m] holds
S1[
m + 1]
proof
let m be non
empty Nat;
:: thesis: ( S1[m] implies S1[m + 1] )
assume A13:
S1[
m]
;
:: thesis: S1[m + 1]
let k be
Nat;
:: thesis: ( 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 A14:
k < 2
to_power (m + 1)
;
:: thesis: 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 ;
:: thesis: ( y = 0* (m + 1) & (m + 1) -BinarySequence k = 'not' y implies k = (2 to_power (m + 1)) - 1 )
assume that A15:
y = 0* (m + 1)
and A16:
(m + 1) -BinarySequence k = 'not' y
;
:: thesis: k = (2 to_power (m + 1)) - 1
A17:
len y = m + 1
by FINSEQ_1:def 18;
A18:
len ('not' y) = m + 1
by FINSEQ_1:def 18;
A19:
m + 1
in Seg (m + 1)
by FINSEQ_1:6;
0 <= m
by NAT_1:2;
then A20:
0 + 1
<= m + 1
by XREAL_1:8;
A21:
y . (m + 1) = FALSE
by A15, FINSEQ_1:6, FUNCOP_1:13;
A22:
((m + 1) -BinarySequence k) . (m + 1) =
('not' y) /. (m + 1)
by A16, A18, A20, FINSEQ_4:24
.=
'not' (y /. (m + 1))
by A19, BINARITH:def 4
.=
'not' FALSE
by A17, A20, A21, FINSEQ_4:24
.=
TRUE
;
then A23:
(m + 1) -BinarySequence k = (m -BinarySequence (k -' (2 to_power m))) ^ <*TRUE *>
by A14, Lm3, Th27;
k < (2 to_power m) * (2 to_power 1)
by A14, POWER:32;
then
k < 2
* (2 to_power m)
by POWER:30;
then
k < (2 to_power m) + (2 to_power m)
;
then
k - (2 to_power m) < 2
to_power m
by XREAL_1:21;
then A24:
k -' (2 to_power m) < 2
to_power m
by A22, Th27, XREAL_1:235;
0* m in BOOLEAN *
by Th5;
then A25:
0* m is
FinSequence of
BOOLEAN
by FINSEQ_1:def 11;
len (0* m) = m
by FINSEQ_1:def 18;
then reconsider y1 =
0* m as
Tuple of
m,
BOOLEAN by A25, FINSEQ_2:110;
y = y1 ^ <*0 *>
by A15, FINSEQ_2:74;
then
(m -BinarySequence (k -' (2 to_power m))) ^ <*TRUE *> = ('not' y1) ^ <*('not' FALSE )*>
by A16, A23, BINARI_2:11;
then
m -BinarySequence (k -' (2 to_power m)) = 'not' y1
by FINSEQ_2:20;
then
k -' (2 to_power m) = (2 to_power m) - 1
by A13, A24;
then
k - (2 to_power m) = (2 to_power m) - 1
by A22, Th27, XREAL_1:235;
hence k =
((2 to_power m) * 2) - 1
.=
((2 to_power m) * (2 to_power 1)) - 1
by POWER:30
.=
(2 to_power (m + 1)) - 1
by POWER:32
;
:: thesis: verum
end;
for
m being non
empty Nat holds
S1[
m]
from NAT_1:sch 10(A4, A12);
hence
k = (2 to_power n) - 1
by A1, A2, A3;
:: thesis: verum
end;
assume A26:
k = (2 to_power n) - 1
; :: thesis: n -BinarySequence k = 'not' x
now let i be
Nat;
:: thesis: ( i in Seg n implies (n -BinarySequence k) . i = ('not' x) . i )assume A27:
i in Seg n
;
:: thesis: (n -BinarySequence k) . i = ('not' x) . ithen
i in Seg (len (n -BinarySequence k))
by FINSEQ_1:def 18;
then A28:
i in dom (n -BinarySequence k)
by FINSEQ_1:def 3;
A29:
len x = n
by FINSEQ_1:def 18;
A30:
len ('not' x) = n
by FINSEQ_1:def 18;
A31:
( 1
<= i &
i <= n )
by A27, FINSEQ_1:3;
A32:
x . i = FALSE
by A2, A27, FUNCOP_1:13;
2
to_power (i -' 1) > 0
by POWER:39;
then A33:
2
to_power (i -' 1) >= 0 + 1
by NAT_1:13;
A34:
( 1
<= i &
i <= n )
by A27, FINSEQ_1:3;
then
i < n + 1
by NAT_1:13;
then
i - 1
< (n + 1) - 1
by XREAL_1:11;
then A35:
0 + (i -' 1) < n
by A34, XREAL_1:235;
then
n - (i -' 1) > 0
by XREAL_1:22;
then
n -' (i -' 1) > 0
by A35, XREAL_1:235;
then A36:
(2 to_power (n -' (i -' 1))) mod 2
= 0
by NAT_2:19;
A37:
2
to_power (n -' (i -' 1)) > 0
by POWER:39;
then A38:
2
to_power (n -' (i -' 1)) >= 0 + 1
by NAT_1:13;
2
to_power n > 0
by POWER:39;
then A39:
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 A26, XREAL_1:235
.=
((2 to_power n) div (2 to_power (i -' 1))) - 1
by A33, A35, A39, NAT_2:13, NAT_2:17
.=
(2 to_power (n -' (i -' 1))) - 1
by A35, NAT_2:18
.=
(2 to_power (n -' (i -' 1))) -' 1
by A38, XREAL_1:235
;
then A40:
(k div (2 to_power (i -' 1))) mod 2
= 1
by A36, A37, NAT_2:20;
reconsider z =
i as
Nat ;
thus (n -BinarySequence k) . i =
(n -BinarySequence k) /. i
by A28, PARTFUN1:def 8
.=
IFEQ ((k div (2 to_power (i -' 1))) mod 2),
0 ,
FALSE ,
TRUE
by A27, Def1
.=
'not' FALSE
by A40, FUNCOP_1:def 8
.=
'not' (x /. z)
by A29, A31, A32, FINSEQ_4:24
.=
('not' x) /. z
by A27, BINARITH:def 4
.=
('not' x) . i
by A30, A31, FINSEQ_4:24
;
:: thesis: verum end;
hence
n -BinarySequence k = 'not' x
by FINSEQ_2:139; :: thesis: verum