let K be non zero Nat; for x, y being Tuple of K, BOOLEAN st y = 0* K holds
( x + y = x & y + x = x )
let x, y be Tuple of K, BOOLEAN ; ( y = 0* K implies ( x + y = x & y + x = x ) )
assume AS:
y = 0* K
; ( x + y = x & y + x = x )
for i being Nat st i in Seg K holds
(x + y) . i = x . i
proof
let i be
Nat;
( i in Seg K implies (x + y) . i = x . i )
assume A1:
i in Seg K
;
(x + y) . i = x . i
then A4:
( 1
<= i &
i <= K &
i <> 0 )
by FINSEQ_1:1;
A2:
y /. i = 0
by AS, A4, LMExtBit4;
A3:
(carry (x,y)) /. i = 0
by AS, A4, LMExtBit3;
len x = K
by CARD_1:def 7;
then D1:
dom x = Seg K
by FINSEQ_1:def 3;
len (x + y) = K
by CARD_1:def 7;
then D2:
dom (x + y) = Seg K
by FINSEQ_1:def 3;
thus (x + y) . i =
(x + y) /. i
by D2, A1, PARTFUN1:def 6
.=
((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i)
by BINARITH:def 5, A1
.=
x . i
by D1, A1, PARTFUN1:def 6, A2, A3
;
verum
end;
hence
x + y = x
by FINSEQ_2:119; y + x = x
hence
y + x = x
by LMExtBit500; verum