let n be non empty Nat; :: thesis: for x, y being Tuple of n,BOOLEAN st y = 0* n & x /. n = TRUE & (carry x,(Bin1 n)) /. n = TRUE holds
x = 'not' y
let x, y be Tuple of n,BOOLEAN ; :: thesis: ( y = 0* n & x /. n = TRUE & (carry x,(Bin1 n)) /. n = TRUE implies x = 'not' y )
assume that
A1: y = 0* n and
A2: x /. n = TRUE and
A3: (carry x,(Bin1 n)) /. n = TRUE ; :: thesis: x = 'not' y
A4: len x = n by FINSEQ_1:def 18;
A5: len y = n by FINSEQ_1:def 18;
A6: len ('not' y) = n by FINSEQ_1:def 18;
A7: len (carry x,(Bin1 n)) = n by FINSEQ_1:def 18;

now

let i be Nat; :: thesis: ( i in Seg n implies x . i = ('not' y) . i )
assume A8: i in Seg n ; :: thesis: x . i = ('not' y) . i
then A9: ( 1 <= i & i <= n ) by FINSEQ_1:3;
reconsider z = i as Nat ;
A10: y . i = FALSE by A1, A8, FUNCOP_1:13;

now

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

suppose A11: i = 1 ; :: thesis: x . i = ('not' y) . i

A12: n >= 1 by NAT_1:14;

now

per cases ( n = 1 or n > 1 ) by A12, XXREAL_0:1;

suppose n = 1 ; :: thesis: x . i = ('not' y) . i

hence x . i = ('not' y) . i by A3, BINARITH:def 5; :: thesis: verum

end;

suppose A13: n > 1 ; :: thesis: x . i = ('not' y) . i

then A14: 1 + 1 <= n by NAT_1:13;
then A15: 2 in Seg n by FINSEQ_1:3;
A16: len ('not' (Bin1 n)) = n by FINSEQ_1:def 18;
A17: (carry x,(Bin1 n)) /. i = FALSE by A11, BINARITH:def 5;
then A18: ( (x /. i) '&' ((carry x,(Bin1 n)) /. i) = FALSE & ((Bin1 n) /. i) '&' ((carry x,(Bin1 n)) /. i) = FALSE ) ;
(carry x,(Bin1 n)) . (i + 1) = ('not' (Bin1 n)) . 2 by A2, A3, A11, Th21
.= ('not' (Bin1 n)) /. 2 by A14, A16, FINSEQ_4:24
.= 'not' ((Bin1 n) /. 2) by A15, BINARITH:def 4
.= 'not' FALSE by A15, BINARI_2:8
.= TRUE ;
then A19: TRUE = (carry x,(Bin1 n)) /. (i + 1) by A7, A11, A14, FINSEQ_4:24
.= ((x /. i) '&' ((Bin1 n) /. i)) 'or' ((x /. i) '&' ((carry x,(Bin1 n)) /. i)) by A11, A13, A18, BINARITH:def 5
.= (x /. i) '&' ((Bin1 n) /. i) by A17 ;
thus x . i = x /. z by A4, A9, FINSEQ_4:24
.= 'not' FALSE by A19, MARGREL1:45
.= 'not' (y /. z) by A5, A9, A10, FINSEQ_4:24
.= ('not' y) /. z by A8, BINARITH:def 4
.= ('not' y) . i by A6, A9, FINSEQ_4:24 ; :: thesis: verum

end;

end;

end;

hence x . i = ('not' y) . i ; :: thesis: verum

end;

suppose A20: i <> 1 ; :: thesis: x . i = ('not' y) . i

A21: not i is empty by A8, FINSEQ_1:3;
thus x . i = x /. z by A4, A9, FINSEQ_4:24
.= 'not' FALSE by A2, A3, A9, A20, A21, Th20
.= 'not' (y /. z) by A5, A9, A10, FINSEQ_4:24
.= ('not' y) /. z by A8, BINARITH:def 4
.= ('not' y) . i by A6, A9, FINSEQ_4:24 ; :: thesis: verum

end;

end;

end;

hence x . i = ('not' y) . i ; :: thesis: verum

end;

hence x = 'not' y by FINSEQ_2:139; :: thesis: verum