let n be non zero 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) )
A1: n >= 1 by NAT_1:14;
A2: len y = n by CARD_1:def 7;
assume A3: y = 0* n ; :: thesis: carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)
then A4: y . n = 0 by FINSEQ_1:3, FUNCOP_1:7;
n in Seg n by FINSEQ_1:3;
then A5: ('not' y) /. n = 'not' (y /. n) by BINARITH:def 1
.= 'not' FALSE by A1, A4, A2, FINSEQ_4:15
.= TRUE ;

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

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

now :: thesis: for i being Nat st i in Seg n holds
(carry (('not' y),(Bin1 n))) . i = ('not' (Bin1 n)) . i

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

end;

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

end;

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

then A10: not n is trivial by NAT_2:def 1;
defpred S₁[ Nat] means ( $1 <= n implies (carry (('not' y),(Bin1 n))) /. $1 = TRUE );
A11: 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
A12: ( i <= n implies (carry (('not' y),(Bin1 n))) /. i = TRUE ) and
A13: i + 1 <= n ; :: thesis: (carry (('not' y),(Bin1 n))) /. (i + 1) = TRUE
A14: 1 <= i by NAT_1:14;
A15: i < n by A13, NAT_1:13;
then A16: i in Seg n by A14, FINSEQ_1:1;
then A17: y . i = FALSE by A3, FUNCOP_1:7;
A18: ('not' y) /. i = 'not' (y /. i) by A16, BINARITH:def 1
.= 'not' FALSE by A2, A14, A15, A17, FINSEQ_4:15
.= TRUE ;
i <> 1 by NAT_2:def 1;
then A19: (Bin1 n) /. i = FALSE by A16, BINARI_2:6;
then ((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 A14, A15, A19, BINARITH:def 2
.= TRUE by A12, A13, A18, NAT_1:13 ;
:: thesis: verum

end;

A20: S₁[2]

proof

assume 2 <= n ; :: thesis: (carry (('not' y),(Bin1 n))) /. 2 = TRUE
then 1 + 1 <= n ;
then A21: 1 < n by NAT_1:13;
then A22: 1 in Seg n by FINSEQ_1:1;
then A23: y . 1 = FALSE by A3, FUNCOP_1:7;
('not' y) /. 1 = 'not' (y /. 1) by A22, BINARITH:def 1
.= 'not' FALSE by A2, A21, A23, FINSEQ_4:15
.= TRUE ;
then A24: (('not' y) /. 1) '&' ((Bin1 n) /. 1) = TRUE by A22, BINARI_2:5;
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 A21, BINARITH:def 2
.= TRUE by A24 ; :: thesis: verum

end;

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

end;

end;