gaussian_common_divisor_euclidean_forward

Exact expanded first-order arithmetic statement

forall d a b q r. (exists ge_division_product_euclid_forward_equation. ((exists ge_first_rp_euclid_forward_equationproduct ge_first_rn_euclid_forward_equationproduct ge_first_ip_euclid_forward_equationproduct ge_first_in_euclid_forward_equationproduct ge_second_rp_euclid_forward_equationproduct ge_second_rn_euclid_forward_equationproduct ge_second_ip_euclid_forward_equationproduct ge_second_in_euclid_forward_equationproduct. ((exists ge_representation_real_code_euclid_forward_equationproductfirst ge_representation_imaginary_code_euclid_forward_equationproductfirst. (((b) = ((ge_representation_real_code_euclid_forward_equationproductfirst) + (ge_representation_imaginary_code_euclid_forward_equationproductfirst)) * S ((ge_representation_real_code_euclid_forward_equationproductfirst) + (ge_representation_imaginary_code_euclid_forward_equationproductfirst)) + ((ge_representation_imaginary_code_euclid_forward_equationproductfirst) + (ge_representation_imaginary_code_euclid_forward_equationproductfirst))) /\ ((exists ge_balance_positive_euclid_forward_equationproductfirstreal ge_balance_negative_euclid_forward_equationproductfirstreal. (((((ge_representation_real_code_euclid_forward_equationproductfirst) = 2 * (ge_balance_positive_euclid_forward_equationproductfirstreal) /\ (ge_balance_negative_euclid_forward_equationproductfirstreal) = 0) \/ exists ge_signed_half_euclid_forward_equationproductfirstrealdecode. (((ge_representation_real_code_euclid_forward_equationproductfirst) = 2 * ge_signed_half_euclid_forward_equationproductfirstrealdecode + 1 /\ (ge_balance_positive_euclid_forward_equationproductfirstreal) = 0) /\ (ge_balance_negative_euclid_forward_equationproductfirstreal) = S ge_signed_half_euclid_forward_equationproductfirstrealdecode))) /\ ((ge_first_rp_euclid_forward_equationproduct) + ge_balance_negative_euclid_forward_equationproductfirstreal = (ge_first_rn_euclid_forward_equationproduct) + ge_balance_positive_euclid_forward_equationproductfirstreal))) /\ (exists ge_balance_positive_euclid_forward_equationproductfirstimaginary ge_balance_negative_euclid_forward_equationproductfirstimaginary. (((((ge_representation_imaginary_code_euclid_forward_equationproductfirst) = 2 * (ge_balance_positive_euclid_forward_equationproductfirstimaginary) /\ (ge_balance_negative_euclid_forward_equationproductfirstimaginary) = 0) \/ exists ge_signed_half_euclid_forward_equationproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_equationproductfirst) = 2 * ge_signed_half_euclid_forward_equationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_equationproductfirstimaginary) = 0) /\ (ge_balance_negative_euclid_forward_equationproductfirstimaginary) = S ge_signed_half_euclid_forward_equationproductfirstimaginarydecode))) /\ ((ge_first_ip_euclid_forward_equationproduct) + ge_balance_negative_euclid_forward_equationproductfirstimaginary = (ge_first_in_euclid_forward_equationproduct) + ge_balance_positive_euclid_forward_equationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_forward_equationproductsecond ge_representation_imaginary_code_euclid_forward_equationproductsecond. (((q) = ((ge_representation_real_code_euclid_forward_equationproductsecond) + (ge_representation_imaginary_code_euclid_forward_equationproductsecond)) * S ((ge_representation_real_code_euclid_forward_equationproductsecond) + (ge_representation_imaginary_code_euclid_forward_equationproductsecond)) + ((ge_representation_imaginary_code_euclid_forward_equationproductsecond) + (ge_representation_imaginary_code_euclid_forward_equationproductsecond))) /\ ((exists ge_balance_positive_euclid_forward_equationproductsecondreal ge_balance_negative_euclid_forward_equationproductsecondreal. (((((ge_representation_real_code_euclid_forward_equationproductsecond) = 2 * (ge_balance_positive_euclid_forward_equationproductsecondreal) /\ (ge_balance_negative_euclid_forward_equationproductsecondreal) = 0) \/ exists ge_signed_half_euclid_forward_equationproductsecondrealdecode. (((ge_representation_real_code_euclid_forward_equationproductsecond) = 2 * ge_signed_half_euclid_forward_equationproductsecondrealdecode + 1 /\ (ge_balance_positive_euclid_forward_equationproductsecondreal) = 0) /\ (ge_balance_negative_euclid_forward_equationproductsecondreal) = S ge_signed_half_euclid_forward_equationproductsecondrealdecode))) /\ ((ge_second_rp_euclid_forward_equationproduct) + ge_balance_negative_euclid_forward_equationproductsecondreal = (ge_second_rn_euclid_forward_equationproduct) + ge_balance_positive_euclid_forward_equationproductsecondreal))) /\ (exists ge_balance_positive_euclid_forward_equationproductsecondimaginary ge_balance_negative_euclid_forward_equationproductsecondimaginary. (((((ge_representation_imaginary_code_euclid_forward_equationproductsecond) = 2 * (ge_balance_positive_euclid_forward_equationproductsecondimaginary) /\ (ge_balance_negative_euclid_forward_equationproductsecondimaginary) = 0) \/ exists ge_signed_half_euclid_forward_equationproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_equationproductsecond) = 2 * ge_signed_half_euclid_forward_equationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_equationproductsecondimaginary) = 0) /\ (ge_balance_negative_euclid_forward_equationproductsecondimaginary) = S ge_signed_half_euclid_forward_equationproductsecondimaginarydecode))) /\ ((ge_second_ip_euclid_forward_equationproduct) + ge_balance_negative_euclid_forward_equationproductsecondimaginary = (ge_second_in_euclid_forward_equationproduct) + ge_balance_positive_euclid_forward_equationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_forward_equationproductoutput ge_representation_imaginary_code_euclid_forward_equationproductoutput. (((ge_division_product_euclid_forward_equation) = ((ge_representation_real_code_euclid_forward_equationproductoutput) + (ge_representation_imaginary_code_euclid_forward_equationproductoutput)) * S ((ge_representation_real_code_euclid_forward_equationproductoutput) + (ge_representation_imaginary_code_euclid_forward_equationproductoutput)) + ((ge_representation_imaginary_code_euclid_forward_equationproductoutput) + (ge_representation_imaginary_code_euclid_forward_equationproductoutput))) /\ ((exists ge_balance_positive_euclid_forward_equationproductoutputreal ge_balance_negative_euclid_forward_equationproductoutputreal. (((((ge_representation_real_code_euclid_forward_equationproductoutput) = 2 * (ge_balance_positive_euclid_forward_equationproductoutputreal) /\ (ge_balance_negative_euclid_forward_equationproductoutputreal) = 0) \/ exists ge_signed_half_euclid_forward_equationproductoutputrealdecode. (((ge_representation_real_code_euclid_forward_equationproductoutput) = 2 * ge_signed_half_euclid_forward_equationproductoutputrealdecode + 1 /\ (ge_balance_positive_euclid_forward_equationproductoutputreal) = 0) /\ (ge_balance_negative_euclid_forward_equationproductoutputreal) = S ge_signed_half_euclid_forward_equationproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclid_forward_equationproduct) * (ge_second_rp_euclid_forward_equationproduct))) + (((ge_first_rn_euclid_forward_equationproduct) * (ge_second_rn_euclid_forward_equationproduct))))) + (((((ge_first_ip_euclid_forward_equationproduct) * (ge_second_in_euclid_forward_equationproduct))) + (((ge_first_in_euclid_forward_equationproduct) * (ge_second_ip_euclid_forward_equationproduct))))))) + ge_balance_negative_euclid_forward_equationproductoutputreal = (((((((ge_first_rp_euclid_forward_equationproduct) * (ge_second_rn_euclid_forward_equationproduct))) + (((ge_first_rn_euclid_forward_equationproduct) * (ge_second_rp_euclid_forward_equationproduct))))) + (((((ge_first_ip_euclid_forward_equationproduct) * (ge_second_ip_euclid_forward_equationproduct))) + (((ge_first_in_euclid_forward_equationproduct) * (ge_second_in_euclid_forward_equationproduct))))))) + ge_balance_positive_euclid_forward_equationproductoutputreal))) /\ (exists ge_balance_positive_euclid_forward_equationproductoutputimaginary ge_balance_negative_euclid_forward_equationproductoutputimaginary. (((((ge_representation_imaginary_code_euclid_forward_equationproductoutput) = 2 * (ge_balance_positive_euclid_forward_equationproductoutputimaginary) /\ (ge_balance_negative_euclid_forward_equationproductoutputimaginary) = 0) \/ exists ge_signed_half_euclid_forward_equationproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_equationproductoutput) = 2 * ge_signed_half_euclid_forward_equationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_equationproductoutputimaginary) = 0) /\ (ge_balance_negative_euclid_forward_equationproductoutputimaginary) = S ge_signed_half_euclid_forward_equationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclid_forward_equationproduct) * (ge_second_ip_euclid_forward_equationproduct))) + (((ge_first_rn_euclid_forward_equationproduct) * (ge_second_in_euclid_forward_equationproduct))))) + (((((ge_first_ip_euclid_forward_equationproduct) * (ge_second_rp_euclid_forward_equationproduct))) + (((ge_first_in_euclid_forward_equationproduct) * (ge_second_rn_euclid_forward_equationproduct))))))) + ge_balance_negative_euclid_forward_equationproductoutputimaginary = (((((((ge_first_rp_euclid_forward_equationproduct) * (ge_second_in_euclid_forward_equationproduct))) + (((ge_first_rn_euclid_forward_equationproduct) * (ge_second_ip_euclid_forward_equationproduct))))) + (((((ge_first_ip_euclid_forward_equationproduct) * (ge_second_rn_euclid_forward_equationproduct))) + (((ge_first_in_euclid_forward_equationproduct) * (ge_second_rp_euclid_forward_equationproduct))))))) + ge_balance_positive_euclid_forward_equationproductoutputimaginary))))))))) /\ (exists ge_first_rp_euclid_forward_equationsum ge_first_rn_euclid_forward_equationsum ge_first_ip_euclid_forward_equationsum ge_first_in_euclid_forward_equationsum ge_second_rp_euclid_forward_equationsum ge_second_rn_euclid_forward_equationsum ge_second_ip_euclid_forward_equationsum ge_second_in_euclid_forward_equationsum. ((exists ge_representation_real_code_euclid_forward_equationsumfirst ge_representation_imaginary_code_euclid_forward_equationsumfirst. (((ge_division_product_euclid_forward_equation) = ((ge_representation_real_code_euclid_forward_equationsumfirst) + (ge_representation_imaginary_code_euclid_forward_equationsumfirst)) * S ((ge_representation_real_code_euclid_forward_equationsumfirst) + (ge_representation_imaginary_code_euclid_forward_equationsumfirst)) + ((ge_representation_imaginary_code_euclid_forward_equationsumfirst) + (ge_representation_imaginary_code_euclid_forward_equationsumfirst))) /\ ((exists ge_balance_positive_euclid_forward_equationsumfirstreal ge_balance_negative_euclid_forward_equationsumfirstreal. (((((ge_representation_real_code_euclid_forward_equationsumfirst) = 2 * (ge_balance_positive_euclid_forward_equationsumfirstreal) /\ (ge_balance_negative_euclid_forward_equationsumfirstreal) = 0) \/ exists ge_signed_half_euclid_forward_equationsumfirstrealdecode. (((ge_representation_real_code_euclid_forward_equationsumfirst) = 2 * ge_signed_half_euclid_forward_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_euclid_forward_equationsumfirstreal) = 0) /\ (ge_balance_negative_euclid_forward_equationsumfirstreal) = S ge_signed_half_euclid_forward_equationsumfirstrealdecode))) /\ ((ge_first_rp_euclid_forward_equationsum) + ge_balance_negative_euclid_forward_equationsumfirstreal = (ge_first_rn_euclid_forward_equationsum) + ge_balance_positive_euclid_forward_equationsumfirstreal))) /\ (exists ge_balance_positive_euclid_forward_equationsumfirstimaginary ge_balance_negative_euclid_forward_equationsumfirstimaginary. (((((ge_representation_imaginary_code_euclid_forward_equationsumfirst) = 2 * (ge_balance_positive_euclid_forward_equationsumfirstimaginary) /\ (ge_balance_negative_euclid_forward_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_euclid_forward_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_equationsumfirst) = 2 * ge_signed_half_euclid_forward_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_euclid_forward_equationsumfirstimaginary) = S ge_signed_half_euclid_forward_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_euclid_forward_equationsum) + ge_balance_negative_euclid_forward_equationsumfirstimaginary = (ge_first_in_euclid_forward_equationsum) + ge_balance_positive_euclid_forward_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_forward_equationsumsecond ge_representation_imaginary_code_euclid_forward_equationsumsecond. (((r) = ((ge_representation_real_code_euclid_forward_equationsumsecond) + (ge_representation_imaginary_code_euclid_forward_equationsumsecond)) * S ((ge_representation_real_code_euclid_forward_equationsumsecond) + (ge_representation_imaginary_code_euclid_forward_equationsumsecond)) + ((ge_representation_imaginary_code_euclid_forward_equationsumsecond) + (ge_representation_imaginary_code_euclid_forward_equationsumsecond))) /\ ((exists ge_balance_positive_euclid_forward_equationsumsecondreal ge_balance_negative_euclid_forward_equationsumsecondreal. (((((ge_representation_real_code_euclid_forward_equationsumsecond) = 2 * (ge_balance_positive_euclid_forward_equationsumsecondreal) /\ (ge_balance_negative_euclid_forward_equationsumsecondreal) = 0) \/ exists ge_signed_half_euclid_forward_equationsumsecondrealdecode. (((ge_representation_real_code_euclid_forward_equationsumsecond) = 2 * ge_signed_half_euclid_forward_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_euclid_forward_equationsumsecondreal) = 0) /\ (ge_balance_negative_euclid_forward_equationsumsecondreal) = S ge_signed_half_euclid_forward_equationsumsecondrealdecode))) /\ ((ge_second_rp_euclid_forward_equationsum) + ge_balance_negative_euclid_forward_equationsumsecondreal = (ge_second_rn_euclid_forward_equationsum) + ge_balance_positive_euclid_forward_equationsumsecondreal))) /\ (exists ge_balance_positive_euclid_forward_equationsumsecondimaginary ge_balance_negative_euclid_forward_equationsumsecondimaginary. (((((ge_representation_imaginary_code_euclid_forward_equationsumsecond) = 2 * (ge_balance_positive_euclid_forward_equationsumsecondimaginary) /\ (ge_balance_negative_euclid_forward_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_euclid_forward_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_equationsumsecond) = 2 * ge_signed_half_euclid_forward_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_euclid_forward_equationsumsecondimaginary) = S ge_signed_half_euclid_forward_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_euclid_forward_equationsum) + ge_balance_negative_euclid_forward_equationsumsecondimaginary = (ge_second_in_euclid_forward_equationsum) + ge_balance_positive_euclid_forward_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_forward_equationsumoutput ge_representation_imaginary_code_euclid_forward_equationsumoutput. (((a) = ((ge_representation_real_code_euclid_forward_equationsumoutput) + (ge_representation_imaginary_code_euclid_forward_equationsumoutput)) * S ((ge_representation_real_code_euclid_forward_equationsumoutput) + (ge_representation_imaginary_code_euclid_forward_equationsumoutput)) + ((ge_representation_imaginary_code_euclid_forward_equationsumoutput) + (ge_representation_imaginary_code_euclid_forward_equationsumoutput))) /\ ((exists ge_balance_positive_euclid_forward_equationsumoutputreal ge_balance_negative_euclid_forward_equationsumoutputreal. (((((ge_representation_real_code_euclid_forward_equationsumoutput) = 2 * (ge_balance_positive_euclid_forward_equationsumoutputreal) /\ (ge_balance_negative_euclid_forward_equationsumoutputreal) = 0) \/ exists ge_signed_half_euclid_forward_equationsumoutputrealdecode. (((ge_representation_real_code_euclid_forward_equationsumoutput) = 2 * ge_signed_half_euclid_forward_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_euclid_forward_equationsumoutputreal) = 0) /\ (ge_balance_negative_euclid_forward_equationsumoutputreal) = S ge_signed_half_euclid_forward_equationsumoutputrealdecode))) /\ ((((ge_first_rp_euclid_forward_equationsum) + (ge_second_rp_euclid_forward_equationsum))) + ge_balance_negative_euclid_forward_equationsumoutputreal = (((ge_first_rn_euclid_forward_equationsum) + (ge_second_rn_euclid_forward_equationsum))) + ge_balance_positive_euclid_forward_equationsumoutputreal))) /\ (exists ge_balance_positive_euclid_forward_equationsumoutputimaginary ge_balance_negative_euclid_forward_equationsumoutputimaginary. (((((ge_representation_imaginary_code_euclid_forward_equationsumoutput) = 2 * (ge_balance_positive_euclid_forward_equationsumoutputimaginary) /\ (ge_balance_negative_euclid_forward_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_euclid_forward_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_equationsumoutput) = 2 * ge_signed_half_euclid_forward_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_euclid_forward_equationsumoutputimaginary) = S ge_signed_half_euclid_forward_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_euclid_forward_equationsum) + (ge_second_ip_euclid_forward_equationsum))) + ge_balance_negative_euclid_forward_equationsumoutputimaginary = (((ge_first_in_euclid_forward_equationsum) + (ge_second_in_euclid_forward_equationsum))) + ge_balance_positive_euclid_forward_equationsumoutputimaginary))))))))))) -> (exists gr_quotient_euclid_forward_divisor. (exists ge_first_rp_euclid_forward_divisorproduct ge_first_rn_euclid_forward_divisorproduct ge_first_ip_euclid_forward_divisorproduct ge_first_in_euclid_forward_divisorproduct ge_second_rp_euclid_forward_divisorproduct ge_second_rn_euclid_forward_divisorproduct ge_second_ip_euclid_forward_divisorproduct ge_second_in_euclid_forward_divisorproduct. ((exists ge_representation_real_code_euclid_forward_divisorproductfirst ge_representation_imaginary_code_euclid_forward_divisorproductfirst. (((d) = ((ge_representation_real_code_euclid_forward_divisorproductfirst) + (ge_representation_imaginary_code_euclid_forward_divisorproductfirst)) * S ((ge_representation_real_code_euclid_forward_divisorproductfirst) + (ge_representation_imaginary_code_euclid_forward_divisorproductfirst)) + ((ge_representation_imaginary_code_euclid_forward_divisorproductfirst) + (ge_representation_imaginary_code_euclid_forward_divisorproductfirst))) /\ ((exists ge_balance_positive_euclid_forward_divisorproductfirstreal ge_balance_negative_euclid_forward_divisorproductfirstreal. (((((ge_representation_real_code_euclid_forward_divisorproductfirst) = 2 * (ge_balance_positive_euclid_forward_divisorproductfirstreal) /\ (ge_balance_negative_euclid_forward_divisorproductfirstreal) = 0) \/ exists ge_signed_half_euclid_forward_divisorproductfirstrealdecode. (((ge_representation_real_code_euclid_forward_divisorproductfirst) = 2 * ge_signed_half_euclid_forward_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_euclid_forward_divisorproductfirstreal) = 0) /\ (ge_balance_negative_euclid_forward_divisorproductfirstreal) = S ge_signed_half_euclid_forward_divisorproductfirstrealdecode))) /\ ((ge_first_rp_euclid_forward_divisorproduct) + ge_balance_negative_euclid_forward_divisorproductfirstreal = (ge_first_rn_euclid_forward_divisorproduct) + ge_balance_positive_euclid_forward_divisorproductfirstreal))) /\ (exists ge_balance_positive_euclid_forward_divisorproductfirstimaginary ge_balance_negative_euclid_forward_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_euclid_forward_divisorproductfirst) = 2 * (ge_balance_positive_euclid_forward_divisorproductfirstimaginary) /\ (ge_balance_negative_euclid_forward_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_euclid_forward_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_divisorproductfirst) = 2 * ge_signed_half_euclid_forward_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_euclid_forward_divisorproductfirstimaginary) = S ge_signed_half_euclid_forward_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_euclid_forward_divisorproduct) + ge_balance_negative_euclid_forward_divisorproductfirstimaginary = (ge_first_in_euclid_forward_divisorproduct) + ge_balance_positive_euclid_forward_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_forward_divisorproductsecond ge_representation_imaginary_code_euclid_forward_divisorproductsecond. (((gr_quotient_euclid_forward_divisor) = ((ge_representation_real_code_euclid_forward_divisorproductsecond) + (ge_representation_imaginary_code_euclid_forward_divisorproductsecond)) * S ((ge_representation_real_code_euclid_forward_divisorproductsecond) + (ge_representation_imaginary_code_euclid_forward_divisorproductsecond)) + ((ge_representation_imaginary_code_euclid_forward_divisorproductsecond) + (ge_representation_imaginary_code_euclid_forward_divisorproductsecond))) /\ ((exists ge_balance_positive_euclid_forward_divisorproductsecondreal ge_balance_negative_euclid_forward_divisorproductsecondreal. (((((ge_representation_real_code_euclid_forward_divisorproductsecond) = 2 * (ge_balance_positive_euclid_forward_divisorproductsecondreal) /\ (ge_balance_negative_euclid_forward_divisorproductsecondreal) = 0) \/ exists ge_signed_half_euclid_forward_divisorproductsecondrealdecode. (((ge_representation_real_code_euclid_forward_divisorproductsecond) = 2 * ge_signed_half_euclid_forward_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_euclid_forward_divisorproductsecondreal) = 0) /\ (ge_balance_negative_euclid_forward_divisorproductsecondreal) = S ge_signed_half_euclid_forward_divisorproductsecondrealdecode))) /\ ((ge_second_rp_euclid_forward_divisorproduct) + ge_balance_negative_euclid_forward_divisorproductsecondreal = (ge_second_rn_euclid_forward_divisorproduct) + ge_balance_positive_euclid_forward_divisorproductsecondreal))) /\ (exists ge_balance_positive_euclid_forward_divisorproductsecondimaginary ge_balance_negative_euclid_forward_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_euclid_forward_divisorproductsecond) = 2 * (ge_balance_positive_euclid_forward_divisorproductsecondimaginary) /\ (ge_balance_negative_euclid_forward_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_euclid_forward_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_divisorproductsecond) = 2 * ge_signed_half_euclid_forward_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_euclid_forward_divisorproductsecondimaginary) = S ge_signed_half_euclid_forward_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_euclid_forward_divisorproduct) + ge_balance_negative_euclid_forward_divisorproductsecondimaginary = (ge_second_in_euclid_forward_divisorproduct) + ge_balance_positive_euclid_forward_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_forward_divisorproductoutput ge_representation_imaginary_code_euclid_forward_divisorproductoutput. (((b) = ((ge_representation_real_code_euclid_forward_divisorproductoutput) + (ge_representation_imaginary_code_euclid_forward_divisorproductoutput)) * S ((ge_representation_real_code_euclid_forward_divisorproductoutput) + (ge_representation_imaginary_code_euclid_forward_divisorproductoutput)) + ((ge_representation_imaginary_code_euclid_forward_divisorproductoutput) + (ge_representation_imaginary_code_euclid_forward_divisorproductoutput))) /\ ((exists ge_balance_positive_euclid_forward_divisorproductoutputreal ge_balance_negative_euclid_forward_divisorproductoutputreal. (((((ge_representation_real_code_euclid_forward_divisorproductoutput) = 2 * (ge_balance_positive_euclid_forward_divisorproductoutputreal) /\ (ge_balance_negative_euclid_forward_divisorproductoutputreal) = 0) \/ exists ge_signed_half_euclid_forward_divisorproductoutputrealdecode. (((ge_representation_real_code_euclid_forward_divisorproductoutput) = 2 * ge_signed_half_euclid_forward_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_euclid_forward_divisorproductoutputreal) = 0) /\ (ge_balance_negative_euclid_forward_divisorproductoutputreal) = S ge_signed_half_euclid_forward_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclid_forward_divisorproduct) * (ge_second_rp_euclid_forward_divisorproduct))) + (((ge_first_rn_euclid_forward_divisorproduct) * (ge_second_rn_euclid_forward_divisorproduct))))) + (((((ge_first_ip_euclid_forward_divisorproduct) * (ge_second_in_euclid_forward_divisorproduct))) + (((ge_first_in_euclid_forward_divisorproduct) * (ge_second_ip_euclid_forward_divisorproduct))))))) + ge_balance_negative_euclid_forward_divisorproductoutputreal = (((((((ge_first_rp_euclid_forward_divisorproduct) * (ge_second_rn_euclid_forward_divisorproduct))) + (((ge_first_rn_euclid_forward_divisorproduct) * (ge_second_rp_euclid_forward_divisorproduct))))) + (((((ge_first_ip_euclid_forward_divisorproduct) * (ge_second_ip_euclid_forward_divisorproduct))) + (((ge_first_in_euclid_forward_divisorproduct) * (ge_second_in_euclid_forward_divisorproduct))))))) + ge_balance_positive_euclid_forward_divisorproductoutputreal))) /\ (exists ge_balance_positive_euclid_forward_divisorproductoutputimaginary ge_balance_negative_euclid_forward_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_euclid_forward_divisorproductoutput) = 2 * (ge_balance_positive_euclid_forward_divisorproductoutputimaginary) /\ (ge_balance_negative_euclid_forward_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_euclid_forward_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_divisorproductoutput) = 2 * ge_signed_half_euclid_forward_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_euclid_forward_divisorproductoutputimaginary) = S ge_signed_half_euclid_forward_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclid_forward_divisorproduct) * (ge_second_ip_euclid_forward_divisorproduct))) + (((ge_first_rn_euclid_forward_divisorproduct) * (ge_second_in_euclid_forward_divisorproduct))))) + (((((ge_first_ip_euclid_forward_divisorproduct) * (ge_second_rp_euclid_forward_divisorproduct))) + (((ge_first_in_euclid_forward_divisorproduct) * (ge_second_rn_euclid_forward_divisorproduct))))))) + ge_balance_negative_euclid_forward_divisorproductoutputimaginary = (((((((ge_first_rp_euclid_forward_divisorproduct) * (ge_second_in_euclid_forward_divisorproduct))) + (((ge_first_rn_euclid_forward_divisorproduct) * (ge_second_ip_euclid_forward_divisorproduct))))) + (((((ge_first_ip_euclid_forward_divisorproduct) * (ge_second_rn_euclid_forward_divisorproduct))) + (((ge_first_in_euclid_forward_divisorproduct) * (ge_second_rp_euclid_forward_divisorproduct))))))) + ge_balance_positive_euclid_forward_divisorproductoutputimaginary)))))))))) -> (exists gr_quotient_euclid_forward_remainder. (exists ge_first_rp_euclid_forward_remainderproduct ge_first_rn_euclid_forward_remainderproduct ge_first_ip_euclid_forward_remainderproduct ge_first_in_euclid_forward_remainderproduct ge_second_rp_euclid_forward_remainderproduct ge_second_rn_euclid_forward_remainderproduct ge_second_ip_euclid_forward_remainderproduct ge_second_in_euclid_forward_remainderproduct. ((exists ge_representation_real_code_euclid_forward_remainderproductfirst ge_representation_imaginary_code_euclid_forward_remainderproductfirst. (((d) = ((ge_representation_real_code_euclid_forward_remainderproductfirst) + (ge_representation_imaginary_code_euclid_forward_remainderproductfirst)) * S ((ge_representation_real_code_euclid_forward_remainderproductfirst) + (ge_representation_imaginary_code_euclid_forward_remainderproductfirst)) + ((ge_representation_imaginary_code_euclid_forward_remainderproductfirst) + (ge_representation_imaginary_code_euclid_forward_remainderproductfirst))) /\ ((exists ge_balance_positive_euclid_forward_remainderproductfirstreal ge_balance_negative_euclid_forward_remainderproductfirstreal. (((((ge_representation_real_code_euclid_forward_remainderproductfirst) = 2 * (ge_balance_positive_euclid_forward_remainderproductfirstreal) /\ (ge_balance_negative_euclid_forward_remainderproductfirstreal) = 0) \/ exists ge_signed_half_euclid_forward_remainderproductfirstrealdecode. (((ge_representation_real_code_euclid_forward_remainderproductfirst) = 2 * ge_signed_half_euclid_forward_remainderproductfirstrealdecode + 1 /\ (ge_balance_positive_euclid_forward_remainderproductfirstreal) = 0) /\ (ge_balance_negative_euclid_forward_remainderproductfirstreal) = S ge_signed_half_euclid_forward_remainderproductfirstrealdecode))) /\ ((ge_first_rp_euclid_forward_remainderproduct) + ge_balance_negative_euclid_forward_remainderproductfirstreal = (ge_first_rn_euclid_forward_remainderproduct) + ge_balance_positive_euclid_forward_remainderproductfirstreal))) /\ (exists ge_balance_positive_euclid_forward_remainderproductfirstimaginary ge_balance_negative_euclid_forward_remainderproductfirstimaginary. (((((ge_representation_imaginary_code_euclid_forward_remainderproductfirst) = 2 * (ge_balance_positive_euclid_forward_remainderproductfirstimaginary) /\ (ge_balance_negative_euclid_forward_remainderproductfirstimaginary) = 0) \/ exists ge_signed_half_euclid_forward_remainderproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_remainderproductfirst) = 2 * ge_signed_half_euclid_forward_remainderproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_remainderproductfirstimaginary) = 0) /\ (ge_balance_negative_euclid_forward_remainderproductfirstimaginary) = S ge_signed_half_euclid_forward_remainderproductfirstimaginarydecode))) /\ ((ge_first_ip_euclid_forward_remainderproduct) + ge_balance_negative_euclid_forward_remainderproductfirstimaginary = (ge_first_in_euclid_forward_remainderproduct) + ge_balance_positive_euclid_forward_remainderproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_forward_remainderproductsecond ge_representation_imaginary_code_euclid_forward_remainderproductsecond. (((gr_quotient_euclid_forward_remainder) = ((ge_representation_real_code_euclid_forward_remainderproductsecond) + (ge_representation_imaginary_code_euclid_forward_remainderproductsecond)) * S ((ge_representation_real_code_euclid_forward_remainderproductsecond) + (ge_representation_imaginary_code_euclid_forward_remainderproductsecond)) + ((ge_representation_imaginary_code_euclid_forward_remainderproductsecond) + (ge_representation_imaginary_code_euclid_forward_remainderproductsecond))) /\ ((exists ge_balance_positive_euclid_forward_remainderproductsecondreal ge_balance_negative_euclid_forward_remainderproductsecondreal. (((((ge_representation_real_code_euclid_forward_remainderproductsecond) = 2 * (ge_balance_positive_euclid_forward_remainderproductsecondreal) /\ (ge_balance_negative_euclid_forward_remainderproductsecondreal) = 0) \/ exists ge_signed_half_euclid_forward_remainderproductsecondrealdecode. (((ge_representation_real_code_euclid_forward_remainderproductsecond) = 2 * ge_signed_half_euclid_forward_remainderproductsecondrealdecode + 1 /\ (ge_balance_positive_euclid_forward_remainderproductsecondreal) = 0) /\ (ge_balance_negative_euclid_forward_remainderproductsecondreal) = S ge_signed_half_euclid_forward_remainderproductsecondrealdecode))) /\ ((ge_second_rp_euclid_forward_remainderproduct) + ge_balance_negative_euclid_forward_remainderproductsecondreal = (ge_second_rn_euclid_forward_remainderproduct) + ge_balance_positive_euclid_forward_remainderproductsecondreal))) /\ (exists ge_balance_positive_euclid_forward_remainderproductsecondimaginary ge_balance_negative_euclid_forward_remainderproductsecondimaginary. (((((ge_representation_imaginary_code_euclid_forward_remainderproductsecond) = 2 * (ge_balance_positive_euclid_forward_remainderproductsecondimaginary) /\ (ge_balance_negative_euclid_forward_remainderproductsecondimaginary) = 0) \/ exists ge_signed_half_euclid_forward_remainderproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_remainderproductsecond) = 2 * ge_signed_half_euclid_forward_remainderproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_remainderproductsecondimaginary) = 0) /\ (ge_balance_negative_euclid_forward_remainderproductsecondimaginary) = S ge_signed_half_euclid_forward_remainderproductsecondimaginarydecode))) /\ ((ge_second_ip_euclid_forward_remainderproduct) + ge_balance_negative_euclid_forward_remainderproductsecondimaginary = (ge_second_in_euclid_forward_remainderproduct) + ge_balance_positive_euclid_forward_remainderproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_forward_remainderproductoutput ge_representation_imaginary_code_euclid_forward_remainderproductoutput. (((r) = ((ge_representation_real_code_euclid_forward_remainderproductoutput) + (ge_representation_imaginary_code_euclid_forward_remainderproductoutput)) * S ((ge_representation_real_code_euclid_forward_remainderproductoutput) + (ge_representation_imaginary_code_euclid_forward_remainderproductoutput)) + ((ge_representation_imaginary_code_euclid_forward_remainderproductoutput) + (ge_representation_imaginary_code_euclid_forward_remainderproductoutput))) /\ ((exists ge_balance_positive_euclid_forward_remainderproductoutputreal ge_balance_negative_euclid_forward_remainderproductoutputreal. (((((ge_representation_real_code_euclid_forward_remainderproductoutput) = 2 * (ge_balance_positive_euclid_forward_remainderproductoutputreal) /\ (ge_balance_negative_euclid_forward_remainderproductoutputreal) = 0) \/ exists ge_signed_half_euclid_forward_remainderproductoutputrealdecode. (((ge_representation_real_code_euclid_forward_remainderproductoutput) = 2 * ge_signed_half_euclid_forward_remainderproductoutputrealdecode + 1 /\ (ge_balance_positive_euclid_forward_remainderproductoutputreal) = 0) /\ (ge_balance_negative_euclid_forward_remainderproductoutputreal) = S ge_signed_half_euclid_forward_remainderproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclid_forward_remainderproduct) * (ge_second_rp_euclid_forward_remainderproduct))) + (((ge_first_rn_euclid_forward_remainderproduct) * (ge_second_rn_euclid_forward_remainderproduct))))) + (((((ge_first_ip_euclid_forward_remainderproduct) * (ge_second_in_euclid_forward_remainderproduct))) + (((ge_first_in_euclid_forward_remainderproduct) * (ge_second_ip_euclid_forward_remainderproduct))))))) + ge_balance_negative_euclid_forward_remainderproductoutputreal = (((((((ge_first_rp_euclid_forward_remainderproduct) * (ge_second_rn_euclid_forward_remainderproduct))) + (((ge_first_rn_euclid_forward_remainderproduct) * (ge_second_rp_euclid_forward_remainderproduct))))) + (((((ge_first_ip_euclid_forward_remainderproduct) * (ge_second_ip_euclid_forward_remainderproduct))) + (((ge_first_in_euclid_forward_remainderproduct) * (ge_second_in_euclid_forward_remainderproduct))))))) + ge_balance_positive_euclid_forward_remainderproductoutputreal))) /\ (exists ge_balance_positive_euclid_forward_remainderproductoutputimaginary ge_balance_negative_euclid_forward_remainderproductoutputimaginary. (((((ge_representation_imaginary_code_euclid_forward_remainderproductoutput) = 2 * (ge_balance_positive_euclid_forward_remainderproductoutputimaginary) /\ (ge_balance_negative_euclid_forward_remainderproductoutputimaginary) = 0) \/ exists ge_signed_half_euclid_forward_remainderproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_remainderproductoutput) = 2 * ge_signed_half_euclid_forward_remainderproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_remainderproductoutputimaginary) = 0) /\ (ge_balance_negative_euclid_forward_remainderproductoutputimaginary) = S ge_signed_half_euclid_forward_remainderproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclid_forward_remainderproduct) * (ge_second_ip_euclid_forward_remainderproduct))) + (((ge_first_rn_euclid_forward_remainderproduct) * (ge_second_in_euclid_forward_remainderproduct))))) + (((((ge_first_ip_euclid_forward_remainderproduct) * (ge_second_rp_euclid_forward_remainderproduct))) + (((ge_first_in_euclid_forward_remainderproduct) * (ge_second_rn_euclid_forward_remainderproduct))))))) + ge_balance_negative_euclid_forward_remainderproductoutputimaginary = (((((((ge_first_rp_euclid_forward_remainderproduct) * (ge_second_in_euclid_forward_remainderproduct))) + (((ge_first_rn_euclid_forward_remainderproduct) * (ge_second_ip_euclid_forward_remainderproduct))))) + (((((ge_first_ip_euclid_forward_remainderproduct) * (ge_second_rn_euclid_forward_remainderproduct))) + (((ge_first_in_euclid_forward_remainderproduct) * (ge_second_rp_euclid_forward_remainderproduct))))))) + ge_balance_positive_euclid_forward_remainderproductoutputimaginary)))))))))) -> (exists gr_quotient_euclid_forward_result. (exists ge_first_rp_euclid_forward_resultproduct ge_first_rn_euclid_forward_resultproduct ge_first_ip_euclid_forward_resultproduct ge_first_in_euclid_forward_resultproduct ge_second_rp_euclid_forward_resultproduct ge_second_rn_euclid_forward_resultproduct ge_second_ip_euclid_forward_resultproduct ge_second_in_euclid_forward_resultproduct. ((exists ge_representation_real_code_euclid_forward_resultproductfirst ge_representation_imaginary_code_euclid_forward_resultproductfirst. (((d) = ((ge_representation_real_code_euclid_forward_resultproductfirst) + (ge_representation_imaginary_code_euclid_forward_resultproductfirst)) * S ((ge_representation_real_code_euclid_forward_resultproductfirst) + (ge_representation_imaginary_code_euclid_forward_resultproductfirst)) + ((ge_representation_imaginary_code_euclid_forward_resultproductfirst) + (ge_representation_imaginary_code_euclid_forward_resultproductfirst))) /\ ((exists ge_balance_positive_euclid_forward_resultproductfirstreal ge_balance_negative_euclid_forward_resultproductfirstreal. (((((ge_representation_real_code_euclid_forward_resultproductfirst) = 2 * (ge_balance_positive_euclid_forward_resultproductfirstreal) /\ (ge_balance_negative_euclid_forward_resultproductfirstreal) = 0) \/ exists ge_signed_half_euclid_forward_resultproductfirstrealdecode. (((ge_representation_real_code_euclid_forward_resultproductfirst) = 2 * ge_signed_half_euclid_forward_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_euclid_forward_resultproductfirstreal) = 0) /\ (ge_balance_negative_euclid_forward_resultproductfirstreal) = S ge_signed_half_euclid_forward_resultproductfirstrealdecode))) /\ ((ge_first_rp_euclid_forward_resultproduct) + ge_balance_negative_euclid_forward_resultproductfirstreal = (ge_first_rn_euclid_forward_resultproduct) + ge_balance_positive_euclid_forward_resultproductfirstreal))) /\ (exists ge_balance_positive_euclid_forward_resultproductfirstimaginary ge_balance_negative_euclid_forward_resultproductfirstimaginary. (((((ge_representation_imaginary_code_euclid_forward_resultproductfirst) = 2 * (ge_balance_positive_euclid_forward_resultproductfirstimaginary) /\ (ge_balance_negative_euclid_forward_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_euclid_forward_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_resultproductfirst) = 2 * ge_signed_half_euclid_forward_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_euclid_forward_resultproductfirstimaginary) = S ge_signed_half_euclid_forward_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_euclid_forward_resultproduct) + ge_balance_negative_euclid_forward_resultproductfirstimaginary = (ge_first_in_euclid_forward_resultproduct) + ge_balance_positive_euclid_forward_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclid_forward_resultproductsecond ge_representation_imaginary_code_euclid_forward_resultproductsecond. (((gr_quotient_euclid_forward_result) = ((ge_representation_real_code_euclid_forward_resultproductsecond) + (ge_representation_imaginary_code_euclid_forward_resultproductsecond)) * S ((ge_representation_real_code_euclid_forward_resultproductsecond) + (ge_representation_imaginary_code_euclid_forward_resultproductsecond)) + ((ge_representation_imaginary_code_euclid_forward_resultproductsecond) + (ge_representation_imaginary_code_euclid_forward_resultproductsecond))) /\ ((exists ge_balance_positive_euclid_forward_resultproductsecondreal ge_balance_negative_euclid_forward_resultproductsecondreal. (((((ge_representation_real_code_euclid_forward_resultproductsecond) = 2 * (ge_balance_positive_euclid_forward_resultproductsecondreal) /\ (ge_balance_negative_euclid_forward_resultproductsecondreal) = 0) \/ exists ge_signed_half_euclid_forward_resultproductsecondrealdecode. (((ge_representation_real_code_euclid_forward_resultproductsecond) = 2 * ge_signed_half_euclid_forward_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_euclid_forward_resultproductsecondreal) = 0) /\ (ge_balance_negative_euclid_forward_resultproductsecondreal) = S ge_signed_half_euclid_forward_resultproductsecondrealdecode))) /\ ((ge_second_rp_euclid_forward_resultproduct) + ge_balance_negative_euclid_forward_resultproductsecondreal = (ge_second_rn_euclid_forward_resultproduct) + ge_balance_positive_euclid_forward_resultproductsecondreal))) /\ (exists ge_balance_positive_euclid_forward_resultproductsecondimaginary ge_balance_negative_euclid_forward_resultproductsecondimaginary. (((((ge_representation_imaginary_code_euclid_forward_resultproductsecond) = 2 * (ge_balance_positive_euclid_forward_resultproductsecondimaginary) /\ (ge_balance_negative_euclid_forward_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_euclid_forward_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_resultproductsecond) = 2 * ge_signed_half_euclid_forward_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_euclid_forward_resultproductsecondimaginary) = S ge_signed_half_euclid_forward_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_euclid_forward_resultproduct) + ge_balance_negative_euclid_forward_resultproductsecondimaginary = (ge_second_in_euclid_forward_resultproduct) + ge_balance_positive_euclid_forward_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclid_forward_resultproductoutput ge_representation_imaginary_code_euclid_forward_resultproductoutput. (((a) = ((ge_representation_real_code_euclid_forward_resultproductoutput) + (ge_representation_imaginary_code_euclid_forward_resultproductoutput)) * S ((ge_representation_real_code_euclid_forward_resultproductoutput) + (ge_representation_imaginary_code_euclid_forward_resultproductoutput)) + ((ge_representation_imaginary_code_euclid_forward_resultproductoutput) + (ge_representation_imaginary_code_euclid_forward_resultproductoutput))) /\ ((exists ge_balance_positive_euclid_forward_resultproductoutputreal ge_balance_negative_euclid_forward_resultproductoutputreal. (((((ge_representation_real_code_euclid_forward_resultproductoutput) = 2 * (ge_balance_positive_euclid_forward_resultproductoutputreal) /\ (ge_balance_negative_euclid_forward_resultproductoutputreal) = 0) \/ exists ge_signed_half_euclid_forward_resultproductoutputrealdecode. (((ge_representation_real_code_euclid_forward_resultproductoutput) = 2 * ge_signed_half_euclid_forward_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_euclid_forward_resultproductoutputreal) = 0) /\ (ge_balance_negative_euclid_forward_resultproductoutputreal) = S ge_signed_half_euclid_forward_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_euclid_forward_resultproduct) * (ge_second_rp_euclid_forward_resultproduct))) + (((ge_first_rn_euclid_forward_resultproduct) * (ge_second_rn_euclid_forward_resultproduct))))) + (((((ge_first_ip_euclid_forward_resultproduct) * (ge_second_in_euclid_forward_resultproduct))) + (((ge_first_in_euclid_forward_resultproduct) * (ge_second_ip_euclid_forward_resultproduct))))))) + ge_balance_negative_euclid_forward_resultproductoutputreal = (((((((ge_first_rp_euclid_forward_resultproduct) * (ge_second_rn_euclid_forward_resultproduct))) + (((ge_first_rn_euclid_forward_resultproduct) * (ge_second_rp_euclid_forward_resultproduct))))) + (((((ge_first_ip_euclid_forward_resultproduct) * (ge_second_ip_euclid_forward_resultproduct))) + (((ge_first_in_euclid_forward_resultproduct) * (ge_second_in_euclid_forward_resultproduct))))))) + ge_balance_positive_euclid_forward_resultproductoutputreal))) /\ (exists ge_balance_positive_euclid_forward_resultproductoutputimaginary ge_balance_negative_euclid_forward_resultproductoutputimaginary. (((((ge_representation_imaginary_code_euclid_forward_resultproductoutput) = 2 * (ge_balance_positive_euclid_forward_resultproductoutputimaginary) /\ (ge_balance_negative_euclid_forward_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_euclid_forward_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclid_forward_resultproductoutput) = 2 * ge_signed_half_euclid_forward_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclid_forward_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_euclid_forward_resultproductoutputimaginary) = S ge_signed_half_euclid_forward_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_euclid_forward_resultproduct) * (ge_second_ip_euclid_forward_resultproduct))) + (((ge_first_rn_euclid_forward_resultproduct) * (ge_second_in_euclid_forward_resultproduct))))) + (((((ge_first_ip_euclid_forward_resultproduct) * (ge_second_rp_euclid_forward_resultproduct))) + (((ge_first_in_euclid_forward_resultproduct) * (ge_second_rn_euclid_forward_resultproduct))))))) + ge_balance_negative_euclid_forward_resultproductoutputimaginary = (((((((ge_first_rp_euclid_forward_resultproduct) * (ge_second_in_euclid_forward_resultproduct))) + (((ge_first_rn_euclid_forward_resultproduct) * (ge_second_ip_euclid_forward_resultproduct))))) + (((((ge_first_ip_euclid_forward_resultproduct) * (ge_second_rn_euclid_forward_resultproduct))) + (((ge_first_in_euclid_forward_resultproduct) * (ge_second_rp_euclid_forward_resultproduct))))))) + ge_balance_positive_euclid_forward_resultproductoutputimaginary))))))))))