let K be non zero Nat; for x, y being Tuple of K, BOOLEAN st x,y are_summable & x . (len x) = 1 holds
(x + y) . (len (x + y)) = 1
let x, y be Tuple of K, BOOLEAN ; ( x,y are_summable & x . (len x) = 1 implies (x + y) . (len (x + y)) = 1 )
assume AS:
( x,y are_summable & x . (len x) = 1 )
; (x + y) . (len (x + y)) = 1
L0:
len y = K
by CARD_1:def 7;
1 <= len y
by NAT_1:25;
then
len y in Seg K
by L0, FINSEQ_1:1;
then L1:
len y in dom y
by L0, FINSEQ_1:def 3;
R0:
len x = K
by CARD_1:def 7;
1 <= len x
by NAT_1:25;
then PR2:
len x in dom x
by FINSEQ_3:25;
P1:
y . (len y) = 0
P2:
len (x + y) = K
by CARD_1:def 7;
1 <= len (x + y)
by NAT_1:25;
then P3:
len (x + y) in Seg K
by P2, FINSEQ_1:1;
then PP5:
len (x + y) in dom (x + y)
by P2, FINSEQ_1:def 3;
R3:
x /. (len (x + y)) = 1
by PR2, P2, R0, AS, PARTFUN1:def 6;
L3:
y /. (len (x + y)) = 0
by P2, L0, P1, L1, PARTFUN1:def 6;
K1:
(carry (x,y)) /. (len (x + y)) = 0
(x + y) /. (len (x + y)) =
((x /. (len (x + y))) 'xor' (y /. (len (x + y)))) 'xor' ((carry (x,y)) /. (len (x + y)))
by P3, BINARITH:def 5
.=
1
by L3, K1, PR2, P2, R0, AS, PARTFUN1:def 6
;
hence
(x + y) . (len (x + y)) = 1
by PP5, PARTFUN1:def 6; verum