gaussian_multiply_add_distribute

Exact expanded first-order arithmetic statement

forall a b c s p q t. (exists ge_first_rp_expand_sum ge_first_rn_expand_sum ge_first_ip_expand_sum ge_first_in_expand_sum ge_second_rp_expand_sum ge_second_rn_expand_sum ge_second_ip_expand_sum ge_second_in_expand_sum. ((exists ge_representation_real_code_expand_sumfirst ge_representation_imaginary_code_expand_sumfirst. (((b) = ((ge_representation_real_code_expand_sumfirst) + (ge_representation_imaginary_code_expand_sumfirst)) * S ((ge_representation_real_code_expand_sumfirst) + (ge_representation_imaginary_code_expand_sumfirst)) + ((ge_representation_imaginary_code_expand_sumfirst) + (ge_representation_imaginary_code_expand_sumfirst))) /\ ((exists ge_balance_positive_expand_sumfirstreal ge_balance_negative_expand_sumfirstreal. (((((ge_representation_real_code_expand_sumfirst) = 2 * (ge_balance_positive_expand_sumfirstreal) /\ (ge_balance_negative_expand_sumfirstreal) = 0) \/ exists ge_signed_half_expand_sumfirstrealdecode. (((ge_representation_real_code_expand_sumfirst) = 2 * ge_signed_half_expand_sumfirstrealdecode + 1 /\ (ge_balance_positive_expand_sumfirstreal) = 0) /\ (ge_balance_negative_expand_sumfirstreal) = S ge_signed_half_expand_sumfirstrealdecode))) /\ ((ge_first_rp_expand_sum) + ge_balance_negative_expand_sumfirstreal = (ge_first_rn_expand_sum) + ge_balance_positive_expand_sumfirstreal))) /\ (exists ge_balance_positive_expand_sumfirstimaginary ge_balance_negative_expand_sumfirstimaginary. (((((ge_representation_imaginary_code_expand_sumfirst) = 2 * (ge_balance_positive_expand_sumfirstimaginary) /\ (ge_balance_negative_expand_sumfirstimaginary) = 0) \/ exists ge_signed_half_expand_sumfirstimaginarydecode. (((ge_representation_imaginary_code_expand_sumfirst) = 2 * ge_signed_half_expand_sumfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_sumfirstimaginary) = 0) /\ (ge_balance_negative_expand_sumfirstimaginary) = S ge_signed_half_expand_sumfirstimaginarydecode))) /\ ((ge_first_ip_expand_sum) + ge_balance_negative_expand_sumfirstimaginary = (ge_first_in_expand_sum) + ge_balance_positive_expand_sumfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_sumsecond ge_representation_imaginary_code_expand_sumsecond. (((c) = ((ge_representation_real_code_expand_sumsecond) + (ge_representation_imaginary_code_expand_sumsecond)) * S ((ge_representation_real_code_expand_sumsecond) + (ge_representation_imaginary_code_expand_sumsecond)) + ((ge_representation_imaginary_code_expand_sumsecond) + (ge_representation_imaginary_code_expand_sumsecond))) /\ ((exists ge_balance_positive_expand_sumsecondreal ge_balance_negative_expand_sumsecondreal. (((((ge_representation_real_code_expand_sumsecond) = 2 * (ge_balance_positive_expand_sumsecondreal) /\ (ge_balance_negative_expand_sumsecondreal) = 0) \/ exists ge_signed_half_expand_sumsecondrealdecode. (((ge_representation_real_code_expand_sumsecond) = 2 * ge_signed_half_expand_sumsecondrealdecode + 1 /\ (ge_balance_positive_expand_sumsecondreal) = 0) /\ (ge_balance_negative_expand_sumsecondreal) = S ge_signed_half_expand_sumsecondrealdecode))) /\ ((ge_second_rp_expand_sum) + ge_balance_negative_expand_sumsecondreal = (ge_second_rn_expand_sum) + ge_balance_positive_expand_sumsecondreal))) /\ (exists ge_balance_positive_expand_sumsecondimaginary ge_balance_negative_expand_sumsecondimaginary. (((((ge_representation_imaginary_code_expand_sumsecond) = 2 * (ge_balance_positive_expand_sumsecondimaginary) /\ (ge_balance_negative_expand_sumsecondimaginary) = 0) \/ exists ge_signed_half_expand_sumsecondimaginarydecode. (((ge_representation_imaginary_code_expand_sumsecond) = 2 * ge_signed_half_expand_sumsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_sumsecondimaginary) = 0) /\ (ge_balance_negative_expand_sumsecondimaginary) = S ge_signed_half_expand_sumsecondimaginarydecode))) /\ ((ge_second_ip_expand_sum) + ge_balance_negative_expand_sumsecondimaginary = (ge_second_in_expand_sum) + ge_balance_positive_expand_sumsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_sumoutput ge_representation_imaginary_code_expand_sumoutput. (((s) = ((ge_representation_real_code_expand_sumoutput) + (ge_representation_imaginary_code_expand_sumoutput)) * S ((ge_representation_real_code_expand_sumoutput) + (ge_representation_imaginary_code_expand_sumoutput)) + ((ge_representation_imaginary_code_expand_sumoutput) + (ge_representation_imaginary_code_expand_sumoutput))) /\ ((exists ge_balance_positive_expand_sumoutputreal ge_balance_negative_expand_sumoutputreal. (((((ge_representation_real_code_expand_sumoutput) = 2 * (ge_balance_positive_expand_sumoutputreal) /\ (ge_balance_negative_expand_sumoutputreal) = 0) \/ exists ge_signed_half_expand_sumoutputrealdecode. (((ge_representation_real_code_expand_sumoutput) = 2 * ge_signed_half_expand_sumoutputrealdecode + 1 /\ (ge_balance_positive_expand_sumoutputreal) = 0) /\ (ge_balance_negative_expand_sumoutputreal) = S ge_signed_half_expand_sumoutputrealdecode))) /\ ((((ge_first_rp_expand_sum) + (ge_second_rp_expand_sum))) + ge_balance_negative_expand_sumoutputreal = (((ge_first_rn_expand_sum) + (ge_second_rn_expand_sum))) + ge_balance_positive_expand_sumoutputreal))) /\ (exists ge_balance_positive_expand_sumoutputimaginary ge_balance_negative_expand_sumoutputimaginary. (((((ge_representation_imaginary_code_expand_sumoutput) = 2 * (ge_balance_positive_expand_sumoutputimaginary) /\ (ge_balance_negative_expand_sumoutputimaginary) = 0) \/ exists ge_signed_half_expand_sumoutputimaginarydecode. (((ge_representation_imaginary_code_expand_sumoutput) = 2 * ge_signed_half_expand_sumoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_sumoutputimaginary) = 0) /\ (ge_balance_negative_expand_sumoutputimaginary) = S ge_signed_half_expand_sumoutputimaginarydecode))) /\ ((((ge_first_ip_expand_sum) + (ge_second_ip_expand_sum))) + ge_balance_negative_expand_sumoutputimaginary = (((ge_first_in_expand_sum) + (ge_second_in_expand_sum))) + ge_balance_positive_expand_sumoutputimaginary))))))))) -> (exists ge_first_rp_expand_first ge_first_rn_expand_first ge_first_ip_expand_first ge_first_in_expand_first ge_second_rp_expand_first ge_second_rn_expand_first ge_second_ip_expand_first ge_second_in_expand_first. ((exists ge_representation_real_code_expand_firstfirst ge_representation_imaginary_code_expand_firstfirst. (((a) = ((ge_representation_real_code_expand_firstfirst) + (ge_representation_imaginary_code_expand_firstfirst)) * S ((ge_representation_real_code_expand_firstfirst) + (ge_representation_imaginary_code_expand_firstfirst)) + ((ge_representation_imaginary_code_expand_firstfirst) + (ge_representation_imaginary_code_expand_firstfirst))) /\ ((exists ge_balance_positive_expand_firstfirstreal ge_balance_negative_expand_firstfirstreal. (((((ge_representation_real_code_expand_firstfirst) = 2 * (ge_balance_positive_expand_firstfirstreal) /\ (ge_balance_negative_expand_firstfirstreal) = 0) \/ exists ge_signed_half_expand_firstfirstrealdecode. (((ge_representation_real_code_expand_firstfirst) = 2 * ge_signed_half_expand_firstfirstrealdecode + 1 /\ (ge_balance_positive_expand_firstfirstreal) = 0) /\ (ge_balance_negative_expand_firstfirstreal) = S ge_signed_half_expand_firstfirstrealdecode))) /\ ((ge_first_rp_expand_first) + ge_balance_negative_expand_firstfirstreal = (ge_first_rn_expand_first) + ge_balance_positive_expand_firstfirstreal))) /\ (exists ge_balance_positive_expand_firstfirstimaginary ge_balance_negative_expand_firstfirstimaginary. (((((ge_representation_imaginary_code_expand_firstfirst) = 2 * (ge_balance_positive_expand_firstfirstimaginary) /\ (ge_balance_negative_expand_firstfirstimaginary) = 0) \/ exists ge_signed_half_expand_firstfirstimaginarydecode. (((ge_representation_imaginary_code_expand_firstfirst) = 2 * ge_signed_half_expand_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_firstfirstimaginary) = 0) /\ (ge_balance_negative_expand_firstfirstimaginary) = S ge_signed_half_expand_firstfirstimaginarydecode))) /\ ((ge_first_ip_expand_first) + ge_balance_negative_expand_firstfirstimaginary = (ge_first_in_expand_first) + ge_balance_positive_expand_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_firstsecond ge_representation_imaginary_code_expand_firstsecond. (((b) = ((ge_representation_real_code_expand_firstsecond) + (ge_representation_imaginary_code_expand_firstsecond)) * S ((ge_representation_real_code_expand_firstsecond) + (ge_representation_imaginary_code_expand_firstsecond)) + ((ge_representation_imaginary_code_expand_firstsecond) + (ge_representation_imaginary_code_expand_firstsecond))) /\ ((exists ge_balance_positive_expand_firstsecondreal ge_balance_negative_expand_firstsecondreal. (((((ge_representation_real_code_expand_firstsecond) = 2 * (ge_balance_positive_expand_firstsecondreal) /\ (ge_balance_negative_expand_firstsecondreal) = 0) \/ exists ge_signed_half_expand_firstsecondrealdecode. (((ge_representation_real_code_expand_firstsecond) = 2 * ge_signed_half_expand_firstsecondrealdecode + 1 /\ (ge_balance_positive_expand_firstsecondreal) = 0) /\ (ge_balance_negative_expand_firstsecondreal) = S ge_signed_half_expand_firstsecondrealdecode))) /\ ((ge_second_rp_expand_first) + ge_balance_negative_expand_firstsecondreal = (ge_second_rn_expand_first) + ge_balance_positive_expand_firstsecondreal))) /\ (exists ge_balance_positive_expand_firstsecondimaginary ge_balance_negative_expand_firstsecondimaginary. (((((ge_representation_imaginary_code_expand_firstsecond) = 2 * (ge_balance_positive_expand_firstsecondimaginary) /\ (ge_balance_negative_expand_firstsecondimaginary) = 0) \/ exists ge_signed_half_expand_firstsecondimaginarydecode. (((ge_representation_imaginary_code_expand_firstsecond) = 2 * ge_signed_half_expand_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_firstsecondimaginary) = 0) /\ (ge_balance_negative_expand_firstsecondimaginary) = S ge_signed_half_expand_firstsecondimaginarydecode))) /\ ((ge_second_ip_expand_first) + ge_balance_negative_expand_firstsecondimaginary = (ge_second_in_expand_first) + ge_balance_positive_expand_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_firstoutput ge_representation_imaginary_code_expand_firstoutput. (((p) = ((ge_representation_real_code_expand_firstoutput) + (ge_representation_imaginary_code_expand_firstoutput)) * S ((ge_representation_real_code_expand_firstoutput) + (ge_representation_imaginary_code_expand_firstoutput)) + ((ge_representation_imaginary_code_expand_firstoutput) + (ge_representation_imaginary_code_expand_firstoutput))) /\ ((exists ge_balance_positive_expand_firstoutputreal ge_balance_negative_expand_firstoutputreal. (((((ge_representation_real_code_expand_firstoutput) = 2 * (ge_balance_positive_expand_firstoutputreal) /\ (ge_balance_negative_expand_firstoutputreal) = 0) \/ exists ge_signed_half_expand_firstoutputrealdecode. (((ge_representation_real_code_expand_firstoutput) = 2 * ge_signed_half_expand_firstoutputrealdecode + 1 /\ (ge_balance_positive_expand_firstoutputreal) = 0) /\ (ge_balance_negative_expand_firstoutputreal) = S ge_signed_half_expand_firstoutputrealdecode))) /\ ((((((((ge_first_rp_expand_first) * (ge_second_rp_expand_first))) + (((ge_first_rn_expand_first) * (ge_second_rn_expand_first))))) + (((((ge_first_ip_expand_first) * (ge_second_in_expand_first))) + (((ge_first_in_expand_first) * (ge_second_ip_expand_first))))))) + ge_balance_negative_expand_firstoutputreal = (((((((ge_first_rp_expand_first) * (ge_second_rn_expand_first))) + (((ge_first_rn_expand_first) * (ge_second_rp_expand_first))))) + (((((ge_first_ip_expand_first) * (ge_second_ip_expand_first))) + (((ge_first_in_expand_first) * (ge_second_in_expand_first))))))) + ge_balance_positive_expand_firstoutputreal))) /\ (exists ge_balance_positive_expand_firstoutputimaginary ge_balance_negative_expand_firstoutputimaginary. (((((ge_representation_imaginary_code_expand_firstoutput) = 2 * (ge_balance_positive_expand_firstoutputimaginary) /\ (ge_balance_negative_expand_firstoutputimaginary) = 0) \/ exists ge_signed_half_expand_firstoutputimaginarydecode. (((ge_representation_imaginary_code_expand_firstoutput) = 2 * ge_signed_half_expand_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_firstoutputimaginary) = 0) /\ (ge_balance_negative_expand_firstoutputimaginary) = S ge_signed_half_expand_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_first) * (ge_second_ip_expand_first))) + (((ge_first_rn_expand_first) * (ge_second_in_expand_first))))) + (((((ge_first_ip_expand_first) * (ge_second_rp_expand_first))) + (((ge_first_in_expand_first) * (ge_second_rn_expand_first))))))) + ge_balance_negative_expand_firstoutputimaginary = (((((((ge_first_rp_expand_first) * (ge_second_in_expand_first))) + (((ge_first_rn_expand_first) * (ge_second_ip_expand_first))))) + (((((ge_first_ip_expand_first) * (ge_second_rn_expand_first))) + (((ge_first_in_expand_first) * (ge_second_rp_expand_first))))))) + ge_balance_positive_expand_firstoutputimaginary))))))))) -> (exists ge_first_rp_expand_second ge_first_rn_expand_second ge_first_ip_expand_second ge_first_in_expand_second ge_second_rp_expand_second ge_second_rn_expand_second ge_second_ip_expand_second ge_second_in_expand_second. ((exists ge_representation_real_code_expand_secondfirst ge_representation_imaginary_code_expand_secondfirst. (((a) = ((ge_representation_real_code_expand_secondfirst) + (ge_representation_imaginary_code_expand_secondfirst)) * S ((ge_representation_real_code_expand_secondfirst) + (ge_representation_imaginary_code_expand_secondfirst)) + ((ge_representation_imaginary_code_expand_secondfirst) + (ge_representation_imaginary_code_expand_secondfirst))) /\ ((exists ge_balance_positive_expand_secondfirstreal ge_balance_negative_expand_secondfirstreal. (((((ge_representation_real_code_expand_secondfirst) = 2 * (ge_balance_positive_expand_secondfirstreal) /\ (ge_balance_negative_expand_secondfirstreal) = 0) \/ exists ge_signed_half_expand_secondfirstrealdecode. (((ge_representation_real_code_expand_secondfirst) = 2 * ge_signed_half_expand_secondfirstrealdecode + 1 /\ (ge_balance_positive_expand_secondfirstreal) = 0) /\ (ge_balance_negative_expand_secondfirstreal) = S ge_signed_half_expand_secondfirstrealdecode))) /\ ((ge_first_rp_expand_second) + ge_balance_negative_expand_secondfirstreal = (ge_first_rn_expand_second) + ge_balance_positive_expand_secondfirstreal))) /\ (exists ge_balance_positive_expand_secondfirstimaginary ge_balance_negative_expand_secondfirstimaginary. (((((ge_representation_imaginary_code_expand_secondfirst) = 2 * (ge_balance_positive_expand_secondfirstimaginary) /\ (ge_balance_negative_expand_secondfirstimaginary) = 0) \/ exists ge_signed_half_expand_secondfirstimaginarydecode. (((ge_representation_imaginary_code_expand_secondfirst) = 2 * ge_signed_half_expand_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_secondfirstimaginary) = 0) /\ (ge_balance_negative_expand_secondfirstimaginary) = S ge_signed_half_expand_secondfirstimaginarydecode))) /\ ((ge_first_ip_expand_second) + ge_balance_negative_expand_secondfirstimaginary = (ge_first_in_expand_second) + ge_balance_positive_expand_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_secondsecond ge_representation_imaginary_code_expand_secondsecond. (((c) = ((ge_representation_real_code_expand_secondsecond) + (ge_representation_imaginary_code_expand_secondsecond)) * S ((ge_representation_real_code_expand_secondsecond) + (ge_representation_imaginary_code_expand_secondsecond)) + ((ge_representation_imaginary_code_expand_secondsecond) + (ge_representation_imaginary_code_expand_secondsecond))) /\ ((exists ge_balance_positive_expand_secondsecondreal ge_balance_negative_expand_secondsecondreal. (((((ge_representation_real_code_expand_secondsecond) = 2 * (ge_balance_positive_expand_secondsecondreal) /\ (ge_balance_negative_expand_secondsecondreal) = 0) \/ exists ge_signed_half_expand_secondsecondrealdecode. (((ge_representation_real_code_expand_secondsecond) = 2 * ge_signed_half_expand_secondsecondrealdecode + 1 /\ (ge_balance_positive_expand_secondsecondreal) = 0) /\ (ge_balance_negative_expand_secondsecondreal) = S ge_signed_half_expand_secondsecondrealdecode))) /\ ((ge_second_rp_expand_second) + ge_balance_negative_expand_secondsecondreal = (ge_second_rn_expand_second) + ge_balance_positive_expand_secondsecondreal))) /\ (exists ge_balance_positive_expand_secondsecondimaginary ge_balance_negative_expand_secondsecondimaginary. (((((ge_representation_imaginary_code_expand_secondsecond) = 2 * (ge_balance_positive_expand_secondsecondimaginary) /\ (ge_balance_negative_expand_secondsecondimaginary) = 0) \/ exists ge_signed_half_expand_secondsecondimaginarydecode. (((ge_representation_imaginary_code_expand_secondsecond) = 2 * ge_signed_half_expand_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_secondsecondimaginary) = 0) /\ (ge_balance_negative_expand_secondsecondimaginary) = S ge_signed_half_expand_secondsecondimaginarydecode))) /\ ((ge_second_ip_expand_second) + ge_balance_negative_expand_secondsecondimaginary = (ge_second_in_expand_second) + ge_balance_positive_expand_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_secondoutput ge_representation_imaginary_code_expand_secondoutput. (((q) = ((ge_representation_real_code_expand_secondoutput) + (ge_representation_imaginary_code_expand_secondoutput)) * S ((ge_representation_real_code_expand_secondoutput) + (ge_representation_imaginary_code_expand_secondoutput)) + ((ge_representation_imaginary_code_expand_secondoutput) + (ge_representation_imaginary_code_expand_secondoutput))) /\ ((exists ge_balance_positive_expand_secondoutputreal ge_balance_negative_expand_secondoutputreal. (((((ge_representation_real_code_expand_secondoutput) = 2 * (ge_balance_positive_expand_secondoutputreal) /\ (ge_balance_negative_expand_secondoutputreal) = 0) \/ exists ge_signed_half_expand_secondoutputrealdecode. (((ge_representation_real_code_expand_secondoutput) = 2 * ge_signed_half_expand_secondoutputrealdecode + 1 /\ (ge_balance_positive_expand_secondoutputreal) = 0) /\ (ge_balance_negative_expand_secondoutputreal) = S ge_signed_half_expand_secondoutputrealdecode))) /\ ((((((((ge_first_rp_expand_second) * (ge_second_rp_expand_second))) + (((ge_first_rn_expand_second) * (ge_second_rn_expand_second))))) + (((((ge_first_ip_expand_second) * (ge_second_in_expand_second))) + (((ge_first_in_expand_second) * (ge_second_ip_expand_second))))))) + ge_balance_negative_expand_secondoutputreal = (((((((ge_first_rp_expand_second) * (ge_second_rn_expand_second))) + (((ge_first_rn_expand_second) * (ge_second_rp_expand_second))))) + (((((ge_first_ip_expand_second) * (ge_second_ip_expand_second))) + (((ge_first_in_expand_second) * (ge_second_in_expand_second))))))) + ge_balance_positive_expand_secondoutputreal))) /\ (exists ge_balance_positive_expand_secondoutputimaginary ge_balance_negative_expand_secondoutputimaginary. (((((ge_representation_imaginary_code_expand_secondoutput) = 2 * (ge_balance_positive_expand_secondoutputimaginary) /\ (ge_balance_negative_expand_secondoutputimaginary) = 0) \/ exists ge_signed_half_expand_secondoutputimaginarydecode. (((ge_representation_imaginary_code_expand_secondoutput) = 2 * ge_signed_half_expand_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_secondoutputimaginary) = 0) /\ (ge_balance_negative_expand_secondoutputimaginary) = S ge_signed_half_expand_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_second) * (ge_second_ip_expand_second))) + (((ge_first_rn_expand_second) * (ge_second_in_expand_second))))) + (((((ge_first_ip_expand_second) * (ge_second_rp_expand_second))) + (((ge_first_in_expand_second) * (ge_second_rn_expand_second))))))) + ge_balance_negative_expand_secondoutputimaginary = (((((((ge_first_rp_expand_second) * (ge_second_in_expand_second))) + (((ge_first_rn_expand_second) * (ge_second_ip_expand_second))))) + (((((ge_first_ip_expand_second) * (ge_second_rn_expand_second))) + (((ge_first_in_expand_second) * (ge_second_rp_expand_second))))))) + ge_balance_positive_expand_secondoutputimaginary))))))))) -> (exists ge_first_rp_expand_product ge_first_rn_expand_product ge_first_ip_expand_product ge_first_in_expand_product ge_second_rp_expand_product ge_second_rn_expand_product ge_second_ip_expand_product ge_second_in_expand_product. ((exists ge_representation_real_code_expand_productfirst ge_representation_imaginary_code_expand_productfirst. (((a) = ((ge_representation_real_code_expand_productfirst) + (ge_representation_imaginary_code_expand_productfirst)) * S ((ge_representation_real_code_expand_productfirst) + (ge_representation_imaginary_code_expand_productfirst)) + ((ge_representation_imaginary_code_expand_productfirst) + (ge_representation_imaginary_code_expand_productfirst))) /\ ((exists ge_balance_positive_expand_productfirstreal ge_balance_negative_expand_productfirstreal. (((((ge_representation_real_code_expand_productfirst) = 2 * (ge_balance_positive_expand_productfirstreal) /\ (ge_balance_negative_expand_productfirstreal) = 0) \/ exists ge_signed_half_expand_productfirstrealdecode. (((ge_representation_real_code_expand_productfirst) = 2 * ge_signed_half_expand_productfirstrealdecode + 1 /\ (ge_balance_positive_expand_productfirstreal) = 0) /\ (ge_balance_negative_expand_productfirstreal) = S ge_signed_half_expand_productfirstrealdecode))) /\ ((ge_first_rp_expand_product) + ge_balance_negative_expand_productfirstreal = (ge_first_rn_expand_product) + ge_balance_positive_expand_productfirstreal))) /\ (exists ge_balance_positive_expand_productfirstimaginary ge_balance_negative_expand_productfirstimaginary. (((((ge_representation_imaginary_code_expand_productfirst) = 2 * (ge_balance_positive_expand_productfirstimaginary) /\ (ge_balance_negative_expand_productfirstimaginary) = 0) \/ exists ge_signed_half_expand_productfirstimaginarydecode. (((ge_representation_imaginary_code_expand_productfirst) = 2 * ge_signed_half_expand_productfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_productfirstimaginary) = 0) /\ (ge_balance_negative_expand_productfirstimaginary) = S ge_signed_half_expand_productfirstimaginarydecode))) /\ ((ge_first_ip_expand_product) + ge_balance_negative_expand_productfirstimaginary = (ge_first_in_expand_product) + ge_balance_positive_expand_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_productsecond ge_representation_imaginary_code_expand_productsecond. (((s) = ((ge_representation_real_code_expand_productsecond) + (ge_representation_imaginary_code_expand_productsecond)) * S ((ge_representation_real_code_expand_productsecond) + (ge_representation_imaginary_code_expand_productsecond)) + ((ge_representation_imaginary_code_expand_productsecond) + (ge_representation_imaginary_code_expand_productsecond))) /\ ((exists ge_balance_positive_expand_productsecondreal ge_balance_negative_expand_productsecondreal. (((((ge_representation_real_code_expand_productsecond) = 2 * (ge_balance_positive_expand_productsecondreal) /\ (ge_balance_negative_expand_productsecondreal) = 0) \/ exists ge_signed_half_expand_productsecondrealdecode. (((ge_representation_real_code_expand_productsecond) = 2 * ge_signed_half_expand_productsecondrealdecode + 1 /\ (ge_balance_positive_expand_productsecondreal) = 0) /\ (ge_balance_negative_expand_productsecondreal) = S ge_signed_half_expand_productsecondrealdecode))) /\ ((ge_second_rp_expand_product) + ge_balance_negative_expand_productsecondreal = (ge_second_rn_expand_product) + ge_balance_positive_expand_productsecondreal))) /\ (exists ge_balance_positive_expand_productsecondimaginary ge_balance_negative_expand_productsecondimaginary. (((((ge_representation_imaginary_code_expand_productsecond) = 2 * (ge_balance_positive_expand_productsecondimaginary) /\ (ge_balance_negative_expand_productsecondimaginary) = 0) \/ exists ge_signed_half_expand_productsecondimaginarydecode. (((ge_representation_imaginary_code_expand_productsecond) = 2 * ge_signed_half_expand_productsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_productsecondimaginary) = 0) /\ (ge_balance_negative_expand_productsecondimaginary) = S ge_signed_half_expand_productsecondimaginarydecode))) /\ ((ge_second_ip_expand_product) + ge_balance_negative_expand_productsecondimaginary = (ge_second_in_expand_product) + ge_balance_positive_expand_productsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_productoutput ge_representation_imaginary_code_expand_productoutput. (((t) = ((ge_representation_real_code_expand_productoutput) + (ge_representation_imaginary_code_expand_productoutput)) * S ((ge_representation_real_code_expand_productoutput) + (ge_representation_imaginary_code_expand_productoutput)) + ((ge_representation_imaginary_code_expand_productoutput) + (ge_representation_imaginary_code_expand_productoutput))) /\ ((exists ge_balance_positive_expand_productoutputreal ge_balance_negative_expand_productoutputreal. (((((ge_representation_real_code_expand_productoutput) = 2 * (ge_balance_positive_expand_productoutputreal) /\ (ge_balance_negative_expand_productoutputreal) = 0) \/ exists ge_signed_half_expand_productoutputrealdecode. (((ge_representation_real_code_expand_productoutput) = 2 * ge_signed_half_expand_productoutputrealdecode + 1 /\ (ge_balance_positive_expand_productoutputreal) = 0) /\ (ge_balance_negative_expand_productoutputreal) = S ge_signed_half_expand_productoutputrealdecode))) /\ ((((((((ge_first_rp_expand_product) * (ge_second_rp_expand_product))) + (((ge_first_rn_expand_product) * (ge_second_rn_expand_product))))) + (((((ge_first_ip_expand_product) * (ge_second_in_expand_product))) + (((ge_first_in_expand_product) * (ge_second_ip_expand_product))))))) + ge_balance_negative_expand_productoutputreal = (((((((ge_first_rp_expand_product) * (ge_second_rn_expand_product))) + (((ge_first_rn_expand_product) * (ge_second_rp_expand_product))))) + (((((ge_first_ip_expand_product) * (ge_second_ip_expand_product))) + (((ge_first_in_expand_product) * (ge_second_in_expand_product))))))) + ge_balance_positive_expand_productoutputreal))) /\ (exists ge_balance_positive_expand_productoutputimaginary ge_balance_negative_expand_productoutputimaginary. (((((ge_representation_imaginary_code_expand_productoutput) = 2 * (ge_balance_positive_expand_productoutputimaginary) /\ (ge_balance_negative_expand_productoutputimaginary) = 0) \/ exists ge_signed_half_expand_productoutputimaginarydecode. (((ge_representation_imaginary_code_expand_productoutput) = 2 * ge_signed_half_expand_productoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_productoutputimaginary) = 0) /\ (ge_balance_negative_expand_productoutputimaginary) = S ge_signed_half_expand_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_product) * (ge_second_ip_expand_product))) + (((ge_first_rn_expand_product) * (ge_second_in_expand_product))))) + (((((ge_first_ip_expand_product) * (ge_second_rp_expand_product))) + (((ge_first_in_expand_product) * (ge_second_rn_expand_product))))))) + ge_balance_negative_expand_productoutputimaginary = (((((((ge_first_rp_expand_product) * (ge_second_in_expand_product))) + (((ge_first_rn_expand_product) * (ge_second_ip_expand_product))))) + (((((ge_first_ip_expand_product) * (ge_second_rn_expand_product))) + (((ge_first_in_expand_product) * (ge_second_rp_expand_product))))))) + ge_balance_positive_expand_productoutputimaginary))))))))) -> (exists ge_first_rp_expand_result ge_first_rn_expand_result ge_first_ip_expand_result ge_first_in_expand_result ge_second_rp_expand_result ge_second_rn_expand_result ge_second_ip_expand_result ge_second_in_expand_result. ((exists ge_representation_real_code_expand_resultfirst ge_representation_imaginary_code_expand_resultfirst. (((p) = ((ge_representation_real_code_expand_resultfirst) + (ge_representation_imaginary_code_expand_resultfirst)) * S ((ge_representation_real_code_expand_resultfirst) + (ge_representation_imaginary_code_expand_resultfirst)) + ((ge_representation_imaginary_code_expand_resultfirst) + (ge_representation_imaginary_code_expand_resultfirst))) /\ ((exists ge_balance_positive_expand_resultfirstreal ge_balance_negative_expand_resultfirstreal. (((((ge_representation_real_code_expand_resultfirst) = 2 * (ge_balance_positive_expand_resultfirstreal) /\ (ge_balance_negative_expand_resultfirstreal) = 0) \/ exists ge_signed_half_expand_resultfirstrealdecode. (((ge_representation_real_code_expand_resultfirst) = 2 * ge_signed_half_expand_resultfirstrealdecode + 1 /\ (ge_balance_positive_expand_resultfirstreal) = 0) /\ (ge_balance_negative_expand_resultfirstreal) = S ge_signed_half_expand_resultfirstrealdecode))) /\ ((ge_first_rp_expand_result) + ge_balance_negative_expand_resultfirstreal = (ge_first_rn_expand_result) + ge_balance_positive_expand_resultfirstreal))) /\ (exists ge_balance_positive_expand_resultfirstimaginary ge_balance_negative_expand_resultfirstimaginary. (((((ge_representation_imaginary_code_expand_resultfirst) = 2 * (ge_balance_positive_expand_resultfirstimaginary) /\ (ge_balance_negative_expand_resultfirstimaginary) = 0) \/ exists ge_signed_half_expand_resultfirstimaginarydecode. (((ge_representation_imaginary_code_expand_resultfirst) = 2 * ge_signed_half_expand_resultfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_resultfirstimaginary) = 0) /\ (ge_balance_negative_expand_resultfirstimaginary) = S ge_signed_half_expand_resultfirstimaginarydecode))) /\ ((ge_first_ip_expand_result) + ge_balance_negative_expand_resultfirstimaginary = (ge_first_in_expand_result) + ge_balance_positive_expand_resultfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_resultsecond ge_representation_imaginary_code_expand_resultsecond. (((q) = ((ge_representation_real_code_expand_resultsecond) + (ge_representation_imaginary_code_expand_resultsecond)) * S ((ge_representation_real_code_expand_resultsecond) + (ge_representation_imaginary_code_expand_resultsecond)) + ((ge_representation_imaginary_code_expand_resultsecond) + (ge_representation_imaginary_code_expand_resultsecond))) /\ ((exists ge_balance_positive_expand_resultsecondreal ge_balance_negative_expand_resultsecondreal. (((((ge_representation_real_code_expand_resultsecond) = 2 * (ge_balance_positive_expand_resultsecondreal) /\ (ge_balance_negative_expand_resultsecondreal) = 0) \/ exists ge_signed_half_expand_resultsecondrealdecode. (((ge_representation_real_code_expand_resultsecond) = 2 * ge_signed_half_expand_resultsecondrealdecode + 1 /\ (ge_balance_positive_expand_resultsecondreal) = 0) /\ (ge_balance_negative_expand_resultsecondreal) = S ge_signed_half_expand_resultsecondrealdecode))) /\ ((ge_second_rp_expand_result) + ge_balance_negative_expand_resultsecondreal = (ge_second_rn_expand_result) + ge_balance_positive_expand_resultsecondreal))) /\ (exists ge_balance_positive_expand_resultsecondimaginary ge_balance_negative_expand_resultsecondimaginary. (((((ge_representation_imaginary_code_expand_resultsecond) = 2 * (ge_balance_positive_expand_resultsecondimaginary) /\ (ge_balance_negative_expand_resultsecondimaginary) = 0) \/ exists ge_signed_half_expand_resultsecondimaginarydecode. (((ge_representation_imaginary_code_expand_resultsecond) = 2 * ge_signed_half_expand_resultsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_resultsecondimaginary) = 0) /\ (ge_balance_negative_expand_resultsecondimaginary) = S ge_signed_half_expand_resultsecondimaginarydecode))) /\ ((ge_second_ip_expand_result) + ge_balance_negative_expand_resultsecondimaginary = (ge_second_in_expand_result) + ge_balance_positive_expand_resultsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_resultoutput ge_representation_imaginary_code_expand_resultoutput. (((t) = ((ge_representation_real_code_expand_resultoutput) + (ge_representation_imaginary_code_expand_resultoutput)) * S ((ge_representation_real_code_expand_resultoutput) + (ge_representation_imaginary_code_expand_resultoutput)) + ((ge_representation_imaginary_code_expand_resultoutput) + (ge_representation_imaginary_code_expand_resultoutput))) /\ ((exists ge_balance_positive_expand_resultoutputreal ge_balance_negative_expand_resultoutputreal. (((((ge_representation_real_code_expand_resultoutput) = 2 * (ge_balance_positive_expand_resultoutputreal) /\ (ge_balance_negative_expand_resultoutputreal) = 0) \/ exists ge_signed_half_expand_resultoutputrealdecode. (((ge_representation_real_code_expand_resultoutput) = 2 * ge_signed_half_expand_resultoutputrealdecode + 1 /\ (ge_balance_positive_expand_resultoutputreal) = 0) /\ (ge_balance_negative_expand_resultoutputreal) = S ge_signed_half_expand_resultoutputrealdecode))) /\ ((((ge_first_rp_expand_result) + (ge_second_rp_expand_result))) + ge_balance_negative_expand_resultoutputreal = (((ge_first_rn_expand_result) + (ge_second_rn_expand_result))) + ge_balance_positive_expand_resultoutputreal))) /\ (exists ge_balance_positive_expand_resultoutputimaginary ge_balance_negative_expand_resultoutputimaginary. (((((ge_representation_imaginary_code_expand_resultoutput) = 2 * (ge_balance_positive_expand_resultoutputimaginary) /\ (ge_balance_negative_expand_resultoutputimaginary) = 0) \/ exists ge_signed_half_expand_resultoutputimaginarydecode. (((ge_representation_imaginary_code_expand_resultoutput) = 2 * ge_signed_half_expand_resultoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_resultoutputimaginary) = 0) /\ (ge_balance_negative_expand_resultoutputimaginary) = S ge_signed_half_expand_resultoutputimaginarydecode))) /\ ((((ge_first_ip_expand_result) + (ge_second_ip_expand_result))) + ge_balance_negative_expand_resultoutputimaginary = (((ge_first_in_expand_result) + (ge_second_in_expand_result))) + ge_balance_positive_expand_resultoutputimaginary)))))))))