let n be non zero Nat; for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
carry (x,y) = 0* n
let x, y be Tuple of n, BOOLEAN ; ( x = 0* n & y = 0* n implies carry (x,y) = 0* n )
assume that
A1:
x = 0* n
and
A2:
y = 0* n
; carry (x,y) = 0* n
A3:
for j being Nat st 1 < j & j <= n holds
(carry (x,y)) . j = 0
proof
let j be
Nat;
( 1 < j & j <= n implies (carry (x,y)) . j = 0 )
assume that A4:
1
< j
and A5:
j <= n
;
(carry (x,y)) . j = 0
reconsider k =
j - 1 as
Element of
NAT by A4, INT_1:5;
k + 1
= j
;
then A6:
( 1
<= k &
k < n )
by A4, A5, NAT_1:13;
len (0* n) = n
by CARD_1:def 7;
then A7:
x /. k =
(0* n) . k
by A1, A6, FINSEQ_4:15
.=
FALSE
;
A8:
j = k + 1
;
len (carry (x,y)) = n
by CARD_1:def 7;
then (carry (x,y)) . j =
(carry (x,y)) /. j
by A4, A5, FINSEQ_4:15
.=
((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (x,y)) /. k))) 'or' (FALSE '&' ((carry (x,y)) /. k))
by A1, A2, A6, A8, A7, BINARITH:def 2
.=
FALSE
;
hence
(carry (x,y)) . j = 0
;
verum
end;
1 <= len (carry (x,y))
by NAT_1:14;
then A9: (carry (x,y)) . 1 =
(carry (x,y)) /. 1
by FINSEQ_4:15
.=
0
by BINARITH:def 2
;
for l being Nat st l in Seg n holds
(carry (x,y)) . l = (0* n) . l
hence
carry (x,y) = 0* n
by A1, FINSEQ_2:119; verum