gaussian_prime_is_irreducible

Exact expanded first-order arithmetic statement

forall p. (((exists ge_real_positive_prime_irreducible_sourcecarrier ge_real_negative_prime_irreducible_sourcecarrier ge_imaginary_positive_prime_irreducible_sourcecarrier ge_imaginary_negative_prime_irreducible_sourcecarrier. (exists ge_real_code_prime_irreducible_sourcecarrierdecode ge_imaginary_code_prime_irreducible_sourcecarrierdecode. (((p) = ((ge_real_code_prime_irreducible_sourcecarrierdecode) + (ge_imaginary_code_prime_irreducible_sourcecarrierdecode)) * S ((ge_real_code_prime_irreducible_sourcecarrierdecode) + (ge_imaginary_code_prime_irreducible_sourcecarrierdecode)) + ((ge_imaginary_code_prime_irreducible_sourcecarrierdecode) + (ge_imaginary_code_prime_irreducible_sourcecarrierdecode))) /\ (((((ge_real_code_prime_irreducible_sourcecarrierdecode) = 2 * (ge_real_positive_prime_irreducible_sourcecarrier) /\ (ge_real_negative_prime_irreducible_sourcecarrier) = 0) \/ exists ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_real. (((ge_real_code_prime_irreducible_sourcecarrierdecode) = 2 * ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_real + 1 /\ (ge_real_positive_prime_irreducible_sourcecarrier) = 0) /\ (ge_real_negative_prime_irreducible_sourcecarrier) = S ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_irreducible_sourcecarrierdecode) = 2 * (ge_imaginary_positive_prime_irreducible_sourcecarrier) /\ (ge_imaginary_negative_prime_irreducible_sourcecarrier) = 0) \/ exists ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_imaginary. (((ge_imaginary_code_prime_irreducible_sourcecarrierdecode) = 2 * ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_irreducible_sourcecarrier) = 0) /\ (ge_imaginary_negative_prime_irreducible_sourcecarrier) = S ge_signed_half_ge_prime_irreducible_sourcecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_prime_irreducible_sourcenonunit. (exists ge_first_rp_prime_irreducible_sourcenonunitidentity ge_first_rn_prime_irreducible_sourcenonunitidentity ge_first_ip_prime_irreducible_sourcenonunitidentity ge_first_in_prime_irreducible_sourcenonunitidentity ge_second_rp_prime_irreducible_sourcenonunitidentity ge_second_rn_prime_irreducible_sourcenonunitidentity ge_second_ip_prime_irreducible_sourcenonunitidentity ge_second_in_prime_irreducible_sourcenonunitidentity. ((exists ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst. (((p) = ((ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst)) * S ((ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstreal ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstreal. (((((ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstreal) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourcenonunitidentityfirst) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstreal) = S ge_signed_half_prime_irreducible_sourcenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourcenonunitidentity) + ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstreal = (ge_first_rn_prime_irreducible_sourcenonunitidentity) + ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstimaginary ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityfirst) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstimaginary) = S ge_signed_half_prime_irreducible_sourcenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourcenonunitidentity) + ge_balance_negative_prime_irreducible_sourcenonunitidentityfirstimaginary = (ge_first_in_prime_irreducible_sourcenonunitidentity) + ge_balance_positive_prime_irreducible_sourcenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond. (((gr_inverse_prime_irreducible_sourcenonunit) = ((ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond)) * S ((ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondreal ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondreal. (((((ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondreal) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourcenonunitidentitysecond) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondreal) = S ge_signed_half_prime_irreducible_sourcenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourcenonunitidentity) + ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondreal = (ge_second_rn_prime_irreducible_sourcenonunitidentity) + ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondimaginary ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentitysecond) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondimaginary) = S ge_signed_half_prime_irreducible_sourcenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourcenonunitidentity) + ge_balance_negative_prime_irreducible_sourcenonunitidentitysecondimaginary = (ge_second_in_prime_irreducible_sourcenonunitidentity) + ge_balance_positive_prime_irreducible_sourcenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput)) * S ((ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputreal ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputreal. (((((ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputreal) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourcenonunitidentityoutput) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputreal) = S ge_signed_half_prime_irreducible_sourcenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcenonunitidentity) * (ge_second_rp_prime_irreducible_sourcenonunitidentity))) + (((ge_first_rn_prime_irreducible_sourcenonunitidentity) * (ge_second_rn_prime_irreducible_sourcenonunitidentity))))) + (((((ge_first_ip_prime_irreducible_sourcenonunitidentity) * (ge_second_in_prime_irreducible_sourcenonunitidentity))) + (((ge_first_in_prime_irreducible_sourcenonunitidentity) * (ge_second_ip_prime_irreducible_sourcenonunitidentity))))))) + ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputreal = (((((((ge_first_rp_prime_irreducible_sourcenonunitidentity) * (ge_second_rn_prime_irreducible_sourcenonunitidentity))) + (((ge_first_rn_prime_irreducible_sourcenonunitidentity) * (ge_second_rp_prime_irreducible_sourcenonunitidentity))))) + (((((ge_first_ip_prime_irreducible_sourcenonunitidentity) * (ge_second_ip_prime_irreducible_sourcenonunitidentity))) + (((ge_first_in_prime_irreducible_sourcenonunitidentity) * (ge_second_in_prime_irreducible_sourcenonunitidentity))))))) + ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputimaginary ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcenonunitidentityoutput) = 2 * ge_signed_half_prime_irreducible_sourcenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputimaginary) = S ge_signed_half_prime_irreducible_sourcenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcenonunitidentity) * (ge_second_ip_prime_irreducible_sourcenonunitidentity))) + (((ge_first_rn_prime_irreducible_sourcenonunitidentity) * (ge_second_in_prime_irreducible_sourcenonunitidentity))))) + (((((ge_first_ip_prime_irreducible_sourcenonunitidentity) * (ge_second_rp_prime_irreducible_sourcenonunitidentity))) + (((ge_first_in_prime_irreducible_sourcenonunitidentity) * (ge_second_rn_prime_irreducible_sourcenonunitidentity))))))) + ge_balance_negative_prime_irreducible_sourcenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourcenonunitidentity) * (ge_second_in_prime_irreducible_sourcenonunitidentity))) + (((ge_first_rn_prime_irreducible_sourcenonunitidentity) * (ge_second_ip_prime_irreducible_sourcenonunitidentity))))) + (((((ge_first_ip_prime_irreducible_sourcenonunitidentity) * (ge_second_rn_prime_irreducible_sourcenonunitidentity))) + (((ge_first_in_prime_irreducible_sourcenonunitidentity) * (ge_second_rp_prime_irreducible_sourcenonunitidentity))))))) + ge_balance_positive_prime_irreducible_sourcenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_irreducible_source gr_second_factor_prime_irreducible_source gr_product_prime_irreducible_source. (exists ge_first_rp_prime_irreducible_sourceproduct ge_first_rn_prime_irreducible_sourceproduct ge_first_ip_prime_irreducible_sourceproduct ge_first_in_prime_irreducible_sourceproduct ge_second_rp_prime_irreducible_sourceproduct ge_second_rn_prime_irreducible_sourceproduct ge_second_ip_prime_irreducible_sourceproduct ge_second_in_prime_irreducible_sourceproduct. ((exists ge_representation_real_code_prime_irreducible_sourceproductfirst ge_representation_imaginary_code_prime_irreducible_sourceproductfirst. (((gr_first_factor_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourceproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourceproductfirst)) * S ((ge_representation_real_code_prime_irreducible_sourceproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourceproductfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourceproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourceproductfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourceproductfirstreal ge_balance_negative_prime_irreducible_sourceproductfirstreal. (((((ge_representation_real_code_prime_irreducible_sourceproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourceproductfirstreal) /\ (ge_balance_negative_prime_irreducible_sourceproductfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourceproductfirst) = 2 * ge_signed_half_prime_irreducible_sourceproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductfirstreal) = S ge_signed_half_prime_irreducible_sourceproductfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourceproduct) + ge_balance_negative_prime_irreducible_sourceproductfirstreal = (ge_first_rn_prime_irreducible_sourceproduct) + ge_balance_positive_prime_irreducible_sourceproductfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourceproductfirstimaginary ge_balance_negative_prime_irreducible_sourceproductfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourceproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourceproductfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourceproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourceproductfirst) = 2 * ge_signed_half_prime_irreducible_sourceproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductfirstimaginary) = S ge_signed_half_prime_irreducible_sourceproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourceproduct) + ge_balance_negative_prime_irreducible_sourceproductfirstimaginary = (ge_first_in_prime_irreducible_sourceproduct) + ge_balance_positive_prime_irreducible_sourceproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourceproductsecond ge_representation_imaginary_code_prime_irreducible_sourceproductsecond. (((gr_second_factor_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourceproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourceproductsecond)) * S ((ge_representation_real_code_prime_irreducible_sourceproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourceproductsecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourceproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourceproductsecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourceproductsecondreal ge_balance_negative_prime_irreducible_sourceproductsecondreal. (((((ge_representation_real_code_prime_irreducible_sourceproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourceproductsecondreal) /\ (ge_balance_negative_prime_irreducible_sourceproductsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductsecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourceproductsecond) = 2 * ge_signed_half_prime_irreducible_sourceproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductsecondreal) = S ge_signed_half_prime_irreducible_sourceproductsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourceproduct) + ge_balance_negative_prime_irreducible_sourceproductsecondreal = (ge_second_rn_prime_irreducible_sourceproduct) + ge_balance_positive_prime_irreducible_sourceproductsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourceproductsecondimaginary ge_balance_negative_prime_irreducible_sourceproductsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourceproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourceproductsecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourceproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourceproductsecond) = 2 * ge_signed_half_prime_irreducible_sourceproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductsecondimaginary) = S ge_signed_half_prime_irreducible_sourceproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourceproduct) + ge_balance_negative_prime_irreducible_sourceproductsecondimaginary = (ge_second_in_prime_irreducible_sourceproduct) + ge_balance_positive_prime_irreducible_sourceproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourceproductoutput ge_representation_imaginary_code_prime_irreducible_sourceproductoutput. (((gr_product_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourceproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourceproductoutput)) * S ((ge_representation_real_code_prime_irreducible_sourceproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourceproductoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourceproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourceproductoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourceproductoutputreal ge_balance_negative_prime_irreducible_sourceproductoutputreal. (((((ge_representation_real_code_prime_irreducible_sourceproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourceproductoutputreal) /\ (ge_balance_negative_prime_irreducible_sourceproductoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourceproductoutput) = 2 * ge_signed_half_prime_irreducible_sourceproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductoutputreal) = S ge_signed_half_prime_irreducible_sourceproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourceproduct) * (ge_second_rp_prime_irreducible_sourceproduct))) + (((ge_first_rn_prime_irreducible_sourceproduct) * (ge_second_rn_prime_irreducible_sourceproduct))))) + (((((ge_first_ip_prime_irreducible_sourceproduct) * (ge_second_in_prime_irreducible_sourceproduct))) + (((ge_first_in_prime_irreducible_sourceproduct) * (ge_second_ip_prime_irreducible_sourceproduct))))))) + ge_balance_negative_prime_irreducible_sourceproductoutputreal = (((((((ge_first_rp_prime_irreducible_sourceproduct) * (ge_second_rn_prime_irreducible_sourceproduct))) + (((ge_first_rn_prime_irreducible_sourceproduct) * (ge_second_rp_prime_irreducible_sourceproduct))))) + (((((ge_first_ip_prime_irreducible_sourceproduct) * (ge_second_ip_prime_irreducible_sourceproduct))) + (((ge_first_in_prime_irreducible_sourceproduct) * (ge_second_in_prime_irreducible_sourceproduct))))))) + ge_balance_positive_prime_irreducible_sourceproductoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourceproductoutputimaginary ge_balance_negative_prime_irreducible_sourceproductoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourceproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourceproductoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourceproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourceproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourceproductoutput) = 2 * ge_signed_half_prime_irreducible_sourceproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourceproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourceproductoutputimaginary) = S ge_signed_half_prime_irreducible_sourceproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourceproduct) * (ge_second_ip_prime_irreducible_sourceproduct))) + (((ge_first_rn_prime_irreducible_sourceproduct) * (ge_second_in_prime_irreducible_sourceproduct))))) + (((((ge_first_ip_prime_irreducible_sourceproduct) * (ge_second_rp_prime_irreducible_sourceproduct))) + (((ge_first_in_prime_irreducible_sourceproduct) * (ge_second_rn_prime_irreducible_sourceproduct))))))) + ge_balance_negative_prime_irreducible_sourceproductoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourceproduct) * (ge_second_in_prime_irreducible_sourceproduct))) + (((ge_first_rn_prime_irreducible_sourceproduct) * (ge_second_ip_prime_irreducible_sourceproduct))))) + (((((ge_first_ip_prime_irreducible_sourceproduct) * (ge_second_rn_prime_irreducible_sourceproduct))) + (((ge_first_in_prime_irreducible_sourceproduct) * (ge_second_rp_prime_irreducible_sourceproduct))))))) + ge_balance_positive_prime_irreducible_sourceproductoutputimaginary))))))))) -> (exists gr_quotient_prime_irreducible_sourcedivisor. (exists ge_first_rp_prime_irreducible_sourcedivisorproduct ge_first_rn_prime_irreducible_sourcedivisorproduct ge_first_ip_prime_irreducible_sourcedivisorproduct ge_first_in_prime_irreducible_sourcedivisorproduct ge_second_rp_prime_irreducible_sourcedivisorproduct ge_second_rn_prime_irreducible_sourcedivisorproduct ge_second_ip_prime_irreducible_sourcedivisorproduct ge_second_in_prime_irreducible_sourcedivisorproduct. ((exists ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst. (((p) = ((ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst)) * S ((ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourcedivisorproductfirstreal ge_balance_negative_prime_irreducible_sourcedivisorproductfirstreal. (((((ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductfirstreal) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourcedivisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductfirstreal) = S ge_signed_half_prime_irreducible_sourcedivisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourcedivisorproduct) + ge_balance_negative_prime_irreducible_sourcedivisorproductfirstreal = (ge_first_rn_prime_irreducible_sourcedivisorproduct) + ge_balance_positive_prime_irreducible_sourcedivisorproductfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcedivisorproductfirstimaginary ge_balance_negative_prime_irreducible_sourcedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductfirstimaginary) = S ge_signed_half_prime_irreducible_sourcedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourcedivisorproduct) + ge_balance_negative_prime_irreducible_sourcedivisorproductfirstimaginary = (ge_first_in_prime_irreducible_sourcedivisorproduct) + ge_balance_positive_prime_irreducible_sourcedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond. (((gr_quotient_prime_irreducible_sourcedivisor) = ((ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond)) * S ((ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourcedivisorproductsecondreal ge_balance_negative_prime_irreducible_sourcedivisorproductsecondreal. (((((ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductsecondreal) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductsecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourcedivisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductsecondreal) = S ge_signed_half_prime_irreducible_sourcedivisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourcedivisorproduct) + ge_balance_negative_prime_irreducible_sourcedivisorproductsecondreal = (ge_second_rn_prime_irreducible_sourcedivisorproduct) + ge_balance_positive_prime_irreducible_sourcedivisorproductsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcedivisorproductsecondimaginary ge_balance_negative_prime_irreducible_sourcedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductsecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductsecondimaginary) = S ge_signed_half_prime_irreducible_sourcedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourcedivisorproduct) + ge_balance_negative_prime_irreducible_sourcedivisorproductsecondimaginary = (ge_second_in_prime_irreducible_sourcedivisorproduct) + ge_balance_positive_prime_irreducible_sourcedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput. (((gr_product_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput)) * S ((ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourcedivisorproductoutputreal ge_balance_negative_prime_irreducible_sourcedivisorproductoutputreal. (((((ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductoutputreal) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourcedivisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductoutputreal) = S ge_signed_half_prime_irreducible_sourcedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcedivisorproduct) * (ge_second_rp_prime_irreducible_sourcedivisorproduct))) + (((ge_first_rn_prime_irreducible_sourcedivisorproduct) * (ge_second_rn_prime_irreducible_sourcedivisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcedivisorproduct) * (ge_second_in_prime_irreducible_sourcedivisorproduct))) + (((ge_first_in_prime_irreducible_sourcedivisorproduct) * (ge_second_ip_prime_irreducible_sourcedivisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcedivisorproductoutputreal = (((((((ge_first_rp_prime_irreducible_sourcedivisorproduct) * (ge_second_rn_prime_irreducible_sourcedivisorproduct))) + (((ge_first_rn_prime_irreducible_sourcedivisorproduct) * (ge_second_rp_prime_irreducible_sourcedivisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcedivisorproduct) * (ge_second_ip_prime_irreducible_sourcedivisorproduct))) + (((ge_first_in_prime_irreducible_sourcedivisorproduct) * (ge_second_in_prime_irreducible_sourcedivisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcedivisorproductoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcedivisorproductoutputimaginary ge_balance_negative_prime_irreducible_sourcedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcedivisorproductoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcedivisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcedivisorproductoutputimaginary) = S ge_signed_half_prime_irreducible_sourcedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcedivisorproduct) * (ge_second_ip_prime_irreducible_sourcedivisorproduct))) + (((ge_first_rn_prime_irreducible_sourcedivisorproduct) * (ge_second_in_prime_irreducible_sourcedivisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcedivisorproduct) * (ge_second_rp_prime_irreducible_sourcedivisorproduct))) + (((ge_first_in_prime_irreducible_sourcedivisorproduct) * (ge_second_rn_prime_irreducible_sourcedivisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcedivisorproductoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourcedivisorproduct) * (ge_second_in_prime_irreducible_sourcedivisorproduct))) + (((ge_first_rn_prime_irreducible_sourcedivisorproduct) * (ge_second_ip_prime_irreducible_sourcedivisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcedivisorproduct) * (ge_second_rn_prime_irreducible_sourcedivisorproduct))) + (((ge_first_in_prime_irreducible_sourcedivisorproduct) * (ge_second_rp_prime_irreducible_sourcedivisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_prime_irreducible_sourcefirst_divisor. (exists ge_first_rp_prime_irreducible_sourcefirst_divisorproduct ge_first_rn_prime_irreducible_sourcefirst_divisorproduct ge_first_ip_prime_irreducible_sourcefirst_divisorproduct ge_first_in_prime_irreducible_sourcefirst_divisorproduct ge_second_rp_prime_irreducible_sourcefirst_divisorproduct ge_second_rn_prime_irreducible_sourcefirst_divisorproduct ge_second_ip_prime_irreducible_sourcefirst_divisorproduct ge_second_in_prime_irreducible_sourcefirst_divisorproduct. ((exists ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst. (((p) = ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst)) * S ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstreal ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstreal. (((((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstreal) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstreal) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstreal = (ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstimaginary ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstimaginary) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductfirstimaginary = (ge_first_in_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond. (((gr_quotient_prime_irreducible_sourcefirst_divisor) = ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond)) * S ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondreal ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondreal. (((((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondreal) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondreal) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondreal = (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondimaginary ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondimaginary) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductsecondimaginary = (ge_second_in_prime_irreducible_sourcefirst_divisorproduct) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput. (((gr_first_factor_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput)) * S ((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputreal ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputreal. (((((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputreal) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourcefirst_divisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputreal) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rp_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_in_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_ip_prime_irreducible_sourcefirst_divisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputreal = (((((((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rp_prime_irreducible_sourcefirst_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_ip_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_in_prime_irreducible_sourcefirst_divisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputimaginary ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcefirst_divisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputimaginary) = S ge_signed_half_prime_irreducible_sourcefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_ip_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_in_prime_irreducible_sourcefirst_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rp_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcefirst_divisorproductoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_in_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_ip_prime_irreducible_sourcefirst_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rn_prime_irreducible_sourcefirst_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcefirst_divisorproduct) * (ge_second_rp_prime_irreducible_sourcefirst_divisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_prime_irreducible_sourcesecond_divisor. (exists ge_first_rp_prime_irreducible_sourcesecond_divisorproduct ge_first_rn_prime_irreducible_sourcesecond_divisorproduct ge_first_ip_prime_irreducible_sourcesecond_divisorproduct ge_first_in_prime_irreducible_sourcesecond_divisorproduct ge_second_rp_prime_irreducible_sourcesecond_divisorproduct ge_second_rn_prime_irreducible_sourcesecond_divisorproduct ge_second_ip_prime_irreducible_sourcesecond_divisorproduct ge_second_in_prime_irreducible_sourcesecond_divisorproduct. ((exists ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst. (((p) = ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst)) * S ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstreal ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstreal. (((((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstreal) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstreal) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstreal = (ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstimaginary ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductfirst) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstimaginary) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductfirstimaginary = (ge_first_in_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond. (((gr_quotient_prime_irreducible_sourcesecond_divisor) = ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond)) * S ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondreal ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondreal. (((((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondreal) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondreal) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondreal = (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondimaginary ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductsecond) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondimaginary) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductsecondimaginary = (ge_second_in_prime_irreducible_sourcesecond_divisorproduct) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput. (((gr_second_factor_prime_irreducible_source) = ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput)) * S ((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputreal ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputreal. (((((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputreal) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_irreducible_sourcesecond_divisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputreal) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rp_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_in_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_ip_prime_irreducible_sourcesecond_divisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputreal = (((((((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rp_prime_irreducible_sourcesecond_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_ip_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_in_prime_irreducible_sourcesecond_divisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputimaginary ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_sourcesecond_divisorproductoutput) = 2 * ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputimaginary) = S ge_signed_half_prime_irreducible_sourcesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_ip_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_in_prime_irreducible_sourcesecond_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rp_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct))))))) + ge_balance_negative_prime_irreducible_sourcesecond_divisorproductoutputimaginary = (((((((ge_first_rp_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_in_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_rn_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_ip_prime_irreducible_sourcesecond_divisorproduct))))) + (((((ge_first_ip_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rn_prime_irreducible_sourcesecond_divisorproduct))) + (((ge_first_in_prime_irreducible_sourcesecond_divisorproduct) * (ge_second_rp_prime_irreducible_sourcesecond_divisorproduct))))))) + ge_balance_positive_prime_irreducible_sourcesecond_divisorproductoutputimaginary))))))))))))))) -> (((exists ge_real_positive_prime_irreducible_resultcarrier ge_real_negative_prime_irreducible_resultcarrier ge_imaginary_positive_prime_irreducible_resultcarrier ge_imaginary_negative_prime_irreducible_resultcarrier. (exists ge_real_code_prime_irreducible_resultcarrierdecode ge_imaginary_code_prime_irreducible_resultcarrierdecode. (((p) = ((ge_real_code_prime_irreducible_resultcarrierdecode) + (ge_imaginary_code_prime_irreducible_resultcarrierdecode)) * S ((ge_real_code_prime_irreducible_resultcarrierdecode) + (ge_imaginary_code_prime_irreducible_resultcarrierdecode)) + ((ge_imaginary_code_prime_irreducible_resultcarrierdecode) + (ge_imaginary_code_prime_irreducible_resultcarrierdecode))) /\ (((((ge_real_code_prime_irreducible_resultcarrierdecode) = 2 * (ge_real_positive_prime_irreducible_resultcarrier) /\ (ge_real_negative_prime_irreducible_resultcarrier) = 0) \/ exists ge_signed_half_ge_prime_irreducible_resultcarrierdecode_real. (((ge_real_code_prime_irreducible_resultcarrierdecode) = 2 * ge_signed_half_ge_prime_irreducible_resultcarrierdecode_real + 1 /\ (ge_real_positive_prime_irreducible_resultcarrier) = 0) /\ (ge_real_negative_prime_irreducible_resultcarrier) = S ge_signed_half_ge_prime_irreducible_resultcarrierdecode_real))) /\ ((((ge_imaginary_code_prime_irreducible_resultcarrierdecode) = 2 * (ge_imaginary_positive_prime_irreducible_resultcarrier) /\ (ge_imaginary_negative_prime_irreducible_resultcarrier) = 0) \/ exists ge_signed_half_ge_prime_irreducible_resultcarrierdecode_imaginary. (((ge_imaginary_code_prime_irreducible_resultcarrierdecode) = 2 * ge_signed_half_ge_prime_irreducible_resultcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_irreducible_resultcarrier) = 0) /\ (ge_imaginary_negative_prime_irreducible_resultcarrier) = S ge_signed_half_ge_prime_irreducible_resultcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_prime_irreducible_resultnonunit. (exists ge_first_rp_prime_irreducible_resultnonunitidentity ge_first_rn_prime_irreducible_resultnonunitidentity ge_first_ip_prime_irreducible_resultnonunitidentity ge_first_in_prime_irreducible_resultnonunitidentity ge_second_rp_prime_irreducible_resultnonunitidentity ge_second_rn_prime_irreducible_resultnonunitidentity ge_second_ip_prime_irreducible_resultnonunitidentity ge_second_in_prime_irreducible_resultnonunitidentity. ((exists ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst. (((p) = ((ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst)) * S ((ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreducible_resultnonunitidentityfirstreal ge_balance_negative_prime_irreducible_resultnonunitidentityfirstreal. (((((ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentityfirstreal) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreducible_resultnonunitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityfirstreal) = S ge_signed_half_prime_irreducible_resultnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_resultnonunitidentity) + ge_balance_negative_prime_irreducible_resultnonunitidentityfirstreal = (ge_first_rn_prime_irreducible_resultnonunitidentity) + ge_balance_positive_prime_irreducible_resultnonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_resultnonunitidentityfirstimaginary ge_balance_negative_prime_irreducible_resultnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityfirstimaginary) = S ge_signed_half_prime_irreducible_resultnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_resultnonunitidentity) + ge_balance_negative_prime_irreducible_resultnonunitidentityfirstimaginary = (ge_first_in_prime_irreducible_resultnonunitidentity) + ge_balance_positive_prime_irreducible_resultnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond. (((gr_inverse_prime_irreducible_resultnonunit) = ((ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond)) * S ((ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreducible_resultnonunitidentitysecondreal ge_balance_negative_prime_irreducible_resultnonunitidentitysecondreal. (((((ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentitysecondreal) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreducible_resultnonunitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentitysecondreal) = S ge_signed_half_prime_irreducible_resultnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_resultnonunitidentity) + ge_balance_negative_prime_irreducible_resultnonunitidentitysecondreal = (ge_second_rn_prime_irreducible_resultnonunitidentity) + ge_balance_positive_prime_irreducible_resultnonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreducible_resultnonunitidentitysecondimaginary ge_balance_negative_prime_irreducible_resultnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentitysecondimaginary) = S ge_signed_half_prime_irreducible_resultnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_resultnonunitidentity) + ge_balance_negative_prime_irreducible_resultnonunitidentitysecondimaginary = (ge_second_in_prime_irreducible_resultnonunitidentity) + ge_balance_positive_prime_irreducible_resultnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput)) * S ((ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreducible_resultnonunitidentityoutputreal ge_balance_negative_prime_irreducible_resultnonunitidentityoutputreal. (((((ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentityoutputreal) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreducible_resultnonunitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityoutputreal) = S ge_signed_half_prime_irreducible_resultnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultnonunitidentity) * (ge_second_rp_prime_irreducible_resultnonunitidentity))) + (((ge_first_rn_prime_irreducible_resultnonunitidentity) * (ge_second_rn_prime_irreducible_resultnonunitidentity))))) + (((((ge_first_ip_prime_irreducible_resultnonunitidentity) * (ge_second_in_prime_irreducible_resultnonunitidentity))) + (((ge_first_in_prime_irreducible_resultnonunitidentity) * (ge_second_ip_prime_irreducible_resultnonunitidentity))))))) + ge_balance_negative_prime_irreducible_resultnonunitidentityoutputreal = (((((((ge_first_rp_prime_irreducible_resultnonunitidentity) * (ge_second_rn_prime_irreducible_resultnonunitidentity))) + (((ge_first_rn_prime_irreducible_resultnonunitidentity) * (ge_second_rp_prime_irreducible_resultnonunitidentity))))) + (((((ge_first_ip_prime_irreducible_resultnonunitidentity) * (ge_second_ip_prime_irreducible_resultnonunitidentity))) + (((ge_first_in_prime_irreducible_resultnonunitidentity) * (ge_second_in_prime_irreducible_resultnonunitidentity))))))) + ge_balance_positive_prime_irreducible_resultnonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_resultnonunitidentityoutputimaginary ge_balance_negative_prime_irreducible_resultnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultnonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultnonunitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultnonunitidentityoutputimaginary) = S ge_signed_half_prime_irreducible_resultnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultnonunitidentity) * (ge_second_ip_prime_irreducible_resultnonunitidentity))) + (((ge_first_rn_prime_irreducible_resultnonunitidentity) * (ge_second_in_prime_irreducible_resultnonunitidentity))))) + (((((ge_first_ip_prime_irreducible_resultnonunitidentity) * (ge_second_rp_prime_irreducible_resultnonunitidentity))) + (((ge_first_in_prime_irreducible_resultnonunitidentity) * (ge_second_rn_prime_irreducible_resultnonunitidentity))))))) + ge_balance_negative_prime_irreducible_resultnonunitidentityoutputimaginary = (((((((ge_first_rp_prime_irreducible_resultnonunitidentity) * (ge_second_in_prime_irreducible_resultnonunitidentity))) + (((ge_first_rn_prime_irreducible_resultnonunitidentity) * (ge_second_ip_prime_irreducible_resultnonunitidentity))))) + (((((ge_first_ip_prime_irreducible_resultnonunitidentity) * (ge_second_rn_prime_irreducible_resultnonunitidentity))) + (((ge_first_in_prime_irreducible_resultnonunitidentity) * (ge_second_rp_prime_irreducible_resultnonunitidentity))))))) + ge_balance_positive_prime_irreducible_resultnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_irreducible_result gr_second_factor_prime_irreducible_result. (exists ge_first_rp_prime_irreducible_resultfactorization ge_first_rn_prime_irreducible_resultfactorization ge_first_ip_prime_irreducible_resultfactorization ge_first_in_prime_irreducible_resultfactorization ge_second_rp_prime_irreducible_resultfactorization ge_second_rn_prime_irreducible_resultfactorization ge_second_ip_prime_irreducible_resultfactorization ge_second_in_prime_irreducible_resultfactorization. ((exists ge_representation_real_code_prime_irreducible_resultfactorizationfirst ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst. (((gr_first_factor_prime_irreducible_result) = ((ge_representation_real_code_prime_irreducible_resultfactorizationfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst)) * S ((ge_representation_real_code_prime_irreducible_resultfactorizationfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst)) + ((ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst))) /\ ((exists ge_balance_positive_prime_irreducible_resultfactorizationfirstreal ge_balance_negative_prime_irreducible_resultfactorizationfirstreal. (((((ge_representation_real_code_prime_irreducible_resultfactorizationfirst) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationfirstreal) /\ (ge_balance_negative_prime_irreducible_resultfactorizationfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationfirstrealdecode. (((ge_representation_real_code_prime_irreducible_resultfactorizationfirst) = 2 * ge_signed_half_prime_irreducible_resultfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationfirstreal) = S ge_signed_half_prime_irreducible_resultfactorizationfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_resultfactorization) + ge_balance_negative_prime_irreducible_resultfactorizationfirstreal = (ge_first_rn_prime_irreducible_resultfactorization) + ge_balance_positive_prime_irreducible_resultfactorizationfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfactorizationfirstimaginary ge_balance_negative_prime_irreducible_resultfactorizationfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationfirstimaginary) /\ (ge_balance_negative_prime_irreducible_resultfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfactorizationfirst) = 2 * ge_signed_half_prime_irreducible_resultfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationfirstimaginary) = S ge_signed_half_prime_irreducible_resultfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_resultfactorization) + ge_balance_negative_prime_irreducible_resultfactorizationfirstimaginary = (ge_first_in_prime_irreducible_resultfactorization) + ge_balance_positive_prime_irreducible_resultfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_resultfactorizationsecond ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond. (((gr_second_factor_prime_irreducible_result) = ((ge_representation_real_code_prime_irreducible_resultfactorizationsecond) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond)) * S ((ge_representation_real_code_prime_irreducible_resultfactorizationsecond) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond)) + ((ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond))) /\ ((exists ge_balance_positive_prime_irreducible_resultfactorizationsecondreal ge_balance_negative_prime_irreducible_resultfactorizationsecondreal. (((((ge_representation_real_code_prime_irreducible_resultfactorizationsecond) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationsecondreal) /\ (ge_balance_negative_prime_irreducible_resultfactorizationsecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationsecondrealdecode. (((ge_representation_real_code_prime_irreducible_resultfactorizationsecond) = 2 * ge_signed_half_prime_irreducible_resultfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationsecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationsecondreal) = S ge_signed_half_prime_irreducible_resultfactorizationsecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_resultfactorization) + ge_balance_negative_prime_irreducible_resultfactorizationsecondreal = (ge_second_rn_prime_irreducible_resultfactorization) + ge_balance_positive_prime_irreducible_resultfactorizationsecondreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfactorizationsecondimaginary ge_balance_negative_prime_irreducible_resultfactorizationsecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationsecondimaginary) /\ (ge_balance_negative_prime_irreducible_resultfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfactorizationsecond) = 2 * ge_signed_half_prime_irreducible_resultfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationsecondimaginary) = S ge_signed_half_prime_irreducible_resultfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_resultfactorization) + ge_balance_negative_prime_irreducible_resultfactorizationsecondimaginary = (ge_second_in_prime_irreducible_resultfactorization) + ge_balance_positive_prime_irreducible_resultfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_resultfactorizationoutput ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput. (((p) = ((ge_representation_real_code_prime_irreducible_resultfactorizationoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput)) * S ((ge_representation_real_code_prime_irreducible_resultfactorizationoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput)) + ((ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput))) /\ ((exists ge_balance_positive_prime_irreducible_resultfactorizationoutputreal ge_balance_negative_prime_irreducible_resultfactorizationoutputreal. (((((ge_representation_real_code_prime_irreducible_resultfactorizationoutput) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationoutputreal) /\ (ge_balance_negative_prime_irreducible_resultfactorizationoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationoutputrealdecode. (((ge_representation_real_code_prime_irreducible_resultfactorizationoutput) = 2 * ge_signed_half_prime_irreducible_resultfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationoutputreal) = S ge_signed_half_prime_irreducible_resultfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultfactorization) * (ge_second_rp_prime_irreducible_resultfactorization))) + (((ge_first_rn_prime_irreducible_resultfactorization) * (ge_second_rn_prime_irreducible_resultfactorization))))) + (((((ge_first_ip_prime_irreducible_resultfactorization) * (ge_second_in_prime_irreducible_resultfactorization))) + (((ge_first_in_prime_irreducible_resultfactorization) * (ge_second_ip_prime_irreducible_resultfactorization))))))) + ge_balance_negative_prime_irreducible_resultfactorizationoutputreal = (((((((ge_first_rp_prime_irreducible_resultfactorization) * (ge_second_rn_prime_irreducible_resultfactorization))) + (((ge_first_rn_prime_irreducible_resultfactorization) * (ge_second_rp_prime_irreducible_resultfactorization))))) + (((((ge_first_ip_prime_irreducible_resultfactorization) * (ge_second_ip_prime_irreducible_resultfactorization))) + (((ge_first_in_prime_irreducible_resultfactorization) * (ge_second_in_prime_irreducible_resultfactorization))))))) + ge_balance_positive_prime_irreducible_resultfactorizationoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfactorizationoutputimaginary ge_balance_negative_prime_irreducible_resultfactorizationoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput) = 2 * (ge_balance_positive_prime_irreducible_resultfactorizationoutputimaginary) /\ (ge_balance_negative_prime_irreducible_resultfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfactorizationoutput) = 2 * ge_signed_half_prime_irreducible_resultfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfactorizationoutputimaginary) = S ge_signed_half_prime_irreducible_resultfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultfactorization) * (ge_second_ip_prime_irreducible_resultfactorization))) + (((ge_first_rn_prime_irreducible_resultfactorization) * (ge_second_in_prime_irreducible_resultfactorization))))) + (((((ge_first_ip_prime_irreducible_resultfactorization) * (ge_second_rp_prime_irreducible_resultfactorization))) + (((ge_first_in_prime_irreducible_resultfactorization) * (ge_second_rn_prime_irreducible_resultfactorization))))))) + ge_balance_negative_prime_irreducible_resultfactorizationoutputimaginary = (((((((ge_first_rp_prime_irreducible_resultfactorization) * (ge_second_in_prime_irreducible_resultfactorization))) + (((ge_first_rn_prime_irreducible_resultfactorization) * (ge_second_ip_prime_irreducible_resultfactorization))))) + (((((ge_first_ip_prime_irreducible_resultfactorization) * (ge_second_rn_prime_irreducible_resultfactorization))) + (((ge_first_in_prime_irreducible_resultfactorization) * (ge_second_rp_prime_irreducible_resultfactorization))))))) + ge_balance_positive_prime_irreducible_resultfactorizationoutputimaginary))))))))) -> (exists gr_inverse_prime_irreducible_resultfirst_unit. (exists ge_first_rp_prime_irreducible_resultfirst_unitidentity ge_first_rn_prime_irreducible_resultfirst_unitidentity ge_first_ip_prime_irreducible_resultfirst_unitidentity ge_first_in_prime_irreducible_resultfirst_unitidentity ge_second_rp_prime_irreducible_resultfirst_unitidentity ge_second_rn_prime_irreducible_resultfirst_unitidentity ge_second_ip_prime_irreducible_resultfirst_unitidentity ge_second_in_prime_irreducible_resultfirst_unitidentity. ((exists ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst. (((gr_first_factor_prime_irreducible_result) = ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst)) * S ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstreal ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstreal. (((((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstreal) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstreal) = S ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_resultfirst_unitidentity) + ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstreal = (ge_first_rn_prime_irreducible_resultfirst_unitidentity) + ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstimaginary ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstimaginary) = S ge_signed_half_prime_irreducible_resultfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_resultfirst_unitidentity) + ge_balance_negative_prime_irreducible_resultfirst_unitidentityfirstimaginary = (ge_first_in_prime_irreducible_resultfirst_unitidentity) + ge_balance_positive_prime_irreducible_resultfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond. (((gr_inverse_prime_irreducible_resultfirst_unit) = ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond)) * S ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondreal ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondreal. (((((ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondreal) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreducible_resultfirst_unitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondreal) = S ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_resultfirst_unitidentity) + ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondreal = (ge_second_rn_prime_irreducible_resultfirst_unitidentity) + ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondimaginary ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondimaginary) = S ge_signed_half_prime_irreducible_resultfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_resultfirst_unitidentity) + ge_balance_negative_prime_irreducible_resultfirst_unitidentitysecondimaginary = (ge_second_in_prime_irreducible_resultfirst_unitidentity) + ge_balance_positive_prime_irreducible_resultfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput)) * S ((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputreal ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputreal. (((((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputreal) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreducible_resultfirst_unitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputreal) = S ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultfirst_unitidentity) * (ge_second_rp_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_rn_prime_irreducible_resultfirst_unitidentity) * (ge_second_rn_prime_irreducible_resultfirst_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultfirst_unitidentity) * (ge_second_in_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_in_prime_irreducible_resultfirst_unitidentity) * (ge_second_ip_prime_irreducible_resultfirst_unitidentity))))))) + ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputreal = (((((((ge_first_rp_prime_irreducible_resultfirst_unitidentity) * (ge_second_rn_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_rn_prime_irreducible_resultfirst_unitidentity) * (ge_second_rp_prime_irreducible_resultfirst_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultfirst_unitidentity) * (ge_second_ip_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_in_prime_irreducible_resultfirst_unitidentity) * (ge_second_in_prime_irreducible_resultfirst_unitidentity))))))) + ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputimaginary ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultfirst_unitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputimaginary) = S ge_signed_half_prime_irreducible_resultfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultfirst_unitidentity) * (ge_second_ip_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_rn_prime_irreducible_resultfirst_unitidentity) * (ge_second_in_prime_irreducible_resultfirst_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultfirst_unitidentity) * (ge_second_rp_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_in_prime_irreducible_resultfirst_unitidentity) * (ge_second_rn_prime_irreducible_resultfirst_unitidentity))))))) + ge_balance_negative_prime_irreducible_resultfirst_unitidentityoutputimaginary = (((((((ge_first_rp_prime_irreducible_resultfirst_unitidentity) * (ge_second_in_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_rn_prime_irreducible_resultfirst_unitidentity) * (ge_second_ip_prime_irreducible_resultfirst_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultfirst_unitidentity) * (ge_second_rn_prime_irreducible_resultfirst_unitidentity))) + (((ge_first_in_prime_irreducible_resultfirst_unitidentity) * (ge_second_rp_prime_irreducible_resultfirst_unitidentity))))))) + ge_balance_positive_prime_irreducible_resultfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_prime_irreducible_resultsecond_unit. (exists ge_first_rp_prime_irreducible_resultsecond_unitidentity ge_first_rn_prime_irreducible_resultsecond_unitidentity ge_first_ip_prime_irreducible_resultsecond_unitidentity ge_first_in_prime_irreducible_resultsecond_unitidentity ge_second_rp_prime_irreducible_resultsecond_unitidentity ge_second_rn_prime_irreducible_resultsecond_unitidentity ge_second_ip_prime_irreducible_resultsecond_unitidentity ge_second_in_prime_irreducible_resultsecond_unitidentity. ((exists ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst. (((gr_second_factor_prime_irreducible_result) = ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst)) * S ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstreal ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstreal. (((((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstreal) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstreal) = S ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreducible_resultsecond_unitidentity) + ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstreal = (ge_first_rn_prime_irreducible_resultsecond_unitidentity) + ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstimaginary ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityfirst) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstimaginary) = S ge_signed_half_prime_irreducible_resultsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreducible_resultsecond_unitidentity) + ge_balance_negative_prime_irreducible_resultsecond_unitidentityfirstimaginary = (ge_first_in_prime_irreducible_resultsecond_unitidentity) + ge_balance_positive_prime_irreducible_resultsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond. (((gr_inverse_prime_irreducible_resultsecond_unit) = ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond)) * S ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondreal ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondreal. (((((ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondreal) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreducible_resultsecond_unitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondreal) = S ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreducible_resultsecond_unitidentity) + ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondreal = (ge_second_rn_prime_irreducible_resultsecond_unitidentity) + ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondimaginary ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentitysecond) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondimaginary) = S ge_signed_half_prime_irreducible_resultsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreducible_resultsecond_unitidentity) + ge_balance_negative_prime_irreducible_resultsecond_unitidentitysecondimaginary = (ge_second_in_prime_irreducible_resultsecond_unitidentity) + ge_balance_positive_prime_irreducible_resultsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput)) * S ((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputreal ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputreal. (((((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputreal) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreducible_resultsecond_unitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputreal) = S ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultsecond_unitidentity) * (ge_second_rp_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_rn_prime_irreducible_resultsecond_unitidentity) * (ge_second_rn_prime_irreducible_resultsecond_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultsecond_unitidentity) * (ge_second_in_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_in_prime_irreducible_resultsecond_unitidentity) * (ge_second_ip_prime_irreducible_resultsecond_unitidentity))))))) + ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputreal = (((((((ge_first_rp_prime_irreducible_resultsecond_unitidentity) * (ge_second_rn_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_rn_prime_irreducible_resultsecond_unitidentity) * (ge_second_rp_prime_irreducible_resultsecond_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultsecond_unitidentity) * (ge_second_ip_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_in_prime_irreducible_resultsecond_unitidentity) * (ge_second_in_prime_irreducible_resultsecond_unitidentity))))))) + ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputimaginary ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreducible_resultsecond_unitidentityoutput) = 2 * ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputimaginary) = S ge_signed_half_prime_irreducible_resultsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreducible_resultsecond_unitidentity) * (ge_second_ip_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_rn_prime_irreducible_resultsecond_unitidentity) * (ge_second_in_prime_irreducible_resultsecond_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultsecond_unitidentity) * (ge_second_rp_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_in_prime_irreducible_resultsecond_unitidentity) * (ge_second_rn_prime_irreducible_resultsecond_unitidentity))))))) + ge_balance_negative_prime_irreducible_resultsecond_unitidentityoutputimaginary = (((((((ge_first_rp_prime_irreducible_resultsecond_unitidentity) * (ge_second_in_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_rn_prime_irreducible_resultsecond_unitidentity) * (ge_second_ip_prime_irreducible_resultsecond_unitidentity))))) + (((((ge_first_ip_prime_irreducible_resultsecond_unitidentity) * (ge_second_rn_prime_irreducible_resultsecond_unitidentity))) + (((ge_first_in_prime_irreducible_resultsecond_unitidentity) * (ge_second_rp_prime_irreducible_resultsecond_unitidentity))))))) + ge_balance_positive_prime_irreducible_resultsecond_unitidentityoutputimaginary)))))))))))))))