gaussian_divides_transitive

Exact expanded first-order arithmetic statement

forall d a z. (exists gr_quotient_transitive_first. (exists ge_first_rp_transitive_firstproduct ge_first_rn_transitive_firstproduct ge_first_ip_transitive_firstproduct ge_first_in_transitive_firstproduct ge_second_rp_transitive_firstproduct ge_second_rn_transitive_firstproduct ge_second_ip_transitive_firstproduct ge_second_in_transitive_firstproduct. ((exists ge_representation_real_code_transitive_firstproductfirst ge_representation_imaginary_code_transitive_firstproductfirst. (((d) = ((ge_representation_real_code_transitive_firstproductfirst) + (ge_representation_imaginary_code_transitive_firstproductfirst)) * S ((ge_representation_real_code_transitive_firstproductfirst) + (ge_representation_imaginary_code_transitive_firstproductfirst)) + ((ge_representation_imaginary_code_transitive_firstproductfirst) + (ge_representation_imaginary_code_transitive_firstproductfirst))) /\ ((exists ge_balance_positive_transitive_firstproductfirstreal ge_balance_negative_transitive_firstproductfirstreal. (((((ge_representation_real_code_transitive_firstproductfirst) = 2 * (ge_balance_positive_transitive_firstproductfirstreal) /\ (ge_balance_negative_transitive_firstproductfirstreal) = 0) \/ exists ge_signed_half_transitive_firstproductfirstrealdecode. (((ge_representation_real_code_transitive_firstproductfirst) = 2 * ge_signed_half_transitive_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_transitive_firstproductfirstreal) = 0) /\ (ge_balance_negative_transitive_firstproductfirstreal) = S ge_signed_half_transitive_firstproductfirstrealdecode))) /\ ((ge_first_rp_transitive_firstproduct) + ge_balance_negative_transitive_firstproductfirstreal = (ge_first_rn_transitive_firstproduct) + ge_balance_positive_transitive_firstproductfirstreal))) /\ (exists ge_balance_positive_transitive_firstproductfirstimaginary ge_balance_negative_transitive_firstproductfirstimaginary. (((((ge_representation_imaginary_code_transitive_firstproductfirst) = 2 * (ge_balance_positive_transitive_firstproductfirstimaginary) /\ (ge_balance_negative_transitive_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_transitive_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_transitive_firstproductfirst) = 2 * ge_signed_half_transitive_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_transitive_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_transitive_firstproductfirstimaginary) = S ge_signed_half_transitive_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_transitive_firstproduct) + ge_balance_negative_transitive_firstproductfirstimaginary = (ge_first_in_transitive_firstproduct) + ge_balance_positive_transitive_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_transitive_firstproductsecond ge_representation_imaginary_code_transitive_firstproductsecond. (((gr_quotient_transitive_first) = ((ge_representation_real_code_transitive_firstproductsecond) + (ge_representation_imaginary_code_transitive_firstproductsecond)) * S ((ge_representation_real_code_transitive_firstproductsecond) + (ge_representation_imaginary_code_transitive_firstproductsecond)) + ((ge_representation_imaginary_code_transitive_firstproductsecond) + (ge_representation_imaginary_code_transitive_firstproductsecond))) /\ ((exists ge_balance_positive_transitive_firstproductsecondreal ge_balance_negative_transitive_firstproductsecondreal. (((((ge_representation_real_code_transitive_firstproductsecond) = 2 * (ge_balance_positive_transitive_firstproductsecondreal) /\ (ge_balance_negative_transitive_firstproductsecondreal) = 0) \/ exists ge_signed_half_transitive_firstproductsecondrealdecode. (((ge_representation_real_code_transitive_firstproductsecond) = 2 * ge_signed_half_transitive_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_transitive_firstproductsecondreal) = 0) /\ (ge_balance_negative_transitive_firstproductsecondreal) = S ge_signed_half_transitive_firstproductsecondrealdecode))) /\ ((ge_second_rp_transitive_firstproduct) + ge_balance_negative_transitive_firstproductsecondreal = (ge_second_rn_transitive_firstproduct) + ge_balance_positive_transitive_firstproductsecondreal))) /\ (exists ge_balance_positive_transitive_firstproductsecondimaginary ge_balance_negative_transitive_firstproductsecondimaginary. (((((ge_representation_imaginary_code_transitive_firstproductsecond) = 2 * (ge_balance_positive_transitive_firstproductsecondimaginary) /\ (ge_balance_negative_transitive_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_transitive_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_transitive_firstproductsecond) = 2 * ge_signed_half_transitive_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_transitive_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_transitive_firstproductsecondimaginary) = S ge_signed_half_transitive_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_transitive_firstproduct) + ge_balance_negative_transitive_firstproductsecondimaginary = (ge_second_in_transitive_firstproduct) + ge_balance_positive_transitive_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_transitive_firstproductoutput ge_representation_imaginary_code_transitive_firstproductoutput. (((a) = ((ge_representation_real_code_transitive_firstproductoutput) + (ge_representation_imaginary_code_transitive_firstproductoutput)) * S ((ge_representation_real_code_transitive_firstproductoutput) + (ge_representation_imaginary_code_transitive_firstproductoutput)) + ((ge_representation_imaginary_code_transitive_firstproductoutput) + (ge_representation_imaginary_code_transitive_firstproductoutput))) /\ ((exists ge_balance_positive_transitive_firstproductoutputreal ge_balance_negative_transitive_firstproductoutputreal. (((((ge_representation_real_code_transitive_firstproductoutput) = 2 * (ge_balance_positive_transitive_firstproductoutputreal) /\ (ge_balance_negative_transitive_firstproductoutputreal) = 0) \/ exists ge_signed_half_transitive_firstproductoutputrealdecode. (((ge_representation_real_code_transitive_firstproductoutput) = 2 * ge_signed_half_transitive_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_transitive_firstproductoutputreal) = 0) /\ (ge_balance_negative_transitive_firstproductoutputreal) = S ge_signed_half_transitive_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_transitive_firstproduct) * (ge_second_rp_transitive_firstproduct))) + (((ge_first_rn_transitive_firstproduct) * (ge_second_rn_transitive_firstproduct))))) + (((((ge_first_ip_transitive_firstproduct) * (ge_second_in_transitive_firstproduct))) + (((ge_first_in_transitive_firstproduct) * (ge_second_ip_transitive_firstproduct))))))) + ge_balance_negative_transitive_firstproductoutputreal = (((((((ge_first_rp_transitive_firstproduct) * (ge_second_rn_transitive_firstproduct))) + (((ge_first_rn_transitive_firstproduct) * (ge_second_rp_transitive_firstproduct))))) + (((((ge_first_ip_transitive_firstproduct) * (ge_second_ip_transitive_firstproduct))) + (((ge_first_in_transitive_firstproduct) * (ge_second_in_transitive_firstproduct))))))) + ge_balance_positive_transitive_firstproductoutputreal))) /\ (exists ge_balance_positive_transitive_firstproductoutputimaginary ge_balance_negative_transitive_firstproductoutputimaginary. (((((ge_representation_imaginary_code_transitive_firstproductoutput) = 2 * (ge_balance_positive_transitive_firstproductoutputimaginary) /\ (ge_balance_negative_transitive_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_transitive_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_transitive_firstproductoutput) = 2 * ge_signed_half_transitive_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_transitive_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_transitive_firstproductoutputimaginary) = S ge_signed_half_transitive_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_transitive_firstproduct) * (ge_second_ip_transitive_firstproduct))) + (((ge_first_rn_transitive_firstproduct) * (ge_second_in_transitive_firstproduct))))) + (((((ge_first_ip_transitive_firstproduct) * (ge_second_rp_transitive_firstproduct))) + (((ge_first_in_transitive_firstproduct) * (ge_second_rn_transitive_firstproduct))))))) + ge_balance_negative_transitive_firstproductoutputimaginary = (((((((ge_first_rp_transitive_firstproduct) * (ge_second_in_transitive_firstproduct))) + (((ge_first_rn_transitive_firstproduct) * (ge_second_ip_transitive_firstproduct))))) + (((((ge_first_ip_transitive_firstproduct) * (ge_second_rn_transitive_firstproduct))) + (((ge_first_in_transitive_firstproduct) * (ge_second_rp_transitive_firstproduct))))))) + ge_balance_positive_transitive_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_transitive_second. (exists ge_first_rp_transitive_secondproduct ge_first_rn_transitive_secondproduct ge_first_ip_transitive_secondproduct ge_first_in_transitive_secondproduct ge_second_rp_transitive_secondproduct ge_second_rn_transitive_secondproduct ge_second_ip_transitive_secondproduct ge_second_in_transitive_secondproduct. ((exists ge_representation_real_code_transitive_secondproductfirst ge_representation_imaginary_code_transitive_secondproductfirst. (((a) = ((ge_representation_real_code_transitive_secondproductfirst) + (ge_representation_imaginary_code_transitive_secondproductfirst)) * S ((ge_representation_real_code_transitive_secondproductfirst) + (ge_representation_imaginary_code_transitive_secondproductfirst)) + ((ge_representation_imaginary_code_transitive_secondproductfirst) + (ge_representation_imaginary_code_transitive_secondproductfirst))) /\ ((exists ge_balance_positive_transitive_secondproductfirstreal ge_balance_negative_transitive_secondproductfirstreal. (((((ge_representation_real_code_transitive_secondproductfirst) = 2 * (ge_balance_positive_transitive_secondproductfirstreal) /\ (ge_balance_negative_transitive_secondproductfirstreal) = 0) \/ exists ge_signed_half_transitive_secondproductfirstrealdecode. (((ge_representation_real_code_transitive_secondproductfirst) = 2 * ge_signed_half_transitive_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_transitive_secondproductfirstreal) = 0) /\ (ge_balance_negative_transitive_secondproductfirstreal) = S ge_signed_half_transitive_secondproductfirstrealdecode))) /\ ((ge_first_rp_transitive_secondproduct) + ge_balance_negative_transitive_secondproductfirstreal = (ge_first_rn_transitive_secondproduct) + ge_balance_positive_transitive_secondproductfirstreal))) /\ (exists ge_balance_positive_transitive_secondproductfirstimaginary ge_balance_negative_transitive_secondproductfirstimaginary. (((((ge_representation_imaginary_code_transitive_secondproductfirst) = 2 * (ge_balance_positive_transitive_secondproductfirstimaginary) /\ (ge_balance_negative_transitive_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_transitive_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_transitive_secondproductfirst) = 2 * ge_signed_half_transitive_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_transitive_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_transitive_secondproductfirstimaginary) = S ge_signed_half_transitive_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_transitive_secondproduct) + ge_balance_negative_transitive_secondproductfirstimaginary = (ge_first_in_transitive_secondproduct) + ge_balance_positive_transitive_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_transitive_secondproductsecond ge_representation_imaginary_code_transitive_secondproductsecond. (((gr_quotient_transitive_second) = ((ge_representation_real_code_transitive_secondproductsecond) + (ge_representation_imaginary_code_transitive_secondproductsecond)) * S ((ge_representation_real_code_transitive_secondproductsecond) + (ge_representation_imaginary_code_transitive_secondproductsecond)) + ((ge_representation_imaginary_code_transitive_secondproductsecond) + (ge_representation_imaginary_code_transitive_secondproductsecond))) /\ ((exists ge_balance_positive_transitive_secondproductsecondreal ge_balance_negative_transitive_secondproductsecondreal. (((((ge_representation_real_code_transitive_secondproductsecond) = 2 * (ge_balance_positive_transitive_secondproductsecondreal) /\ (ge_balance_negative_transitive_secondproductsecondreal) = 0) \/ exists ge_signed_half_transitive_secondproductsecondrealdecode. (((ge_representation_real_code_transitive_secondproductsecond) = 2 * ge_signed_half_transitive_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_transitive_secondproductsecondreal) = 0) /\ (ge_balance_negative_transitive_secondproductsecondreal) = S ge_signed_half_transitive_secondproductsecondrealdecode))) /\ ((ge_second_rp_transitive_secondproduct) + ge_balance_negative_transitive_secondproductsecondreal = (ge_second_rn_transitive_secondproduct) + ge_balance_positive_transitive_secondproductsecondreal))) /\ (exists ge_balance_positive_transitive_secondproductsecondimaginary ge_balance_negative_transitive_secondproductsecondimaginary. (((((ge_representation_imaginary_code_transitive_secondproductsecond) = 2 * (ge_balance_positive_transitive_secondproductsecondimaginary) /\ (ge_balance_negative_transitive_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_transitive_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_transitive_secondproductsecond) = 2 * ge_signed_half_transitive_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_transitive_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_transitive_secondproductsecondimaginary) = S ge_signed_half_transitive_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_transitive_secondproduct) + ge_balance_negative_transitive_secondproductsecondimaginary = (ge_second_in_transitive_secondproduct) + ge_balance_positive_transitive_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_transitive_secondproductoutput ge_representation_imaginary_code_transitive_secondproductoutput. (((z) = ((ge_representation_real_code_transitive_secondproductoutput) + (ge_representation_imaginary_code_transitive_secondproductoutput)) * S ((ge_representation_real_code_transitive_secondproductoutput) + (ge_representation_imaginary_code_transitive_secondproductoutput)) + ((ge_representation_imaginary_code_transitive_secondproductoutput) + (ge_representation_imaginary_code_transitive_secondproductoutput))) /\ ((exists ge_balance_positive_transitive_secondproductoutputreal ge_balance_negative_transitive_secondproductoutputreal. (((((ge_representation_real_code_transitive_secondproductoutput) = 2 * (ge_balance_positive_transitive_secondproductoutputreal) /\ (ge_balance_negative_transitive_secondproductoutputreal) = 0) \/ exists ge_signed_half_transitive_secondproductoutputrealdecode. (((ge_representation_real_code_transitive_secondproductoutput) = 2 * ge_signed_half_transitive_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_transitive_secondproductoutputreal) = 0) /\ (ge_balance_negative_transitive_secondproductoutputreal) = S ge_signed_half_transitive_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_transitive_secondproduct) * (ge_second_rp_transitive_secondproduct))) + (((ge_first_rn_transitive_secondproduct) * (ge_second_rn_transitive_secondproduct))))) + (((((ge_first_ip_transitive_secondproduct) * (ge_second_in_transitive_secondproduct))) + (((ge_first_in_transitive_secondproduct) * (ge_second_ip_transitive_secondproduct))))))) + ge_balance_negative_transitive_secondproductoutputreal = (((((((ge_first_rp_transitive_secondproduct) * (ge_second_rn_transitive_secondproduct))) + (((ge_first_rn_transitive_secondproduct) * (ge_second_rp_transitive_secondproduct))))) + (((((ge_first_ip_transitive_secondproduct) * (ge_second_ip_transitive_secondproduct))) + (((ge_first_in_transitive_secondproduct) * (ge_second_in_transitive_secondproduct))))))) + ge_balance_positive_transitive_secondproductoutputreal))) /\ (exists ge_balance_positive_transitive_secondproductoutputimaginary ge_balance_negative_transitive_secondproductoutputimaginary. (((((ge_representation_imaginary_code_transitive_secondproductoutput) = 2 * (ge_balance_positive_transitive_secondproductoutputimaginary) /\ (ge_balance_negative_transitive_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_transitive_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_transitive_secondproductoutput) = 2 * ge_signed_half_transitive_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_transitive_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_transitive_secondproductoutputimaginary) = S ge_signed_half_transitive_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_transitive_secondproduct) * (ge_second_ip_transitive_secondproduct))) + (((ge_first_rn_transitive_secondproduct) * (ge_second_in_transitive_secondproduct))))) + (((((ge_first_ip_transitive_secondproduct) * (ge_second_rp_transitive_secondproduct))) + (((ge_first_in_transitive_secondproduct) * (ge_second_rn_transitive_secondproduct))))))) + ge_balance_negative_transitive_secondproductoutputimaginary = (((((((ge_first_rp_transitive_secondproduct) * (ge_second_in_transitive_secondproduct))) + (((ge_first_rn_transitive_secondproduct) * (ge_second_ip_transitive_secondproduct))))) + (((((ge_first_ip_transitive_secondproduct) * (ge_second_rn_transitive_secondproduct))) + (((ge_first_in_transitive_secondproduct) * (ge_second_rp_transitive_secondproduct))))))) + ge_balance_positive_transitive_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_transitive_result. (exists ge_first_rp_transitive_resultproduct ge_first_rn_transitive_resultproduct ge_first_ip_transitive_resultproduct ge_first_in_transitive_resultproduct ge_second_rp_transitive_resultproduct ge_second_rn_transitive_resultproduct ge_second_ip_transitive_resultproduct ge_second_in_transitive_resultproduct. ((exists ge_representation_real_code_transitive_resultproductfirst ge_representation_imaginary_code_transitive_resultproductfirst. (((d) = ((ge_representation_real_code_transitive_resultproductfirst) + (ge_representation_imaginary_code_transitive_resultproductfirst)) * S ((ge_representation_real_code_transitive_resultproductfirst) + (ge_representation_imaginary_code_transitive_resultproductfirst)) + ((ge_representation_imaginary_code_transitive_resultproductfirst) + (ge_representation_imaginary_code_transitive_resultproductfirst))) /\ ((exists ge_balance_positive_transitive_resultproductfirstreal ge_balance_negative_transitive_resultproductfirstreal. (((((ge_representation_real_code_transitive_resultproductfirst) = 2 * (ge_balance_positive_transitive_resultproductfirstreal) /\ (ge_balance_negative_transitive_resultproductfirstreal) = 0) \/ exists ge_signed_half_transitive_resultproductfirstrealdecode. (((ge_representation_real_code_transitive_resultproductfirst) = 2 * ge_signed_half_transitive_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_transitive_resultproductfirstreal) = 0) /\ (ge_balance_negative_transitive_resultproductfirstreal) = S ge_signed_half_transitive_resultproductfirstrealdecode))) /\ ((ge_first_rp_transitive_resultproduct) + ge_balance_negative_transitive_resultproductfirstreal = (ge_first_rn_transitive_resultproduct) + ge_balance_positive_transitive_resultproductfirstreal))) /\ (exists ge_balance_positive_transitive_resultproductfirstimaginary ge_balance_negative_transitive_resultproductfirstimaginary. (((((ge_representation_imaginary_code_transitive_resultproductfirst) = 2 * (ge_balance_positive_transitive_resultproductfirstimaginary) /\ (ge_balance_negative_transitive_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_transitive_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_transitive_resultproductfirst) = 2 * ge_signed_half_transitive_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_transitive_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_transitive_resultproductfirstimaginary) = S ge_signed_half_transitive_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_transitive_resultproduct) + ge_balance_negative_transitive_resultproductfirstimaginary = (ge_first_in_transitive_resultproduct) + ge_balance_positive_transitive_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_transitive_resultproductsecond ge_representation_imaginary_code_transitive_resultproductsecond. (((gr_quotient_transitive_result) = ((ge_representation_real_code_transitive_resultproductsecond) + (ge_representation_imaginary_code_transitive_resultproductsecond)) * S ((ge_representation_real_code_transitive_resultproductsecond) + (ge_representation_imaginary_code_transitive_resultproductsecond)) + ((ge_representation_imaginary_code_transitive_resultproductsecond) + (ge_representation_imaginary_code_transitive_resultproductsecond))) /\ ((exists ge_balance_positive_transitive_resultproductsecondreal ge_balance_negative_transitive_resultproductsecondreal. (((((ge_representation_real_code_transitive_resultproductsecond) = 2 * (ge_balance_positive_transitive_resultproductsecondreal) /\ (ge_balance_negative_transitive_resultproductsecondreal) = 0) \/ exists ge_signed_half_transitive_resultproductsecondrealdecode. (((ge_representation_real_code_transitive_resultproductsecond) = 2 * ge_signed_half_transitive_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_transitive_resultproductsecondreal) = 0) /\ (ge_balance_negative_transitive_resultproductsecondreal) = S ge_signed_half_transitive_resultproductsecondrealdecode))) /\ ((ge_second_rp_transitive_resultproduct) + ge_balance_negative_transitive_resultproductsecondreal = (ge_second_rn_transitive_resultproduct) + ge_balance_positive_transitive_resultproductsecondreal))) /\ (exists ge_balance_positive_transitive_resultproductsecondimaginary ge_balance_negative_transitive_resultproductsecondimaginary. (((((ge_representation_imaginary_code_transitive_resultproductsecond) = 2 * (ge_balance_positive_transitive_resultproductsecondimaginary) /\ (ge_balance_negative_transitive_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_transitive_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_transitive_resultproductsecond) = 2 * ge_signed_half_transitive_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_transitive_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_transitive_resultproductsecondimaginary) = S ge_signed_half_transitive_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_transitive_resultproduct) + ge_balance_negative_transitive_resultproductsecondimaginary = (ge_second_in_transitive_resultproduct) + ge_balance_positive_transitive_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_transitive_resultproductoutput ge_representation_imaginary_code_transitive_resultproductoutput. (((z) = ((ge_representation_real_code_transitive_resultproductoutput) + (ge_representation_imaginary_code_transitive_resultproductoutput)) * S ((ge_representation_real_code_transitive_resultproductoutput) + (ge_representation_imaginary_code_transitive_resultproductoutput)) + ((ge_representation_imaginary_code_transitive_resultproductoutput) + (ge_representation_imaginary_code_transitive_resultproductoutput))) /\ ((exists ge_balance_positive_transitive_resultproductoutputreal ge_balance_negative_transitive_resultproductoutputreal. (((((ge_representation_real_code_transitive_resultproductoutput) = 2 * (ge_balance_positive_transitive_resultproductoutputreal) /\ (ge_balance_negative_transitive_resultproductoutputreal) = 0) \/ exists ge_signed_half_transitive_resultproductoutputrealdecode. (((ge_representation_real_code_transitive_resultproductoutput) = 2 * ge_signed_half_transitive_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_transitive_resultproductoutputreal) = 0) /\ (ge_balance_negative_transitive_resultproductoutputreal) = S ge_signed_half_transitive_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_transitive_resultproduct) * (ge_second_rp_transitive_resultproduct))) + (((ge_first_rn_transitive_resultproduct) * (ge_second_rn_transitive_resultproduct))))) + (((((ge_first_ip_transitive_resultproduct) * (ge_second_in_transitive_resultproduct))) + (((ge_first_in_transitive_resultproduct) * (ge_second_ip_transitive_resultproduct))))))) + ge_balance_negative_transitive_resultproductoutputreal = (((((((ge_first_rp_transitive_resultproduct) * (ge_second_rn_transitive_resultproduct))) + (((ge_first_rn_transitive_resultproduct) * (ge_second_rp_transitive_resultproduct))))) + (((((ge_first_ip_transitive_resultproduct) * (ge_second_ip_transitive_resultproduct))) + (((ge_first_in_transitive_resultproduct) * (ge_second_in_transitive_resultproduct))))))) + ge_balance_positive_transitive_resultproductoutputreal))) /\ (exists ge_balance_positive_transitive_resultproductoutputimaginary ge_balance_negative_transitive_resultproductoutputimaginary. (((((ge_representation_imaginary_code_transitive_resultproductoutput) = 2 * (ge_balance_positive_transitive_resultproductoutputimaginary) /\ (ge_balance_negative_transitive_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_transitive_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_transitive_resultproductoutput) = 2 * ge_signed_half_transitive_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_transitive_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_transitive_resultproductoutputimaginary) = S ge_signed_half_transitive_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_transitive_resultproduct) * (ge_second_ip_transitive_resultproduct))) + (((ge_first_rn_transitive_resultproduct) * (ge_second_in_transitive_resultproduct))))) + (((((ge_first_ip_transitive_resultproduct) * (ge_second_rp_transitive_resultproduct))) + (((ge_first_in_transitive_resultproduct) * (ge_second_rn_transitive_resultproduct))))))) + ge_balance_negative_transitive_resultproductoutputimaginary = (((((((ge_first_rp_transitive_resultproduct) * (ge_second_in_transitive_resultproduct))) + (((ge_first_rn_transitive_resultproduct) * (ge_second_ip_transitive_resultproduct))))) + (((((ge_first_ip_transitive_resultproduct) * (ge_second_rn_transitive_resultproduct))) + (((ge_first_in_transitive_resultproduct) * (ge_second_rp_transitive_resultproduct))))))) + ge_balance_positive_transitive_resultproductoutputimaginary))))))))))