A[]((A_eof == 1 imply (A_diff == 0 and B_res == 0)) and (B_eof == 1 imply (B_diff == 0 and A_res == 0)))