let n be non zero Nat; 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 ; ( 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
; x = 'not' y
A4:
len x = n
by CARD_1:def 7;
A5:
len ('not' y) = n
by CARD_1:def 7;
A6:
len y = n
by CARD_1:def 7;
A7:
len (carry (x,(Bin1 n))) = n
by CARD_1:def 7;
now for i being Nat st i in Seg n holds
x . i = ('not' y) . ilet i be
Nat;
( i in Seg n implies x . i = ('not' y) . i )reconsider z =
i as
Nat ;
assume A8:
i in Seg n
;
x . i = ('not' y) . ithen A9:
1
<= i
by FINSEQ_1:1;
A10:
i <= n
by A8, FINSEQ_1:1;
A11:
y . i = FALSE
by A1, A8, FUNCOP_1:7;
now x . i = ('not' y) . iper cases
( i = 1 or i <> 1 )
;
suppose A12:
i = 1
;
x . i = ('not' y) . iA13:
n >= 1
by NAT_1:14;
now x . i = ('not' y) . iper cases
( n = 1 or n > 1 )
by A13, XXREAL_0:1;
suppose A14:
n > 1
;
x . i = ('not' y) . iA15:
len ('not' (Bin1 n)) = n
by CARD_1:def 7;
A16:
(carry (x,(Bin1 n))) /. i = FALSE
by A12, BINARITH:def 2;
then A17:
((Bin1 n) /. i) '&' ((carry (x,(Bin1 n))) /. i) = FALSE
;
A18:
1
+ 1
<= n
by A14, NAT_1:13;
then A19:
2
in Seg n
by FINSEQ_1:1;
(carry (x,(Bin1 n))) . (i + 1) =
('not' (Bin1 n)) . 2
by A2, A3, A12, Th20
.=
('not' (Bin1 n)) /. 2
by A18, A15, FINSEQ_4:15
.=
'not' ((Bin1 n) /. 2)
by A19, BINARITH:def 1
.=
'not' FALSE
by A19, BINARI_2:6
.=
TRUE
;
then A20:
TRUE =
(carry (x,(Bin1 n))) /. (i + 1)
by A7, A12, A18, FINSEQ_4:15
.=
((x /. i) '&' ((Bin1 n) /. i)) 'or' ((x /. i) '&' ((carry (x,(Bin1 n))) /. i))
by A12, A14, A16, A17, BINARITH:def 2
.=
(x /. i) '&' ((Bin1 n) /. i)
by A16
;
thus x . i =
x /. z
by A4, A9, A10, FINSEQ_4:15
.=
'not' FALSE
by A20, MARGREL1:12
.=
'not' (y /. z)
by A6, A9, A10, A11, FINSEQ_4:15
.=
('not' y) /. z
by A8, BINARITH:def 1
.=
('not' y) . i
by A5, A9, A10, FINSEQ_4:15
;
verum end; end; end; hence
x . i = ('not' y) . i
;
verum end; suppose A21:
i <> 1
;
x . i = ('not' y) . i
1
<= i
by A8, FINSEQ_1:1;
then
0 < i
;
then A22:
not
i is
empty
;
thus x . i =
x /. z
by A4, A9, A10, FINSEQ_4:15
.=
'not' FALSE
by A2, A3, A10, A21, A22, Th19
.=
'not' (y /. z)
by A6, A9, A10, A11, FINSEQ_4:15
.=
('not' y) /. z
by A8, BINARITH:def 1
.=
('not' y) . i
by A5, A9, A10, FINSEQ_4:15
;
verum end; end; end; hence
x . i = ('not' y) . i
;
verum end;
hence
x = 'not' y
by FINSEQ_2:119; verum