gaussian_multiply_add_compose

Exact expanded first-order arithmetic statement

forall a b c s p q t. (exists ge_first_rp_distribute_sum ge_first_rn_distribute_sum ge_first_ip_distribute_sum ge_first_in_distribute_sum ge_second_rp_distribute_sum ge_second_rn_distribute_sum ge_second_ip_distribute_sum ge_second_in_distribute_sum. ((exists ge_representation_real_code_distribute_sumfirst ge_representation_imaginary_code_distribute_sumfirst. (((b) = ((ge_representation_real_code_distribute_sumfirst) + (ge_representation_imaginary_code_distribute_sumfirst)) * S ((ge_representation_real_code_distribute_sumfirst) + (ge_representation_imaginary_code_distribute_sumfirst)) + ((ge_representation_imaginary_code_distribute_sumfirst) + (ge_representation_imaginary_code_distribute_sumfirst))) /\ ((exists ge_balance_positive_distribute_sumfirstreal ge_balance_negative_distribute_sumfirstreal. (((((ge_representation_real_code_distribute_sumfirst) = 2 * (ge_balance_positive_distribute_sumfirstreal) /\ (ge_balance_negative_distribute_sumfirstreal) = 0) \/ exists ge_signed_half_distribute_sumfirstrealdecode. (((ge_representation_real_code_distribute_sumfirst) = 2 * ge_signed_half_distribute_sumfirstrealdecode + 1 /\ (ge_balance_positive_distribute_sumfirstreal) = 0) /\ (ge_balance_negative_distribute_sumfirstreal) = S ge_signed_half_distribute_sumfirstrealdecode))) /\ ((ge_first_rp_distribute_sum) + ge_balance_negative_distribute_sumfirstreal = (ge_first_rn_distribute_sum) + ge_balance_positive_distribute_sumfirstreal))) /\ (exists ge_balance_positive_distribute_sumfirstimaginary ge_balance_negative_distribute_sumfirstimaginary. (((((ge_representation_imaginary_code_distribute_sumfirst) = 2 * (ge_balance_positive_distribute_sumfirstimaginary) /\ (ge_balance_negative_distribute_sumfirstimaginary) = 0) \/ exists ge_signed_half_distribute_sumfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_sumfirst) = 2 * ge_signed_half_distribute_sumfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_sumfirstimaginary) = 0) /\ (ge_balance_negative_distribute_sumfirstimaginary) = S ge_signed_half_distribute_sumfirstimaginarydecode))) /\ ((ge_first_ip_distribute_sum) + ge_balance_negative_distribute_sumfirstimaginary = (ge_first_in_distribute_sum) + ge_balance_positive_distribute_sumfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_sumsecond ge_representation_imaginary_code_distribute_sumsecond. (((c) = ((ge_representation_real_code_distribute_sumsecond) + (ge_representation_imaginary_code_distribute_sumsecond)) * S ((ge_representation_real_code_distribute_sumsecond) + (ge_representation_imaginary_code_distribute_sumsecond)) + ((ge_representation_imaginary_code_distribute_sumsecond) + (ge_representation_imaginary_code_distribute_sumsecond))) /\ ((exists ge_balance_positive_distribute_sumsecondreal ge_balance_negative_distribute_sumsecondreal. (((((ge_representation_real_code_distribute_sumsecond) = 2 * (ge_balance_positive_distribute_sumsecondreal) /\ (ge_balance_negative_distribute_sumsecondreal) = 0) \/ exists ge_signed_half_distribute_sumsecondrealdecode. (((ge_representation_real_code_distribute_sumsecond) = 2 * ge_signed_half_distribute_sumsecondrealdecode + 1 /\ (ge_balance_positive_distribute_sumsecondreal) = 0) /\ (ge_balance_negative_distribute_sumsecondreal) = S ge_signed_half_distribute_sumsecondrealdecode))) /\ ((ge_second_rp_distribute_sum) + ge_balance_negative_distribute_sumsecondreal = (ge_second_rn_distribute_sum) + ge_balance_positive_distribute_sumsecondreal))) /\ (exists ge_balance_positive_distribute_sumsecondimaginary ge_balance_negative_distribute_sumsecondimaginary. (((((ge_representation_imaginary_code_distribute_sumsecond) = 2 * (ge_balance_positive_distribute_sumsecondimaginary) /\ (ge_balance_negative_distribute_sumsecondimaginary) = 0) \/ exists ge_signed_half_distribute_sumsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_sumsecond) = 2 * ge_signed_half_distribute_sumsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_sumsecondimaginary) = 0) /\ (ge_balance_negative_distribute_sumsecondimaginary) = S ge_signed_half_distribute_sumsecondimaginarydecode))) /\ ((ge_second_ip_distribute_sum) + ge_balance_negative_distribute_sumsecondimaginary = (ge_second_in_distribute_sum) + ge_balance_positive_distribute_sumsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_sumoutput ge_representation_imaginary_code_distribute_sumoutput. (((s) = ((ge_representation_real_code_distribute_sumoutput) + (ge_representation_imaginary_code_distribute_sumoutput)) * S ((ge_representation_real_code_distribute_sumoutput) + (ge_representation_imaginary_code_distribute_sumoutput)) + ((ge_representation_imaginary_code_distribute_sumoutput) + (ge_representation_imaginary_code_distribute_sumoutput))) /\ ((exists ge_balance_positive_distribute_sumoutputreal ge_balance_negative_distribute_sumoutputreal. (((((ge_representation_real_code_distribute_sumoutput) = 2 * (ge_balance_positive_distribute_sumoutputreal) /\ (ge_balance_negative_distribute_sumoutputreal) = 0) \/ exists ge_signed_half_distribute_sumoutputrealdecode. (((ge_representation_real_code_distribute_sumoutput) = 2 * ge_signed_half_distribute_sumoutputrealdecode + 1 /\ (ge_balance_positive_distribute_sumoutputreal) = 0) /\ (ge_balance_negative_distribute_sumoutputreal) = S ge_signed_half_distribute_sumoutputrealdecode))) /\ ((((ge_first_rp_distribute_sum) + (ge_second_rp_distribute_sum))) + ge_balance_negative_distribute_sumoutputreal = (((ge_first_rn_distribute_sum) + (ge_second_rn_distribute_sum))) + ge_balance_positive_distribute_sumoutputreal))) /\ (exists ge_balance_positive_distribute_sumoutputimaginary ge_balance_negative_distribute_sumoutputimaginary. (((((ge_representation_imaginary_code_distribute_sumoutput) = 2 * (ge_balance_positive_distribute_sumoutputimaginary) /\ (ge_balance_negative_distribute_sumoutputimaginary) = 0) \/ exists ge_signed_half_distribute_sumoutputimaginarydecode. (((ge_representation_imaginary_code_distribute_sumoutput) = 2 * ge_signed_half_distribute_sumoutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_sumoutputimaginary) = 0) /\ (ge_balance_negative_distribute_sumoutputimaginary) = S ge_signed_half_distribute_sumoutputimaginarydecode))) /\ ((((ge_first_ip_distribute_sum) + (ge_second_ip_distribute_sum))) + ge_balance_negative_distribute_sumoutputimaginary = (((ge_first_in_distribute_sum) + (ge_second_in_distribute_sum))) + ge_balance_positive_distribute_sumoutputimaginary))))))))) -> (exists ge_first_rp_distribute_first ge_first_rn_distribute_first ge_first_ip_distribute_first ge_first_in_distribute_first ge_second_rp_distribute_first ge_second_rn_distribute_first ge_second_ip_distribute_first ge_second_in_distribute_first. ((exists ge_representation_real_code_distribute_firstfirst ge_representation_imaginary_code_distribute_firstfirst. (((a) = ((ge_representation_real_code_distribute_firstfirst) + (ge_representation_imaginary_code_distribute_firstfirst)) * S ((ge_representation_real_code_distribute_firstfirst) + (ge_representation_imaginary_code_distribute_firstfirst)) + ((ge_representation_imaginary_code_distribute_firstfirst) + (ge_representation_imaginary_code_distribute_firstfirst))) /\ ((exists ge_balance_positive_distribute_firstfirstreal ge_balance_negative_distribute_firstfirstreal. (((((ge_representation_real_code_distribute_firstfirst) = 2 * (ge_balance_positive_distribute_firstfirstreal) /\ (ge_balance_negative_distribute_firstfirstreal) = 0) \/ exists ge_signed_half_distribute_firstfirstrealdecode. (((ge_representation_real_code_distribute_firstfirst) = 2 * ge_signed_half_distribute_firstfirstrealdecode + 1 /\ (ge_balance_positive_distribute_firstfirstreal) = 0) /\ (ge_balance_negative_distribute_firstfirstreal) = S ge_signed_half_distribute_firstfirstrealdecode))) /\ ((ge_first_rp_distribute_first) + ge_balance_negative_distribute_firstfirstreal = (ge_first_rn_distribute_first) + ge_balance_positive_distribute_firstfirstreal))) /\ (exists ge_balance_positive_distribute_firstfirstimaginary ge_balance_negative_distribute_firstfirstimaginary. (((((ge_representation_imaginary_code_distribute_firstfirst) = 2 * (ge_balance_positive_distribute_firstfirstimaginary) /\ (ge_balance_negative_distribute_firstfirstimaginary) = 0) \/ exists ge_signed_half_distribute_firstfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_firstfirst) = 2 * ge_signed_half_distribute_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_firstfirstimaginary) = 0) /\ (ge_balance_negative_distribute_firstfirstimaginary) = S ge_signed_half_distribute_firstfirstimaginarydecode))) /\ ((ge_first_ip_distribute_first) + ge_balance_negative_distribute_firstfirstimaginary = (ge_first_in_distribute_first) + ge_balance_positive_distribute_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_firstsecond ge_representation_imaginary_code_distribute_firstsecond. (((b) = ((ge_representation_real_code_distribute_firstsecond) + (ge_representation_imaginary_code_distribute_firstsecond)) * S ((ge_representation_real_code_distribute_firstsecond) + (ge_representation_imaginary_code_distribute_firstsecond)) + ((ge_representation_imaginary_code_distribute_firstsecond) + (ge_representation_imaginary_code_distribute_firstsecond))) /\ ((exists ge_balance_positive_distribute_firstsecondreal ge_balance_negative_distribute_firstsecondreal. (((((ge_representation_real_code_distribute_firstsecond) = 2 * (ge_balance_positive_distribute_firstsecondreal) /\ (ge_balance_negative_distribute_firstsecondreal) = 0) \/ exists ge_signed_half_distribute_firstsecondrealdecode. (((ge_representation_real_code_distribute_firstsecond) = 2 * ge_signed_half_distribute_firstsecondrealdecode + 1 /\ (ge_balance_positive_distribute_firstsecondreal) = 0) /\ (ge_balance_negative_distribute_firstsecondreal) = S ge_signed_half_distribute_firstsecondrealdecode))) /\ ((ge_second_rp_distribute_first) + ge_balance_negative_distribute_firstsecondreal = (ge_second_rn_distribute_first) + ge_balance_positive_distribute_firstsecondreal))) /\ (exists ge_balance_positive_distribute_firstsecondimaginary ge_balance_negative_distribute_firstsecondimaginary. (((((ge_representation_imaginary_code_distribute_firstsecond) = 2 * (ge_balance_positive_distribute_firstsecondimaginary) /\ (ge_balance_negative_distribute_firstsecondimaginary) = 0) \/ exists ge_signed_half_distribute_firstsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_firstsecond) = 2 * ge_signed_half_distribute_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_firstsecondimaginary) = 0) /\ (ge_balance_negative_distribute_firstsecondimaginary) = S ge_signed_half_distribute_firstsecondimaginarydecode))) /\ ((ge_second_ip_distribute_first) + ge_balance_negative_distribute_firstsecondimaginary = (ge_second_in_distribute_first) + ge_balance_positive_distribute_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_firstoutput ge_representation_imaginary_code_distribute_firstoutput. (((p) = ((ge_representation_real_code_distribute_firstoutput) + (ge_representation_imaginary_code_distribute_firstoutput)) * S ((ge_representation_real_code_distribute_firstoutput) + (ge_representation_imaginary_code_distribute_firstoutput)) + ((ge_representation_imaginary_code_distribute_firstoutput) + (ge_representation_imaginary_code_distribute_firstoutput))) /\ ((exists ge_balance_positive_distribute_firstoutputreal ge_balance_negative_distribute_firstoutputreal. (((((ge_representation_real_code_distribute_firstoutput) = 2 * (ge_balance_positive_distribute_firstoutputreal) /\ (ge_balance_negative_distribute_firstoutputreal) = 0) \/ exists ge_signed_half_distribute_firstoutputrealdecode. (((ge_representation_real_code_distribute_firstoutput) = 2 * ge_signed_half_distribute_firstoutputrealdecode + 1 /\ (ge_balance_positive_distribute_firstoutputreal) = 0) /\ (ge_balance_negative_distribute_firstoutputreal) = S ge_signed_half_distribute_firstoutputrealdecode))) /\ ((((((((ge_first_rp_distribute_first) * (ge_second_rp_distribute_first))) + (((ge_first_rn_distribute_first) * (ge_second_rn_distribute_first))))) + (((((ge_first_ip_distribute_first) * (ge_second_in_distribute_first))) + (((ge_first_in_distribute_first) * (ge_second_ip_distribute_first))))))) + ge_balance_negative_distribute_firstoutputreal = (((((((ge_first_rp_distribute_first) * (ge_second_rn_distribute_first))) + (((ge_first_rn_distribute_first) * (ge_second_rp_distribute_first))))) + (((((ge_first_ip_distribute_first) * (ge_second_ip_distribute_first))) + (((ge_first_in_distribute_first) * (ge_second_in_distribute_first))))))) + ge_balance_positive_distribute_firstoutputreal))) /\ (exists ge_balance_positive_distribute_firstoutputimaginary ge_balance_negative_distribute_firstoutputimaginary. (((((ge_representation_imaginary_code_distribute_firstoutput) = 2 * (ge_balance_positive_distribute_firstoutputimaginary) /\ (ge_balance_negative_distribute_firstoutputimaginary) = 0) \/ exists ge_signed_half_distribute_firstoutputimaginarydecode. (((ge_representation_imaginary_code_distribute_firstoutput) = 2 * ge_signed_half_distribute_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_firstoutputimaginary) = 0) /\ (ge_balance_negative_distribute_firstoutputimaginary) = S ge_signed_half_distribute_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_distribute_first) * (ge_second_ip_distribute_first))) + (((ge_first_rn_distribute_first) * (ge_second_in_distribute_first))))) + (((((ge_first_ip_distribute_first) * (ge_second_rp_distribute_first))) + (((ge_first_in_distribute_first) * (ge_second_rn_distribute_first))))))) + ge_balance_negative_distribute_firstoutputimaginary = (((((((ge_first_rp_distribute_first) * (ge_second_in_distribute_first))) + (((ge_first_rn_distribute_first) * (ge_second_ip_distribute_first))))) + (((((ge_first_ip_distribute_first) * (ge_second_rn_distribute_first))) + (((ge_first_in_distribute_first) * (ge_second_rp_distribute_first))))))) + ge_balance_positive_distribute_firstoutputimaginary))))))))) -> (exists ge_first_rp_distribute_second ge_first_rn_distribute_second ge_first_ip_distribute_second ge_first_in_distribute_second ge_second_rp_distribute_second ge_second_rn_distribute_second ge_second_ip_distribute_second ge_second_in_distribute_second. ((exists ge_representation_real_code_distribute_secondfirst ge_representation_imaginary_code_distribute_secondfirst. (((a) = ((ge_representation_real_code_distribute_secondfirst) + (ge_representation_imaginary_code_distribute_secondfirst)) * S ((ge_representation_real_code_distribute_secondfirst) + (ge_representation_imaginary_code_distribute_secondfirst)) + ((ge_representation_imaginary_code_distribute_secondfirst) + (ge_representation_imaginary_code_distribute_secondfirst))) /\ ((exists ge_balance_positive_distribute_secondfirstreal ge_balance_negative_distribute_secondfirstreal. (((((ge_representation_real_code_distribute_secondfirst) = 2 * (ge_balance_positive_distribute_secondfirstreal) /\ (ge_balance_negative_distribute_secondfirstreal) = 0) \/ exists ge_signed_half_distribute_secondfirstrealdecode. (((ge_representation_real_code_distribute_secondfirst) = 2 * ge_signed_half_distribute_secondfirstrealdecode + 1 /\ (ge_balance_positive_distribute_secondfirstreal) = 0) /\ (ge_balance_negative_distribute_secondfirstreal) = S ge_signed_half_distribute_secondfirstrealdecode))) /\ ((ge_first_rp_distribute_second) + ge_balance_negative_distribute_secondfirstreal = (ge_first_rn_distribute_second) + ge_balance_positive_distribute_secondfirstreal))) /\ (exists ge_balance_positive_distribute_secondfirstimaginary ge_balance_negative_distribute_secondfirstimaginary. (((((ge_representation_imaginary_code_distribute_secondfirst) = 2 * (ge_balance_positive_distribute_secondfirstimaginary) /\ (ge_balance_negative_distribute_secondfirstimaginary) = 0) \/ exists ge_signed_half_distribute_secondfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_secondfirst) = 2 * ge_signed_half_distribute_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_secondfirstimaginary) = 0) /\ (ge_balance_negative_distribute_secondfirstimaginary) = S ge_signed_half_distribute_secondfirstimaginarydecode))) /\ ((ge_first_ip_distribute_second) + ge_balance_negative_distribute_secondfirstimaginary = (ge_first_in_distribute_second) + ge_balance_positive_distribute_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_secondsecond ge_representation_imaginary_code_distribute_secondsecond. (((c) = ((ge_representation_real_code_distribute_secondsecond) + (ge_representation_imaginary_code_distribute_secondsecond)) * S ((ge_representation_real_code_distribute_secondsecond) + (ge_representation_imaginary_code_distribute_secondsecond)) + ((ge_representation_imaginary_code_distribute_secondsecond) + (ge_representation_imaginary_code_distribute_secondsecond))) /\ ((exists ge_balance_positive_distribute_secondsecondreal ge_balance_negative_distribute_secondsecondreal. (((((ge_representation_real_code_distribute_secondsecond) = 2 * (ge_balance_positive_distribute_secondsecondreal) /\ (ge_balance_negative_distribute_secondsecondreal) = 0) \/ exists ge_signed_half_distribute_secondsecondrealdecode. (((ge_representation_real_code_distribute_secondsecond) = 2 * ge_signed_half_distribute_secondsecondrealdecode + 1 /\ (ge_balance_positive_distribute_secondsecondreal) = 0) /\ (ge_balance_negative_distribute_secondsecondreal) = S ge_signed_half_distribute_secondsecondrealdecode))) /\ ((ge_second_rp_distribute_second) + ge_balance_negative_distribute_secondsecondreal = (ge_second_rn_distribute_second) + ge_balance_positive_distribute_secondsecondreal))) /\ (exists ge_balance_positive_distribute_secondsecondimaginary ge_balance_negative_distribute_secondsecondimaginary. (((((ge_representation_imaginary_code_distribute_secondsecond) = 2 * (ge_balance_positive_distribute_secondsecondimaginary) /\ (ge_balance_negative_distribute_secondsecondimaginary) = 0) \/ exists ge_signed_half_distribute_secondsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_secondsecond) = 2 * ge_signed_half_distribute_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_secondsecondimaginary) = 0) /\ (ge_balance_negative_distribute_secondsecondimaginary) = S ge_signed_half_distribute_secondsecondimaginarydecode))) /\ ((ge_second_ip_distribute_second) + ge_balance_negative_distribute_secondsecondimaginary = (ge_second_in_distribute_second) + ge_balance_positive_distribute_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_secondoutput ge_representation_imaginary_code_distribute_secondoutput. (((q) = ((ge_representation_real_code_distribute_secondoutput) + (ge_representation_imaginary_code_distribute_secondoutput)) * S ((ge_representation_real_code_distribute_secondoutput) + (ge_representation_imaginary_code_distribute_secondoutput)) + ((ge_representation_imaginary_code_distribute_secondoutput) + (ge_representation_imaginary_code_distribute_secondoutput))) /\ ((exists ge_balance_positive_distribute_secondoutputreal ge_balance_negative_distribute_secondoutputreal. (((((ge_representation_real_code_distribute_secondoutput) = 2 * (ge_balance_positive_distribute_secondoutputreal) /\ (ge_balance_negative_distribute_secondoutputreal) = 0) \/ exists ge_signed_half_distribute_secondoutputrealdecode. (((ge_representation_real_code_distribute_secondoutput) = 2 * ge_signed_half_distribute_secondoutputrealdecode + 1 /\ (ge_balance_positive_distribute_secondoutputreal) = 0) /\ (ge_balance_negative_distribute_secondoutputreal) = S ge_signed_half_distribute_secondoutputrealdecode))) /\ ((((((((ge_first_rp_distribute_second) * (ge_second_rp_distribute_second))) + (((ge_first_rn_distribute_second) * (ge_second_rn_distribute_second))))) + (((((ge_first_ip_distribute_second) * (ge_second_in_distribute_second))) + (((ge_first_in_distribute_second) * (ge_second_ip_distribute_second))))))) + ge_balance_negative_distribute_secondoutputreal = (((((((ge_first_rp_distribute_second) * (ge_second_rn_distribute_second))) + (((ge_first_rn_distribute_second) * (ge_second_rp_distribute_second))))) + (((((ge_first_ip_distribute_second) * (ge_second_ip_distribute_second))) + (((ge_first_in_distribute_second) * (ge_second_in_distribute_second))))))) + ge_balance_positive_distribute_secondoutputreal))) /\ (exists ge_balance_positive_distribute_secondoutputimaginary ge_balance_negative_distribute_secondoutputimaginary. (((((ge_representation_imaginary_code_distribute_secondoutput) = 2 * (ge_balance_positive_distribute_secondoutputimaginary) /\ (ge_balance_negative_distribute_secondoutputimaginary) = 0) \/ exists ge_signed_half_distribute_secondoutputimaginarydecode. (((ge_representation_imaginary_code_distribute_secondoutput) = 2 * ge_signed_half_distribute_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_secondoutputimaginary) = 0) /\ (ge_balance_negative_distribute_secondoutputimaginary) = S ge_signed_half_distribute_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_distribute_second) * (ge_second_ip_distribute_second))) + (((ge_first_rn_distribute_second) * (ge_second_in_distribute_second))))) + (((((ge_first_ip_distribute_second) * (ge_second_rp_distribute_second))) + (((ge_first_in_distribute_second) * (ge_second_rn_distribute_second))))))) + ge_balance_negative_distribute_secondoutputimaginary = (((((((ge_first_rp_distribute_second) * (ge_second_in_distribute_second))) + (((ge_first_rn_distribute_second) * (ge_second_ip_distribute_second))))) + (((((ge_first_ip_distribute_second) * (ge_second_rn_distribute_second))) + (((ge_first_in_distribute_second) * (ge_second_rp_distribute_second))))))) + ge_balance_positive_distribute_secondoutputimaginary))))))))) -> (exists ge_first_rp_distribute_total ge_first_rn_distribute_total ge_first_ip_distribute_total ge_first_in_distribute_total ge_second_rp_distribute_total ge_second_rn_distribute_total ge_second_ip_distribute_total ge_second_in_distribute_total. ((exists ge_representation_real_code_distribute_totalfirst ge_representation_imaginary_code_distribute_totalfirst. (((p) = ((ge_representation_real_code_distribute_totalfirst) + (ge_representation_imaginary_code_distribute_totalfirst)) * S ((ge_representation_real_code_distribute_totalfirst) + (ge_representation_imaginary_code_distribute_totalfirst)) + ((ge_representation_imaginary_code_distribute_totalfirst) + (ge_representation_imaginary_code_distribute_totalfirst))) /\ ((exists ge_balance_positive_distribute_totalfirstreal ge_balance_negative_distribute_totalfirstreal. (((((ge_representation_real_code_distribute_totalfirst) = 2 * (ge_balance_positive_distribute_totalfirstreal) /\ (ge_balance_negative_distribute_totalfirstreal) = 0) \/ exists ge_signed_half_distribute_totalfirstrealdecode. (((ge_representation_real_code_distribute_totalfirst) = 2 * ge_signed_half_distribute_totalfirstrealdecode + 1 /\ (ge_balance_positive_distribute_totalfirstreal) = 0) /\ (ge_balance_negative_distribute_totalfirstreal) = S ge_signed_half_distribute_totalfirstrealdecode))) /\ ((ge_first_rp_distribute_total) + ge_balance_negative_distribute_totalfirstreal = (ge_first_rn_distribute_total) + ge_balance_positive_distribute_totalfirstreal))) /\ (exists ge_balance_positive_distribute_totalfirstimaginary ge_balance_negative_distribute_totalfirstimaginary. (((((ge_representation_imaginary_code_distribute_totalfirst) = 2 * (ge_balance_positive_distribute_totalfirstimaginary) /\ (ge_balance_negative_distribute_totalfirstimaginary) = 0) \/ exists ge_signed_half_distribute_totalfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_totalfirst) = 2 * ge_signed_half_distribute_totalfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_totalfirstimaginary) = 0) /\ (ge_balance_negative_distribute_totalfirstimaginary) = S ge_signed_half_distribute_totalfirstimaginarydecode))) /\ ((ge_first_ip_distribute_total) + ge_balance_negative_distribute_totalfirstimaginary = (ge_first_in_distribute_total) + ge_balance_positive_distribute_totalfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_totalsecond ge_representation_imaginary_code_distribute_totalsecond. (((q) = ((ge_representation_real_code_distribute_totalsecond) + (ge_representation_imaginary_code_distribute_totalsecond)) * S ((ge_representation_real_code_distribute_totalsecond) + (ge_representation_imaginary_code_distribute_totalsecond)) + ((ge_representation_imaginary_code_distribute_totalsecond) + (ge_representation_imaginary_code_distribute_totalsecond))) /\ ((exists ge_balance_positive_distribute_totalsecondreal ge_balance_negative_distribute_totalsecondreal. (((((ge_representation_real_code_distribute_totalsecond) = 2 * (ge_balance_positive_distribute_totalsecondreal) /\ (ge_balance_negative_distribute_totalsecondreal) = 0) \/ exists ge_signed_half_distribute_totalsecondrealdecode. (((ge_representation_real_code_distribute_totalsecond) = 2 * ge_signed_half_distribute_totalsecondrealdecode + 1 /\ (ge_balance_positive_distribute_totalsecondreal) = 0) /\ (ge_balance_negative_distribute_totalsecondreal) = S ge_signed_half_distribute_totalsecondrealdecode))) /\ ((ge_second_rp_distribute_total) + ge_balance_negative_distribute_totalsecondreal = (ge_second_rn_distribute_total) + ge_balance_positive_distribute_totalsecondreal))) /\ (exists ge_balance_positive_distribute_totalsecondimaginary ge_balance_negative_distribute_totalsecondimaginary. (((((ge_representation_imaginary_code_distribute_totalsecond) = 2 * (ge_balance_positive_distribute_totalsecondimaginary) /\ (ge_balance_negative_distribute_totalsecondimaginary) = 0) \/ exists ge_signed_half_distribute_totalsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_totalsecond) = 2 * ge_signed_half_distribute_totalsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_totalsecondimaginary) = 0) /\ (ge_balance_negative_distribute_totalsecondimaginary) = S ge_signed_half_distribute_totalsecondimaginarydecode))) /\ ((ge_second_ip_distribute_total) + ge_balance_negative_distribute_totalsecondimaginary = (ge_second_in_distribute_total) + ge_balance_positive_distribute_totalsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_totaloutput ge_representation_imaginary_code_distribute_totaloutput. (((t) = ((ge_representation_real_code_distribute_totaloutput) + (ge_representation_imaginary_code_distribute_totaloutput)) * S ((ge_representation_real_code_distribute_totaloutput) + (ge_representation_imaginary_code_distribute_totaloutput)) + ((ge_representation_imaginary_code_distribute_totaloutput) + (ge_representation_imaginary_code_distribute_totaloutput))) /\ ((exists ge_balance_positive_distribute_totaloutputreal ge_balance_negative_distribute_totaloutputreal. (((((ge_representation_real_code_distribute_totaloutput) = 2 * (ge_balance_positive_distribute_totaloutputreal) /\ (ge_balance_negative_distribute_totaloutputreal) = 0) \/ exists ge_signed_half_distribute_totaloutputrealdecode. (((ge_representation_real_code_distribute_totaloutput) = 2 * ge_signed_half_distribute_totaloutputrealdecode + 1 /\ (ge_balance_positive_distribute_totaloutputreal) = 0) /\ (ge_balance_negative_distribute_totaloutputreal) = S ge_signed_half_distribute_totaloutputrealdecode))) /\ ((((ge_first_rp_distribute_total) + (ge_second_rp_distribute_total))) + ge_balance_negative_distribute_totaloutputreal = (((ge_first_rn_distribute_total) + (ge_second_rn_distribute_total))) + ge_balance_positive_distribute_totaloutputreal))) /\ (exists ge_balance_positive_distribute_totaloutputimaginary ge_balance_negative_distribute_totaloutputimaginary. (((((ge_representation_imaginary_code_distribute_totaloutput) = 2 * (ge_balance_positive_distribute_totaloutputimaginary) /\ (ge_balance_negative_distribute_totaloutputimaginary) = 0) \/ exists ge_signed_half_distribute_totaloutputimaginarydecode. (((ge_representation_imaginary_code_distribute_totaloutput) = 2 * ge_signed_half_distribute_totaloutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_totaloutputimaginary) = 0) /\ (ge_balance_negative_distribute_totaloutputimaginary) = S ge_signed_half_distribute_totaloutputimaginarydecode))) /\ ((((ge_first_ip_distribute_total) + (ge_second_ip_distribute_total))) + ge_balance_negative_distribute_totaloutputimaginary = (((ge_first_in_distribute_total) + (ge_second_in_distribute_total))) + ge_balance_positive_distribute_totaloutputimaginary))))))))) -> (exists ge_first_rp_distribute_product ge_first_rn_distribute_product ge_first_ip_distribute_product ge_first_in_distribute_product ge_second_rp_distribute_product ge_second_rn_distribute_product ge_second_ip_distribute_product ge_second_in_distribute_product. ((exists ge_representation_real_code_distribute_productfirst ge_representation_imaginary_code_distribute_productfirst. (((a) = ((ge_representation_real_code_distribute_productfirst) + (ge_representation_imaginary_code_distribute_productfirst)) * S ((ge_representation_real_code_distribute_productfirst) + (ge_representation_imaginary_code_distribute_productfirst)) + ((ge_representation_imaginary_code_distribute_productfirst) + (ge_representation_imaginary_code_distribute_productfirst))) /\ ((exists ge_balance_positive_distribute_productfirstreal ge_balance_negative_distribute_productfirstreal. (((((ge_representation_real_code_distribute_productfirst) = 2 * (ge_balance_positive_distribute_productfirstreal) /\ (ge_balance_negative_distribute_productfirstreal) = 0) \/ exists ge_signed_half_distribute_productfirstrealdecode. (((ge_representation_real_code_distribute_productfirst) = 2 * ge_signed_half_distribute_productfirstrealdecode + 1 /\ (ge_balance_positive_distribute_productfirstreal) = 0) /\ (ge_balance_negative_distribute_productfirstreal) = S ge_signed_half_distribute_productfirstrealdecode))) /\ ((ge_first_rp_distribute_product) + ge_balance_negative_distribute_productfirstreal = (ge_first_rn_distribute_product) + ge_balance_positive_distribute_productfirstreal))) /\ (exists ge_balance_positive_distribute_productfirstimaginary ge_balance_negative_distribute_productfirstimaginary. (((((ge_representation_imaginary_code_distribute_productfirst) = 2 * (ge_balance_positive_distribute_productfirstimaginary) /\ (ge_balance_negative_distribute_productfirstimaginary) = 0) \/ exists ge_signed_half_distribute_productfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_productfirst) = 2 * ge_signed_half_distribute_productfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_productfirstimaginary) = 0) /\ (ge_balance_negative_distribute_productfirstimaginary) = S ge_signed_half_distribute_productfirstimaginarydecode))) /\ ((ge_first_ip_distribute_product) + ge_balance_negative_distribute_productfirstimaginary = (ge_first_in_distribute_product) + ge_balance_positive_distribute_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_productsecond ge_representation_imaginary_code_distribute_productsecond. (((s) = ((ge_representation_real_code_distribute_productsecond) + (ge_representation_imaginary_code_distribute_productsecond)) * S ((ge_representation_real_code_distribute_productsecond) + (ge_representation_imaginary_code_distribute_productsecond)) + ((ge_representation_imaginary_code_distribute_productsecond) + (ge_representation_imaginary_code_distribute_productsecond))) /\ ((exists ge_balance_positive_distribute_productsecondreal ge_balance_negative_distribute_productsecondreal. (((((ge_representation_real_code_distribute_productsecond) = 2 * (ge_balance_positive_distribute_productsecondreal) /\ (ge_balance_negative_distribute_productsecondreal) = 0) \/ exists ge_signed_half_distribute_productsecondrealdecode. (((ge_representation_real_code_distribute_productsecond) = 2 * ge_signed_half_distribute_productsecondrealdecode + 1 /\ (ge_balance_positive_distribute_productsecondreal) = 0) /\ (ge_balance_negative_distribute_productsecondreal) = S ge_signed_half_distribute_productsecondrealdecode))) /\ ((ge_second_rp_distribute_product) + ge_balance_negative_distribute_productsecondreal = (ge_second_rn_distribute_product) + ge_balance_positive_distribute_productsecondreal))) /\ (exists ge_balance_positive_distribute_productsecondimaginary ge_balance_negative_distribute_productsecondimaginary. (((((ge_representation_imaginary_code_distribute_productsecond) = 2 * (ge_balance_positive_distribute_productsecondimaginary) /\ (ge_balance_negative_distribute_productsecondimaginary) = 0) \/ exists ge_signed_half_distribute_productsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_productsecond) = 2 * ge_signed_half_distribute_productsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_productsecondimaginary) = 0) /\ (ge_balance_negative_distribute_productsecondimaginary) = S ge_signed_half_distribute_productsecondimaginarydecode))) /\ ((ge_second_ip_distribute_product) + ge_balance_negative_distribute_productsecondimaginary = (ge_second_in_distribute_product) + ge_balance_positive_distribute_productsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_productoutput ge_representation_imaginary_code_distribute_productoutput. (((t) = ((ge_representation_real_code_distribute_productoutput) + (ge_representation_imaginary_code_distribute_productoutput)) * S ((ge_representation_real_code_distribute_productoutput) + (ge_representation_imaginary_code_distribute_productoutput)) + ((ge_representation_imaginary_code_distribute_productoutput) + (ge_representation_imaginary_code_distribute_productoutput))) /\ ((exists ge_balance_positive_distribute_productoutputreal ge_balance_negative_distribute_productoutputreal. (((((ge_representation_real_code_distribute_productoutput) = 2 * (ge_balance_positive_distribute_productoutputreal) /\ (ge_balance_negative_distribute_productoutputreal) = 0) \/ exists ge_signed_half_distribute_productoutputrealdecode. (((ge_representation_real_code_distribute_productoutput) = 2 * ge_signed_half_distribute_productoutputrealdecode + 1 /\ (ge_balance_positive_distribute_productoutputreal) = 0) /\ (ge_balance_negative_distribute_productoutputreal) = S ge_signed_half_distribute_productoutputrealdecode))) /\ ((((((((ge_first_rp_distribute_product) * (ge_second_rp_distribute_product))) + (((ge_first_rn_distribute_product) * (ge_second_rn_distribute_product))))) + (((((ge_first_ip_distribute_product) * (ge_second_in_distribute_product))) + (((ge_first_in_distribute_product) * (ge_second_ip_distribute_product))))))) + ge_balance_negative_distribute_productoutputreal = (((((((ge_first_rp_distribute_product) * (ge_second_rn_distribute_product))) + (((ge_first_rn_distribute_product) * (ge_second_rp_distribute_product))))) + (((((ge_first_ip_distribute_product) * (ge_second_ip_distribute_product))) + (((ge_first_in_distribute_product) * (ge_second_in_distribute_product))))))) + ge_balance_positive_distribute_productoutputreal))) /\ (exists ge_balance_positive_distribute_productoutputimaginary ge_balance_negative_distribute_productoutputimaginary. (((((ge_representation_imaginary_code_distribute_productoutput) = 2 * (ge_balance_positive_distribute_productoutputimaginary) /\ (ge_balance_negative_distribute_productoutputimaginary) = 0) \/ exists ge_signed_half_distribute_productoutputimaginarydecode. (((ge_representation_imaginary_code_distribute_productoutput) = 2 * ge_signed_half_distribute_productoutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_productoutputimaginary) = 0) /\ (ge_balance_negative_distribute_productoutputimaginary) = S ge_signed_half_distribute_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_distribute_product) * (ge_second_ip_distribute_product))) + (((ge_first_rn_distribute_product) * (ge_second_in_distribute_product))))) + (((((ge_first_ip_distribute_product) * (ge_second_rp_distribute_product))) + (((ge_first_in_distribute_product) * (ge_second_rn_distribute_product))))))) + ge_balance_negative_distribute_productoutputimaginary = (((((((ge_first_rp_distribute_product) * (ge_second_in_distribute_product))) + (((ge_first_rn_distribute_product) * (ge_second_ip_distribute_product))))) + (((((ge_first_ip_distribute_product) * (ge_second_rn_distribute_product))) + (((ge_first_in_distribute_product) * (ge_second_rp_distribute_product))))))) + ge_balance_positive_distribute_productoutputimaginary)))))))))