let a, b be Integer; :: thesis: ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) )

per cases ( ( a is even & b is even ) or ( a is odd & b is odd ) or ( a is even & b is odd ) or ( a is odd & b is even ) ) ;

suppose ( a is even & b is even ) ; :: thesis: ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) )

then ( parity a = 0 & parity b = 0 & parity (a + b) = 0 ) ;
hence ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) ) ; :: thesis: verum

end;

suppose ( a is odd & b is odd ) ; :: thesis: ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) )

then ( parity a = 1 & parity b = 1 & parity (a + b) = 0 ) ;
hence ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) ) ; :: thesis: verum

end;

suppose A1: ( a is even & b is odd ) ; :: thesis: ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) )

then a + b is odd ;
hence ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) ) by A1; :: thesis: verum

end;

suppose A1: ( a is odd & b is even ) ; :: thesis: ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) )

then a + b is odd ;
hence ( parity (a + b) = ((parity a) + (parity b)) - ((2 * (parity a)) * (parity b)) & (parity a) - (parity b) = (parity (a + b)) - ((2 * (parity (a + b))) * (parity b)) & (parity a) - (parity b) = ((2 * (parity a)) * (parity (a + b))) - (parity (a + b)) ) by A1; :: thesis: verum

end;

end;