gaussian_add_cancel_right

Exact expanded first-order arithmetic statement

forall a b c t. (exists ge_first_rp_cancel_right_first ge_first_rn_cancel_right_first ge_first_ip_cancel_right_first ge_first_in_cancel_right_first ge_second_rp_cancel_right_first ge_second_rn_cancel_right_first ge_second_ip_cancel_right_first ge_second_in_cancel_right_first. ((exists ge_representation_real_code_cancel_right_firstfirst ge_representation_imaginary_code_cancel_right_firstfirst. (((a) = ((ge_representation_real_code_cancel_right_firstfirst) + (ge_representation_imaginary_code_cancel_right_firstfirst)) * S ((ge_representation_real_code_cancel_right_firstfirst) + (ge_representation_imaginary_code_cancel_right_firstfirst)) + ((ge_representation_imaginary_code_cancel_right_firstfirst) + (ge_representation_imaginary_code_cancel_right_firstfirst))) /\ ((exists ge_balance_positive_cancel_right_firstfirstreal ge_balance_negative_cancel_right_firstfirstreal. (((((ge_representation_real_code_cancel_right_firstfirst) = 2 * (ge_balance_positive_cancel_right_firstfirstreal) /\ (ge_balance_negative_cancel_right_firstfirstreal) = 0) \/ exists ge_signed_half_cancel_right_firstfirstrealdecode. (((ge_representation_real_code_cancel_right_firstfirst) = 2 * ge_signed_half_cancel_right_firstfirstrealdecode + 1 /\ (ge_balance_positive_cancel_right_firstfirstreal) = 0) /\ (ge_balance_negative_cancel_right_firstfirstreal) = S ge_signed_half_cancel_right_firstfirstrealdecode))) /\ ((ge_first_rp_cancel_right_first) + ge_balance_negative_cancel_right_firstfirstreal = (ge_first_rn_cancel_right_first) + ge_balance_positive_cancel_right_firstfirstreal))) /\ (exists ge_balance_positive_cancel_right_firstfirstimaginary ge_balance_negative_cancel_right_firstfirstimaginary. (((((ge_representation_imaginary_code_cancel_right_firstfirst) = 2 * (ge_balance_positive_cancel_right_firstfirstimaginary) /\ (ge_balance_negative_cancel_right_firstfirstimaginary) = 0) \/ exists ge_signed_half_cancel_right_firstfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_right_firstfirst) = 2 * ge_signed_half_cancel_right_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_firstfirstimaginary) = 0) /\ (ge_balance_negative_cancel_right_firstfirstimaginary) = S ge_signed_half_cancel_right_firstfirstimaginarydecode))) /\ ((ge_first_ip_cancel_right_first) + ge_balance_negative_cancel_right_firstfirstimaginary = (ge_first_in_cancel_right_first) + ge_balance_positive_cancel_right_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_right_firstsecond ge_representation_imaginary_code_cancel_right_firstsecond. (((c) = ((ge_representation_real_code_cancel_right_firstsecond) + (ge_representation_imaginary_code_cancel_right_firstsecond)) * S ((ge_representation_real_code_cancel_right_firstsecond) + (ge_representation_imaginary_code_cancel_right_firstsecond)) + ((ge_representation_imaginary_code_cancel_right_firstsecond) + (ge_representation_imaginary_code_cancel_right_firstsecond))) /\ ((exists ge_balance_positive_cancel_right_firstsecondreal ge_balance_negative_cancel_right_firstsecondreal. (((((ge_representation_real_code_cancel_right_firstsecond) = 2 * (ge_balance_positive_cancel_right_firstsecondreal) /\ (ge_balance_negative_cancel_right_firstsecondreal) = 0) \/ exists ge_signed_half_cancel_right_firstsecondrealdecode. (((ge_representation_real_code_cancel_right_firstsecond) = 2 * ge_signed_half_cancel_right_firstsecondrealdecode + 1 /\ (ge_balance_positive_cancel_right_firstsecondreal) = 0) /\ (ge_balance_negative_cancel_right_firstsecondreal) = S ge_signed_half_cancel_right_firstsecondrealdecode))) /\ ((ge_second_rp_cancel_right_first) + ge_balance_negative_cancel_right_firstsecondreal = (ge_second_rn_cancel_right_first) + ge_balance_positive_cancel_right_firstsecondreal))) /\ (exists ge_balance_positive_cancel_right_firstsecondimaginary ge_balance_negative_cancel_right_firstsecondimaginary. (((((ge_representation_imaginary_code_cancel_right_firstsecond) = 2 * (ge_balance_positive_cancel_right_firstsecondimaginary) /\ (ge_balance_negative_cancel_right_firstsecondimaginary) = 0) \/ exists ge_signed_half_cancel_right_firstsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_right_firstsecond) = 2 * ge_signed_half_cancel_right_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_firstsecondimaginary) = 0) /\ (ge_balance_negative_cancel_right_firstsecondimaginary) = S ge_signed_half_cancel_right_firstsecondimaginarydecode))) /\ ((ge_second_ip_cancel_right_first) + ge_balance_negative_cancel_right_firstsecondimaginary = (ge_second_in_cancel_right_first) + ge_balance_positive_cancel_right_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_right_firstoutput ge_representation_imaginary_code_cancel_right_firstoutput. (((t) = ((ge_representation_real_code_cancel_right_firstoutput) + (ge_representation_imaginary_code_cancel_right_firstoutput)) * S ((ge_representation_real_code_cancel_right_firstoutput) + (ge_representation_imaginary_code_cancel_right_firstoutput)) + ((ge_representation_imaginary_code_cancel_right_firstoutput) + (ge_representation_imaginary_code_cancel_right_firstoutput))) /\ ((exists ge_balance_positive_cancel_right_firstoutputreal ge_balance_negative_cancel_right_firstoutputreal. (((((ge_representation_real_code_cancel_right_firstoutput) = 2 * (ge_balance_positive_cancel_right_firstoutputreal) /\ (ge_balance_negative_cancel_right_firstoutputreal) = 0) \/ exists ge_signed_half_cancel_right_firstoutputrealdecode. (((ge_representation_real_code_cancel_right_firstoutput) = 2 * ge_signed_half_cancel_right_firstoutputrealdecode + 1 /\ (ge_balance_positive_cancel_right_firstoutputreal) = 0) /\ (ge_balance_negative_cancel_right_firstoutputreal) = S ge_signed_half_cancel_right_firstoutputrealdecode))) /\ ((((ge_first_rp_cancel_right_first) + (ge_second_rp_cancel_right_first))) + ge_balance_negative_cancel_right_firstoutputreal = (((ge_first_rn_cancel_right_first) + (ge_second_rn_cancel_right_first))) + ge_balance_positive_cancel_right_firstoutputreal))) /\ (exists ge_balance_positive_cancel_right_firstoutputimaginary ge_balance_negative_cancel_right_firstoutputimaginary. (((((ge_representation_imaginary_code_cancel_right_firstoutput) = 2 * (ge_balance_positive_cancel_right_firstoutputimaginary) /\ (ge_balance_negative_cancel_right_firstoutputimaginary) = 0) \/ exists ge_signed_half_cancel_right_firstoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_right_firstoutput) = 2 * ge_signed_half_cancel_right_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_firstoutputimaginary) = 0) /\ (ge_balance_negative_cancel_right_firstoutputimaginary) = S ge_signed_half_cancel_right_firstoutputimaginarydecode))) /\ ((((ge_first_ip_cancel_right_first) + (ge_second_ip_cancel_right_first))) + ge_balance_negative_cancel_right_firstoutputimaginary = (((ge_first_in_cancel_right_first) + (ge_second_in_cancel_right_first))) + ge_balance_positive_cancel_right_firstoutputimaginary))))))))) -> (exists ge_first_rp_cancel_right_second ge_first_rn_cancel_right_second ge_first_ip_cancel_right_second ge_first_in_cancel_right_second ge_second_rp_cancel_right_second ge_second_rn_cancel_right_second ge_second_ip_cancel_right_second ge_second_in_cancel_right_second. ((exists ge_representation_real_code_cancel_right_secondfirst ge_representation_imaginary_code_cancel_right_secondfirst. (((b) = ((ge_representation_real_code_cancel_right_secondfirst) + (ge_representation_imaginary_code_cancel_right_secondfirst)) * S ((ge_representation_real_code_cancel_right_secondfirst) + (ge_representation_imaginary_code_cancel_right_secondfirst)) + ((ge_representation_imaginary_code_cancel_right_secondfirst) + (ge_representation_imaginary_code_cancel_right_secondfirst))) /\ ((exists ge_balance_positive_cancel_right_secondfirstreal ge_balance_negative_cancel_right_secondfirstreal. (((((ge_representation_real_code_cancel_right_secondfirst) = 2 * (ge_balance_positive_cancel_right_secondfirstreal) /\ (ge_balance_negative_cancel_right_secondfirstreal) = 0) \/ exists ge_signed_half_cancel_right_secondfirstrealdecode. (((ge_representation_real_code_cancel_right_secondfirst) = 2 * ge_signed_half_cancel_right_secondfirstrealdecode + 1 /\ (ge_balance_positive_cancel_right_secondfirstreal) = 0) /\ (ge_balance_negative_cancel_right_secondfirstreal) = S ge_signed_half_cancel_right_secondfirstrealdecode))) /\ ((ge_first_rp_cancel_right_second) + ge_balance_negative_cancel_right_secondfirstreal = (ge_first_rn_cancel_right_second) + ge_balance_positive_cancel_right_secondfirstreal))) /\ (exists ge_balance_positive_cancel_right_secondfirstimaginary ge_balance_negative_cancel_right_secondfirstimaginary. (((((ge_representation_imaginary_code_cancel_right_secondfirst) = 2 * (ge_balance_positive_cancel_right_secondfirstimaginary) /\ (ge_balance_negative_cancel_right_secondfirstimaginary) = 0) \/ exists ge_signed_half_cancel_right_secondfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_right_secondfirst) = 2 * ge_signed_half_cancel_right_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_secondfirstimaginary) = 0) /\ (ge_balance_negative_cancel_right_secondfirstimaginary) = S ge_signed_half_cancel_right_secondfirstimaginarydecode))) /\ ((ge_first_ip_cancel_right_second) + ge_balance_negative_cancel_right_secondfirstimaginary = (ge_first_in_cancel_right_second) + ge_balance_positive_cancel_right_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_right_secondsecond ge_representation_imaginary_code_cancel_right_secondsecond. (((c) = ((ge_representation_real_code_cancel_right_secondsecond) + (ge_representation_imaginary_code_cancel_right_secondsecond)) * S ((ge_representation_real_code_cancel_right_secondsecond) + (ge_representation_imaginary_code_cancel_right_secondsecond)) + ((ge_representation_imaginary_code_cancel_right_secondsecond) + (ge_representation_imaginary_code_cancel_right_secondsecond))) /\ ((exists ge_balance_positive_cancel_right_secondsecondreal ge_balance_negative_cancel_right_secondsecondreal. (((((ge_representation_real_code_cancel_right_secondsecond) = 2 * (ge_balance_positive_cancel_right_secondsecondreal) /\ (ge_balance_negative_cancel_right_secondsecondreal) = 0) \/ exists ge_signed_half_cancel_right_secondsecondrealdecode. (((ge_representation_real_code_cancel_right_secondsecond) = 2 * ge_signed_half_cancel_right_secondsecondrealdecode + 1 /\ (ge_balance_positive_cancel_right_secondsecondreal) = 0) /\ (ge_balance_negative_cancel_right_secondsecondreal) = S ge_signed_half_cancel_right_secondsecondrealdecode))) /\ ((ge_second_rp_cancel_right_second) + ge_balance_negative_cancel_right_secondsecondreal = (ge_second_rn_cancel_right_second) + ge_balance_positive_cancel_right_secondsecondreal))) /\ (exists ge_balance_positive_cancel_right_secondsecondimaginary ge_balance_negative_cancel_right_secondsecondimaginary. (((((ge_representation_imaginary_code_cancel_right_secondsecond) = 2 * (ge_balance_positive_cancel_right_secondsecondimaginary) /\ (ge_balance_negative_cancel_right_secondsecondimaginary) = 0) \/ exists ge_signed_half_cancel_right_secondsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_right_secondsecond) = 2 * ge_signed_half_cancel_right_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_secondsecondimaginary) = 0) /\ (ge_balance_negative_cancel_right_secondsecondimaginary) = S ge_signed_half_cancel_right_secondsecondimaginarydecode))) /\ ((ge_second_ip_cancel_right_second) + ge_balance_negative_cancel_right_secondsecondimaginary = (ge_second_in_cancel_right_second) + ge_balance_positive_cancel_right_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_right_secondoutput ge_representation_imaginary_code_cancel_right_secondoutput. (((t) = ((ge_representation_real_code_cancel_right_secondoutput) + (ge_representation_imaginary_code_cancel_right_secondoutput)) * S ((ge_representation_real_code_cancel_right_secondoutput) + (ge_representation_imaginary_code_cancel_right_secondoutput)) + ((ge_representation_imaginary_code_cancel_right_secondoutput) + (ge_representation_imaginary_code_cancel_right_secondoutput))) /\ ((exists ge_balance_positive_cancel_right_secondoutputreal ge_balance_negative_cancel_right_secondoutputreal. (((((ge_representation_real_code_cancel_right_secondoutput) = 2 * (ge_balance_positive_cancel_right_secondoutputreal) /\ (ge_balance_negative_cancel_right_secondoutputreal) = 0) \/ exists ge_signed_half_cancel_right_secondoutputrealdecode. (((ge_representation_real_code_cancel_right_secondoutput) = 2 * ge_signed_half_cancel_right_secondoutputrealdecode + 1 /\ (ge_balance_positive_cancel_right_secondoutputreal) = 0) /\ (ge_balance_negative_cancel_right_secondoutputreal) = S ge_signed_half_cancel_right_secondoutputrealdecode))) /\ ((((ge_first_rp_cancel_right_second) + (ge_second_rp_cancel_right_second))) + ge_balance_negative_cancel_right_secondoutputreal = (((ge_first_rn_cancel_right_second) + (ge_second_rn_cancel_right_second))) + ge_balance_positive_cancel_right_secondoutputreal))) /\ (exists ge_balance_positive_cancel_right_secondoutputimaginary ge_balance_negative_cancel_right_secondoutputimaginary. (((((ge_representation_imaginary_code_cancel_right_secondoutput) = 2 * (ge_balance_positive_cancel_right_secondoutputimaginary) /\ (ge_balance_negative_cancel_right_secondoutputimaginary) = 0) \/ exists ge_signed_half_cancel_right_secondoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_right_secondoutput) = 2 * ge_signed_half_cancel_right_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_secondoutputimaginary) = 0) /\ (ge_balance_negative_cancel_right_secondoutputimaginary) = S ge_signed_half_cancel_right_secondoutputimaginarydecode))) /\ ((((ge_first_ip_cancel_right_second) + (ge_second_ip_cancel_right_second))) + ge_balance_negative_cancel_right_secondoutputimaginary = (((ge_first_in_cancel_right_second) + (ge_second_in_cancel_right_second))) + ge_balance_positive_cancel_right_secondoutputimaginary))))))))) -> a=b