let n be non zero 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 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 ; :: thesis: ( 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 ; :: thesis: for k being non zero Nat st k <> 1 & k <= n holds

( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )

defpred S_{1}[ 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; :: 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 )

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 S_{1}[j] holds

S_{1}[j + 1]

(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: S_{1}[1]
by A1, A2, NAT_1:14, XREAL_1:235;

for j being non zero Nat holds S_{1}[j]
from NAT_1:sch 10(A21, A6);

hence ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) by A19, A20; :: thesis: verum

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 ; :: thesis: ( 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 ; :: thesis: for k being non zero Nat st k <> 1 & k <= n holds

( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )

defpred S

let k be non zero 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 )

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 S

S

proof

A17:
1 <= (n -' k) + 1
by NAT_1:11;
let j be non zero Nat; :: thesis: ( S_{1}[j] implies S_{1}[j + 1] )

assume that

A7: S_{1}[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: 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; :: thesis: (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; :: thesis: verum

end;assume that

A7: S

A8: j + 1 in Seg (n -' 1) ; :: thesis: ( 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; :: thesis: (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; :: thesis: verum

(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: S

for j being non zero Nat holds S

hence ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) by A19, A20; :: thesis: verum