let K be non zero Nat; for x, y being Tuple of K, BOOLEAN holds carry (x,y) = carry (y,x)
let x, y be Tuple of K, BOOLEAN ; carry (x,y) = carry (y,x)
A1:
( (carry (x,y)) /. 1 = FALSE & ( for i being Nat st 1 <= i & i < K holds
(carry (x,y)) /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' ((carry (x,y)) /. i))) 'or' ((y /. i) '&' ((carry (x,y)) /. i)) ) )
by BINARITH:def 2;
for i being Nat st 1 <= i & i < K holds
(carry (x,y)) /. (i + 1) = (((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' ((carry (x,y)) /. i))) 'or' ((x /. i) '&' ((carry (x,y)) /. i))
proof
let i be
Nat;
( 1 <= i & i < K implies (carry (x,y)) /. (i + 1) = (((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' ((carry (x,y)) /. i))) 'or' ((x /. i) '&' ((carry (x,y)) /. i)) )
assume
( 1
<= i &
i < K )
;
(carry (x,y)) /. (i + 1) = (((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' ((carry (x,y)) /. i))) 'or' ((x /. i) '&' ((carry (x,y)) /. i))
hence (carry (x,y)) /. (i + 1) =
(((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' ((carry (x,y)) /. i))) 'or' ((y /. i) '&' ((carry (x,y)) /. i))
by BINARITH:def 2
.=
(((y /. i) '&' (x /. i)) 'or' ((y /. i) '&' ((carry (x,y)) /. i))) 'or' ((x /. i) '&' ((carry (x,y)) /. i))
;
verum
end;
hence
carry (x,y) = carry (y,x)
by A1, BINARITH:def 2; verum