let n be non zero Nat; 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 ; ( 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
; 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
;
carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)now for i being Nat st i in Seg n holds
(carry (('not' y),(Bin1 n))) . i = ('not' (Bin1 n)) . ilet i be
Nat;
( 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
;
(carry (('not' y),(Bin1 n))) . i = ('not' (Bin1 n)) . ithen 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
;
verum end; hence
carry (
('not' y),
(Bin1 n))
= 'not' (Bin1 n)
by FINSEQ_2:119;
verum end; suppose
n <> 1
;
carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)then A10:
not
n is
trivial
by NAT_2:def 1;
defpred S1[
Nat]
means ( $1
<= n implies
(carry (('not' y),(Bin1 n))) /. $1
= TRUE );
A11:
for
i being non
trivial Nat st
S1[
i] holds
S1[
i + 1]
proof
let i be non
trivial Nat;
( S1[i] implies S1[i + 1] )
assume that A12:
(
i <= n implies
(carry (('not' y),(Bin1 n))) /. i = TRUE )
and A13:
i + 1
<= n
;
(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
;
verum
end; A20:
S1[2]
proof
assume
2
<= n
;
(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
;
verum
end;
for
i being non
trivial Nat holds
S1[
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;
verum end; end;