let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN st x,y are_summable holds
y,x are_summable
let x, y be Tuple of K, BOOLEAN ; :: thesis: ( x,y are_summable implies y,x are_summable )
assume x,y are_summable ; :: thesis: y,x are_summable
then add_ovfl (x,y) = 0 by BINARITH:def 7;
then P1: (((x /. K) '&' (y /. K)) 'or' ((x /. K) '&' ((carry (x,y)) /. K))) 'or' ((y /. K) '&' ((carry (x,y)) /. K)) = 0 by BINARITH:def 6;
(carry (x,y)) /. K = (carry (y,x)) /. K by LMExtBit501;
then (((y /. K) '&' (x /. K)) 'or' ((y /. K) '&' ((carry (y,x)) /. K))) 'or' ((x /. K) '&' ((carry (y,x)) /. K)) = 0 by P1;
then add_ovfl (y,x) = 0 by BINARITH:def 6;
hence y,x are_summable by BINARITH:def 7; :: thesis: verum