let n be non empty Nat; :: thesis: for x, y being Tuple of n,BOOLEAN st x /. n = TRUE & (carry x,(Bin1 n)) /. n = TRUE holds
for k being non empty Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry x,(Bin1 n)) /. k = TRUE )
let x, y be Tuple of n,BOOLEAN ; :: thesis: ( x /. n = TRUE & (carry x,(Bin1 n)) /. n = TRUE implies for k being non empty 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
; :: thesis: for k being non empty Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry x,(Bin1 n)) /. k = TRUE )
let k be non empty Nat; :: thesis: ( k <> 1 & k <= n implies ( x /. k = TRUE & (carry x,(Bin1 n)) /. k = TRUE ) )
assume that
A3:
k <> 1
and
A4:
k <= n
; :: thesis: ( 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 ) );
A5:
S1[1]
by A1, A2, NAT_1:14, XREAL_1:237;
A6:
for j being non empty Nat st S1[j] holds
S1[j + 1]
proof
let j be non
empty Nat;
:: thesis: ( S1[j] implies S1[j + 1] )
assume that A7:
S1[
j]
and A8:
j + 1
in Seg (n -' 1)
;
:: thesis: ( x /. ((n -' (j + 1)) + 1) = TRUE & (carry x,(Bin1 n)) /. ((n -' (j + 1)) + 1) = TRUE )
A9:
( 1
<= j + 1 &
j + 1
<= n -' 1 )
by A8, FINSEQ_1:3;
A10:
1
<= j
by NAT_1:14;
A11:
j < n -' 1
by A9, NAT_1:13;
then
j < n - 1
by NAT_1:14, XREAL_1:235;
then
j + 1
< n
by XREAL_1:22;
then A12:
j < n
by NAT_1:13;
A13:
n -' j < n
by NAT_2:11;
j + 1
<= n - 1
by A9, NAT_1:14, XREAL_1:235;
then
1
<= (n - 1) - j
by XREAL_1:21;
then
1
<= (n - j) - 1
;
then
1
+ 1
<= n - j
by XREAL_1:21;
then
1
+ 1
<= n -' j
by A12, XREAL_1:235;
then A14:
n -' j > 1
by NAT_1:13;
then
n -' j in Seg n
by A13, FINSEQ_1:3;
then A15:
(Bin1 n) /. (n -' j) = FALSE
by A14, BINARI_2:8;
then
(
(x /. (n -' j)) '&' ((Bin1 n) /. (n -' j)) = FALSE &
((Bin1 n) /. (n -' j)) '&' ((carry x,(Bin1 n)) /. (n -' j)) = FALSE )
;
then TRUE =
((x /. (n -' j)) '&' ((Bin1 n) /. (n -' j))) 'or' ((x /. (n -' j)) '&' ((carry x,(Bin1 n)) /. (n -' j)))
by A7, A10, A11, A13, A14, BINARITH:def 5, FINSEQ_1:3
.=
(x /. (n -' j)) '&' ((carry x,(Bin1 n)) /. (n -' j))
by A15
;
then A16:
(
x /. (n -' j) = TRUE &
(carry x,(Bin1 n)) /. (n -' j) = TRUE )
by MARGREL1:45;
hence
x /. ((n -' (j + 1)) + 1) = TRUE
by A12, NAT_2:9;
:: thesis: (carry x,(Bin1 n)) /. ((n -' (j + 1)) + 1) = TRUE
thus
(carry x,(Bin1 n)) /. ((n -' (j + 1)) + 1) = TRUE
by A12, A16, NAT_2:9;
:: thesis: verum
end;
A17:
for j being non empty Nat holds S1[j]
from NAT_1:sch 10(A5, A6);
set i = (n -' k) + 1;
A18:
1 <= (n -' k) + 1
by NAT_1:11;
A19: (n -' k) + 1 =
(n - k) + 1
by A4, XREAL_1:235
.=
n - (k - 1)
;
1 < k
by A3, NAT_2:21;
then
1 + 1 <= k
by NAT_1:13;
then
1 <= k - 1
by XREAL_1:21;
then A20:
(n -' k) + 1 <= n - 1
by A19, XREAL_1:15;
then A21:
(n -' k) + 1 <= n -' 1
by NAT_1:14, XREAL_1:235;
((n -' k) + 1) + 1 <= n
by A20, XREAL_1:21;
then
(n -' k) + 1 < n
by NAT_1:13;
then A22:
k = (n -' ((n -' k) + 1)) + 1
by A4, NAT_2:7;
(n -' k) + 1 in Seg (n -' 1)
by A18, A21, FINSEQ_1:3;
hence
( x /. k = TRUE & (carry x,(Bin1 n)) /. k = TRUE )
by A17, A22; :: thesis: verum