gaussian_add_associative

Exact expanded first-order arithmetic statement

forall a b c ab bc t. (exists ge_first_rp_associate_first_add ge_first_rn_associate_first_add ge_first_ip_associate_first_add ge_first_in_associate_first_add ge_second_rp_associate_first_add ge_second_rn_associate_first_add ge_second_ip_associate_first_add ge_second_in_associate_first_add. ((exists ge_representation_real_code_associate_first_addfirst ge_representation_imaginary_code_associate_first_addfirst. (((a) = ((ge_representation_real_code_associate_first_addfirst) + (ge_representation_imaginary_code_associate_first_addfirst)) * S ((ge_representation_real_code_associate_first_addfirst) + (ge_representation_imaginary_code_associate_first_addfirst)) + ((ge_representation_imaginary_code_associate_first_addfirst) + (ge_representation_imaginary_code_associate_first_addfirst))) /\ ((exists ge_balance_positive_associate_first_addfirstreal ge_balance_negative_associate_first_addfirstreal. (((((ge_representation_real_code_associate_first_addfirst) = 2 * (ge_balance_positive_associate_first_addfirstreal) /\ (ge_balance_negative_associate_first_addfirstreal) = 0) \/ exists ge_signed_half_associate_first_addfirstrealdecode. (((ge_representation_real_code_associate_first_addfirst) = 2 * ge_signed_half_associate_first_addfirstrealdecode + 1 /\ (ge_balance_positive_associate_first_addfirstreal) = 0) /\ (ge_balance_negative_associate_first_addfirstreal) = S ge_signed_half_associate_first_addfirstrealdecode))) /\ ((ge_first_rp_associate_first_add) + ge_balance_negative_associate_first_addfirstreal = (ge_first_rn_associate_first_add) + ge_balance_positive_associate_first_addfirstreal))) /\ (exists ge_balance_positive_associate_first_addfirstimaginary ge_balance_negative_associate_first_addfirstimaginary. (((((ge_representation_imaginary_code_associate_first_addfirst) = 2 * (ge_balance_positive_associate_first_addfirstimaginary) /\ (ge_balance_negative_associate_first_addfirstimaginary) = 0) \/ exists ge_signed_half_associate_first_addfirstimaginarydecode. (((ge_representation_imaginary_code_associate_first_addfirst) = 2 * ge_signed_half_associate_first_addfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_first_addfirstimaginary) = 0) /\ (ge_balance_negative_associate_first_addfirstimaginary) = S ge_signed_half_associate_first_addfirstimaginarydecode))) /\ ((ge_first_ip_associate_first_add) + ge_balance_negative_associate_first_addfirstimaginary = (ge_first_in_associate_first_add) + ge_balance_positive_associate_first_addfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_first_addsecond ge_representation_imaginary_code_associate_first_addsecond. (((b) = ((ge_representation_real_code_associate_first_addsecond) + (ge_representation_imaginary_code_associate_first_addsecond)) * S ((ge_representation_real_code_associate_first_addsecond) + (ge_representation_imaginary_code_associate_first_addsecond)) + ((ge_representation_imaginary_code_associate_first_addsecond) + (ge_representation_imaginary_code_associate_first_addsecond))) /\ ((exists ge_balance_positive_associate_first_addsecondreal ge_balance_negative_associate_first_addsecondreal. (((((ge_representation_real_code_associate_first_addsecond) = 2 * (ge_balance_positive_associate_first_addsecondreal) /\ (ge_balance_negative_associate_first_addsecondreal) = 0) \/ exists ge_signed_half_associate_first_addsecondrealdecode. (((ge_representation_real_code_associate_first_addsecond) = 2 * ge_signed_half_associate_first_addsecondrealdecode + 1 /\ (ge_balance_positive_associate_first_addsecondreal) = 0) /\ (ge_balance_negative_associate_first_addsecondreal) = S ge_signed_half_associate_first_addsecondrealdecode))) /\ ((ge_second_rp_associate_first_add) + ge_balance_negative_associate_first_addsecondreal = (ge_second_rn_associate_first_add) + ge_balance_positive_associate_first_addsecondreal))) /\ (exists ge_balance_positive_associate_first_addsecondimaginary ge_balance_negative_associate_first_addsecondimaginary. (((((ge_representation_imaginary_code_associate_first_addsecond) = 2 * (ge_balance_positive_associate_first_addsecondimaginary) /\ (ge_balance_negative_associate_first_addsecondimaginary) = 0) \/ exists ge_signed_half_associate_first_addsecondimaginarydecode. (((ge_representation_imaginary_code_associate_first_addsecond) = 2 * ge_signed_half_associate_first_addsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_first_addsecondimaginary) = 0) /\ (ge_balance_negative_associate_first_addsecondimaginary) = S ge_signed_half_associate_first_addsecondimaginarydecode))) /\ ((ge_second_ip_associate_first_add) + ge_balance_negative_associate_first_addsecondimaginary = (ge_second_in_associate_first_add) + ge_balance_positive_associate_first_addsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_first_addoutput ge_representation_imaginary_code_associate_first_addoutput. (((ab) = ((ge_representation_real_code_associate_first_addoutput) + (ge_representation_imaginary_code_associate_first_addoutput)) * S ((ge_representation_real_code_associate_first_addoutput) + (ge_representation_imaginary_code_associate_first_addoutput)) + ((ge_representation_imaginary_code_associate_first_addoutput) + (ge_representation_imaginary_code_associate_first_addoutput))) /\ ((exists ge_balance_positive_associate_first_addoutputreal ge_balance_negative_associate_first_addoutputreal. (((((ge_representation_real_code_associate_first_addoutput) = 2 * (ge_balance_positive_associate_first_addoutputreal) /\ (ge_balance_negative_associate_first_addoutputreal) = 0) \/ exists ge_signed_half_associate_first_addoutputrealdecode. (((ge_representation_real_code_associate_first_addoutput) = 2 * ge_signed_half_associate_first_addoutputrealdecode + 1 /\ (ge_balance_positive_associate_first_addoutputreal) = 0) /\ (ge_balance_negative_associate_first_addoutputreal) = S ge_signed_half_associate_first_addoutputrealdecode))) /\ ((((ge_first_rp_associate_first_add) + (ge_second_rp_associate_first_add))) + ge_balance_negative_associate_first_addoutputreal = (((ge_first_rn_associate_first_add) + (ge_second_rn_associate_first_add))) + ge_balance_positive_associate_first_addoutputreal))) /\ (exists ge_balance_positive_associate_first_addoutputimaginary ge_balance_negative_associate_first_addoutputimaginary. (((((ge_representation_imaginary_code_associate_first_addoutput) = 2 * (ge_balance_positive_associate_first_addoutputimaginary) /\ (ge_balance_negative_associate_first_addoutputimaginary) = 0) \/ exists ge_signed_half_associate_first_addoutputimaginarydecode. (((ge_representation_imaginary_code_associate_first_addoutput) = 2 * ge_signed_half_associate_first_addoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_first_addoutputimaginary) = 0) /\ (ge_balance_negative_associate_first_addoutputimaginary) = S ge_signed_half_associate_first_addoutputimaginarydecode))) /\ ((((ge_first_ip_associate_first_add) + (ge_second_ip_associate_first_add))) + ge_balance_negative_associate_first_addoutputimaginary = (((ge_first_in_associate_first_add) + (ge_second_in_associate_first_add))) + ge_balance_positive_associate_first_addoutputimaginary))))))))) -> (exists ge_first_rp_associate_second_add ge_first_rn_associate_second_add ge_first_ip_associate_second_add ge_first_in_associate_second_add ge_second_rp_associate_second_add ge_second_rn_associate_second_add ge_second_ip_associate_second_add ge_second_in_associate_second_add. ((exists ge_representation_real_code_associate_second_addfirst ge_representation_imaginary_code_associate_second_addfirst. (((ab) = ((ge_representation_real_code_associate_second_addfirst) + (ge_representation_imaginary_code_associate_second_addfirst)) * S ((ge_representation_real_code_associate_second_addfirst) + (ge_representation_imaginary_code_associate_second_addfirst)) + ((ge_representation_imaginary_code_associate_second_addfirst) + (ge_representation_imaginary_code_associate_second_addfirst))) /\ ((exists ge_balance_positive_associate_second_addfirstreal ge_balance_negative_associate_second_addfirstreal. (((((ge_representation_real_code_associate_second_addfirst) = 2 * (ge_balance_positive_associate_second_addfirstreal) /\ (ge_balance_negative_associate_second_addfirstreal) = 0) \/ exists ge_signed_half_associate_second_addfirstrealdecode. (((ge_representation_real_code_associate_second_addfirst) = 2 * ge_signed_half_associate_second_addfirstrealdecode + 1 /\ (ge_balance_positive_associate_second_addfirstreal) = 0) /\ (ge_balance_negative_associate_second_addfirstreal) = S ge_signed_half_associate_second_addfirstrealdecode))) /\ ((ge_first_rp_associate_second_add) + ge_balance_negative_associate_second_addfirstreal = (ge_first_rn_associate_second_add) + ge_balance_positive_associate_second_addfirstreal))) /\ (exists ge_balance_positive_associate_second_addfirstimaginary ge_balance_negative_associate_second_addfirstimaginary. (((((ge_representation_imaginary_code_associate_second_addfirst) = 2 * (ge_balance_positive_associate_second_addfirstimaginary) /\ (ge_balance_negative_associate_second_addfirstimaginary) = 0) \/ exists ge_signed_half_associate_second_addfirstimaginarydecode. (((ge_representation_imaginary_code_associate_second_addfirst) = 2 * ge_signed_half_associate_second_addfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_second_addfirstimaginary) = 0) /\ (ge_balance_negative_associate_second_addfirstimaginary) = S ge_signed_half_associate_second_addfirstimaginarydecode))) /\ ((ge_first_ip_associate_second_add) + ge_balance_negative_associate_second_addfirstimaginary = (ge_first_in_associate_second_add) + ge_balance_positive_associate_second_addfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_second_addsecond ge_representation_imaginary_code_associate_second_addsecond. (((c) = ((ge_representation_real_code_associate_second_addsecond) + (ge_representation_imaginary_code_associate_second_addsecond)) * S ((ge_representation_real_code_associate_second_addsecond) + (ge_representation_imaginary_code_associate_second_addsecond)) + ((ge_representation_imaginary_code_associate_second_addsecond) + (ge_representation_imaginary_code_associate_second_addsecond))) /\ ((exists ge_balance_positive_associate_second_addsecondreal ge_balance_negative_associate_second_addsecondreal. (((((ge_representation_real_code_associate_second_addsecond) = 2 * (ge_balance_positive_associate_second_addsecondreal) /\ (ge_balance_negative_associate_second_addsecondreal) = 0) \/ exists ge_signed_half_associate_second_addsecondrealdecode. (((ge_representation_real_code_associate_second_addsecond) = 2 * ge_signed_half_associate_second_addsecondrealdecode + 1 /\ (ge_balance_positive_associate_second_addsecondreal) = 0) /\ (ge_balance_negative_associate_second_addsecondreal) = S ge_signed_half_associate_second_addsecondrealdecode))) /\ ((ge_second_rp_associate_second_add) + ge_balance_negative_associate_second_addsecondreal = (ge_second_rn_associate_second_add) + ge_balance_positive_associate_second_addsecondreal))) /\ (exists ge_balance_positive_associate_second_addsecondimaginary ge_balance_negative_associate_second_addsecondimaginary. (((((ge_representation_imaginary_code_associate_second_addsecond) = 2 * (ge_balance_positive_associate_second_addsecondimaginary) /\ (ge_balance_negative_associate_second_addsecondimaginary) = 0) \/ exists ge_signed_half_associate_second_addsecondimaginarydecode. (((ge_representation_imaginary_code_associate_second_addsecond) = 2 * ge_signed_half_associate_second_addsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_second_addsecondimaginary) = 0) /\ (ge_balance_negative_associate_second_addsecondimaginary) = S ge_signed_half_associate_second_addsecondimaginarydecode))) /\ ((ge_second_ip_associate_second_add) + ge_balance_negative_associate_second_addsecondimaginary = (ge_second_in_associate_second_add) + ge_balance_positive_associate_second_addsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_second_addoutput ge_representation_imaginary_code_associate_second_addoutput. (((t) = ((ge_representation_real_code_associate_second_addoutput) + (ge_representation_imaginary_code_associate_second_addoutput)) * S ((ge_representation_real_code_associate_second_addoutput) + (ge_representation_imaginary_code_associate_second_addoutput)) + ((ge_representation_imaginary_code_associate_second_addoutput) + (ge_representation_imaginary_code_associate_second_addoutput))) /\ ((exists ge_balance_positive_associate_second_addoutputreal ge_balance_negative_associate_second_addoutputreal. (((((ge_representation_real_code_associate_second_addoutput) = 2 * (ge_balance_positive_associate_second_addoutputreal) /\ (ge_balance_negative_associate_second_addoutputreal) = 0) \/ exists ge_signed_half_associate_second_addoutputrealdecode. (((ge_representation_real_code_associate_second_addoutput) = 2 * ge_signed_half_associate_second_addoutputrealdecode + 1 /\ (ge_balance_positive_associate_second_addoutputreal) = 0) /\ (ge_balance_negative_associate_second_addoutputreal) = S ge_signed_half_associate_second_addoutputrealdecode))) /\ ((((ge_first_rp_associate_second_add) + (ge_second_rp_associate_second_add))) + ge_balance_negative_associate_second_addoutputreal = (((ge_first_rn_associate_second_add) + (ge_second_rn_associate_second_add))) + ge_balance_positive_associate_second_addoutputreal))) /\ (exists ge_balance_positive_associate_second_addoutputimaginary ge_balance_negative_associate_second_addoutputimaginary. (((((ge_representation_imaginary_code_associate_second_addoutput) = 2 * (ge_balance_positive_associate_second_addoutputimaginary) /\ (ge_balance_negative_associate_second_addoutputimaginary) = 0) \/ exists ge_signed_half_associate_second_addoutputimaginarydecode. (((ge_representation_imaginary_code_associate_second_addoutput) = 2 * ge_signed_half_associate_second_addoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_second_addoutputimaginary) = 0) /\ (ge_balance_negative_associate_second_addoutputimaginary) = S ge_signed_half_associate_second_addoutputimaginarydecode))) /\ ((((ge_first_ip_associate_second_add) + (ge_second_ip_associate_second_add))) + ge_balance_negative_associate_second_addoutputimaginary = (((ge_first_in_associate_second_add) + (ge_second_in_associate_second_add))) + ge_balance_positive_associate_second_addoutputimaginary))))))))) -> (exists ge_first_rp_associate_third_add ge_first_rn_associate_third_add ge_first_ip_associate_third_add ge_first_in_associate_third_add ge_second_rp_associate_third_add ge_second_rn_associate_third_add ge_second_ip_associate_third_add ge_second_in_associate_third_add. ((exists ge_representation_real_code_associate_third_addfirst ge_representation_imaginary_code_associate_third_addfirst. (((b) = ((ge_representation_real_code_associate_third_addfirst) + (ge_representation_imaginary_code_associate_third_addfirst)) * S ((ge_representation_real_code_associate_third_addfirst) + (ge_representation_imaginary_code_associate_third_addfirst)) + ((ge_representation_imaginary_code_associate_third_addfirst) + (ge_representation_imaginary_code_associate_third_addfirst))) /\ ((exists ge_balance_positive_associate_third_addfirstreal ge_balance_negative_associate_third_addfirstreal. (((((ge_representation_real_code_associate_third_addfirst) = 2 * (ge_balance_positive_associate_third_addfirstreal) /\ (ge_balance_negative_associate_third_addfirstreal) = 0) \/ exists ge_signed_half_associate_third_addfirstrealdecode. (((ge_representation_real_code_associate_third_addfirst) = 2 * ge_signed_half_associate_third_addfirstrealdecode + 1 /\ (ge_balance_positive_associate_third_addfirstreal) = 0) /\ (ge_balance_negative_associate_third_addfirstreal) = S ge_signed_half_associate_third_addfirstrealdecode))) /\ ((ge_first_rp_associate_third_add) + ge_balance_negative_associate_third_addfirstreal = (ge_first_rn_associate_third_add) + ge_balance_positive_associate_third_addfirstreal))) /\ (exists ge_balance_positive_associate_third_addfirstimaginary ge_balance_negative_associate_third_addfirstimaginary. (((((ge_representation_imaginary_code_associate_third_addfirst) = 2 * (ge_balance_positive_associate_third_addfirstimaginary) /\ (ge_balance_negative_associate_third_addfirstimaginary) = 0) \/ exists ge_signed_half_associate_third_addfirstimaginarydecode. (((ge_representation_imaginary_code_associate_third_addfirst) = 2 * ge_signed_half_associate_third_addfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_third_addfirstimaginary) = 0) /\ (ge_balance_negative_associate_third_addfirstimaginary) = S ge_signed_half_associate_third_addfirstimaginarydecode))) /\ ((ge_first_ip_associate_third_add) + ge_balance_negative_associate_third_addfirstimaginary = (ge_first_in_associate_third_add) + ge_balance_positive_associate_third_addfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_third_addsecond ge_representation_imaginary_code_associate_third_addsecond. (((c) = ((ge_representation_real_code_associate_third_addsecond) + (ge_representation_imaginary_code_associate_third_addsecond)) * S ((ge_representation_real_code_associate_third_addsecond) + (ge_representation_imaginary_code_associate_third_addsecond)) + ((ge_representation_imaginary_code_associate_third_addsecond) + (ge_representation_imaginary_code_associate_third_addsecond))) /\ ((exists ge_balance_positive_associate_third_addsecondreal ge_balance_negative_associate_third_addsecondreal. (((((ge_representation_real_code_associate_third_addsecond) = 2 * (ge_balance_positive_associate_third_addsecondreal) /\ (ge_balance_negative_associate_third_addsecondreal) = 0) \/ exists ge_signed_half_associate_third_addsecondrealdecode. (((ge_representation_real_code_associate_third_addsecond) = 2 * ge_signed_half_associate_third_addsecondrealdecode + 1 /\ (ge_balance_positive_associate_third_addsecondreal) = 0) /\ (ge_balance_negative_associate_third_addsecondreal) = S ge_signed_half_associate_third_addsecondrealdecode))) /\ ((ge_second_rp_associate_third_add) + ge_balance_negative_associate_third_addsecondreal = (ge_second_rn_associate_third_add) + ge_balance_positive_associate_third_addsecondreal))) /\ (exists ge_balance_positive_associate_third_addsecondimaginary ge_balance_negative_associate_third_addsecondimaginary. (((((ge_representation_imaginary_code_associate_third_addsecond) = 2 * (ge_balance_positive_associate_third_addsecondimaginary) /\ (ge_balance_negative_associate_third_addsecondimaginary) = 0) \/ exists ge_signed_half_associate_third_addsecondimaginarydecode. (((ge_representation_imaginary_code_associate_third_addsecond) = 2 * ge_signed_half_associate_third_addsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_third_addsecondimaginary) = 0) /\ (ge_balance_negative_associate_third_addsecondimaginary) = S ge_signed_half_associate_third_addsecondimaginarydecode))) /\ ((ge_second_ip_associate_third_add) + ge_balance_negative_associate_third_addsecondimaginary = (ge_second_in_associate_third_add) + ge_balance_positive_associate_third_addsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_third_addoutput ge_representation_imaginary_code_associate_third_addoutput. (((bc) = ((ge_representation_real_code_associate_third_addoutput) + (ge_representation_imaginary_code_associate_third_addoutput)) * S ((ge_representation_real_code_associate_third_addoutput) + (ge_representation_imaginary_code_associate_third_addoutput)) + ((ge_representation_imaginary_code_associate_third_addoutput) + (ge_representation_imaginary_code_associate_third_addoutput))) /\ ((exists ge_balance_positive_associate_third_addoutputreal ge_balance_negative_associate_third_addoutputreal. (((((ge_representation_real_code_associate_third_addoutput) = 2 * (ge_balance_positive_associate_third_addoutputreal) /\ (ge_balance_negative_associate_third_addoutputreal) = 0) \/ exists ge_signed_half_associate_third_addoutputrealdecode. (((ge_representation_real_code_associate_third_addoutput) = 2 * ge_signed_half_associate_third_addoutputrealdecode + 1 /\ (ge_balance_positive_associate_third_addoutputreal) = 0) /\ (ge_balance_negative_associate_third_addoutputreal) = S ge_signed_half_associate_third_addoutputrealdecode))) /\ ((((ge_first_rp_associate_third_add) + (ge_second_rp_associate_third_add))) + ge_balance_negative_associate_third_addoutputreal = (((ge_first_rn_associate_third_add) + (ge_second_rn_associate_third_add))) + ge_balance_positive_associate_third_addoutputreal))) /\ (exists ge_balance_positive_associate_third_addoutputimaginary ge_balance_negative_associate_third_addoutputimaginary. (((((ge_representation_imaginary_code_associate_third_addoutput) = 2 * (ge_balance_positive_associate_third_addoutputimaginary) /\ (ge_balance_negative_associate_third_addoutputimaginary) = 0) \/ exists ge_signed_half_associate_third_addoutputimaginarydecode. (((ge_representation_imaginary_code_associate_third_addoutput) = 2 * ge_signed_half_associate_third_addoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_third_addoutputimaginary) = 0) /\ (ge_balance_negative_associate_third_addoutputimaginary) = S ge_signed_half_associate_third_addoutputimaginarydecode))) /\ ((((ge_first_ip_associate_third_add) + (ge_second_ip_associate_third_add))) + ge_balance_negative_associate_third_addoutputimaginary = (((ge_first_in_associate_third_add) + (ge_second_in_associate_third_add))) + ge_balance_positive_associate_third_addoutputimaginary))))))))) -> (exists ge_first_rp_associate_output_add ge_first_rn_associate_output_add ge_first_ip_associate_output_add ge_first_in_associate_output_add ge_second_rp_associate_output_add ge_second_rn_associate_output_add ge_second_ip_associate_output_add ge_second_in_associate_output_add. ((exists ge_representation_real_code_associate_output_addfirst ge_representation_imaginary_code_associate_output_addfirst. (((a) = ((ge_representation_real_code_associate_output_addfirst) + (ge_representation_imaginary_code_associate_output_addfirst)) * S ((ge_representation_real_code_associate_output_addfirst) + (ge_representation_imaginary_code_associate_output_addfirst)) + ((ge_representation_imaginary_code_associate_output_addfirst) + (ge_representation_imaginary_code_associate_output_addfirst))) /\ ((exists ge_balance_positive_associate_output_addfirstreal ge_balance_negative_associate_output_addfirstreal. (((((ge_representation_real_code_associate_output_addfirst) = 2 * (ge_balance_positive_associate_output_addfirstreal) /\ (ge_balance_negative_associate_output_addfirstreal) = 0) \/ exists ge_signed_half_associate_output_addfirstrealdecode. (((ge_representation_real_code_associate_output_addfirst) = 2 * ge_signed_half_associate_output_addfirstrealdecode + 1 /\ (ge_balance_positive_associate_output_addfirstreal) = 0) /\ (ge_balance_negative_associate_output_addfirstreal) = S ge_signed_half_associate_output_addfirstrealdecode))) /\ ((ge_first_rp_associate_output_add) + ge_balance_negative_associate_output_addfirstreal = (ge_first_rn_associate_output_add) + ge_balance_positive_associate_output_addfirstreal))) /\ (exists ge_balance_positive_associate_output_addfirstimaginary ge_balance_negative_associate_output_addfirstimaginary. (((((ge_representation_imaginary_code_associate_output_addfirst) = 2 * (ge_balance_positive_associate_output_addfirstimaginary) /\ (ge_balance_negative_associate_output_addfirstimaginary) = 0) \/ exists ge_signed_half_associate_output_addfirstimaginarydecode. (((ge_representation_imaginary_code_associate_output_addfirst) = 2 * ge_signed_half_associate_output_addfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_output_addfirstimaginary) = 0) /\ (ge_balance_negative_associate_output_addfirstimaginary) = S ge_signed_half_associate_output_addfirstimaginarydecode))) /\ ((ge_first_ip_associate_output_add) + ge_balance_negative_associate_output_addfirstimaginary = (ge_first_in_associate_output_add) + ge_balance_positive_associate_output_addfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_output_addsecond ge_representation_imaginary_code_associate_output_addsecond. (((bc) = ((ge_representation_real_code_associate_output_addsecond) + (ge_representation_imaginary_code_associate_output_addsecond)) * S ((ge_representation_real_code_associate_output_addsecond) + (ge_representation_imaginary_code_associate_output_addsecond)) + ((ge_representation_imaginary_code_associate_output_addsecond) + (ge_representation_imaginary_code_associate_output_addsecond))) /\ ((exists ge_balance_positive_associate_output_addsecondreal ge_balance_negative_associate_output_addsecondreal. (((((ge_representation_real_code_associate_output_addsecond) = 2 * (ge_balance_positive_associate_output_addsecondreal) /\ (ge_balance_negative_associate_output_addsecondreal) = 0) \/ exists ge_signed_half_associate_output_addsecondrealdecode. (((ge_representation_real_code_associate_output_addsecond) = 2 * ge_signed_half_associate_output_addsecondrealdecode + 1 /\ (ge_balance_positive_associate_output_addsecondreal) = 0) /\ (ge_balance_negative_associate_output_addsecondreal) = S ge_signed_half_associate_output_addsecondrealdecode))) /\ ((ge_second_rp_associate_output_add) + ge_balance_negative_associate_output_addsecondreal = (ge_second_rn_associate_output_add) + ge_balance_positive_associate_output_addsecondreal))) /\ (exists ge_balance_positive_associate_output_addsecondimaginary ge_balance_negative_associate_output_addsecondimaginary. (((((ge_representation_imaginary_code_associate_output_addsecond) = 2 * (ge_balance_positive_associate_output_addsecondimaginary) /\ (ge_balance_negative_associate_output_addsecondimaginary) = 0) \/ exists ge_signed_half_associate_output_addsecondimaginarydecode. (((ge_representation_imaginary_code_associate_output_addsecond) = 2 * ge_signed_half_associate_output_addsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_output_addsecondimaginary) = 0) /\ (ge_balance_negative_associate_output_addsecondimaginary) = S ge_signed_half_associate_output_addsecondimaginarydecode))) /\ ((ge_second_ip_associate_output_add) + ge_balance_negative_associate_output_addsecondimaginary = (ge_second_in_associate_output_add) + ge_balance_positive_associate_output_addsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_output_addoutput ge_representation_imaginary_code_associate_output_addoutput. (((t) = ((ge_representation_real_code_associate_output_addoutput) + (ge_representation_imaginary_code_associate_output_addoutput)) * S ((ge_representation_real_code_associate_output_addoutput) + (ge_representation_imaginary_code_associate_output_addoutput)) + ((ge_representation_imaginary_code_associate_output_addoutput) + (ge_representation_imaginary_code_associate_output_addoutput))) /\ ((exists ge_balance_positive_associate_output_addoutputreal ge_balance_negative_associate_output_addoutputreal. (((((ge_representation_real_code_associate_output_addoutput) = 2 * (ge_balance_positive_associate_output_addoutputreal) /\ (ge_balance_negative_associate_output_addoutputreal) = 0) \/ exists ge_signed_half_associate_output_addoutputrealdecode. (((ge_representation_real_code_associate_output_addoutput) = 2 * ge_signed_half_associate_output_addoutputrealdecode + 1 /\ (ge_balance_positive_associate_output_addoutputreal) = 0) /\ (ge_balance_negative_associate_output_addoutputreal) = S ge_signed_half_associate_output_addoutputrealdecode))) /\ ((((ge_first_rp_associate_output_add) + (ge_second_rp_associate_output_add))) + ge_balance_negative_associate_output_addoutputreal = (((ge_first_rn_associate_output_add) + (ge_second_rn_associate_output_add))) + ge_balance_positive_associate_output_addoutputreal))) /\ (exists ge_balance_positive_associate_output_addoutputimaginary ge_balance_negative_associate_output_addoutputimaginary. (((((ge_representation_imaginary_code_associate_output_addoutput) = 2 * (ge_balance_positive_associate_output_addoutputimaginary) /\ (ge_balance_negative_associate_output_addoutputimaginary) = 0) \/ exists ge_signed_half_associate_output_addoutputimaginarydecode. (((ge_representation_imaginary_code_associate_output_addoutput) = 2 * ge_signed_half_associate_output_addoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_output_addoutputimaginary) = 0) /\ (ge_balance_negative_associate_output_addoutputimaginary) = S ge_signed_half_associate_output_addoutputimaginarydecode))) /\ ((((ge_first_ip_associate_output_add) + (ge_second_ip_associate_output_add))) + ge_balance_negative_associate_output_addoutputimaginary = (((ge_first_in_associate_output_add) + (ge_second_in_associate_output_add))) + ge_balance_positive_associate_output_addoutputimaginary)))))))))