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

defpred S₁[ 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 ; :: thesis: k = (2 to_power n) - 1
A4: for m being non empty Nat st S₁[m] holds
S₁[m + 1]

proof

let m be non empty Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: S₁[m] ; :: thesis: S₁[m + 1]
A6: m + 1 in Seg (m + 1) by FINSEQ_1:6;
0 <= m by NAT_1:2;
then A7: 0 + 1 <= m + 1 by XREAL_1:8;
0* m in BOOLEAN * by Th5;
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; :: 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 A9: 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
A10: y = 0* (m + 1) and
A11: (m + 1) -BinarySequence k = 'not' y ; :: thesis: k = (2 to_power (m + 1)) - 1
A12: y . (m + 1) = FALSE by A10, FINSEQ_1:6, FUNCOP_1:13;
A13: y = y1 ^ <*0 *> by A10, FINSEQ_2:74;
A14: len y = m + 1 by FINSEQ_1:def 18;
len ('not' y) = m + 1 by FINSEQ_1:def 18;
then A15: ((m + 1) -BinarySequence k) . (m + 1) = ('not' y) /. (m + 1) by A11, A7, FINSEQ_4:24
.= 'not' (y /. (m + 1)) by A6, BINARITH:def 4
.= 'not' FALSE by A14, A7, A12, FINSEQ_4:24
.= TRUE ;
then (m + 1) -BinarySequence k = (m -BinarySequence (k -' (2 to_power m))) ^ <*TRUE *> by A9, Lm3, Th27;
then (m -BinarySequence (k -' (2 to_power m))) ^ <*TRUE *> = ('not' y1) ^ <*('not' FALSE )*> by A11, A13, BINARI_2:11;
then A16: m -BinarySequence (k -' (2 to_power m)) = 'not' y1 by FINSEQ_2:20;
k < (2 to_power m) * (2 to_power 1) by A9, 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 k -' (2 to_power m) < 2 to_power m by A15, Th27, XREAL_1:235;
then k -' (2 to_power m) = (2 to_power m) - 1 by A5, A16;
then k - (2 to_power m) = (2 to_power m) - 1 by A15, 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;

A17: S₁[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 )
A18: 1 <= len (1 -BinarySequence k) by FINSEQ_1:def 18;
assume 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
then A19: k < 2 by POWER:30;
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 A20: y = <*FALSE *> by FINSEQ_2:73;
assume A21: 1 -BinarySequence k = 'not' y ; :: thesis: k = (2 to_power 1) - 1
A22: 1 in Seg 1 by FINSEQ_1:5;
A23: 1 = <*1*> . 1 by FINSEQ_1:57
.= (1 -BinarySequence k) /. 1 by A20, A21, A18, Th15, FINSEQ_4:24
.= IFEQ ((k div (2 to_power (1 -' 1))) mod 2),0 ,FALSE ,TRUE by A22, Def1 ;
k = 1

proof

assume k <> 1 ; :: thesis: contradiction
then k = 0 by A19, NAT_1:23;
then k div (2 to_power (1 -' 1)) = 0 by NAT_D:27, POWER:39;
then (k div (2 to_power (1 -' 1))) mod 2 = 0 by NAT_D:26;
hence contradiction by A23, FUNCOP_1:def 8; :: thesis: verum

end;

hence k = (1 + 1) - 1
.= (2 to_power 1) - 1 by POWER:30 ;
:: thesis: verum

end;

for m being non empty Nat holds S₁[m] from NAT_1:sch 10(A17, A4);
hence k = (2 to_power n) - 1 by A1, A2, A3; :: thesis: verum

end;

assume A24: 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 )
A25: len x = n by FINSEQ_1:def 18;
2 to_power (i -' 1) > 0 by POWER:39;
then A26: 2 to_power (i -' 1) >= 0 + 1 by NAT_1:13;
A27: len ('not' x) = n by FINSEQ_1:def 18;
A28: 2 to_power (n -' (i -' 1)) > 0 by POWER:39;
then A29: 2 to_power (n -' (i -' 1)) >= 0 + 1 by NAT_1:13;
reconsider z = i as Nat ;
assume A30: i in Seg n ; :: thesis: (n -BinarySequence k) . i = ('not' x) . i
then A31: 1 <= i by FINSEQ_1:3;
i <= n by A30, FINSEQ_1:3;
then i < n + 1 by NAT_1:13;
then A32: i - 1 < (n + 1) - 1 by XREAL_1:11;
1 <= i by A30, FINSEQ_1:3;
then A33: 0 + (i -' 1) < n by A32, XREAL_1:235;
then n - (i -' 1) > 0 by XREAL_1:22;
then n -' (i -' 1) > 0 by A33, XREAL_1:235;
then A34: (2 to_power (n -' (i -' 1))) mod 2 = 0 by NAT_2:19;
2 to_power n > 0 by POWER:39;
then A35: 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 A24, XREAL_1:235
.= ((2 to_power n) div (2 to_power (i -' 1))) - 1 by A26, A33, A35, NAT_2:13, NAT_2:17
.= (2 to_power (n -' (i -' 1))) - 1 by A33, NAT_2:18
.= (2 to_power (n -' (i -' 1))) -' 1 by A29, XREAL_1:235 ;
then A36: (k div (2 to_power (i -' 1))) mod 2 = 1 by A34, A28, NAT_2:20;
A37: x . i = FALSE by A2, A30, FUNCOP_1:13;
A38: i <= n by A30, FINSEQ_1:3;
i in Seg (len (n -BinarySequence k)) by A30, FINSEQ_1:def 18;
then i in dom (n -BinarySequence k) by FINSEQ_1:def 3;
hence (n -BinarySequence k) . i = (n -BinarySequence k) /. i by PARTFUN1:def 8
.= IFEQ ((k div (2 to_power (i -' 1))) mod 2),0 ,FALSE ,TRUE by A30, Def1
.= 'not' FALSE by A36, FUNCOP_1:def 8
.= 'not' (x /. z) by A25, A31, A38, A37, FINSEQ_4:24
.= ('not' x) /. z by A30, BINARITH:def 4
.= ('not' x) . i by A27, A31, A38, FINSEQ_4:24 ;
:: thesis: verum

end;

hence n -BinarySequence k = 'not' x by FINSEQ_2:139; :: thesis: verum