gaussian_divisor_of_unit_is_unit

Exact expanded first-order arithmetic statement

forall d u. (exists gr_quotient_unit_divides_given. (exists ge_first_rp_unit_divides_givenproduct ge_first_rn_unit_divides_givenproduct ge_first_ip_unit_divides_givenproduct ge_first_in_unit_divides_givenproduct ge_second_rp_unit_divides_givenproduct ge_second_rn_unit_divides_givenproduct ge_second_ip_unit_divides_givenproduct ge_second_in_unit_divides_givenproduct. ((exists ge_representation_real_code_unit_divides_givenproductfirst ge_representation_imaginary_code_unit_divides_givenproductfirst. (((d) = ((ge_representation_real_code_unit_divides_givenproductfirst) + (ge_representation_imaginary_code_unit_divides_givenproductfirst)) * S ((ge_representation_real_code_unit_divides_givenproductfirst) + (ge_representation_imaginary_code_unit_divides_givenproductfirst)) + ((ge_representation_imaginary_code_unit_divides_givenproductfirst) + (ge_representation_imaginary_code_unit_divides_givenproductfirst))) /\ ((exists ge_balance_positive_unit_divides_givenproductfirstreal ge_balance_negative_unit_divides_givenproductfirstreal. (((((ge_representation_real_code_unit_divides_givenproductfirst) = 2 * (ge_balance_positive_unit_divides_givenproductfirstreal) /\ (ge_balance_negative_unit_divides_givenproductfirstreal) = 0) \/ exists ge_signed_half_unit_divides_givenproductfirstrealdecode. (((ge_representation_real_code_unit_divides_givenproductfirst) = 2 * ge_signed_half_unit_divides_givenproductfirstrealdecode + 1 /\ (ge_balance_positive_unit_divides_givenproductfirstreal) = 0) /\ (ge_balance_negative_unit_divides_givenproductfirstreal) = S ge_signed_half_unit_divides_givenproductfirstrealdecode))) /\ ((ge_first_rp_unit_divides_givenproduct) + ge_balance_negative_unit_divides_givenproductfirstreal = (ge_first_rn_unit_divides_givenproduct) + ge_balance_positive_unit_divides_givenproductfirstreal))) /\ (exists ge_balance_positive_unit_divides_givenproductfirstimaginary ge_balance_negative_unit_divides_givenproductfirstimaginary. (((((ge_representation_imaginary_code_unit_divides_givenproductfirst) = 2 * (ge_balance_positive_unit_divides_givenproductfirstimaginary) /\ (ge_balance_negative_unit_divides_givenproductfirstimaginary) = 0) \/ exists ge_signed_half_unit_divides_givenproductfirstimaginarydecode. (((ge_representation_imaginary_code_unit_divides_givenproductfirst) = 2 * ge_signed_half_unit_divides_givenproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_divides_givenproductfirstimaginary) = 0) /\ (ge_balance_negative_unit_divides_givenproductfirstimaginary) = S ge_signed_half_unit_divides_givenproductfirstimaginarydecode))) /\ ((ge_first_ip_unit_divides_givenproduct) + ge_balance_negative_unit_divides_givenproductfirstimaginary = (ge_first_in_unit_divides_givenproduct) + ge_balance_positive_unit_divides_givenproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_divides_givenproductsecond ge_representation_imaginary_code_unit_divides_givenproductsecond. (((gr_quotient_unit_divides_given) = ((ge_representation_real_code_unit_divides_givenproductsecond) + (ge_representation_imaginary_code_unit_divides_givenproductsecond)) * S ((ge_representation_real_code_unit_divides_givenproductsecond) + (ge_representation_imaginary_code_unit_divides_givenproductsecond)) + ((ge_representation_imaginary_code_unit_divides_givenproductsecond) + (ge_representation_imaginary_code_unit_divides_givenproductsecond))) /\ ((exists ge_balance_positive_unit_divides_givenproductsecondreal ge_balance_negative_unit_divides_givenproductsecondreal. (((((ge_representation_real_code_unit_divides_givenproductsecond) = 2 * (ge_balance_positive_unit_divides_givenproductsecondreal) /\ (ge_balance_negative_unit_divides_givenproductsecondreal) = 0) \/ exists ge_signed_half_unit_divides_givenproductsecondrealdecode. (((ge_representation_real_code_unit_divides_givenproductsecond) = 2 * ge_signed_half_unit_divides_givenproductsecondrealdecode + 1 /\ (ge_balance_positive_unit_divides_givenproductsecondreal) = 0) /\ (ge_balance_negative_unit_divides_givenproductsecondreal) = S ge_signed_half_unit_divides_givenproductsecondrealdecode))) /\ ((ge_second_rp_unit_divides_givenproduct) + ge_balance_negative_unit_divides_givenproductsecondreal = (ge_second_rn_unit_divides_givenproduct) + ge_balance_positive_unit_divides_givenproductsecondreal))) /\ (exists ge_balance_positive_unit_divides_givenproductsecondimaginary ge_balance_negative_unit_divides_givenproductsecondimaginary. (((((ge_representation_imaginary_code_unit_divides_givenproductsecond) = 2 * (ge_balance_positive_unit_divides_givenproductsecondimaginary) /\ (ge_balance_negative_unit_divides_givenproductsecondimaginary) = 0) \/ exists ge_signed_half_unit_divides_givenproductsecondimaginarydecode. (((ge_representation_imaginary_code_unit_divides_givenproductsecond) = 2 * ge_signed_half_unit_divides_givenproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_divides_givenproductsecondimaginary) = 0) /\ (ge_balance_negative_unit_divides_givenproductsecondimaginary) = S ge_signed_half_unit_divides_givenproductsecondimaginarydecode))) /\ ((ge_second_ip_unit_divides_givenproduct) + ge_balance_negative_unit_divides_givenproductsecondimaginary = (ge_second_in_unit_divides_givenproduct) + ge_balance_positive_unit_divides_givenproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_divides_givenproductoutput ge_representation_imaginary_code_unit_divides_givenproductoutput. (((u) = ((ge_representation_real_code_unit_divides_givenproductoutput) + (ge_representation_imaginary_code_unit_divides_givenproductoutput)) * S ((ge_representation_real_code_unit_divides_givenproductoutput) + (ge_representation_imaginary_code_unit_divides_givenproductoutput)) + ((ge_representation_imaginary_code_unit_divides_givenproductoutput) + (ge_representation_imaginary_code_unit_divides_givenproductoutput))) /\ ((exists ge_balance_positive_unit_divides_givenproductoutputreal ge_balance_negative_unit_divides_givenproductoutputreal. (((((ge_representation_real_code_unit_divides_givenproductoutput) = 2 * (ge_balance_positive_unit_divides_givenproductoutputreal) /\ (ge_balance_negative_unit_divides_givenproductoutputreal) = 0) \/ exists ge_signed_half_unit_divides_givenproductoutputrealdecode. (((ge_representation_real_code_unit_divides_givenproductoutput) = 2 * ge_signed_half_unit_divides_givenproductoutputrealdecode + 1 /\ (ge_balance_positive_unit_divides_givenproductoutputreal) = 0) /\ (ge_balance_negative_unit_divides_givenproductoutputreal) = S ge_signed_half_unit_divides_givenproductoutputrealdecode))) /\ ((((((((ge_first_rp_unit_divides_givenproduct) * (ge_second_rp_unit_divides_givenproduct))) + (((ge_first_rn_unit_divides_givenproduct) * (ge_second_rn_unit_divides_givenproduct))))) + (((((ge_first_ip_unit_divides_givenproduct) * (ge_second_in_unit_divides_givenproduct))) + (((ge_first_in_unit_divides_givenproduct) * (ge_second_ip_unit_divides_givenproduct))))))) + ge_balance_negative_unit_divides_givenproductoutputreal = (((((((ge_first_rp_unit_divides_givenproduct) * (ge_second_rn_unit_divides_givenproduct))) + (((ge_first_rn_unit_divides_givenproduct) * (ge_second_rp_unit_divides_givenproduct))))) + (((((ge_first_ip_unit_divides_givenproduct) * (ge_second_ip_unit_divides_givenproduct))) + (((ge_first_in_unit_divides_givenproduct) * (ge_second_in_unit_divides_givenproduct))))))) + ge_balance_positive_unit_divides_givenproductoutputreal))) /\ (exists ge_balance_positive_unit_divides_givenproductoutputimaginary ge_balance_negative_unit_divides_givenproductoutputimaginary. (((((ge_representation_imaginary_code_unit_divides_givenproductoutput) = 2 * (ge_balance_positive_unit_divides_givenproductoutputimaginary) /\ (ge_balance_negative_unit_divides_givenproductoutputimaginary) = 0) \/ exists ge_signed_half_unit_divides_givenproductoutputimaginarydecode. (((ge_representation_imaginary_code_unit_divides_givenproductoutput) = 2 * ge_signed_half_unit_divides_givenproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_divides_givenproductoutputimaginary) = 0) /\ (ge_balance_negative_unit_divides_givenproductoutputimaginary) = S ge_signed_half_unit_divides_givenproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_divides_givenproduct) * (ge_second_ip_unit_divides_givenproduct))) + (((ge_first_rn_unit_divides_givenproduct) * (ge_second_in_unit_divides_givenproduct))))) + (((((ge_first_ip_unit_divides_givenproduct) * (ge_second_rp_unit_divides_givenproduct))) + (((ge_first_in_unit_divides_givenproduct) * (ge_second_rn_unit_divides_givenproduct))))))) + ge_balance_negative_unit_divides_givenproductoutputimaginary = (((((((ge_first_rp_unit_divides_givenproduct) * (ge_second_in_unit_divides_givenproduct))) + (((ge_first_rn_unit_divides_givenproduct) * (ge_second_ip_unit_divides_givenproduct))))) + (((((ge_first_ip_unit_divides_givenproduct) * (ge_second_rn_unit_divides_givenproduct))) + (((ge_first_in_unit_divides_givenproduct) * (ge_second_rp_unit_divides_givenproduct))))))) + ge_balance_positive_unit_divides_givenproductoutputimaginary)))))))))) -> (exists gr_inverse_unit_dividend. (exists ge_first_rp_unit_dividendidentity ge_first_rn_unit_dividendidentity ge_first_ip_unit_dividendidentity ge_first_in_unit_dividendidentity ge_second_rp_unit_dividendidentity ge_second_rn_unit_dividendidentity ge_second_ip_unit_dividendidentity ge_second_in_unit_dividendidentity. ((exists ge_representation_real_code_unit_dividendidentityfirst ge_representation_imaginary_code_unit_dividendidentityfirst. (((u) = ((ge_representation_real_code_unit_dividendidentityfirst) + (ge_representation_imaginary_code_unit_dividendidentityfirst)) * S ((ge_representation_real_code_unit_dividendidentityfirst) + (ge_representation_imaginary_code_unit_dividendidentityfirst)) + ((ge_representation_imaginary_code_unit_dividendidentityfirst) + (ge_representation_imaginary_code_unit_dividendidentityfirst))) /\ ((exists ge_balance_positive_unit_dividendidentityfirstreal ge_balance_negative_unit_dividendidentityfirstreal. (((((ge_representation_real_code_unit_dividendidentityfirst) = 2 * (ge_balance_positive_unit_dividendidentityfirstreal) /\ (ge_balance_negative_unit_dividendidentityfirstreal) = 0) \/ exists ge_signed_half_unit_dividendidentityfirstrealdecode. (((ge_representation_real_code_unit_dividendidentityfirst) = 2 * ge_signed_half_unit_dividendidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_dividendidentityfirstreal) = 0) /\ (ge_balance_negative_unit_dividendidentityfirstreal) = S ge_signed_half_unit_dividendidentityfirstrealdecode))) /\ ((ge_first_rp_unit_dividendidentity) + ge_balance_negative_unit_dividendidentityfirstreal = (ge_first_rn_unit_dividendidentity) + ge_balance_positive_unit_dividendidentityfirstreal))) /\ (exists ge_balance_positive_unit_dividendidentityfirstimaginary ge_balance_negative_unit_dividendidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_dividendidentityfirst) = 2 * (ge_balance_positive_unit_dividendidentityfirstimaginary) /\ (ge_balance_negative_unit_dividendidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_dividendidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_dividendidentityfirst) = 2 * ge_signed_half_unit_dividendidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_dividendidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_dividendidentityfirstimaginary) = S ge_signed_half_unit_dividendidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_dividendidentity) + ge_balance_negative_unit_dividendidentityfirstimaginary = (ge_first_in_unit_dividendidentity) + ge_balance_positive_unit_dividendidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_dividendidentitysecond ge_representation_imaginary_code_unit_dividendidentitysecond. (((gr_inverse_unit_dividend) = ((ge_representation_real_code_unit_dividendidentitysecond) + (ge_representation_imaginary_code_unit_dividendidentitysecond)) * S ((ge_representation_real_code_unit_dividendidentitysecond) + (ge_representation_imaginary_code_unit_dividendidentitysecond)) + ((ge_representation_imaginary_code_unit_dividendidentitysecond) + (ge_representation_imaginary_code_unit_dividendidentitysecond))) /\ ((exists ge_balance_positive_unit_dividendidentitysecondreal ge_balance_negative_unit_dividendidentitysecondreal. (((((ge_representation_real_code_unit_dividendidentitysecond) = 2 * (ge_balance_positive_unit_dividendidentitysecondreal) /\ (ge_balance_negative_unit_dividendidentitysecondreal) = 0) \/ exists ge_signed_half_unit_dividendidentitysecondrealdecode. (((ge_representation_real_code_unit_dividendidentitysecond) = 2 * ge_signed_half_unit_dividendidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_dividendidentitysecondreal) = 0) /\ (ge_balance_negative_unit_dividendidentitysecondreal) = S ge_signed_half_unit_dividendidentitysecondrealdecode))) /\ ((ge_second_rp_unit_dividendidentity) + ge_balance_negative_unit_dividendidentitysecondreal = (ge_second_rn_unit_dividendidentity) + ge_balance_positive_unit_dividendidentitysecondreal))) /\ (exists ge_balance_positive_unit_dividendidentitysecondimaginary ge_balance_negative_unit_dividendidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_dividendidentitysecond) = 2 * (ge_balance_positive_unit_dividendidentitysecondimaginary) /\ (ge_balance_negative_unit_dividendidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_dividendidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_dividendidentitysecond) = 2 * ge_signed_half_unit_dividendidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_dividendidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_dividendidentitysecondimaginary) = S ge_signed_half_unit_dividendidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_dividendidentity) + ge_balance_negative_unit_dividendidentitysecondimaginary = (ge_second_in_unit_dividendidentity) + ge_balance_positive_unit_dividendidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_dividendidentityoutput ge_representation_imaginary_code_unit_dividendidentityoutput. (((6) = ((ge_representation_real_code_unit_dividendidentityoutput) + (ge_representation_imaginary_code_unit_dividendidentityoutput)) * S ((ge_representation_real_code_unit_dividendidentityoutput) + (ge_representation_imaginary_code_unit_dividendidentityoutput)) + ((ge_representation_imaginary_code_unit_dividendidentityoutput) + (ge_representation_imaginary_code_unit_dividendidentityoutput))) /\ ((exists ge_balance_positive_unit_dividendidentityoutputreal ge_balance_negative_unit_dividendidentityoutputreal. (((((ge_representation_real_code_unit_dividendidentityoutput) = 2 * (ge_balance_positive_unit_dividendidentityoutputreal) /\ (ge_balance_negative_unit_dividendidentityoutputreal) = 0) \/ exists ge_signed_half_unit_dividendidentityoutputrealdecode. (((ge_representation_real_code_unit_dividendidentityoutput) = 2 * ge_signed_half_unit_dividendidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_dividendidentityoutputreal) = 0) /\ (ge_balance_negative_unit_dividendidentityoutputreal) = S ge_signed_half_unit_dividendidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_dividendidentity) * (ge_second_rp_unit_dividendidentity))) + (((ge_first_rn_unit_dividendidentity) * (ge_second_rn_unit_dividendidentity))))) + (((((ge_first_ip_unit_dividendidentity) * (ge_second_in_unit_dividendidentity))) + (((ge_first_in_unit_dividendidentity) * (ge_second_ip_unit_dividendidentity))))))) + ge_balance_negative_unit_dividendidentityoutputreal = (((((((ge_first_rp_unit_dividendidentity) * (ge_second_rn_unit_dividendidentity))) + (((ge_first_rn_unit_dividendidentity) * (ge_second_rp_unit_dividendidentity))))) + (((((ge_first_ip_unit_dividendidentity) * (ge_second_ip_unit_dividendidentity))) + (((ge_first_in_unit_dividendidentity) * (ge_second_in_unit_dividendidentity))))))) + ge_balance_positive_unit_dividendidentityoutputreal))) /\ (exists ge_balance_positive_unit_dividendidentityoutputimaginary ge_balance_negative_unit_dividendidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_dividendidentityoutput) = 2 * (ge_balance_positive_unit_dividendidentityoutputimaginary) /\ (ge_balance_negative_unit_dividendidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_dividendidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_dividendidentityoutput) = 2 * ge_signed_half_unit_dividendidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_dividendidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_dividendidentityoutputimaginary) = S ge_signed_half_unit_dividendidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_dividendidentity) * (ge_second_ip_unit_dividendidentity))) + (((ge_first_rn_unit_dividendidentity) * (ge_second_in_unit_dividendidentity))))) + (((((ge_first_ip_unit_dividendidentity) * (ge_second_rp_unit_dividendidentity))) + (((ge_first_in_unit_dividendidentity) * (ge_second_rn_unit_dividendidentity))))))) + ge_balance_negative_unit_dividendidentityoutputimaginary = (((((((ge_first_rp_unit_dividendidentity) * (ge_second_in_unit_dividendidentity))) + (((ge_first_rn_unit_dividendidentity) * (ge_second_ip_unit_dividendidentity))))) + (((((ge_first_ip_unit_dividendidentity) * (ge_second_rn_unit_dividendidentity))) + (((ge_first_in_unit_dividendidentity) * (ge_second_rp_unit_dividendidentity))))))) + ge_balance_positive_unit_dividendidentityoutputimaginary)))))))))) -> (exists gr_inverse_unit_divisor_result. (exists ge_first_rp_unit_divisor_resultidentity ge_first_rn_unit_divisor_resultidentity ge_first_ip_unit_divisor_resultidentity ge_first_in_unit_divisor_resultidentity ge_second_rp_unit_divisor_resultidentity ge_second_rn_unit_divisor_resultidentity ge_second_ip_unit_divisor_resultidentity ge_second_in_unit_divisor_resultidentity. ((exists ge_representation_real_code_unit_divisor_resultidentityfirst ge_representation_imaginary_code_unit_divisor_resultidentityfirst. (((d) = ((ge_representation_real_code_unit_divisor_resultidentityfirst) + (ge_representation_imaginary_code_unit_divisor_resultidentityfirst)) * S ((ge_representation_real_code_unit_divisor_resultidentityfirst) + (ge_representation_imaginary_code_unit_divisor_resultidentityfirst)) + ((ge_representation_imaginary_code_unit_divisor_resultidentityfirst) + (ge_representation_imaginary_code_unit_divisor_resultidentityfirst))) /\ ((exists ge_balance_positive_unit_divisor_resultidentityfirstreal ge_balance_negative_unit_divisor_resultidentityfirstreal. (((((ge_representation_real_code_unit_divisor_resultidentityfirst) = 2 * (ge_balance_positive_unit_divisor_resultidentityfirstreal) /\ (ge_balance_negative_unit_divisor_resultidentityfirstreal) = 0) \/ exists ge_signed_half_unit_divisor_resultidentityfirstrealdecode. (((ge_representation_real_code_unit_divisor_resultidentityfirst) = 2 * ge_signed_half_unit_divisor_resultidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_divisor_resultidentityfirstreal) = 0) /\ (ge_balance_negative_unit_divisor_resultidentityfirstreal) = S ge_signed_half_unit_divisor_resultidentityfirstrealdecode))) /\ ((ge_first_rp_unit_divisor_resultidentity) + ge_balance_negative_unit_divisor_resultidentityfirstreal = (ge_first_rn_unit_divisor_resultidentity) + ge_balance_positive_unit_divisor_resultidentityfirstreal))) /\ (exists ge_balance_positive_unit_divisor_resultidentityfirstimaginary ge_balance_negative_unit_divisor_resultidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_divisor_resultidentityfirst) = 2 * (ge_balance_positive_unit_divisor_resultidentityfirstimaginary) /\ (ge_balance_negative_unit_divisor_resultidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_divisor_resultidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_divisor_resultidentityfirst) = 2 * ge_signed_half_unit_divisor_resultidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_divisor_resultidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_divisor_resultidentityfirstimaginary) = S ge_signed_half_unit_divisor_resultidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_divisor_resultidentity) + ge_balance_negative_unit_divisor_resultidentityfirstimaginary = (ge_first_in_unit_divisor_resultidentity) + ge_balance_positive_unit_divisor_resultidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_divisor_resultidentitysecond ge_representation_imaginary_code_unit_divisor_resultidentitysecond. (((gr_inverse_unit_divisor_result) = ((ge_representation_real_code_unit_divisor_resultidentitysecond) + (ge_representation_imaginary_code_unit_divisor_resultidentitysecond)) * S ((ge_representation_real_code_unit_divisor_resultidentitysecond) + (ge_representation_imaginary_code_unit_divisor_resultidentitysecond)) + ((ge_representation_imaginary_code_unit_divisor_resultidentitysecond) + (ge_representation_imaginary_code_unit_divisor_resultidentitysecond))) /\ ((exists ge_balance_positive_unit_divisor_resultidentitysecondreal ge_balance_negative_unit_divisor_resultidentitysecondreal. (((((ge_representation_real_code_unit_divisor_resultidentitysecond) = 2 * (ge_balance_positive_unit_divisor_resultidentitysecondreal) /\ (ge_balance_negative_unit_divisor_resultidentitysecondreal) = 0) \/ exists ge_signed_half_unit_divisor_resultidentitysecondrealdecode. (((ge_representation_real_code_unit_divisor_resultidentitysecond) = 2 * ge_signed_half_unit_divisor_resultidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_divisor_resultidentitysecondreal) = 0) /\ (ge_balance_negative_unit_divisor_resultidentitysecondreal) = S ge_signed_half_unit_divisor_resultidentitysecondrealdecode))) /\ ((ge_second_rp_unit_divisor_resultidentity) + ge_balance_negative_unit_divisor_resultidentitysecondreal = (ge_second_rn_unit_divisor_resultidentity) + ge_balance_positive_unit_divisor_resultidentitysecondreal))) /\ (exists ge_balance_positive_unit_divisor_resultidentitysecondimaginary ge_balance_negative_unit_divisor_resultidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_divisor_resultidentitysecond) = 2 * (ge_balance_positive_unit_divisor_resultidentitysecondimaginary) /\ (ge_balance_negative_unit_divisor_resultidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_divisor_resultidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_divisor_resultidentitysecond) = 2 * ge_signed_half_unit_divisor_resultidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_divisor_resultidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_divisor_resultidentitysecondimaginary) = S ge_signed_half_unit_divisor_resultidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_divisor_resultidentity) + ge_balance_negative_unit_divisor_resultidentitysecondimaginary = (ge_second_in_unit_divisor_resultidentity) + ge_balance_positive_unit_divisor_resultidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_divisor_resultidentityoutput ge_representation_imaginary_code_unit_divisor_resultidentityoutput. (((6) = ((ge_representation_real_code_unit_divisor_resultidentityoutput) + (ge_representation_imaginary_code_unit_divisor_resultidentityoutput)) * S ((ge_representation_real_code_unit_divisor_resultidentityoutput) + (ge_representation_imaginary_code_unit_divisor_resultidentityoutput)) + ((ge_representation_imaginary_code_unit_divisor_resultidentityoutput) + (ge_representation_imaginary_code_unit_divisor_resultidentityoutput))) /\ ((exists ge_balance_positive_unit_divisor_resultidentityoutputreal ge_balance_negative_unit_divisor_resultidentityoutputreal. (((((ge_representation_real_code_unit_divisor_resultidentityoutput) = 2 * (ge_balance_positive_unit_divisor_resultidentityoutputreal) /\ (ge_balance_negative_unit_divisor_resultidentityoutputreal) = 0) \/ exists ge_signed_half_unit_divisor_resultidentityoutputrealdecode. (((ge_representation_real_code_unit_divisor_resultidentityoutput) = 2 * ge_signed_half_unit_divisor_resultidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_divisor_resultidentityoutputreal) = 0) /\ (ge_balance_negative_unit_divisor_resultidentityoutputreal) = S ge_signed_half_unit_divisor_resultidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_divisor_resultidentity) * (ge_second_rp_unit_divisor_resultidentity))) + (((ge_first_rn_unit_divisor_resultidentity) * (ge_second_rn_unit_divisor_resultidentity))))) + (((((ge_first_ip_unit_divisor_resultidentity) * (ge_second_in_unit_divisor_resultidentity))) + (((ge_first_in_unit_divisor_resultidentity) * (ge_second_ip_unit_divisor_resultidentity))))))) + ge_balance_negative_unit_divisor_resultidentityoutputreal = (((((((ge_first_rp_unit_divisor_resultidentity) * (ge_second_rn_unit_divisor_resultidentity))) + (((ge_first_rn_unit_divisor_resultidentity) * (ge_second_rp_unit_divisor_resultidentity))))) + (((((ge_first_ip_unit_divisor_resultidentity) * (ge_second_ip_unit_divisor_resultidentity))) + (((ge_first_in_unit_divisor_resultidentity) * (ge_second_in_unit_divisor_resultidentity))))))) + ge_balance_positive_unit_divisor_resultidentityoutputreal))) /\ (exists ge_balance_positive_unit_divisor_resultidentityoutputimaginary ge_balance_negative_unit_divisor_resultidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_divisor_resultidentityoutput) = 2 * (ge_balance_positive_unit_divisor_resultidentityoutputimaginary) /\ (ge_balance_negative_unit_divisor_resultidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_divisor_resultidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_divisor_resultidentityoutput) = 2 * ge_signed_half_unit_divisor_resultidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_divisor_resultidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_divisor_resultidentityoutputimaginary) = S ge_signed_half_unit_divisor_resultidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_divisor_resultidentity) * (ge_second_ip_unit_divisor_resultidentity))) + (((ge_first_rn_unit_divisor_resultidentity) * (ge_second_in_unit_divisor_resultidentity))))) + (((((ge_first_ip_unit_divisor_resultidentity) * (ge_second_rp_unit_divisor_resultidentity))) + (((ge_first_in_unit_divisor_resultidentity) * (ge_second_rn_unit_divisor_resultidentity))))))) + ge_balance_negative_unit_divisor_resultidentityoutputimaginary = (((((((ge_first_rp_unit_divisor_resultidentity) * (ge_second_in_unit_divisor_resultidentity))) + (((ge_first_rn_unit_divisor_resultidentity) * (ge_second_ip_unit_divisor_resultidentity))))) + (((((ge_first_ip_unit_divisor_resultidentity) * (ge_second_rn_unit_divisor_resultidentity))) + (((ge_first_in_unit_divisor_resultidentity) * (ge_second_rp_unit_divisor_resultidentity))))))) + ge_balance_positive_unit_divisor_resultidentityoutputimaginary))))))))))