let n be non empty Nat; :: thesis: for y being Tuple of n,BOOLEAN st y = 0* n holds
carry ('not' y),(Bin1 n) = 'not' (Bin1 n)
let y be Tuple of n,BOOLEAN ; :: thesis: ( y = 0* n implies carry ('not' y),(Bin1 n) = 'not' (Bin1 n) )
assume A1: y = 0* n ; :: thesis: carry ('not' y),(Bin1 n) = 'not' (Bin1 n)
A2: n in Seg n by FINSEQ_1:5;
A3: n >= 1 by NAT_1:14;
A4: y . n = 0 by A1, FINSEQ_1:5, FUNCOP_1:13;
A5: len y = n by FINSEQ_1:def 18;
A6: ('not' y) /. n = 'not' (y /. n) by A2, BINARITH:def 4
.= 'not' FALSE by A3, A4, A5, FINSEQ_4:24
.= TRUE ;

per cases ( n = 1 or n <> 1 ) ;

suppose A7: n = 1 ; :: thesis: carry ('not' y),(Bin1 n) = 'not' (Bin1 n)

now

let i be Nat; :: thesis: ( i in Seg n implies (carry ('not' y),(Bin1 n)) . i = ('not' (Bin1 n)) . i )
assume A8: i in Seg n ; :: thesis: (carry ('not' y),(Bin1 n)) . i = ('not' (Bin1 n)) . i
then A9: i = 1 by A7, FINSEQ_1:4, TARSKI:def 1;
A10: len ('not' (Bin1 n)) = n by FINSEQ_1:def 18;
len (carry ('not' y),(Bin1 n)) = n by FINSEQ_1:def 18;
hence (carry ('not' y),(Bin1 n)) . i = (carry ('not' y),(Bin1 n)) /. i by A7, A9, FINSEQ_4:24
.= 'not' TRUE by A9, BINARITH:def 5
.= 'not' ((Bin1 n) /. i) by A8, A9, BINARI_2:7
.= ('not' (Bin1 n)) /. i by A8, BINARITH:def 4
.= ('not' (Bin1 n)) . i by A7, A9, A10, FINSEQ_4:24 ;
:: thesis: verum

end;

hence carry ('not' y),(Bin1 n) = 'not' (Bin1 n) by FINSEQ_2:139; :: thesis: verum

end;

suppose n <> 1 ; :: thesis: carry ('not' y),(Bin1 n) = 'not' (Bin1 n)

then A11: not n is trivial by NAT_2:def 1;
defpred S₁[ Nat] means ( $1 <= n implies (carry ('not' y),(Bin1 n)) /. $1 = TRUE );
A12: S₁[2]

proof

assume 2 <= n ; :: thesis: (carry ('not' y),(Bin1 n)) /. 2 = TRUE
then 1 + 1 <= n ;
then A13: 1 < n by NAT_1:13;
then A14: 1 in Seg n by FINSEQ_1:3;
then A15: y . 1 = FALSE by A1, FUNCOP_1:13;
('not' y) /. 1 = 'not' (y /. 1) by A14, BINARITH:def 4
.= 'not' FALSE by A5, A13, A15, FINSEQ_4:24
.= TRUE ;
then A16: (('not' y) /. 1) '&' ((Bin1 n) /. 1) = TRUE by A14, BINARI_2:7;
thus (carry ('not' y),(Bin1 n)) /. 2 = (carry ('not' y),(Bin1 n)) /. (1 + 1)
.= (((('not' y) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' y) /. 1) '&' ((carry ('not' y),(Bin1 n)) /. 1))) 'or' (((Bin1 n) /. 1) '&' ((carry ('not' y),(Bin1 n)) /. 1)) by A13, BINARITH:def 5
.= TRUE by A16 ; :: thesis: verum

end;

A17: for i being non trivial Nat st S₁[i] holds
S₁[i + 1]

proof

let i be non trivial Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A18: ( i <= n implies (carry ('not' y),(Bin1 n)) /. i = TRUE ) and
A19: i + 1 <= n ; :: thesis: (carry ('not' y),(Bin1 n)) /. (i + 1) = TRUE
A20: 1 <= i by NAT_1:14;
A21: i < n by A19, NAT_1:13;
then A22: i in Seg n by A20, FINSEQ_1:3;
then A23: y . i = FALSE by A1, FUNCOP_1:13;
A24: ('not' y) /. i = 'not' (y /. i) by A22, BINARITH:def 4
.= 'not' FALSE by A5, A20, A21, A23, FINSEQ_4:24
.= TRUE ;
i <> 1 by NAT_2:def 1;
then (Bin1 n) /. i = FALSE by A22, BINARI_2:8;
then ( (('not' y) /. i) '&' ((Bin1 n) /. i) = FALSE & ((Bin1 n) /. i) '&' ((carry ('not' y),(Bin1 n)) /. i) = FALSE ) ;
hence (carry ('not' y),(Bin1 n)) /. (i + 1) = ((('not' y) /. i) '&' ((Bin1 n) /. i)) 'or' ((('not' y) /. i) '&' ((carry ('not' y),(Bin1 n)) /. i)) by A20, A21, BINARITH:def 5
.= TRUE by A18, A19, A24, NAT_1:13 ;
:: thesis: verum

end;

for i being non trivial Nat holds S₁[i] from NAT_2:sch 2(A12, A17);
then (carry ('not' y),(Bin1 n)) /. n = TRUE by A11;
hence carry ('not' y),(Bin1 n) = 'not' (Bin1 n) by A6, Th21; :: thesis: verum

end;

end;