let n be non zero 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 zero Nat st S₁[m] holds
S₁[m + 1]

proof

let m be non zero 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: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; :: 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 A8: 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
A9: y = 0* (m + 1) and
A10: (m + 1) -BinarySequence k = 'not' y ; :: thesis: 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 ;
:: thesis: verum

end;

A16: 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 )
A17: 1 <= len (1 -BinarySequence k) by CARD_1:def 7;
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 A18: k < 2 by POWER:25;
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 A19: y = <*FALSE*> by FINSEQ_2:59;
assume A20: 1 -BinarySequence k = 'not' y ; :: thesis: k = (2 to_power 1) - 1
A21: 1 in Seg 1 by FINSEQ_1:3;
A22: 1 = <*1*> . 1
.= (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

proof

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

end;

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

end;

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

end;

assume A23: k = (2 to_power n) - 1 ; :: thesis: n -BinarySequence k = 'not' x

now :: thesis: for i being Nat st i in Seg n holds
(n -BinarySequence k) . i = ('not' x) . i

let i be Nat; :: thesis: ( 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 ; :: thesis: (n -BinarySequence k) . i = ('not' x) . i
then 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 ;
:: thesis: verum

end;

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