gaussian_multiply_add_distribute_right

Exact expanded first-order arithmetic statement

forall a b c s p q t. (exists ge_first_rp_expand_right_sum ge_first_rn_expand_right_sum ge_first_ip_expand_right_sum ge_first_in_expand_right_sum ge_second_rp_expand_right_sum ge_second_rn_expand_right_sum ge_second_ip_expand_right_sum ge_second_in_expand_right_sum. ((exists ge_representation_real_code_expand_right_sumfirst ge_representation_imaginary_code_expand_right_sumfirst. (((b) = ((ge_representation_real_code_expand_right_sumfirst) + (ge_representation_imaginary_code_expand_right_sumfirst)) * S ((ge_representation_real_code_expand_right_sumfirst) + (ge_representation_imaginary_code_expand_right_sumfirst)) + ((ge_representation_imaginary_code_expand_right_sumfirst) + (ge_representation_imaginary_code_expand_right_sumfirst))) /\ ((exists ge_balance_positive_expand_right_sumfirstreal ge_balance_negative_expand_right_sumfirstreal. (((((ge_representation_real_code_expand_right_sumfirst) = 2 * (ge_balance_positive_expand_right_sumfirstreal) /\ (ge_balance_negative_expand_right_sumfirstreal) = 0) \/ exists ge_signed_half_expand_right_sumfirstrealdecode. (((ge_representation_real_code_expand_right_sumfirst) = 2 * ge_signed_half_expand_right_sumfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_sumfirstreal) = 0) /\ (ge_balance_negative_expand_right_sumfirstreal) = S ge_signed_half_expand_right_sumfirstrealdecode))) /\ ((ge_first_rp_expand_right_sum) + ge_balance_negative_expand_right_sumfirstreal = (ge_first_rn_expand_right_sum) + ge_balance_positive_expand_right_sumfirstreal))) /\ (exists ge_balance_positive_expand_right_sumfirstimaginary ge_balance_negative_expand_right_sumfirstimaginary. (((((ge_representation_imaginary_code_expand_right_sumfirst) = 2 * (ge_balance_positive_expand_right_sumfirstimaginary) /\ (ge_balance_negative_expand_right_sumfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_sumfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_sumfirst) = 2 * ge_signed_half_expand_right_sumfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_sumfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_sumfirstimaginary) = S ge_signed_half_expand_right_sumfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_sum) + ge_balance_negative_expand_right_sumfirstimaginary = (ge_first_in_expand_right_sum) + ge_balance_positive_expand_right_sumfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_sumsecond ge_representation_imaginary_code_expand_right_sumsecond. (((c) = ((ge_representation_real_code_expand_right_sumsecond) + (ge_representation_imaginary_code_expand_right_sumsecond)) * S ((ge_representation_real_code_expand_right_sumsecond) + (ge_representation_imaginary_code_expand_right_sumsecond)) + ((ge_representation_imaginary_code_expand_right_sumsecond) + (ge_representation_imaginary_code_expand_right_sumsecond))) /\ ((exists ge_balance_positive_expand_right_sumsecondreal ge_balance_negative_expand_right_sumsecondreal. (((((ge_representation_real_code_expand_right_sumsecond) = 2 * (ge_balance_positive_expand_right_sumsecondreal) /\ (ge_balance_negative_expand_right_sumsecondreal) = 0) \/ exists ge_signed_half_expand_right_sumsecondrealdecode. (((ge_representation_real_code_expand_right_sumsecond) = 2 * ge_signed_half_expand_right_sumsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_sumsecondreal) = 0) /\ (ge_balance_negative_expand_right_sumsecondreal) = S ge_signed_half_expand_right_sumsecondrealdecode))) /\ ((ge_second_rp_expand_right_sum) + ge_balance_negative_expand_right_sumsecondreal = (ge_second_rn_expand_right_sum) + ge_balance_positive_expand_right_sumsecondreal))) /\ (exists ge_balance_positive_expand_right_sumsecondimaginary ge_balance_negative_expand_right_sumsecondimaginary. (((((ge_representation_imaginary_code_expand_right_sumsecond) = 2 * (ge_balance_positive_expand_right_sumsecondimaginary) /\ (ge_balance_negative_expand_right_sumsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_sumsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_sumsecond) = 2 * ge_signed_half_expand_right_sumsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_sumsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_sumsecondimaginary) = S ge_signed_half_expand_right_sumsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_sum) + ge_balance_negative_expand_right_sumsecondimaginary = (ge_second_in_expand_right_sum) + ge_balance_positive_expand_right_sumsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_sumoutput ge_representation_imaginary_code_expand_right_sumoutput. (((s) = ((ge_representation_real_code_expand_right_sumoutput) + (ge_representation_imaginary_code_expand_right_sumoutput)) * S ((ge_representation_real_code_expand_right_sumoutput) + (ge_representation_imaginary_code_expand_right_sumoutput)) + ((ge_representation_imaginary_code_expand_right_sumoutput) + (ge_representation_imaginary_code_expand_right_sumoutput))) /\ ((exists ge_balance_positive_expand_right_sumoutputreal ge_balance_negative_expand_right_sumoutputreal. (((((ge_representation_real_code_expand_right_sumoutput) = 2 * (ge_balance_positive_expand_right_sumoutputreal) /\ (ge_balance_negative_expand_right_sumoutputreal) = 0) \/ exists ge_signed_half_expand_right_sumoutputrealdecode. (((ge_representation_real_code_expand_right_sumoutput) = 2 * ge_signed_half_expand_right_sumoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_sumoutputreal) = 0) /\ (ge_balance_negative_expand_right_sumoutputreal) = S ge_signed_half_expand_right_sumoutputrealdecode))) /\ ((((ge_first_rp_expand_right_sum) + (ge_second_rp_expand_right_sum))) + ge_balance_negative_expand_right_sumoutputreal = (((ge_first_rn_expand_right_sum) + (ge_second_rn_expand_right_sum))) + ge_balance_positive_expand_right_sumoutputreal))) /\ (exists ge_balance_positive_expand_right_sumoutputimaginary ge_balance_negative_expand_right_sumoutputimaginary. (((((ge_representation_imaginary_code_expand_right_sumoutput) = 2 * (ge_balance_positive_expand_right_sumoutputimaginary) /\ (ge_balance_negative_expand_right_sumoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_sumoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_sumoutput) = 2 * ge_signed_half_expand_right_sumoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_sumoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_sumoutputimaginary) = S ge_signed_half_expand_right_sumoutputimaginarydecode))) /\ ((((ge_first_ip_expand_right_sum) + (ge_second_ip_expand_right_sum))) + ge_balance_negative_expand_right_sumoutputimaginary = (((ge_first_in_expand_right_sum) + (ge_second_in_expand_right_sum))) + ge_balance_positive_expand_right_sumoutputimaginary))))))))) -> (exists ge_first_rp_expand_right_first ge_first_rn_expand_right_first ge_first_ip_expand_right_first ge_first_in_expand_right_first ge_second_rp_expand_right_first ge_second_rn_expand_right_first ge_second_ip_expand_right_first ge_second_in_expand_right_first. ((exists ge_representation_real_code_expand_right_firstfirst ge_representation_imaginary_code_expand_right_firstfirst. (((b) = ((ge_representation_real_code_expand_right_firstfirst) + (ge_representation_imaginary_code_expand_right_firstfirst)) * S ((ge_representation_real_code_expand_right_firstfirst) + (ge_representation_imaginary_code_expand_right_firstfirst)) + ((ge_representation_imaginary_code_expand_right_firstfirst) + (ge_representation_imaginary_code_expand_right_firstfirst))) /\ ((exists ge_balance_positive_expand_right_firstfirstreal ge_balance_negative_expand_right_firstfirstreal. (((((ge_representation_real_code_expand_right_firstfirst) = 2 * (ge_balance_positive_expand_right_firstfirstreal) /\ (ge_balance_negative_expand_right_firstfirstreal) = 0) \/ exists ge_signed_half_expand_right_firstfirstrealdecode. (((ge_representation_real_code_expand_right_firstfirst) = 2 * ge_signed_half_expand_right_firstfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_firstfirstreal) = 0) /\ (ge_balance_negative_expand_right_firstfirstreal) = S ge_signed_half_expand_right_firstfirstrealdecode))) /\ ((ge_first_rp_expand_right_first) + ge_balance_negative_expand_right_firstfirstreal = (ge_first_rn_expand_right_first) + ge_balance_positive_expand_right_firstfirstreal))) /\ (exists ge_balance_positive_expand_right_firstfirstimaginary ge_balance_negative_expand_right_firstfirstimaginary. (((((ge_representation_imaginary_code_expand_right_firstfirst) = 2 * (ge_balance_positive_expand_right_firstfirstimaginary) /\ (ge_balance_negative_expand_right_firstfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_firstfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_firstfirst) = 2 * ge_signed_half_expand_right_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_firstfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_firstfirstimaginary) = S ge_signed_half_expand_right_firstfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_first) + ge_balance_negative_expand_right_firstfirstimaginary = (ge_first_in_expand_right_first) + ge_balance_positive_expand_right_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_firstsecond ge_representation_imaginary_code_expand_right_firstsecond. (((a) = ((ge_representation_real_code_expand_right_firstsecond) + (ge_representation_imaginary_code_expand_right_firstsecond)) * S ((ge_representation_real_code_expand_right_firstsecond) + (ge_representation_imaginary_code_expand_right_firstsecond)) + ((ge_representation_imaginary_code_expand_right_firstsecond) + (ge_representation_imaginary_code_expand_right_firstsecond))) /\ ((exists ge_balance_positive_expand_right_firstsecondreal ge_balance_negative_expand_right_firstsecondreal. (((((ge_representation_real_code_expand_right_firstsecond) = 2 * (ge_balance_positive_expand_right_firstsecondreal) /\ (ge_balance_negative_expand_right_firstsecondreal) = 0) \/ exists ge_signed_half_expand_right_firstsecondrealdecode. (((ge_representation_real_code_expand_right_firstsecond) = 2 * ge_signed_half_expand_right_firstsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_firstsecondreal) = 0) /\ (ge_balance_negative_expand_right_firstsecondreal) = S ge_signed_half_expand_right_firstsecondrealdecode))) /\ ((ge_second_rp_expand_right_first) + ge_balance_negative_expand_right_firstsecondreal = (ge_second_rn_expand_right_first) + ge_balance_positive_expand_right_firstsecondreal))) /\ (exists ge_balance_positive_expand_right_firstsecondimaginary ge_balance_negative_expand_right_firstsecondimaginary. (((((ge_representation_imaginary_code_expand_right_firstsecond) = 2 * (ge_balance_positive_expand_right_firstsecondimaginary) /\ (ge_balance_negative_expand_right_firstsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_firstsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_firstsecond) = 2 * ge_signed_half_expand_right_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_firstsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_firstsecondimaginary) = S ge_signed_half_expand_right_firstsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_first) + ge_balance_negative_expand_right_firstsecondimaginary = (ge_second_in_expand_right_first) + ge_balance_positive_expand_right_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_firstoutput ge_representation_imaginary_code_expand_right_firstoutput. (((p) = ((ge_representation_real_code_expand_right_firstoutput) + (ge_representation_imaginary_code_expand_right_firstoutput)) * S ((ge_representation_real_code_expand_right_firstoutput) + (ge_representation_imaginary_code_expand_right_firstoutput)) + ((ge_representation_imaginary_code_expand_right_firstoutput) + (ge_representation_imaginary_code_expand_right_firstoutput))) /\ ((exists ge_balance_positive_expand_right_firstoutputreal ge_balance_negative_expand_right_firstoutputreal. (((((ge_representation_real_code_expand_right_firstoutput) = 2 * (ge_balance_positive_expand_right_firstoutputreal) /\ (ge_balance_negative_expand_right_firstoutputreal) = 0) \/ exists ge_signed_half_expand_right_firstoutputrealdecode. (((ge_representation_real_code_expand_right_firstoutput) = 2 * ge_signed_half_expand_right_firstoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_firstoutputreal) = 0) /\ (ge_balance_negative_expand_right_firstoutputreal) = S ge_signed_half_expand_right_firstoutputrealdecode))) /\ ((((((((ge_first_rp_expand_right_first) * (ge_second_rp_expand_right_first))) + (((ge_first_rn_expand_right_first) * (ge_second_rn_expand_right_first))))) + (((((ge_first_ip_expand_right_first) * (ge_second_in_expand_right_first))) + (((ge_first_in_expand_right_first) * (ge_second_ip_expand_right_first))))))) + ge_balance_negative_expand_right_firstoutputreal = (((((((ge_first_rp_expand_right_first) * (ge_second_rn_expand_right_first))) + (((ge_first_rn_expand_right_first) * (ge_second_rp_expand_right_first))))) + (((((ge_first_ip_expand_right_first) * (ge_second_ip_expand_right_first))) + (((ge_first_in_expand_right_first) * (ge_second_in_expand_right_first))))))) + ge_balance_positive_expand_right_firstoutputreal))) /\ (exists ge_balance_positive_expand_right_firstoutputimaginary ge_balance_negative_expand_right_firstoutputimaginary. (((((ge_representation_imaginary_code_expand_right_firstoutput) = 2 * (ge_balance_positive_expand_right_firstoutputimaginary) /\ (ge_balance_negative_expand_right_firstoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_firstoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_firstoutput) = 2 * ge_signed_half_expand_right_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_firstoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_firstoutputimaginary) = S ge_signed_half_expand_right_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_right_first) * (ge_second_ip_expand_right_first))) + (((ge_first_rn_expand_right_first) * (ge_second_in_expand_right_first))))) + (((((ge_first_ip_expand_right_first) * (ge_second_rp_expand_right_first))) + (((ge_first_in_expand_right_first) * (ge_second_rn_expand_right_first))))))) + ge_balance_negative_expand_right_firstoutputimaginary = (((((((ge_first_rp_expand_right_first) * (ge_second_in_expand_right_first))) + (((ge_first_rn_expand_right_first) * (ge_second_ip_expand_right_first))))) + (((((ge_first_ip_expand_right_first) * (ge_second_rn_expand_right_first))) + (((ge_first_in_expand_right_first) * (ge_second_rp_expand_right_first))))))) + ge_balance_positive_expand_right_firstoutputimaginary))))))))) -> (exists ge_first_rp_expand_right_second ge_first_rn_expand_right_second ge_first_ip_expand_right_second ge_first_in_expand_right_second ge_second_rp_expand_right_second ge_second_rn_expand_right_second ge_second_ip_expand_right_second ge_second_in_expand_right_second. ((exists ge_representation_real_code_expand_right_secondfirst ge_representation_imaginary_code_expand_right_secondfirst. (((c) = ((ge_representation_real_code_expand_right_secondfirst) + (ge_representation_imaginary_code_expand_right_secondfirst)) * S ((ge_representation_real_code_expand_right_secondfirst) + (ge_representation_imaginary_code_expand_right_secondfirst)) + ((ge_representation_imaginary_code_expand_right_secondfirst) + (ge_representation_imaginary_code_expand_right_secondfirst))) /\ ((exists ge_balance_positive_expand_right_secondfirstreal ge_balance_negative_expand_right_secondfirstreal. (((((ge_representation_real_code_expand_right_secondfirst) = 2 * (ge_balance_positive_expand_right_secondfirstreal) /\ (ge_balance_negative_expand_right_secondfirstreal) = 0) \/ exists ge_signed_half_expand_right_secondfirstrealdecode. (((ge_representation_real_code_expand_right_secondfirst) = 2 * ge_signed_half_expand_right_secondfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_secondfirstreal) = 0) /\ (ge_balance_negative_expand_right_secondfirstreal) = S ge_signed_half_expand_right_secondfirstrealdecode))) /\ ((ge_first_rp_expand_right_second) + ge_balance_negative_expand_right_secondfirstreal = (ge_first_rn_expand_right_second) + ge_balance_positive_expand_right_secondfirstreal))) /\ (exists ge_balance_positive_expand_right_secondfirstimaginary ge_balance_negative_expand_right_secondfirstimaginary. (((((ge_representation_imaginary_code_expand_right_secondfirst) = 2 * (ge_balance_positive_expand_right_secondfirstimaginary) /\ (ge_balance_negative_expand_right_secondfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_secondfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_secondfirst) = 2 * ge_signed_half_expand_right_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_secondfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_secondfirstimaginary) = S ge_signed_half_expand_right_secondfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_second) + ge_balance_negative_expand_right_secondfirstimaginary = (ge_first_in_expand_right_second) + ge_balance_positive_expand_right_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_secondsecond ge_representation_imaginary_code_expand_right_secondsecond. (((a) = ((ge_representation_real_code_expand_right_secondsecond) + (ge_representation_imaginary_code_expand_right_secondsecond)) * S ((ge_representation_real_code_expand_right_secondsecond) + (ge_representation_imaginary_code_expand_right_secondsecond)) + ((ge_representation_imaginary_code_expand_right_secondsecond) + (ge_representation_imaginary_code_expand_right_secondsecond))) /\ ((exists ge_balance_positive_expand_right_secondsecondreal ge_balance_negative_expand_right_secondsecondreal. (((((ge_representation_real_code_expand_right_secondsecond) = 2 * (ge_balance_positive_expand_right_secondsecondreal) /\ (ge_balance_negative_expand_right_secondsecondreal) = 0) \/ exists ge_signed_half_expand_right_secondsecondrealdecode. (((ge_representation_real_code_expand_right_secondsecond) = 2 * ge_signed_half_expand_right_secondsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_secondsecondreal) = 0) /\ (ge_balance_negative_expand_right_secondsecondreal) = S ge_signed_half_expand_right_secondsecondrealdecode))) /\ ((ge_second_rp_expand_right_second) + ge_balance_negative_expand_right_secondsecondreal = (ge_second_rn_expand_right_second) + ge_balance_positive_expand_right_secondsecondreal))) /\ (exists ge_balance_positive_expand_right_secondsecondimaginary ge_balance_negative_expand_right_secondsecondimaginary. (((((ge_representation_imaginary_code_expand_right_secondsecond) = 2 * (ge_balance_positive_expand_right_secondsecondimaginary) /\ (ge_balance_negative_expand_right_secondsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_secondsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_secondsecond) = 2 * ge_signed_half_expand_right_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_secondsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_secondsecondimaginary) = S ge_signed_half_expand_right_secondsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_second) + ge_balance_negative_expand_right_secondsecondimaginary = (ge_second_in_expand_right_second) + ge_balance_positive_expand_right_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_secondoutput ge_representation_imaginary_code_expand_right_secondoutput. (((q) = ((ge_representation_real_code_expand_right_secondoutput) + (ge_representation_imaginary_code_expand_right_secondoutput)) * S ((ge_representation_real_code_expand_right_secondoutput) + (ge_representation_imaginary_code_expand_right_secondoutput)) + ((ge_representation_imaginary_code_expand_right_secondoutput) + (ge_representation_imaginary_code_expand_right_secondoutput))) /\ ((exists ge_balance_positive_expand_right_secondoutputreal ge_balance_negative_expand_right_secondoutputreal. (((((ge_representation_real_code_expand_right_secondoutput) = 2 * (ge_balance_positive_expand_right_secondoutputreal) /\ (ge_balance_negative_expand_right_secondoutputreal) = 0) \/ exists ge_signed_half_expand_right_secondoutputrealdecode. (((ge_representation_real_code_expand_right_secondoutput) = 2 * ge_signed_half_expand_right_secondoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_secondoutputreal) = 0) /\ (ge_balance_negative_expand_right_secondoutputreal) = S ge_signed_half_expand_right_secondoutputrealdecode))) /\ ((((((((ge_first_rp_expand_right_second) * (ge_second_rp_expand_right_second))) + (((ge_first_rn_expand_right_second) * (ge_second_rn_expand_right_second))))) + (((((ge_first_ip_expand_right_second) * (ge_second_in_expand_right_second))) + (((ge_first_in_expand_right_second) * (ge_second_ip_expand_right_second))))))) + ge_balance_negative_expand_right_secondoutputreal = (((((((ge_first_rp_expand_right_second) * (ge_second_rn_expand_right_second))) + (((ge_first_rn_expand_right_second) * (ge_second_rp_expand_right_second))))) + (((((ge_first_ip_expand_right_second) * (ge_second_ip_expand_right_second))) + (((ge_first_in_expand_right_second) * (ge_second_in_expand_right_second))))))) + ge_balance_positive_expand_right_secondoutputreal))) /\ (exists ge_balance_positive_expand_right_secondoutputimaginary ge_balance_negative_expand_right_secondoutputimaginary. (((((ge_representation_imaginary_code_expand_right_secondoutput) = 2 * (ge_balance_positive_expand_right_secondoutputimaginary) /\ (ge_balance_negative_expand_right_secondoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_secondoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_secondoutput) = 2 * ge_signed_half_expand_right_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_secondoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_secondoutputimaginary) = S ge_signed_half_expand_right_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_right_second) * (ge_second_ip_expand_right_second))) + (((ge_first_rn_expand_right_second) * (ge_second_in_expand_right_second))))) + (((((ge_first_ip_expand_right_second) * (ge_second_rp_expand_right_second))) + (((ge_first_in_expand_right_second) * (ge_second_rn_expand_right_second))))))) + ge_balance_negative_expand_right_secondoutputimaginary = (((((((ge_first_rp_expand_right_second) * (ge_second_in_expand_right_second))) + (((ge_first_rn_expand_right_second) * (ge_second_ip_expand_right_second))))) + (((((ge_first_ip_expand_right_second) * (ge_second_rn_expand_right_second))) + (((ge_first_in_expand_right_second) * (ge_second_rp_expand_right_second))))))) + ge_balance_positive_expand_right_secondoutputimaginary))))))))) -> (exists ge_first_rp_expand_right_product ge_first_rn_expand_right_product ge_first_ip_expand_right_product ge_first_in_expand_right_product ge_second_rp_expand_right_product ge_second_rn_expand_right_product ge_second_ip_expand_right_product ge_second_in_expand_right_product. ((exists ge_representation_real_code_expand_right_productfirst ge_representation_imaginary_code_expand_right_productfirst. (((s) = ((ge_representation_real_code_expand_right_productfirst) + (ge_representation_imaginary_code_expand_right_productfirst)) * S ((ge_representation_real_code_expand_right_productfirst) + (ge_representation_imaginary_code_expand_right_productfirst)) + ((ge_representation_imaginary_code_expand_right_productfirst) + (ge_representation_imaginary_code_expand_right_productfirst))) /\ ((exists ge_balance_positive_expand_right_productfirstreal ge_balance_negative_expand_right_productfirstreal. (((((ge_representation_real_code_expand_right_productfirst) = 2 * (ge_balance_positive_expand_right_productfirstreal) /\ (ge_balance_negative_expand_right_productfirstreal) = 0) \/ exists ge_signed_half_expand_right_productfirstrealdecode. (((ge_representation_real_code_expand_right_productfirst) = 2 * ge_signed_half_expand_right_productfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_productfirstreal) = 0) /\ (ge_balance_negative_expand_right_productfirstreal) = S ge_signed_half_expand_right_productfirstrealdecode))) /\ ((ge_first_rp_expand_right_product) + ge_balance_negative_expand_right_productfirstreal = (ge_first_rn_expand_right_product) + ge_balance_positive_expand_right_productfirstreal))) /\ (exists ge_balance_positive_expand_right_productfirstimaginary ge_balance_negative_expand_right_productfirstimaginary. (((((ge_representation_imaginary_code_expand_right_productfirst) = 2 * (ge_balance_positive_expand_right_productfirstimaginary) /\ (ge_balance_negative_expand_right_productfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_productfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_productfirst) = 2 * ge_signed_half_expand_right_productfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_productfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_productfirstimaginary) = S ge_signed_half_expand_right_productfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_product) + ge_balance_negative_expand_right_productfirstimaginary = (ge_first_in_expand_right_product) + ge_balance_positive_expand_right_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_productsecond ge_representation_imaginary_code_expand_right_productsecond. (((a) = ((ge_representation_real_code_expand_right_productsecond) + (ge_representation_imaginary_code_expand_right_productsecond)) * S ((ge_representation_real_code_expand_right_productsecond) + (ge_representation_imaginary_code_expand_right_productsecond)) + ((ge_representation_imaginary_code_expand_right_productsecond) + (ge_representation_imaginary_code_expand_right_productsecond))) /\ ((exists ge_balance_positive_expand_right_productsecondreal ge_balance_negative_expand_right_productsecondreal. (((((ge_representation_real_code_expand_right_productsecond) = 2 * (ge_balance_positive_expand_right_productsecondreal) /\ (ge_balance_negative_expand_right_productsecondreal) = 0) \/ exists ge_signed_half_expand_right_productsecondrealdecode. (((ge_representation_real_code_expand_right_productsecond) = 2 * ge_signed_half_expand_right_productsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_productsecondreal) = 0) /\ (ge_balance_negative_expand_right_productsecondreal) = S ge_signed_half_expand_right_productsecondrealdecode))) /\ ((ge_second_rp_expand_right_product) + ge_balance_negative_expand_right_productsecondreal = (ge_second_rn_expand_right_product) + ge_balance_positive_expand_right_productsecondreal))) /\ (exists ge_balance_positive_expand_right_productsecondimaginary ge_balance_negative_expand_right_productsecondimaginary. (((((ge_representation_imaginary_code_expand_right_productsecond) = 2 * (ge_balance_positive_expand_right_productsecondimaginary) /\ (ge_balance_negative_expand_right_productsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_productsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_productsecond) = 2 * ge_signed_half_expand_right_productsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_productsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_productsecondimaginary) = S ge_signed_half_expand_right_productsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_product) + ge_balance_negative_expand_right_productsecondimaginary = (ge_second_in_expand_right_product) + ge_balance_positive_expand_right_productsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_productoutput ge_representation_imaginary_code_expand_right_productoutput. (((t) = ((ge_representation_real_code_expand_right_productoutput) + (ge_representation_imaginary_code_expand_right_productoutput)) * S ((ge_representation_real_code_expand_right_productoutput) + (ge_representation_imaginary_code_expand_right_productoutput)) + ((ge_representation_imaginary_code_expand_right_productoutput) + (ge_representation_imaginary_code_expand_right_productoutput))) /\ ((exists ge_balance_positive_expand_right_productoutputreal ge_balance_negative_expand_right_productoutputreal. (((((ge_representation_real_code_expand_right_productoutput) = 2 * (ge_balance_positive_expand_right_productoutputreal) /\ (ge_balance_negative_expand_right_productoutputreal) = 0) \/ exists ge_signed_half_expand_right_productoutputrealdecode. (((ge_representation_real_code_expand_right_productoutput) = 2 * ge_signed_half_expand_right_productoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_productoutputreal) = 0) /\ (ge_balance_negative_expand_right_productoutputreal) = S ge_signed_half_expand_right_productoutputrealdecode))) /\ ((((((((ge_first_rp_expand_right_product) * (ge_second_rp_expand_right_product))) + (((ge_first_rn_expand_right_product) * (ge_second_rn_expand_right_product))))) + (((((ge_first_ip_expand_right_product) * (ge_second_in_expand_right_product))) + (((ge_first_in_expand_right_product) * (ge_second_ip_expand_right_product))))))) + ge_balance_negative_expand_right_productoutputreal = (((((((ge_first_rp_expand_right_product) * (ge_second_rn_expand_right_product))) + (((ge_first_rn_expand_right_product) * (ge_second_rp_expand_right_product))))) + (((((ge_first_ip_expand_right_product) * (ge_second_ip_expand_right_product))) + (((ge_first_in_expand_right_product) * (ge_second_in_expand_right_product))))))) + ge_balance_positive_expand_right_productoutputreal))) /\ (exists ge_balance_positive_expand_right_productoutputimaginary ge_balance_negative_expand_right_productoutputimaginary. (((((ge_representation_imaginary_code_expand_right_productoutput) = 2 * (ge_balance_positive_expand_right_productoutputimaginary) /\ (ge_balance_negative_expand_right_productoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_productoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_productoutput) = 2 * ge_signed_half_expand_right_productoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_productoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_productoutputimaginary) = S ge_signed_half_expand_right_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_right_product) * (ge_second_ip_expand_right_product))) + (((ge_first_rn_expand_right_product) * (ge_second_in_expand_right_product))))) + (((((ge_first_ip_expand_right_product) * (ge_second_rp_expand_right_product))) + (((ge_first_in_expand_right_product) * (ge_second_rn_expand_right_product))))))) + ge_balance_negative_expand_right_productoutputimaginary = (((((((ge_first_rp_expand_right_product) * (ge_second_in_expand_right_product))) + (((ge_first_rn_expand_right_product) * (ge_second_ip_expand_right_product))))) + (((((ge_first_ip_expand_right_product) * (ge_second_rn_expand_right_product))) + (((ge_first_in_expand_right_product) * (ge_second_rp_expand_right_product))))))) + ge_balance_positive_expand_right_productoutputimaginary))))))))) -> (exists ge_first_rp_expand_right_result ge_first_rn_expand_right_result ge_first_ip_expand_right_result ge_first_in_expand_right_result ge_second_rp_expand_right_result ge_second_rn_expand_right_result ge_second_ip_expand_right_result ge_second_in_expand_right_result. ((exists ge_representation_real_code_expand_right_resultfirst ge_representation_imaginary_code_expand_right_resultfirst. (((p) = ((ge_representation_real_code_expand_right_resultfirst) + (ge_representation_imaginary_code_expand_right_resultfirst)) * S ((ge_representation_real_code_expand_right_resultfirst) + (ge_representation_imaginary_code_expand_right_resultfirst)) + ((ge_representation_imaginary_code_expand_right_resultfirst) + (ge_representation_imaginary_code_expand_right_resultfirst))) /\ ((exists ge_balance_positive_expand_right_resultfirstreal ge_balance_negative_expand_right_resultfirstreal. (((((ge_representation_real_code_expand_right_resultfirst) = 2 * (ge_balance_positive_expand_right_resultfirstreal) /\ (ge_balance_negative_expand_right_resultfirstreal) = 0) \/ exists ge_signed_half_expand_right_resultfirstrealdecode. (((ge_representation_real_code_expand_right_resultfirst) = 2 * ge_signed_half_expand_right_resultfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_resultfirstreal) = 0) /\ (ge_balance_negative_expand_right_resultfirstreal) = S ge_signed_half_expand_right_resultfirstrealdecode))) /\ ((ge_first_rp_expand_right_result) + ge_balance_negative_expand_right_resultfirstreal = (ge_first_rn_expand_right_result) + ge_balance_positive_expand_right_resultfirstreal))) /\ (exists ge_balance_positive_expand_right_resultfirstimaginary ge_balance_negative_expand_right_resultfirstimaginary. (((((ge_representation_imaginary_code_expand_right_resultfirst) = 2 * (ge_balance_positive_expand_right_resultfirstimaginary) /\ (ge_balance_negative_expand_right_resultfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_resultfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_resultfirst) = 2 * ge_signed_half_expand_right_resultfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_resultfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_resultfirstimaginary) = S ge_signed_half_expand_right_resultfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_result) + ge_balance_negative_expand_right_resultfirstimaginary = (ge_first_in_expand_right_result) + ge_balance_positive_expand_right_resultfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_resultsecond ge_representation_imaginary_code_expand_right_resultsecond. (((q) = ((ge_representation_real_code_expand_right_resultsecond) + (ge_representation_imaginary_code_expand_right_resultsecond)) * S ((ge_representation_real_code_expand_right_resultsecond) + (ge_representation_imaginary_code_expand_right_resultsecond)) + ((ge_representation_imaginary_code_expand_right_resultsecond) + (ge_representation_imaginary_code_expand_right_resultsecond))) /\ ((exists ge_balance_positive_expand_right_resultsecondreal ge_balance_negative_expand_right_resultsecondreal. (((((ge_representation_real_code_expand_right_resultsecond) = 2 * (ge_balance_positive_expand_right_resultsecondreal) /\ (ge_balance_negative_expand_right_resultsecondreal) = 0) \/ exists ge_signed_half_expand_right_resultsecondrealdecode. (((ge_representation_real_code_expand_right_resultsecond) = 2 * ge_signed_half_expand_right_resultsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_resultsecondreal) = 0) /\ (ge_balance_negative_expand_right_resultsecondreal) = S ge_signed_half_expand_right_resultsecondrealdecode))) /\ ((ge_second_rp_expand_right_result) + ge_balance_negative_expand_right_resultsecondreal = (ge_second_rn_expand_right_result) + ge_balance_positive_expand_right_resultsecondreal))) /\ (exists ge_balance_positive_expand_right_resultsecondimaginary ge_balance_negative_expand_right_resultsecondimaginary. (((((ge_representation_imaginary_code_expand_right_resultsecond) = 2 * (ge_balance_positive_expand_right_resultsecondimaginary) /\ (ge_balance_negative_expand_right_resultsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_resultsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_resultsecond) = 2 * ge_signed_half_expand_right_resultsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_resultsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_resultsecondimaginary) = S ge_signed_half_expand_right_resultsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_result) + ge_balance_negative_expand_right_resultsecondimaginary = (ge_second_in_expand_right_result) + ge_balance_positive_expand_right_resultsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_resultoutput ge_representation_imaginary_code_expand_right_resultoutput. (((t) = ((ge_representation_real_code_expand_right_resultoutput) + (ge_representation_imaginary_code_expand_right_resultoutput)) * S ((ge_representation_real_code_expand_right_resultoutput) + (ge_representation_imaginary_code_expand_right_resultoutput)) + ((ge_representation_imaginary_code_expand_right_resultoutput) + (ge_representation_imaginary_code_expand_right_resultoutput))) /\ ((exists ge_balance_positive_expand_right_resultoutputreal ge_balance_negative_expand_right_resultoutputreal. (((((ge_representation_real_code_expand_right_resultoutput) = 2 * (ge_balance_positive_expand_right_resultoutputreal) /\ (ge_balance_negative_expand_right_resultoutputreal) = 0) \/ exists ge_signed_half_expand_right_resultoutputrealdecode. (((ge_representation_real_code_expand_right_resultoutput) = 2 * ge_signed_half_expand_right_resultoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_resultoutputreal) = 0) /\ (ge_balance_negative_expand_right_resultoutputreal) = S ge_signed_half_expand_right_resultoutputrealdecode))) /\ ((((ge_first_rp_expand_right_result) + (ge_second_rp_expand_right_result))) + ge_balance_negative_expand_right_resultoutputreal = (((ge_first_rn_expand_right_result) + (ge_second_rn_expand_right_result))) + ge_balance_positive_expand_right_resultoutputreal))) /\ (exists ge_balance_positive_expand_right_resultoutputimaginary ge_balance_negative_expand_right_resultoutputimaginary. (((((ge_representation_imaginary_code_expand_right_resultoutput) = 2 * (ge_balance_positive_expand_right_resultoutputimaginary) /\ (ge_balance_negative_expand_right_resultoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_resultoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_resultoutput) = 2 * ge_signed_half_expand_right_resultoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_resultoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_resultoutputimaginary) = S ge_signed_half_expand_right_resultoutputimaginarydecode))) /\ ((((ge_first_ip_expand_right_result) + (ge_second_ip_expand_right_result))) + ge_balance_negative_expand_right_resultoutputimaginary = (((ge_first_in_expand_right_result) + (ge_second_in_expand_right_result))) + ge_balance_positive_expand_right_resultoutputimaginary)))))))))