let n be non zero Nat; for x, y being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
for k being non zero Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
let x, y be Tuple of n, BOOLEAN ; ( x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE implies for k being non zero Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) )
assume that
A1:
x /. n = TRUE
and
A2:
(carry (x,(Bin1 n))) /. n = TRUE
; for k being non zero Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
defpred S1[ Nat] means ( $1 in Seg (n -' 1) implies ( x /. ((n -' $1) + 1) = TRUE & (carry (x,(Bin1 n))) /. ((n -' $1) + 1) = TRUE ) );
let k be non zero Nat; ( k <> 1 & k <= n implies ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) )
assume that
A3:
k <> 1
and
A4:
k <= n
; ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
set i = (n -' k) + 1;
1 < k
by A3, NAT_2:19;
then
1 + 1 <= k
by NAT_1:13;
then A5:
1 <= k - 1
by XREAL_1:19;
A6:
for j being non zero Nat st S1[j] holds
S1[j + 1]
proof
let j be non
zero Nat;
( S1[j] implies S1[j + 1] )
assume that A7:
S1[
j]
and A8:
j + 1
in Seg (n -' 1)
;
( x /. ((n -' (j + 1)) + 1) = TRUE & (carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE )
A9:
j + 1
<= n -' 1
by A8, FINSEQ_1:1;
then A10:
j < n -' 1
by NAT_1:13;
then
j < n - 1
by NAT_1:14, XREAL_1:233;
then
j + 1
< n
by XREAL_1:20;
then A11:
j < n
by NAT_1:13;
j + 1
<= n - 1
by A9, NAT_1:14, XREAL_1:233;
then
1
<= (n - 1) - j
by XREAL_1:19;
then
1
<= (n - j) - 1
;
then
1
+ 1
<= n - j
by XREAL_1:19;
then
1
+ 1
<= n -' j
by A11, XREAL_1:233;
then A12:
n -' j > 1
by NAT_1:13;
A13:
1
<= j
by NAT_1:14;
A14:
n -' j < n
by NAT_2:9;
then
n -' j in Seg n
by A12, FINSEQ_1:1;
then A15:
(Bin1 n) /. (n -' j) = FALSE
by A12, BINARI_2:6;
then
((Bin1 n) /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j)) = FALSE
;
then A16:
TRUE =
((x /. (n -' j)) '&' ((Bin1 n) /. (n -' j))) 'or' ((x /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j)))
by A7, A13, A10, A14, A12, A15, BINARITH:def 2, FINSEQ_1:1
.=
(x /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j))
by A15
;
then
x /. (n -' j) = TRUE
by MARGREL1:12;
hence
x /. ((n -' (j + 1)) + 1) = TRUE
by A11, NAT_2:7;
(carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE
(carry (x,(Bin1 n))) /. (n -' j) = TRUE
by A16, MARGREL1:12;
hence
(carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE
by A11, NAT_2:7;
verum
end;
A17:
1 <= (n -' k) + 1
by NAT_1:11;
(n -' k) + 1 =
(n - k) + 1
by A4, XREAL_1:233
.=
n - (k - 1)
;
then A18:
(n -' k) + 1 <= n - 1
by A5, XREAL_1:13;
then
((n -' k) + 1) + 1 <= n
by XREAL_1:19;
then
(n -' k) + 1 < n
by NAT_1:13;
then A19:
k = (n -' ((n -' k) + 1)) + 1
by A4, NAT_2:5;
(n -' k) + 1 <= n -' 1
by A18, NAT_1:14, XREAL_1:233;
then A20:
(n -' k) + 1 in Seg (n -' 1)
by A17, FINSEQ_1:1;
A21:
S1[1]
by A1, A2, NAT_1:14, XREAL_1:235;
for j being non zero Nat holds S1[j]
from NAT_1:sch 10(A21, A6);
hence
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
by A19, A20; verum