gaussian_common_divisor_euclidean_backward

Exact expanded first-order arithmetic statement

forall d a b q r. (exists ge_division_product_euclid_backward_equation. ((exists ge_first_rp_euclid_backward_equationproduct ge_first_rn_euclid_backward_equationproduct ge_first_ip_euclid_backward_equationproduct ge_first_in_euclid_backward_equationproduct ge_second_rp_euclid_backward_equationproduct ge_second_rn_euclid_backward_equationproduct ge_second_ip_euclid_backward_equationproduct ge_second_in_euclid_backward_equationproduct. ((exists ge_representation_real_code_euclid_backward_equationproductfirst ge_representation_imaginary_code_euclid_backward_equationproductfirst. (((b) = ((ge_representation_real_code_euclid_backward_equationproductfirst) + (ge_representation_imaginary_code_euclid_backward_equationproductfirst)) * S ((ge_representation_real_code_euclid_backward_equationproductfirst) + (ge_representation_imaginary_code_euclid_backward_equationproductfirst)) + ((ge_representation_imaginary_code_euclid_backward_equationproductfirst) + (ge_representation_imaginary_code_euclid_backward_equationproductfirst))) /\ ((exists ge_balance_positive_euclid_backward_equationproductfirstreal ge_balance_negative_euclid_backward_equationproductfirstreal. (((((ge_representation_real_code_euclid_backward_equationproductfirst) = 2 * (ge_balance_positive_euclid_backward_equationproductfirstreal) /\ (ge_balance_negative_euclid_backward_equationproductfirstreal) = 0) \/ exists ge_signed_half_euclid_backward_equationproductfirstrealdecode. (((ge_representation_real_code_euclid_backward_equationproductfirst) = 2 * ge_signed_half_euclid_backward_equationproductfirstrealdecode + 1 /\ (ge_balance_positive_euclid_backward_equationproductfirstreal) = 0) /\ (ge_balance_negative_euclid_backward_equationproductfirstreal) = S ge_signed_half_euclid_backward_equationproductfirstrealdecode))) /\ ((ge_first_rp_euclid_backward_equationproduct) + ge_balance_negative_euclid_backward_equationproductfirstreal = (ge_first_rn_euclid_backward_equationproduct) + ge_balance_positive_euclid_backward_equationproductfirstreal))) /\ (exists ge_balance_positive_euclid_backward_equationproductfirstimaginary ge_balance_negative_euclid_backward_equationproductfirstimaginary. (((((ge_representation_imaginary_code_euclid_backward_equationproductfirst) = 2 * (ge_balance_positive_euclid_backward_equationproductfirstimaginary) /\ (ge_balance_negative_euclid_backward_equationproductfirstimaginary) = 0) \/ exists ge_signed_half_euclid_backward_equationproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_equationproductfirst) = 2 * ge_signed_half_euclid_backward_equationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_equationproductfirstimaginary) = 0) /\ (ge_balance_negative_euclid_backward_equationproductfirstimaginary) = S ge_signed_half_euclid_backward_equationproductfirstimaginarydecode))) /\ ((ge_first_ip_euclid_backward_equationproduct) + ge_balance_negative_euclid_backward_equationproductfirstimaginary = (ge_first_in_euclid_backward_equationproduct) + ge_balance_positive_euclid_backward_equationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_backward_equationproductsecond ge_representation_imaginary_code_euclid_backward_equationproductsecond. (((q) = ((ge_representation_real_code_euclid_backward_equationproductsecond) + (ge_representation_imaginary_code_euclid_backward_equationproductsecond)) * S ((ge_representation_real_code_euclid_backward_equationproductsecond) + (ge_representation_imaginary_code_euclid_backward_equationproductsecond)) + ((ge_representation_imaginary_code_euclid_backward_equationproductsecond) + (ge_representation_imaginary_code_euclid_backward_equationproductsecond))) /\ ((exists ge_balance_positive_euclid_backward_equationproductsecondreal ge_balance_negative_euclid_backward_equationproductsecondreal. (((((ge_representation_real_code_euclid_backward_equationproductsecond) = 2 * (ge_balance_positive_euclid_backward_equationproductsecondreal) /\ (ge_balance_negative_euclid_backward_equationproductsecondreal) = 0) \/ exists ge_signed_half_euclid_backward_equationproductsecondrealdecode. (((ge_representation_real_code_euclid_backward_equationproductsecond) = 2 * ge_signed_half_euclid_backward_equationproductsecondrealdecode + 1 /\ (ge_balance_positive_euclid_backward_equationproductsecondreal) = 0) /\ (ge_balance_negative_euclid_backward_equationproductsecondreal) = S ge_signed_half_euclid_backward_equationproductsecondrealdecode))) /\ ((ge_second_rp_euclid_backward_equationproduct) + ge_balance_negative_euclid_backward_equationproductsecondreal = (ge_second_rn_euclid_backward_equationproduct) + ge_balance_positive_euclid_backward_equationproductsecondreal))) /\ (exists ge_balance_positive_euclid_backward_equationproductsecondimaginary ge_balance_negative_euclid_backward_equationproductsecondimaginary. (((((ge_representation_imaginary_code_euclid_backward_equationproductsecond) = 2 * (ge_balance_positive_euclid_backward_equationproductsecondimaginary) /\ (ge_balance_negative_euclid_backward_equationproductsecondimaginary) = 0) \/ exists ge_signed_half_euclid_backward_equationproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_equationproductsecond) = 2 * ge_signed_half_euclid_backward_equationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_equationproductsecondimaginary) = 0) /\ (ge_balance_negative_euclid_backward_equationproductsecondimaginary) = S ge_signed_half_euclid_backward_equationproductsecondimaginarydecode))) /\ ((ge_second_ip_euclid_backward_equationproduct) + ge_balance_negative_euclid_backward_equationproductsecondimaginary = (ge_second_in_euclid_backward_equationproduct) + ge_balance_positive_euclid_backward_equationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_backward_equationproductoutput ge_representation_imaginary_code_euclid_backward_equationproductoutput. (((ge_division_product_euclid_backward_equation) = ((ge_representation_real_code_euclid_backward_equationproductoutput) + (ge_representation_imaginary_code_euclid_backward_equationproductoutput)) * S ((ge_representation_real_code_euclid_backward_equationproductoutput) + (ge_representation_imaginary_code_euclid_backward_equationproductoutput)) + ((ge_representation_imaginary_code_euclid_backward_equationproductoutput) + (ge_representation_imaginary_code_euclid_backward_equationproductoutput))) /\ ((exists ge_balance_positive_euclid_backward_equationproductoutputreal ge_balance_negative_euclid_backward_equationproductoutputreal. (((((ge_representation_real_code_euclid_backward_equationproductoutput) = 2 * (ge_balance_positive_euclid_backward_equationproductoutputreal) /\ (ge_balance_negative_euclid_backward_equationproductoutputreal) = 0) \/ exists ge_signed_half_euclid_backward_equationproductoutputrealdecode. (((ge_representation_real_code_euclid_backward_equationproductoutput) = 2 * ge_signed_half_euclid_backward_equationproductoutputrealdecode + 1 /\ (ge_balance_positive_euclid_backward_equationproductoutputreal) = 0) /\ (ge_balance_negative_euclid_backward_equationproductoutputreal) = S ge_signed_half_euclid_backward_equationproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclid_backward_equationproduct) * (ge_second_rp_euclid_backward_equationproduct))) + (((ge_first_rn_euclid_backward_equationproduct) * (ge_second_rn_euclid_backward_equationproduct))))) + (((((ge_first_ip_euclid_backward_equationproduct) * (ge_second_in_euclid_backward_equationproduct))) + (((ge_first_in_euclid_backward_equationproduct) * (ge_second_ip_euclid_backward_equationproduct))))))) + ge_balance_negative_euclid_backward_equationproductoutputreal = (((((((ge_first_rp_euclid_backward_equationproduct) * (ge_second_rn_euclid_backward_equationproduct))) + (((ge_first_rn_euclid_backward_equationproduct) * (ge_second_rp_euclid_backward_equationproduct))))) + (((((ge_first_ip_euclid_backward_equationproduct) * (ge_second_ip_euclid_backward_equationproduct))) + (((ge_first_in_euclid_backward_equationproduct) * (ge_second_in_euclid_backward_equationproduct))))))) + ge_balance_positive_euclid_backward_equationproductoutputreal))) /\ (exists ge_balance_positive_euclid_backward_equationproductoutputimaginary ge_balance_negative_euclid_backward_equationproductoutputimaginary. (((((ge_representation_imaginary_code_euclid_backward_equationproductoutput) = 2 * (ge_balance_positive_euclid_backward_equationproductoutputimaginary) /\ (ge_balance_negative_euclid_backward_equationproductoutputimaginary) = 0) \/ exists ge_signed_half_euclid_backward_equationproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_equationproductoutput) = 2 * ge_signed_half_euclid_backward_equationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_equationproductoutputimaginary) = 0) /\ (ge_balance_negative_euclid_backward_equationproductoutputimaginary) = S ge_signed_half_euclid_backward_equationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclid_backward_equationproduct) * (ge_second_ip_euclid_backward_equationproduct))) + (((ge_first_rn_euclid_backward_equationproduct) * (ge_second_in_euclid_backward_equationproduct))))) + (((((ge_first_ip_euclid_backward_equationproduct) * (ge_second_rp_euclid_backward_equationproduct))) + (((ge_first_in_euclid_backward_equationproduct) * (ge_second_rn_euclid_backward_equationproduct))))))) + ge_balance_negative_euclid_backward_equationproductoutputimaginary = (((((((ge_first_rp_euclid_backward_equationproduct) * (ge_second_in_euclid_backward_equationproduct))) + (((ge_first_rn_euclid_backward_equationproduct) * (ge_second_ip_euclid_backward_equationproduct))))) + (((((ge_first_ip_euclid_backward_equationproduct) * (ge_second_rn_euclid_backward_equationproduct))) + (((ge_first_in_euclid_backward_equationproduct) * (ge_second_rp_euclid_backward_equationproduct))))))) + ge_balance_positive_euclid_backward_equationproductoutputimaginary))))))))) /\ (exists ge_first_rp_euclid_backward_equationsum ge_first_rn_euclid_backward_equationsum ge_first_ip_euclid_backward_equationsum ge_first_in_euclid_backward_equationsum ge_second_rp_euclid_backward_equationsum ge_second_rn_euclid_backward_equationsum ge_second_ip_euclid_backward_equationsum ge_second_in_euclid_backward_equationsum. ((exists ge_representation_real_code_euclid_backward_equationsumfirst ge_representation_imaginary_code_euclid_backward_equationsumfirst. (((ge_division_product_euclid_backward_equation) = ((ge_representation_real_code_euclid_backward_equationsumfirst) + (ge_representation_imaginary_code_euclid_backward_equationsumfirst)) * S ((ge_representation_real_code_euclid_backward_equationsumfirst) + (ge_representation_imaginary_code_euclid_backward_equationsumfirst)) + ((ge_representation_imaginary_code_euclid_backward_equationsumfirst) + (ge_representation_imaginary_code_euclid_backward_equationsumfirst))) /\ ((exists ge_balance_positive_euclid_backward_equationsumfirstreal ge_balance_negative_euclid_backward_equationsumfirstreal. (((((ge_representation_real_code_euclid_backward_equationsumfirst) = 2 * (ge_balance_positive_euclid_backward_equationsumfirstreal) /\ (ge_balance_negative_euclid_backward_equationsumfirstreal) = 0) \/ exists ge_signed_half_euclid_backward_equationsumfirstrealdecode. (((ge_representation_real_code_euclid_backward_equationsumfirst) = 2 * ge_signed_half_euclid_backward_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_euclid_backward_equationsumfirstreal) = 0) /\ (ge_balance_negative_euclid_backward_equationsumfirstreal) = S ge_signed_half_euclid_backward_equationsumfirstrealdecode))) /\ ((ge_first_rp_euclid_backward_equationsum) + ge_balance_negative_euclid_backward_equationsumfirstreal = (ge_first_rn_euclid_backward_equationsum) + ge_balance_positive_euclid_backward_equationsumfirstreal))) /\ (exists ge_balance_positive_euclid_backward_equationsumfirstimaginary ge_balance_negative_euclid_backward_equationsumfirstimaginary. (((((ge_representation_imaginary_code_euclid_backward_equationsumfirst) = 2 * (ge_balance_positive_euclid_backward_equationsumfirstimaginary) /\ (ge_balance_negative_euclid_backward_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_euclid_backward_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_equationsumfirst) = 2 * ge_signed_half_euclid_backward_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_euclid_backward_equationsumfirstimaginary) = S ge_signed_half_euclid_backward_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_euclid_backward_equationsum) + ge_balance_negative_euclid_backward_equationsumfirstimaginary = (ge_first_in_euclid_backward_equationsum) + ge_balance_positive_euclid_backward_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_backward_equationsumsecond ge_representation_imaginary_code_euclid_backward_equationsumsecond. (((r) = ((ge_representation_real_code_euclid_backward_equationsumsecond) + (ge_representation_imaginary_code_euclid_backward_equationsumsecond)) * S ((ge_representation_real_code_euclid_backward_equationsumsecond) + (ge_representation_imaginary_code_euclid_backward_equationsumsecond)) + ((ge_representation_imaginary_code_euclid_backward_equationsumsecond) + (ge_representation_imaginary_code_euclid_backward_equationsumsecond))) /\ ((exists ge_balance_positive_euclid_backward_equationsumsecondreal ge_balance_negative_euclid_backward_equationsumsecondreal. (((((ge_representation_real_code_euclid_backward_equationsumsecond) = 2 * (ge_balance_positive_euclid_backward_equationsumsecondreal) /\ (ge_balance_negative_euclid_backward_equationsumsecondreal) = 0) \/ exists ge_signed_half_euclid_backward_equationsumsecondrealdecode. (((ge_representation_real_code_euclid_backward_equationsumsecond) = 2 * ge_signed_half_euclid_backward_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_euclid_backward_equationsumsecondreal) = 0) /\ (ge_balance_negative_euclid_backward_equationsumsecondreal) = S ge_signed_half_euclid_backward_equationsumsecondrealdecode))) /\ ((ge_second_rp_euclid_backward_equationsum) + ge_balance_negative_euclid_backward_equationsumsecondreal = (ge_second_rn_euclid_backward_equationsum) + ge_balance_positive_euclid_backward_equationsumsecondreal))) /\ (exists ge_balance_positive_euclid_backward_equationsumsecondimaginary ge_balance_negative_euclid_backward_equationsumsecondimaginary. (((((ge_representation_imaginary_code_euclid_backward_equationsumsecond) = 2 * (ge_balance_positive_euclid_backward_equationsumsecondimaginary) /\ (ge_balance_negative_euclid_backward_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_euclid_backward_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_equationsumsecond) = 2 * ge_signed_half_euclid_backward_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_euclid_backward_equationsumsecondimaginary) = S ge_signed_half_euclid_backward_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_euclid_backward_equationsum) + ge_balance_negative_euclid_backward_equationsumsecondimaginary = (ge_second_in_euclid_backward_equationsum) + ge_balance_positive_euclid_backward_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_backward_equationsumoutput ge_representation_imaginary_code_euclid_backward_equationsumoutput. (((a) = ((ge_representation_real_code_euclid_backward_equationsumoutput) + (ge_representation_imaginary_code_euclid_backward_equationsumoutput)) * S ((ge_representation_real_code_euclid_backward_equationsumoutput) + (ge_representation_imaginary_code_euclid_backward_equationsumoutput)) + ((ge_representation_imaginary_code_euclid_backward_equationsumoutput) + (ge_representation_imaginary_code_euclid_backward_equationsumoutput))) /\ ((exists ge_balance_positive_euclid_backward_equationsumoutputreal ge_balance_negative_euclid_backward_equationsumoutputreal. (((((ge_representation_real_code_euclid_backward_equationsumoutput) = 2 * (ge_balance_positive_euclid_backward_equationsumoutputreal) /\ (ge_balance_negative_euclid_backward_equationsumoutputreal) = 0) \/ exists ge_signed_half_euclid_backward_equationsumoutputrealdecode. (((ge_representation_real_code_euclid_backward_equationsumoutput) = 2 * ge_signed_half_euclid_backward_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_euclid_backward_equationsumoutputreal) = 0) /\ (ge_balance_negative_euclid_backward_equationsumoutputreal) = S ge_signed_half_euclid_backward_equationsumoutputrealdecode))) /\ ((((ge_first_rp_euclid_backward_equationsum) + (ge_second_rp_euclid_backward_equationsum))) + ge_balance_negative_euclid_backward_equationsumoutputreal = (((ge_first_rn_euclid_backward_equationsum) + (ge_second_rn_euclid_backward_equationsum))) + ge_balance_positive_euclid_backward_equationsumoutputreal))) /\ (exists ge_balance_positive_euclid_backward_equationsumoutputimaginary ge_balance_negative_euclid_backward_equationsumoutputimaginary. (((((ge_representation_imaginary_code_euclid_backward_equationsumoutput) = 2 * (ge_balance_positive_euclid_backward_equationsumoutputimaginary) /\ (ge_balance_negative_euclid_backward_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_euclid_backward_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_equationsumoutput) = 2 * ge_signed_half_euclid_backward_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_euclid_backward_equationsumoutputimaginary) = S ge_signed_half_euclid_backward_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_euclid_backward_equationsum) + (ge_second_ip_euclid_backward_equationsum))) + ge_balance_negative_euclid_backward_equationsumoutputimaginary = (((ge_first_in_euclid_backward_equationsum) + (ge_second_in_euclid_backward_equationsum))) + ge_balance_positive_euclid_backward_equationsumoutputimaginary))))))))))) -> (exists gr_quotient_euclid_backward_dividend. (exists ge_first_rp_euclid_backward_dividendproduct ge_first_rn_euclid_backward_dividendproduct ge_first_ip_euclid_backward_dividendproduct ge_first_in_euclid_backward_dividendproduct ge_second_rp_euclid_backward_dividendproduct ge_second_rn_euclid_backward_dividendproduct ge_second_ip_euclid_backward_dividendproduct ge_second_in_euclid_backward_dividendproduct. ((exists ge_representation_real_code_euclid_backward_dividendproductfirst ge_representation_imaginary_code_euclid_backward_dividendproductfirst. (((d) = ((ge_representation_real_code_euclid_backward_dividendproductfirst) + (ge_representation_imaginary_code_euclid_backward_dividendproductfirst)) * S ((ge_representation_real_code_euclid_backward_dividendproductfirst) + (ge_representation_imaginary_code_euclid_backward_dividendproductfirst)) + ((ge_representation_imaginary_code_euclid_backward_dividendproductfirst) + (ge_representation_imaginary_code_euclid_backward_dividendproductfirst))) /\ ((exists ge_balance_positive_euclid_backward_dividendproductfirstreal ge_balance_negative_euclid_backward_dividendproductfirstreal. (((((ge_representation_real_code_euclid_backward_dividendproductfirst) = 2 * (ge_balance_positive_euclid_backward_dividendproductfirstreal) /\ (ge_balance_negative_euclid_backward_dividendproductfirstreal) = 0) \/ exists ge_signed_half_euclid_backward_dividendproductfirstrealdecode. (((ge_representation_real_code_euclid_backward_dividendproductfirst) = 2 * ge_signed_half_euclid_backward_dividendproductfirstrealdecode + 1 /\ (ge_balance_positive_euclid_backward_dividendproductfirstreal) = 0) /\ (ge_balance_negative_euclid_backward_dividendproductfirstreal) = S ge_signed_half_euclid_backward_dividendproductfirstrealdecode))) /\ ((ge_first_rp_euclid_backward_dividendproduct) + ge_balance_negative_euclid_backward_dividendproductfirstreal = (ge_first_rn_euclid_backward_dividendproduct) + ge_balance_positive_euclid_backward_dividendproductfirstreal))) /\ (exists ge_balance_positive_euclid_backward_dividendproductfirstimaginary ge_balance_negative_euclid_backward_dividendproductfirstimaginary. (((((ge_representation_imaginary_code_euclid_backward_dividendproductfirst) = 2 * (ge_balance_positive_euclid_backward_dividendproductfirstimaginary) /\ (ge_balance_negative_euclid_backward_dividendproductfirstimaginary) = 0) \/ exists ge_signed_half_euclid_backward_dividendproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_dividendproductfirst) = 2 * ge_signed_half_euclid_backward_dividendproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_dividendproductfirstimaginary) = 0) /\ (ge_balance_negative_euclid_backward_dividendproductfirstimaginary) = S ge_signed_half_euclid_backward_dividendproductfirstimaginarydecode))) /\ ((ge_first_ip_euclid_backward_dividendproduct) + ge_balance_negative_euclid_backward_dividendproductfirstimaginary = (ge_first_in_euclid_backward_dividendproduct) + ge_balance_positive_euclid_backward_dividendproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_backward_dividendproductsecond ge_representation_imaginary_code_euclid_backward_dividendproductsecond. (((gr_quotient_euclid_backward_dividend) = ((ge_representation_real_code_euclid_backward_dividendproductsecond) + (ge_representation_imaginary_code_euclid_backward_dividendproductsecond)) * S ((ge_representation_real_code_euclid_backward_dividendproductsecond) + (ge_representation_imaginary_code_euclid_backward_dividendproductsecond)) + ((ge_representation_imaginary_code_euclid_backward_dividendproductsecond) + (ge_representation_imaginary_code_euclid_backward_dividendproductsecond))) /\ ((exists ge_balance_positive_euclid_backward_dividendproductsecondreal ge_balance_negative_euclid_backward_dividendproductsecondreal. (((((ge_representation_real_code_euclid_backward_dividendproductsecond) = 2 * (ge_balance_positive_euclid_backward_dividendproductsecondreal) /\ (ge_balance_negative_euclid_backward_dividendproductsecondreal) = 0) \/ exists ge_signed_half_euclid_backward_dividendproductsecondrealdecode. (((ge_representation_real_code_euclid_backward_dividendproductsecond) = 2 * ge_signed_half_euclid_backward_dividendproductsecondrealdecode + 1 /\ (ge_balance_positive_euclid_backward_dividendproductsecondreal) = 0) /\ (ge_balance_negative_euclid_backward_dividendproductsecondreal) = S ge_signed_half_euclid_backward_dividendproductsecondrealdecode))) /\ ((ge_second_rp_euclid_backward_dividendproduct) + ge_balance_negative_euclid_backward_dividendproductsecondreal = (ge_second_rn_euclid_backward_dividendproduct) + ge_balance_positive_euclid_backward_dividendproductsecondreal))) /\ (exists ge_balance_positive_euclid_backward_dividendproductsecondimaginary ge_balance_negative_euclid_backward_dividendproductsecondimaginary. (((((ge_representation_imaginary_code_euclid_backward_dividendproductsecond) = 2 * (ge_balance_positive_euclid_backward_dividendproductsecondimaginary) /\ (ge_balance_negative_euclid_backward_dividendproductsecondimaginary) = 0) \/ exists ge_signed_half_euclid_backward_dividendproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_dividendproductsecond) = 2 * ge_signed_half_euclid_backward_dividendproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_dividendproductsecondimaginary) = 0) /\ (ge_balance_negative_euclid_backward_dividendproductsecondimaginary) = S ge_signed_half_euclid_backward_dividendproductsecondimaginarydecode))) /\ ((ge_second_ip_euclid_backward_dividendproduct) + ge_balance_negative_euclid_backward_dividendproductsecondimaginary = (ge_second_in_euclid_backward_dividendproduct) + ge_balance_positive_euclid_backward_dividendproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_backward_dividendproductoutput ge_representation_imaginary_code_euclid_backward_dividendproductoutput. (((a) = ((ge_representation_real_code_euclid_backward_dividendproductoutput) + (ge_representation_imaginary_code_euclid_backward_dividendproductoutput)) * S ((ge_representation_real_code_euclid_backward_dividendproductoutput) + (ge_representation_imaginary_code_euclid_backward_dividendproductoutput)) + ((ge_representation_imaginary_code_euclid_backward_dividendproductoutput) + (ge_representation_imaginary_code_euclid_backward_dividendproductoutput))) /\ ((exists ge_balance_positive_euclid_backward_dividendproductoutputreal ge_balance_negative_euclid_backward_dividendproductoutputreal. (((((ge_representation_real_code_euclid_backward_dividendproductoutput) = 2 * (ge_balance_positive_euclid_backward_dividendproductoutputreal) /\ (ge_balance_negative_euclid_backward_dividendproductoutputreal) = 0) \/ exists ge_signed_half_euclid_backward_dividendproductoutputrealdecode. (((ge_representation_real_code_euclid_backward_dividendproductoutput) = 2 * ge_signed_half_euclid_backward_dividendproductoutputrealdecode + 1 /\ (ge_balance_positive_euclid_backward_dividendproductoutputreal) = 0) /\ (ge_balance_negative_euclid_backward_dividendproductoutputreal) = S ge_signed_half_euclid_backward_dividendproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclid_backward_dividendproduct) * (ge_second_rp_euclid_backward_dividendproduct))) + (((ge_first_rn_euclid_backward_dividendproduct) * (ge_second_rn_euclid_backward_dividendproduct))))) + (((((ge_first_ip_euclid_backward_dividendproduct) * (ge_second_in_euclid_backward_dividendproduct))) + (((ge_first_in_euclid_backward_dividendproduct) * (ge_second_ip_euclid_backward_dividendproduct))))))) + ge_balance_negative_euclid_backward_dividendproductoutputreal = (((((((ge_first_rp_euclid_backward_dividendproduct) * (ge_second_rn_euclid_backward_dividendproduct))) + (((ge_first_rn_euclid_backward_dividendproduct) * (ge_second_rp_euclid_backward_dividendproduct))))) + (((((ge_first_ip_euclid_backward_dividendproduct) * (ge_second_ip_euclid_backward_dividendproduct))) + (((ge_first_in_euclid_backward_dividendproduct) * (ge_second_in_euclid_backward_dividendproduct))))))) + ge_balance_positive_euclid_backward_dividendproductoutputreal))) /\ (exists ge_balance_positive_euclid_backward_dividendproductoutputimaginary ge_balance_negative_euclid_backward_dividendproductoutputimaginary. (((((ge_representation_imaginary_code_euclid_backward_dividendproductoutput) = 2 * (ge_balance_positive_euclid_backward_dividendproductoutputimaginary) /\ (ge_balance_negative_euclid_backward_dividendproductoutputimaginary) = 0) \/ exists ge_signed_half_euclid_backward_dividendproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_dividendproductoutput) = 2 * ge_signed_half_euclid_backward_dividendproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_dividendproductoutputimaginary) = 0) /\ (ge_balance_negative_euclid_backward_dividendproductoutputimaginary) = S ge_signed_half_euclid_backward_dividendproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclid_backward_dividendproduct) * (ge_second_ip_euclid_backward_dividendproduct))) + (((ge_first_rn_euclid_backward_dividendproduct) * (ge_second_in_euclid_backward_dividendproduct))))) + (((((ge_first_ip_euclid_backward_dividendproduct) * (ge_second_rp_euclid_backward_dividendproduct))) + (((ge_first_in_euclid_backward_dividendproduct) * (ge_second_rn_euclid_backward_dividendproduct))))))) + ge_balance_negative_euclid_backward_dividendproductoutputimaginary = (((((((ge_first_rp_euclid_backward_dividendproduct) * (ge_second_in_euclid_backward_dividendproduct))) + (((ge_first_rn_euclid_backward_dividendproduct) * (ge_second_ip_euclid_backward_dividendproduct))))) + (((((ge_first_ip_euclid_backward_dividendproduct) * (ge_second_rn_euclid_backward_dividendproduct))) + (((ge_first_in_euclid_backward_dividendproduct) * (ge_second_rp_euclid_backward_dividendproduct))))))) + ge_balance_positive_euclid_backward_dividendproductoutputimaginary)))))))))) -> (exists gr_quotient_euclid_backward_divisor. (exists ge_first_rp_euclid_backward_divisorproduct ge_first_rn_euclid_backward_divisorproduct ge_first_ip_euclid_backward_divisorproduct ge_first_in_euclid_backward_divisorproduct ge_second_rp_euclid_backward_divisorproduct ge_second_rn_euclid_backward_divisorproduct ge_second_ip_euclid_backward_divisorproduct ge_second_in_euclid_backward_divisorproduct. ((exists ge_representation_real_code_euclid_backward_divisorproductfirst ge_representation_imaginary_code_euclid_backward_divisorproductfirst. (((d) = ((ge_representation_real_code_euclid_backward_divisorproductfirst) + (ge_representation_imaginary_code_euclid_backward_divisorproductfirst)) * S ((ge_representation_real_code_euclid_backward_divisorproductfirst) + (ge_representation_imaginary_code_euclid_backward_divisorproductfirst)) + ((ge_representation_imaginary_code_euclid_backward_divisorproductfirst) + (ge_representation_imaginary_code_euclid_backward_divisorproductfirst))) /\ ((exists ge_balance_positive_euclid_backward_divisorproductfirstreal ge_balance_negative_euclid_backward_divisorproductfirstreal. (((((ge_representation_real_code_euclid_backward_divisorproductfirst) = 2 * (ge_balance_positive_euclid_backward_divisorproductfirstreal) /\ (ge_balance_negative_euclid_backward_divisorproductfirstreal) = 0) \/ exists ge_signed_half_euclid_backward_divisorproductfirstrealdecode. (((ge_representation_real_code_euclid_backward_divisorproductfirst) = 2 * ge_signed_half_euclid_backward_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_euclid_backward_divisorproductfirstreal) = 0) /\ (ge_balance_negative_euclid_backward_divisorproductfirstreal) = S ge_signed_half_euclid_backward_divisorproductfirstrealdecode))) /\ ((ge_first_rp_euclid_backward_divisorproduct) + ge_balance_negative_euclid_backward_divisorproductfirstreal = (ge_first_rn_euclid_backward_divisorproduct) + ge_balance_positive_euclid_backward_divisorproductfirstreal))) /\ (exists ge_balance_positive_euclid_backward_divisorproductfirstimaginary ge_balance_negative_euclid_backward_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_euclid_backward_divisorproductfirst) = 2 * (ge_balance_positive_euclid_backward_divisorproductfirstimaginary) /\ (ge_balance_negative_euclid_backward_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_euclid_backward_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_divisorproductfirst) = 2 * ge_signed_half_euclid_backward_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_euclid_backward_divisorproductfirstimaginary) = S ge_signed_half_euclid_backward_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_euclid_backward_divisorproduct) + ge_balance_negative_euclid_backward_divisorproductfirstimaginary = (ge_first_in_euclid_backward_divisorproduct) + ge_balance_positive_euclid_backward_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_backward_divisorproductsecond ge_representation_imaginary_code_euclid_backward_divisorproductsecond. (((gr_quotient_euclid_backward_divisor) = ((ge_representation_real_code_euclid_backward_divisorproductsecond) + (ge_representation_imaginary_code_euclid_backward_divisorproductsecond)) * S ((ge_representation_real_code_euclid_backward_divisorproductsecond) + (ge_representation_imaginary_code_euclid_backward_divisorproductsecond)) + ((ge_representation_imaginary_code_euclid_backward_divisorproductsecond) + (ge_representation_imaginary_code_euclid_backward_divisorproductsecond))) /\ ((exists ge_balance_positive_euclid_backward_divisorproductsecondreal ge_balance_negative_euclid_backward_divisorproductsecondreal. (((((ge_representation_real_code_euclid_backward_divisorproductsecond) = 2 * (ge_balance_positive_euclid_backward_divisorproductsecondreal) /\ (ge_balance_negative_euclid_backward_divisorproductsecondreal) = 0) \/ exists ge_signed_half_euclid_backward_divisorproductsecondrealdecode. (((ge_representation_real_code_euclid_backward_divisorproductsecond) = 2 * ge_signed_half_euclid_backward_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_euclid_backward_divisorproductsecondreal) = 0) /\ (ge_balance_negative_euclid_backward_divisorproductsecondreal) = S ge_signed_half_euclid_backward_divisorproductsecondrealdecode))) /\ ((ge_second_rp_euclid_backward_divisorproduct) + ge_balance_negative_euclid_backward_divisorproductsecondreal = (ge_second_rn_euclid_backward_divisorproduct) + ge_balance_positive_euclid_backward_divisorproductsecondreal))) /\ (exists ge_balance_positive_euclid_backward_divisorproductsecondimaginary ge_balance_negative_euclid_backward_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_euclid_backward_divisorproductsecond) = 2 * (ge_balance_positive_euclid_backward_divisorproductsecondimaginary) /\ (ge_balance_negative_euclid_backward_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_euclid_backward_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_divisorproductsecond) = 2 * ge_signed_half_euclid_backward_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_euclid_backward_divisorproductsecondimaginary) = S ge_signed_half_euclid_backward_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_euclid_backward_divisorproduct) + ge_balance_negative_euclid_backward_divisorproductsecondimaginary = (ge_second_in_euclid_backward_divisorproduct) + ge_balance_positive_euclid_backward_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_backward_divisorproductoutput ge_representation_imaginary_code_euclid_backward_divisorproductoutput. (((b) = ((ge_representation_real_code_euclid_backward_divisorproductoutput) + (ge_representation_imaginary_code_euclid_backward_divisorproductoutput)) * S ((ge_representation_real_code_euclid_backward_divisorproductoutput) + (ge_representation_imaginary_code_euclid_backward_divisorproductoutput)) + ((ge_representation_imaginary_code_euclid_backward_divisorproductoutput) + (ge_representation_imaginary_code_euclid_backward_divisorproductoutput))) /\ ((exists ge_balance_positive_euclid_backward_divisorproductoutputreal ge_balance_negative_euclid_backward_divisorproductoutputreal. (((((ge_representation_real_code_euclid_backward_divisorproductoutput) = 2 * (ge_balance_positive_euclid_backward_divisorproductoutputreal) /\ (ge_balance_negative_euclid_backward_divisorproductoutputreal) = 0) \/ exists ge_signed_half_euclid_backward_divisorproductoutputrealdecode. (((ge_representation_real_code_euclid_backward_divisorproductoutput) = 2 * ge_signed_half_euclid_backward_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_euclid_backward_divisorproductoutputreal) = 0) /\ (ge_balance_negative_euclid_backward_divisorproductoutputreal) = S ge_signed_half_euclid_backward_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclid_backward_divisorproduct) * (ge_second_rp_euclid_backward_divisorproduct))) + (((ge_first_rn_euclid_backward_divisorproduct) * (ge_second_rn_euclid_backward_divisorproduct))))) + (((((ge_first_ip_euclid_backward_divisorproduct) * (ge_second_in_euclid_backward_divisorproduct))) + (((ge_first_in_euclid_backward_divisorproduct) * (ge_second_ip_euclid_backward_divisorproduct))))))) + ge_balance_negative_euclid_backward_divisorproductoutputreal = (((((((ge_first_rp_euclid_backward_divisorproduct) * (ge_second_rn_euclid_backward_divisorproduct))) + (((ge_first_rn_euclid_backward_divisorproduct) * (ge_second_rp_euclid_backward_divisorproduct))))) + (((((ge_first_ip_euclid_backward_divisorproduct) * (ge_second_ip_euclid_backward_divisorproduct))) + (((ge_first_in_euclid_backward_divisorproduct) * (ge_second_in_euclid_backward_divisorproduct))))))) + ge_balance_positive_euclid_backward_divisorproductoutputreal))) /\ (exists ge_balance_positive_euclid_backward_divisorproductoutputimaginary ge_balance_negative_euclid_backward_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_euclid_backward_divisorproductoutput) = 2 * (ge_balance_positive_euclid_backward_divisorproductoutputimaginary) /\ (ge_balance_negative_euclid_backward_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_euclid_backward_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_divisorproductoutput) = 2 * ge_signed_half_euclid_backward_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_euclid_backward_divisorproductoutputimaginary) = S ge_signed_half_euclid_backward_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclid_backward_divisorproduct) * (ge_second_ip_euclid_backward_divisorproduct))) + (((ge_first_rn_euclid_backward_divisorproduct) * (ge_second_in_euclid_backward_divisorproduct))))) + (((((ge_first_ip_euclid_backward_divisorproduct) * (ge_second_rp_euclid_backward_divisorproduct))) + (((ge_first_in_euclid_backward_divisorproduct) * (ge_second_rn_euclid_backward_divisorproduct))))))) + ge_balance_negative_euclid_backward_divisorproductoutputimaginary = (((((((ge_first_rp_euclid_backward_divisorproduct) * (ge_second_in_euclid_backward_divisorproduct))) + (((ge_first_rn_euclid_backward_divisorproduct) * (ge_second_ip_euclid_backward_divisorproduct))))) + (((((ge_first_ip_euclid_backward_divisorproduct) * (ge_second_rn_euclid_backward_divisorproduct))) + (((ge_first_in_euclid_backward_divisorproduct) * (ge_second_rp_euclid_backward_divisorproduct))))))) + ge_balance_positive_euclid_backward_divisorproductoutputimaginary)))))))))) -> (exists gr_quotient_euclid_backward_result. (exists ge_first_rp_euclid_backward_resultproduct ge_first_rn_euclid_backward_resultproduct ge_first_ip_euclid_backward_resultproduct ge_first_in_euclid_backward_resultproduct ge_second_rp_euclid_backward_resultproduct ge_second_rn_euclid_backward_resultproduct ge_second_ip_euclid_backward_resultproduct ge_second_in_euclid_backward_resultproduct. ((exists ge_representation_real_code_euclid_backward_resultproductfirst ge_representation_imaginary_code_euclid_backward_resultproductfirst. (((d) = ((ge_representation_real_code_euclid_backward_resultproductfirst) + (ge_representation_imaginary_code_euclid_backward_resultproductfirst)) * S ((ge_representation_real_code_euclid_backward_resultproductfirst) + (ge_representation_imaginary_code_euclid_backward_resultproductfirst)) + ((ge_representation_imaginary_code_euclid_backward_resultproductfirst) + (ge_representation_imaginary_code_euclid_backward_resultproductfirst))) /\ ((exists ge_balance_positive_euclid_backward_resultproductfirstreal ge_balance_negative_euclid_backward_resultproductfirstreal. (((((ge_representation_real_code_euclid_backward_resultproductfirst) = 2 * (ge_balance_positive_euclid_backward_resultproductfirstreal) /\ (ge_balance_negative_euclid_backward_resultproductfirstreal) = 0) \/ exists ge_signed_half_euclid_backward_resultproductfirstrealdecode. (((ge_representation_real_code_euclid_backward_resultproductfirst) = 2 * ge_signed_half_euclid_backward_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_euclid_backward_resultproductfirstreal) = 0) /\ (ge_balance_negative_euclid_backward_resultproductfirstreal) = S ge_signed_half_euclid_backward_resultproductfirstrealdecode))) /\ ((ge_first_rp_euclid_backward_resultproduct) + ge_balance_negative_euclid_backward_resultproductfirstreal = (ge_first_rn_euclid_backward_resultproduct) + ge_balance_positive_euclid_backward_resultproductfirstreal))) /\ (exists ge_balance_positive_euclid_backward_resultproductfirstimaginary ge_balance_negative_euclid_backward_resultproductfirstimaginary. (((((ge_representation_imaginary_code_euclid_backward_resultproductfirst) = 2 * (ge_balance_positive_euclid_backward_resultproductfirstimaginary) /\ (ge_balance_negative_euclid_backward_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_euclid_backward_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_resultproductfirst) = 2 * ge_signed_half_euclid_backward_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_euclid_backward_resultproductfirstimaginary) = S ge_signed_half_euclid_backward_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_euclid_backward_resultproduct) + ge_balance_negative_euclid_backward_resultproductfirstimaginary = (ge_first_in_euclid_backward_resultproduct) + ge_balance_positive_euclid_backward_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_backward_resultproductsecond ge_representation_imaginary_code_euclid_backward_resultproductsecond. (((gr_quotient_euclid_backward_result) = ((ge_representation_real_code_euclid_backward_resultproductsecond) + (ge_representation_imaginary_code_euclid_backward_resultproductsecond)) * S ((ge_representation_real_code_euclid_backward_resultproductsecond) + (ge_representation_imaginary_code_euclid_backward_resultproductsecond)) + ((ge_representation_imaginary_code_euclid_backward_resultproductsecond) + (ge_representation_imaginary_code_euclid_backward_resultproductsecond))) /\ ((exists ge_balance_positive_euclid_backward_resultproductsecondreal ge_balance_negative_euclid_backward_resultproductsecondreal. (((((ge_representation_real_code_euclid_backward_resultproductsecond) = 2 * (ge_balance_positive_euclid_backward_resultproductsecondreal) /\ (ge_balance_negative_euclid_backward_resultproductsecondreal) = 0) \/ exists ge_signed_half_euclid_backward_resultproductsecondrealdecode. (((ge_representation_real_code_euclid_backward_resultproductsecond) = 2 * ge_signed_half_euclid_backward_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_euclid_backward_resultproductsecondreal) = 0) /\ (ge_balance_negative_euclid_backward_resultproductsecondreal) = S ge_signed_half_euclid_backward_resultproductsecondrealdecode))) /\ ((ge_second_rp_euclid_backward_resultproduct) + ge_balance_negative_euclid_backward_resultproductsecondreal = (ge_second_rn_euclid_backward_resultproduct) + ge_balance_positive_euclid_backward_resultproductsecondreal))) /\ (exists ge_balance_positive_euclid_backward_resultproductsecondimaginary ge_balance_negative_euclid_backward_resultproductsecondimaginary. (((((ge_representation_imaginary_code_euclid_backward_resultproductsecond) = 2 * (ge_balance_positive_euclid_backward_resultproductsecondimaginary) /\ (ge_balance_negative_euclid_backward_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_euclid_backward_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_resultproductsecond) = 2 * ge_signed_half_euclid_backward_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_euclid_backward_resultproductsecondimaginary) = S ge_signed_half_euclid_backward_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_euclid_backward_resultproduct) + ge_balance_negative_euclid_backward_resultproductsecondimaginary = (ge_second_in_euclid_backward_resultproduct) + ge_balance_positive_euclid_backward_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_backward_resultproductoutput ge_representation_imaginary_code_euclid_backward_resultproductoutput. (((r) = ((ge_representation_real_code_euclid_backward_resultproductoutput) + (ge_representation_imaginary_code_euclid_backward_resultproductoutput)) * S ((ge_representation_real_code_euclid_backward_resultproductoutput) + (ge_representation_imaginary_code_euclid_backward_resultproductoutput)) + ((ge_representation_imaginary_code_euclid_backward_resultproductoutput) + (ge_representation_imaginary_code_euclid_backward_resultproductoutput))) /\ ((exists ge_balance_positive_euclid_backward_resultproductoutputreal ge_balance_negative_euclid_backward_resultproductoutputreal. (((((ge_representation_real_code_euclid_backward_resultproductoutput) = 2 * (ge_balance_positive_euclid_backward_resultproductoutputreal) /\ (ge_balance_negative_euclid_backward_resultproductoutputreal) = 0) \/ exists ge_signed_half_euclid_backward_resultproductoutputrealdecode. (((ge_representation_real_code_euclid_backward_resultproductoutput) = 2 * ge_signed_half_euclid_backward_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_euclid_backward_resultproductoutputreal) = 0) /\ (ge_balance_negative_euclid_backward_resultproductoutputreal) = S ge_signed_half_euclid_backward_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclid_backward_resultproduct) * (ge_second_rp_euclid_backward_resultproduct))) + (((ge_first_rn_euclid_backward_resultproduct) * (ge_second_rn_euclid_backward_resultproduct))))) + (((((ge_first_ip_euclid_backward_resultproduct) * (ge_second_in_euclid_backward_resultproduct))) + (((ge_first_in_euclid_backward_resultproduct) * (ge_second_ip_euclid_backward_resultproduct))))))) + ge_balance_negative_euclid_backward_resultproductoutputreal = (((((((ge_first_rp_euclid_backward_resultproduct) * (ge_second_rn_euclid_backward_resultproduct))) + (((ge_first_rn_euclid_backward_resultproduct) * (ge_second_rp_euclid_backward_resultproduct))))) + (((((ge_first_ip_euclid_backward_resultproduct) * (ge_second_ip_euclid_backward_resultproduct))) + (((ge_first_in_euclid_backward_resultproduct) * (ge_second_in_euclid_backward_resultproduct))))))) + ge_balance_positive_euclid_backward_resultproductoutputreal))) /\ (exists ge_balance_positive_euclid_backward_resultproductoutputimaginary ge_balance_negative_euclid_backward_resultproductoutputimaginary. (((((ge_representation_imaginary_code_euclid_backward_resultproductoutput) = 2 * (ge_balance_positive_euclid_backward_resultproductoutputimaginary) /\ (ge_balance_negative_euclid_backward_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_euclid_backward_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_backward_resultproductoutput) = 2 * ge_signed_half_euclid_backward_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_backward_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_euclid_backward_resultproductoutputimaginary) = S ge_signed_half_euclid_backward_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclid_backward_resultproduct) * (ge_second_ip_euclid_backward_resultproduct))) + (((ge_first_rn_euclid_backward_resultproduct) * (ge_second_in_euclid_backward_resultproduct))))) + (((((ge_first_ip_euclid_backward_resultproduct) * (ge_second_rp_euclid_backward_resultproduct))) + (((ge_first_in_euclid_backward_resultproduct) * (ge_second_rn_euclid_backward_resultproduct))))))) + ge_balance_negative_euclid_backward_resultproductoutputimaginary = (((((((ge_first_rp_euclid_backward_resultproduct) * (ge_second_in_euclid_backward_resultproduct))) + (((ge_first_rn_euclid_backward_resultproduct) * (ge_second_ip_euclid_backward_resultproduct))))) + (((((ge_first_ip_euclid_backward_resultproduct) * (ge_second_rn_euclid_backward_resultproduct))) + (((ge_first_in_euclid_backward_resultproduct) * (ge_second_rp_euclid_backward_resultproduct))))))) + ge_balance_positive_euclid_backward_resultproductoutputimaginary))))))))))