gaussian_factor_search_complete

Exact expanded first-order arithmetic statement

forall z N. (exists ge_norm_rp_complete_search_norm ge_norm_rn_complete_search_norm ge_norm_ip_complete_search_norm ge_norm_in_complete_search_norm. ((exists ge_representation_real_code_complete_search_normrepresentation ge_representation_imaginary_code_complete_search_normrepresentation. (((z) = ((ge_representation_real_code_complete_search_normrepresentation) + (ge_representation_imaginary_code_complete_search_normrepresentation)) * S ((ge_representation_real_code_complete_search_normrepresentation) + (ge_representation_imaginary_code_complete_search_normrepresentation)) + ((ge_representation_imaginary_code_complete_search_normrepresentation) + (ge_representation_imaginary_code_complete_search_normrepresentation))) /\ ((exists ge_balance_positive_complete_search_normrepresentationreal ge_balance_negative_complete_search_normrepresentationreal. (((((ge_representation_real_code_complete_search_normrepresentation) = 2 * (ge_balance_positive_complete_search_normrepresentationreal) /\ (ge_balance_negative_complete_search_normrepresentationreal) = 0) \/ exists ge_signed_half_complete_search_normrepresentationrealdecode. (((ge_representation_real_code_complete_search_normrepresentation) = 2 * ge_signed_half_complete_search_normrepresentationrealdecode + 1 /\ (ge_balance_positive_complete_search_normrepresentationreal) = 0) /\ (ge_balance_negative_complete_search_normrepresentationreal) = S ge_signed_half_complete_search_normrepresentationrealdecode))) /\ ((ge_norm_rp_complete_search_norm) + ge_balance_negative_complete_search_normrepresentationreal = (ge_norm_rn_complete_search_norm) + ge_balance_positive_complete_search_normrepresentationreal))) /\ (exists ge_balance_positive_complete_search_normrepresentationimaginary ge_balance_negative_complete_search_normrepresentationimaginary. (((((ge_representation_imaginary_code_complete_search_normrepresentation) = 2 * (ge_balance_positive_complete_search_normrepresentationimaginary) /\ (ge_balance_negative_complete_search_normrepresentationimaginary) = 0) \/ exists ge_signed_half_complete_search_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_complete_search_normrepresentation) = 2 * ge_signed_half_complete_search_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_complete_search_normrepresentationimaginary) = 0) /\ (ge_balance_negative_complete_search_normrepresentationimaginary) = S ge_signed_half_complete_search_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_complete_search_norm) + ge_balance_negative_complete_search_normrepresentationimaginary = (ge_norm_in_complete_search_norm) + ge_balance_positive_complete_search_normrepresentationimaginary)))))) /\ (exists ge_real_square_complete_search_normsquare ge_imaginary_square_complete_search_normsquare. ((((((ge_norm_rp_complete_search_norm) * (ge_norm_rp_complete_search_norm))) + (((ge_norm_rn_complete_search_norm) * (ge_norm_rn_complete_search_norm)))) = ((ge_real_square_complete_search_normsquare) + (((((ge_norm_rp_complete_search_norm) * (ge_norm_rn_complete_search_norm))) + (((ge_norm_rn_complete_search_norm) * (ge_norm_rp_complete_search_norm))))))) /\ ((((((ge_norm_ip_complete_search_norm) * (ge_norm_ip_complete_search_norm))) + (((ge_norm_in_complete_search_norm) * (ge_norm_in_complete_search_norm)))) = ((ge_imaginary_square_complete_search_normsquare) + (((((ge_norm_ip_complete_search_norm) * (ge_norm_in_complete_search_norm))) + (((ge_norm_in_complete_search_norm) * (ge_norm_ip_complete_search_norm))))))) /\ ((N) = ge_real_square_complete_search_normsquare + ge_imaginary_square_complete_search_normsquare)))))) -> ((exists gr_complete_divisor_complete_search. (((~(exists gr_inverse_complete_searchfoundnonunit. (exists ge_first_rp_complete_searchfoundnonunitidentity ge_first_rn_complete_searchfoundnonunitidentity ge_first_ip_complete_searchfoundnonunitidentity ge_first_in_complete_searchfoundnonunitidentity ge_second_rp_complete_searchfoundnonunitidentity ge_second_rn_complete_searchfoundnonunitidentity ge_second_ip_complete_searchfoundnonunitidentity ge_second_in_complete_searchfoundnonunitidentity. ((exists ge_representation_real_code_complete_searchfoundnonunitidentityfirst ge_representation_imaginary_code_complete_searchfoundnonunitidentityfirst. (((gr_complete_divisor_complete_search) = ((ge_representation_real_code_complete_searchfoundnonunitidentityfirst) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentityfirst)) * S ((ge_representation_real_code_complete_searchfoundnonunitidentityfirst) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentityfirst)) + ((ge_representation_imaginary_code_complete_searchfoundnonunitidentityfirst) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentityfirst))) /\ ((exists ge_balance_positive_complete_searchfoundnonunitidentityfirstreal ge_balance_negative_complete_searchfoundnonunitidentityfirstreal. (((((ge_representation_real_code_complete_searchfoundnonunitidentityfirst) = 2 * (ge_balance_positive_complete_searchfoundnonunitidentityfirstreal) /\ (ge_balance_negative_complete_searchfoundnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_complete_searchfoundnonunitidentityfirstrealdecode. (((ge_representation_real_code_complete_searchfoundnonunitidentityfirst) = 2 * ge_signed_half_complete_searchfoundnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_complete_searchfoundnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_complete_searchfoundnonunitidentityfirstreal) = S ge_signed_half_complete_searchfoundnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_complete_searchfoundnonunitidentity) + ge_balance_negative_complete_searchfoundnonunitidentityfirstreal = (ge_first_rn_complete_searchfoundnonunitidentity) + ge_balance_positive_complete_searchfoundnonunitidentityfirstreal))) /\ (exists ge_balance_positive_complete_searchfoundnonunitidentityfirstimaginary ge_balance_negative_complete_searchfoundnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_complete_searchfoundnonunitidentityfirst) = 2 * (ge_balance_positive_complete_searchfoundnonunitidentityfirstimaginary) /\ (ge_balance_negative_complete_searchfoundnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_complete_searchfoundnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_complete_searchfoundnonunitidentityfirst) = 2 * ge_signed_half_complete_searchfoundnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_complete_searchfoundnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_complete_searchfoundnonunitidentityfirstimaginary) = S ge_signed_half_complete_searchfoundnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_complete_searchfoundnonunitidentity) + ge_balance_negative_complete_searchfoundnonunitidentityfirstimaginary = (ge_first_in_complete_searchfoundnonunitidentity) + ge_balance_positive_complete_searchfoundnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_complete_searchfoundnonunitidentitysecond ge_representation_imaginary_code_complete_searchfoundnonunitidentitysecond. (((gr_inverse_complete_searchfoundnonunit) = ((ge_representation_real_code_complete_searchfoundnonunitidentitysecond) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentitysecond)) * S ((ge_representation_real_code_complete_searchfoundnonunitidentitysecond) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentitysecond)) + ((ge_representation_imaginary_code_complete_searchfoundnonunitidentitysecond) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentitysecond))) /\ ((exists ge_balance_positive_complete_searchfoundnonunitidentitysecondreal ge_balance_negative_complete_searchfoundnonunitidentitysecondreal. (((((ge_representation_real_code_complete_searchfoundnonunitidentitysecond) = 2 * (ge_balance_positive_complete_searchfoundnonunitidentitysecondreal) /\ (ge_balance_negative_complete_searchfoundnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_complete_searchfoundnonunitidentitysecondrealdecode. (((ge_representation_real_code_complete_searchfoundnonunitidentitysecond) = 2 * ge_signed_half_complete_searchfoundnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_complete_searchfoundnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_complete_searchfoundnonunitidentitysecondreal) = S ge_signed_half_complete_searchfoundnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_complete_searchfoundnonunitidentity) + ge_balance_negative_complete_searchfoundnonunitidentitysecondreal = (ge_second_rn_complete_searchfoundnonunitidentity) + ge_balance_positive_complete_searchfoundnonunitidentitysecondreal))) /\ (exists ge_balance_positive_complete_searchfoundnonunitidentitysecondimaginary ge_balance_negative_complete_searchfoundnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_complete_searchfoundnonunitidentitysecond) = 2 * (ge_balance_positive_complete_searchfoundnonunitidentitysecondimaginary) /\ (ge_balance_negative_complete_searchfoundnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_complete_searchfoundnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_complete_searchfoundnonunitidentitysecond) = 2 * ge_signed_half_complete_searchfoundnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_complete_searchfoundnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_complete_searchfoundnonunitidentitysecondimaginary) = S ge_signed_half_complete_searchfoundnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_complete_searchfoundnonunitidentity) + ge_balance_negative_complete_searchfoundnonunitidentitysecondimaginary = (ge_second_in_complete_searchfoundnonunitidentity) + ge_balance_positive_complete_searchfoundnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_complete_searchfoundnonunitidentityoutput ge_representation_imaginary_code_complete_searchfoundnonunitidentityoutput. (((6) = ((ge_representation_real_code_complete_searchfoundnonunitidentityoutput) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentityoutput)) * S ((ge_representation_real_code_complete_searchfoundnonunitidentityoutput) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentityoutput)) + ((ge_representation_imaginary_code_complete_searchfoundnonunitidentityoutput) + (ge_representation_imaginary_code_complete_searchfoundnonunitidentityoutput))) /\ ((exists ge_balance_positive_complete_searchfoundnonunitidentityoutputreal ge_balance_negative_complete_searchfoundnonunitidentityoutputreal. (((((ge_representation_real_code_complete_searchfoundnonunitidentityoutput) = 2 * (ge_balance_positive_complete_searchfoundnonunitidentityoutputreal) /\ (ge_balance_negative_complete_searchfoundnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_complete_searchfoundnonunitidentityoutputrealdecode. (((ge_representation_real_code_complete_searchfoundnonunitidentityoutput) = 2 * ge_signed_half_complete_searchfoundnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_complete_searchfoundnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_complete_searchfoundnonunitidentityoutputreal) = S ge_signed_half_complete_searchfoundnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_complete_searchfoundnonunitidentity) * (ge_second_rp_complete_searchfoundnonunitidentity))) + (((ge_first_rn_complete_searchfoundnonunitidentity) * (ge_second_rn_complete_searchfoundnonunitidentity))))) + (((((ge_first_ip_complete_searchfoundnonunitidentity) * (ge_second_in_complete_searchfoundnonunitidentity))) + (((ge_first_in_complete_searchfoundnonunitidentity) * (ge_second_ip_complete_searchfoundnonunitidentity))))))) + ge_balance_negative_complete_searchfoundnonunitidentityoutputreal = (((((((ge_first_rp_complete_searchfoundnonunitidentity) * (ge_second_rn_complete_searchfoundnonunitidentity))) + (((ge_first_rn_complete_searchfoundnonunitidentity) * (ge_second_rp_complete_searchfoundnonunitidentity))))) + (((((ge_first_ip_complete_searchfoundnonunitidentity) * (ge_second_ip_complete_searchfoundnonunitidentity))) + (((ge_first_in_complete_searchfoundnonunitidentity) * (ge_second_in_complete_searchfoundnonunitidentity))))))) + ge_balance_positive_complete_searchfoundnonunitidentityoutputreal))) /\ (exists ge_balance_positive_complete_searchfoundnonunitidentityoutputimaginary ge_balance_negative_complete_searchfoundnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_complete_searchfoundnonunitidentityoutput) = 2 * (ge_balance_positive_complete_searchfoundnonunitidentityoutputimaginary) /\ (ge_balance_negative_complete_searchfoundnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_complete_searchfoundnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_complete_searchfoundnonunitidentityoutput) = 2 * ge_signed_half_complete_searchfoundnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_complete_searchfoundnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_complete_searchfoundnonunitidentityoutputimaginary) = S ge_signed_half_complete_searchfoundnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_complete_searchfoundnonunitidentity) * (ge_second_ip_complete_searchfoundnonunitidentity))) + (((ge_first_rn_complete_searchfoundnonunitidentity) * (ge_second_in_complete_searchfoundnonunitidentity))))) + (((((ge_first_ip_complete_searchfoundnonunitidentity) * (ge_second_rp_complete_searchfoundnonunitidentity))) + (((ge_first_in_complete_searchfoundnonunitidentity) * (ge_second_rn_complete_searchfoundnonunitidentity))))))) + ge_balance_negative_complete_searchfoundnonunitidentityoutputimaginary = (((((((ge_first_rp_complete_searchfoundnonunitidentity) * (ge_second_in_complete_searchfoundnonunitidentity))) + (((ge_first_rn_complete_searchfoundnonunitidentity) * (ge_second_ip_complete_searchfoundnonunitidentity))))) + (((((ge_first_ip_complete_searchfoundnonunitidentity) * (ge_second_rn_complete_searchfoundnonunitidentity))) + (((ge_first_in_complete_searchfoundnonunitidentity) * (ge_second_rp_complete_searchfoundnonunitidentity))))))) + ge_balance_positive_complete_searchfoundnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_complete_searchfoundquotient. (exists ge_first_rp_complete_searchfoundquotientproduct ge_first_rn_complete_searchfoundquotientproduct ge_first_ip_complete_searchfoundquotientproduct ge_first_in_complete_searchfoundquotientproduct ge_second_rp_complete_searchfoundquotientproduct ge_second_rn_complete_searchfoundquotientproduct ge_second_ip_complete_searchfoundquotientproduct ge_second_in_complete_searchfoundquotientproduct. ((exists ge_representation_real_code_complete_searchfoundquotientproductfirst ge_representation_imaginary_code_complete_searchfoundquotientproductfirst. (((gr_complete_divisor_complete_search) = ((ge_representation_real_code_complete_searchfoundquotientproductfirst) + (ge_representation_imaginary_code_complete_searchfoundquotientproductfirst)) * S ((ge_representation_real_code_complete_searchfoundquotientproductfirst) + (ge_representation_imaginary_code_complete_searchfoundquotientproductfirst)) + ((ge_representation_imaginary_code_complete_searchfoundquotientproductfirst) + (ge_representation_imaginary_code_complete_searchfoundquotientproductfirst))) /\ ((exists ge_balance_positive_complete_searchfoundquotientproductfirstreal ge_balance_negative_complete_searchfoundquotientproductfirstreal. (((((ge_representation_real_code_complete_searchfoundquotientproductfirst) = 2 * (ge_balance_positive_complete_searchfoundquotientproductfirstreal) /\ (ge_balance_negative_complete_searchfoundquotientproductfirstreal) = 0) \/ exists ge_signed_half_complete_searchfoundquotientproductfirstrealdecode. (((ge_representation_real_code_complete_searchfoundquotientproductfirst) = 2 * ge_signed_half_complete_searchfoundquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_complete_searchfoundquotientproductfirstreal) = 0) /\ (ge_balance_negative_complete_searchfoundquotientproductfirstreal) = S ge_signed_half_complete_searchfoundquotientproductfirstrealdecode))) /\ ((ge_first_rp_complete_searchfoundquotientproduct) + ge_balance_negative_complete_searchfoundquotientproductfirstreal = (ge_first_rn_complete_searchfoundquotientproduct) + ge_balance_positive_complete_searchfoundquotientproductfirstreal))) /\ (exists ge_balance_positive_complete_searchfoundquotientproductfirstimaginary ge_balance_negative_complete_searchfoundquotientproductfirstimaginary. (((((ge_representation_imaginary_code_complete_searchfoundquotientproductfirst) = 2 * (ge_balance_positive_complete_searchfoundquotientproductfirstimaginary) /\ (ge_balance_negative_complete_searchfoundquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_complete_searchfoundquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_complete_searchfoundquotientproductfirst) = 2 * ge_signed_half_complete_searchfoundquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_complete_searchfoundquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_complete_searchfoundquotientproductfirstimaginary) = S ge_signed_half_complete_searchfoundquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_complete_searchfoundquotientproduct) + ge_balance_negative_complete_searchfoundquotientproductfirstimaginary = (ge_first_in_complete_searchfoundquotientproduct) + ge_balance_positive_complete_searchfoundquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_complete_searchfoundquotientproductsecond ge_representation_imaginary_code_complete_searchfoundquotientproductsecond. (((gr_quotient_complete_searchfoundquotient) = ((ge_representation_real_code_complete_searchfoundquotientproductsecond) + (ge_representation_imaginary_code_complete_searchfoundquotientproductsecond)) * S ((ge_representation_real_code_complete_searchfoundquotientproductsecond) + (ge_representation_imaginary_code_complete_searchfoundquotientproductsecond)) + ((ge_representation_imaginary_code_complete_searchfoundquotientproductsecond) + (ge_representation_imaginary_code_complete_searchfoundquotientproductsecond))) /\ ((exists ge_balance_positive_complete_searchfoundquotientproductsecondreal ge_balance_negative_complete_searchfoundquotientproductsecondreal. (((((ge_representation_real_code_complete_searchfoundquotientproductsecond) = 2 * (ge_balance_positive_complete_searchfoundquotientproductsecondreal) /\ (ge_balance_negative_complete_searchfoundquotientproductsecondreal) = 0) \/ exists ge_signed_half_complete_searchfoundquotientproductsecondrealdecode. (((ge_representation_real_code_complete_searchfoundquotientproductsecond) = 2 * ge_signed_half_complete_searchfoundquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_complete_searchfoundquotientproductsecondreal) = 0) /\ (ge_balance_negative_complete_searchfoundquotientproductsecondreal) = S ge_signed_half_complete_searchfoundquotientproductsecondrealdecode))) /\ ((ge_second_rp_complete_searchfoundquotientproduct) + ge_balance_negative_complete_searchfoundquotientproductsecondreal = (ge_second_rn_complete_searchfoundquotientproduct) + ge_balance_positive_complete_searchfoundquotientproductsecondreal))) /\ (exists ge_balance_positive_complete_searchfoundquotientproductsecondimaginary ge_balance_negative_complete_searchfoundquotientproductsecondimaginary. (((((ge_representation_imaginary_code_complete_searchfoundquotientproductsecond) = 2 * (ge_balance_positive_complete_searchfoundquotientproductsecondimaginary) /\ (ge_balance_negative_complete_searchfoundquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_complete_searchfoundquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_complete_searchfoundquotientproductsecond) = 2 * ge_signed_half_complete_searchfoundquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_complete_searchfoundquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_complete_searchfoundquotientproductsecondimaginary) = S ge_signed_half_complete_searchfoundquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_complete_searchfoundquotientproduct) + ge_balance_negative_complete_searchfoundquotientproductsecondimaginary = (ge_second_in_complete_searchfoundquotientproduct) + ge_balance_positive_complete_searchfoundquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_complete_searchfoundquotientproductoutput ge_representation_imaginary_code_complete_searchfoundquotientproductoutput. (((z) = ((ge_representation_real_code_complete_searchfoundquotientproductoutput) + (ge_representation_imaginary_code_complete_searchfoundquotientproductoutput)) * S ((ge_representation_real_code_complete_searchfoundquotientproductoutput) + (ge_representation_imaginary_code_complete_searchfoundquotientproductoutput)) + ((ge_representation_imaginary_code_complete_searchfoundquotientproductoutput) + (ge_representation_imaginary_code_complete_searchfoundquotientproductoutput))) /\ ((exists ge_balance_positive_complete_searchfoundquotientproductoutputreal ge_balance_negative_complete_searchfoundquotientproductoutputreal. (((((ge_representation_real_code_complete_searchfoundquotientproductoutput) = 2 * (ge_balance_positive_complete_searchfoundquotientproductoutputreal) /\ (ge_balance_negative_complete_searchfoundquotientproductoutputreal) = 0) \/ exists ge_signed_half_complete_searchfoundquotientproductoutputrealdecode. (((ge_representation_real_code_complete_searchfoundquotientproductoutput) = 2 * ge_signed_half_complete_searchfoundquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_complete_searchfoundquotientproductoutputreal) = 0) /\ (ge_balance_negative_complete_searchfoundquotientproductoutputreal) = S ge_signed_half_complete_searchfoundquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_complete_searchfoundquotientproduct) * (ge_second_rp_complete_searchfoundquotientproduct))) + (((ge_first_rn_complete_searchfoundquotientproduct) * (ge_second_rn_complete_searchfoundquotientproduct))))) + (((((ge_first_ip_complete_searchfoundquotientproduct) * (ge_second_in_complete_searchfoundquotientproduct))) + (((ge_first_in_complete_searchfoundquotientproduct) * (ge_second_ip_complete_searchfoundquotientproduct))))))) + ge_balance_negative_complete_searchfoundquotientproductoutputreal = (((((((ge_first_rp_complete_searchfoundquotientproduct) * (ge_second_rn_complete_searchfoundquotientproduct))) + (((ge_first_rn_complete_searchfoundquotientproduct) * (ge_second_rp_complete_searchfoundquotientproduct))))) + (((((ge_first_ip_complete_searchfoundquotientproduct) * (ge_second_ip_complete_searchfoundquotientproduct))) + (((ge_first_in_complete_searchfoundquotientproduct) * (ge_second_in_complete_searchfoundquotientproduct))))))) + ge_balance_positive_complete_searchfoundquotientproductoutputreal))) /\ (exists ge_balance_positive_complete_searchfoundquotientproductoutputimaginary ge_balance_negative_complete_searchfoundquotientproductoutputimaginary. (((((ge_representation_imaginary_code_complete_searchfoundquotientproductoutput) = 2 * (ge_balance_positive_complete_searchfoundquotientproductoutputimaginary) /\ (ge_balance_negative_complete_searchfoundquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_complete_searchfoundquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_complete_searchfoundquotientproductoutput) = 2 * ge_signed_half_complete_searchfoundquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_complete_searchfoundquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_complete_searchfoundquotientproductoutputimaginary) = S ge_signed_half_complete_searchfoundquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_complete_searchfoundquotientproduct) * (ge_second_ip_complete_searchfoundquotientproduct))) + (((ge_first_rn_complete_searchfoundquotientproduct) * (ge_second_in_complete_searchfoundquotientproduct))))) + (((((ge_first_ip_complete_searchfoundquotientproduct) * (ge_second_rp_complete_searchfoundquotientproduct))) + (((ge_first_in_complete_searchfoundquotientproduct) * (ge_second_rn_complete_searchfoundquotientproduct))))))) + ge_balance_negative_complete_searchfoundquotientproductoutputimaginary = (((((((ge_first_rp_complete_searchfoundquotientproduct) * (ge_second_in_complete_searchfoundquotientproduct))) + (((ge_first_rn_complete_searchfoundquotientproduct) * (ge_second_ip_complete_searchfoundquotientproduct))))) + (((((ge_first_ip_complete_searchfoundquotientproduct) * (ge_second_rn_complete_searchfoundquotientproduct))) + (((ge_first_in_complete_searchfoundquotientproduct) * (ge_second_rp_complete_searchfoundquotientproduct))))))) + ge_balance_positive_complete_searchfoundquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_complete_searchfound. ((exists ge_norm_rp_complete_searchfoundnorm ge_norm_rn_complete_searchfoundnorm ge_norm_ip_complete_searchfoundnorm ge_norm_in_complete_searchfoundnorm. ((exists ge_representation_real_code_complete_searchfoundnormrepresentation ge_representation_imaginary_code_complete_searchfoundnormrepresentation. (((gr_complete_divisor_complete_search) = ((ge_representation_real_code_complete_searchfoundnormrepresentation) + (ge_representation_imaginary_code_complete_searchfoundnormrepresentation)) * S ((ge_representation_real_code_complete_searchfoundnormrepresentation) + (ge_representation_imaginary_code_complete_searchfoundnormrepresentation)) + ((ge_representation_imaginary_code_complete_searchfoundnormrepresentation) + (ge_representation_imaginary_code_complete_searchfoundnormrepresentation))) /\ ((exists ge_balance_positive_complete_searchfoundnormrepresentationreal ge_balance_negative_complete_searchfoundnormrepresentationreal. (((((ge_representation_real_code_complete_searchfoundnormrepresentation) = 2 * (ge_balance_positive_complete_searchfoundnormrepresentationreal) /\ (ge_balance_negative_complete_searchfoundnormrepresentationreal) = 0) \/ exists ge_signed_half_complete_searchfoundnormrepresentationrealdecode. (((ge_representation_real_code_complete_searchfoundnormrepresentation) = 2 * ge_signed_half_complete_searchfoundnormrepresentationrealdecode + 1 /\ (ge_balance_positive_complete_searchfoundnormrepresentationreal) = 0) /\ (ge_balance_negative_complete_searchfoundnormrepresentationreal) = S ge_signed_half_complete_searchfoundnormrepresentationrealdecode))) /\ ((ge_norm_rp_complete_searchfoundnorm) + ge_balance_negative_complete_searchfoundnormrepresentationreal = (ge_norm_rn_complete_searchfoundnorm) + ge_balance_positive_complete_searchfoundnormrepresentationreal))) /\ (exists ge_balance_positive_complete_searchfoundnormrepresentationimaginary ge_balance_negative_complete_searchfoundnormrepresentationimaginary. (((((ge_representation_imaginary_code_complete_searchfoundnormrepresentation) = 2 * (ge_balance_positive_complete_searchfoundnormrepresentationimaginary) /\ (ge_balance_negative_complete_searchfoundnormrepresentationimaginary) = 0) \/ exists ge_signed_half_complete_searchfoundnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_complete_searchfoundnormrepresentation) = 2 * ge_signed_half_complete_searchfoundnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_complete_searchfoundnormrepresentationimaginary) = 0) /\ (ge_balance_negative_complete_searchfoundnormrepresentationimaginary) = S ge_signed_half_complete_searchfoundnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_complete_searchfoundnorm) + ge_balance_negative_complete_searchfoundnormrepresentationimaginary = (ge_norm_in_complete_searchfoundnorm) + ge_balance_positive_complete_searchfoundnormrepresentationimaginary)))))) /\ (exists ge_real_square_complete_searchfoundnormsquare ge_imaginary_square_complete_searchfoundnormsquare. ((((((ge_norm_rp_complete_searchfoundnorm) * (ge_norm_rp_complete_searchfoundnorm))) + (((ge_norm_rn_complete_searchfoundnorm) * (ge_norm_rn_complete_searchfoundnorm)))) = ((ge_real_square_complete_searchfoundnormsquare) + (((((ge_norm_rp_complete_searchfoundnorm) * (ge_norm_rn_complete_searchfoundnorm))) + (((ge_norm_rn_complete_searchfoundnorm) * (ge_norm_rp_complete_searchfoundnorm))))))) /\ ((((((ge_norm_ip_complete_searchfoundnorm) * (ge_norm_ip_complete_searchfoundnorm))) + (((ge_norm_in_complete_searchfoundnorm) * (ge_norm_in_complete_searchfoundnorm)))) = ((ge_imaginary_square_complete_searchfoundnormsquare) + (((((ge_norm_ip_complete_searchfoundnorm) * (ge_norm_in_complete_searchfoundnorm))) + (((ge_norm_in_complete_searchfoundnorm) * (ge_norm_ip_complete_searchfoundnorm))))))) /\ ((gr_proper_divisor_norm_complete_searchfound) = ge_real_square_complete_searchfoundnormsquare + ge_imaginary_square_complete_searchfoundnormsquare)))))) /\ (exists ge_gap_complete_searchfoundstrict. ge_gap_complete_searchfoundstrict + S (gr_proper_divisor_norm_complete_searchfound) = (N)))))))) \/ (forall gr_complete_divisor_complete_search. ~(((~(exists gr_inverse_complete_searchabsentnonunit. (exists ge_first_rp_complete_searchabsentnonunitidentity ge_first_rn_complete_searchabsentnonunitidentity ge_first_ip_complete_searchabsentnonunitidentity ge_first_in_complete_searchabsentnonunitidentity ge_second_rp_complete_searchabsentnonunitidentity ge_second_rn_complete_searchabsentnonunitidentity ge_second_ip_complete_searchabsentnonunitidentity ge_second_in_complete_searchabsentnonunitidentity. ((exists ge_representation_real_code_complete_searchabsentnonunitidentityfirst ge_representation_imaginary_code_complete_searchabsentnonunitidentityfirst. (((gr_complete_divisor_complete_search) = ((ge_representation_real_code_complete_searchabsentnonunitidentityfirst) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentityfirst)) * S ((ge_representation_real_code_complete_searchabsentnonunitidentityfirst) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentityfirst)) + ((ge_representation_imaginary_code_complete_searchabsentnonunitidentityfirst) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentityfirst))) /\ ((exists ge_balance_positive_complete_searchabsentnonunitidentityfirstreal ge_balance_negative_complete_searchabsentnonunitidentityfirstreal. (((((ge_representation_real_code_complete_searchabsentnonunitidentityfirst) = 2 * (ge_balance_positive_complete_searchabsentnonunitidentityfirstreal) /\ (ge_balance_negative_complete_searchabsentnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_complete_searchabsentnonunitidentityfirstrealdecode. (((ge_representation_real_code_complete_searchabsentnonunitidentityfirst) = 2 * ge_signed_half_complete_searchabsentnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_complete_searchabsentnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_complete_searchabsentnonunitidentityfirstreal) = S ge_signed_half_complete_searchabsentnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_complete_searchabsentnonunitidentity) + ge_balance_negative_complete_searchabsentnonunitidentityfirstreal = (ge_first_rn_complete_searchabsentnonunitidentity) + ge_balance_positive_complete_searchabsentnonunitidentityfirstreal))) /\ (exists ge_balance_positive_complete_searchabsentnonunitidentityfirstimaginary ge_balance_negative_complete_searchabsentnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_complete_searchabsentnonunitidentityfirst) = 2 * (ge_balance_positive_complete_searchabsentnonunitidentityfirstimaginary) /\ (ge_balance_negative_complete_searchabsentnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_complete_searchabsentnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_complete_searchabsentnonunitidentityfirst) = 2 * ge_signed_half_complete_searchabsentnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_complete_searchabsentnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_complete_searchabsentnonunitidentityfirstimaginary) = S ge_signed_half_complete_searchabsentnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_complete_searchabsentnonunitidentity) + ge_balance_negative_complete_searchabsentnonunitidentityfirstimaginary = (ge_first_in_complete_searchabsentnonunitidentity) + ge_balance_positive_complete_searchabsentnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_complete_searchabsentnonunitidentitysecond ge_representation_imaginary_code_complete_searchabsentnonunitidentitysecond. (((gr_inverse_complete_searchabsentnonunit) = ((ge_representation_real_code_complete_searchabsentnonunitidentitysecond) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentitysecond)) * S ((ge_representation_real_code_complete_searchabsentnonunitidentitysecond) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentitysecond)) + ((ge_representation_imaginary_code_complete_searchabsentnonunitidentitysecond) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentitysecond))) /\ ((exists ge_balance_positive_complete_searchabsentnonunitidentitysecondreal ge_balance_negative_complete_searchabsentnonunitidentitysecondreal. (((((ge_representation_real_code_complete_searchabsentnonunitidentitysecond) = 2 * (ge_balance_positive_complete_searchabsentnonunitidentitysecondreal) /\ (ge_balance_negative_complete_searchabsentnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_complete_searchabsentnonunitidentitysecondrealdecode. (((ge_representation_real_code_complete_searchabsentnonunitidentitysecond) = 2 * ge_signed_half_complete_searchabsentnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_complete_searchabsentnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_complete_searchabsentnonunitidentitysecondreal) = S ge_signed_half_complete_searchabsentnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_complete_searchabsentnonunitidentity) + ge_balance_negative_complete_searchabsentnonunitidentitysecondreal = (ge_second_rn_complete_searchabsentnonunitidentity) + ge_balance_positive_complete_searchabsentnonunitidentitysecondreal))) /\ (exists ge_balance_positive_complete_searchabsentnonunitidentitysecondimaginary ge_balance_negative_complete_searchabsentnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_complete_searchabsentnonunitidentitysecond) = 2 * (ge_balance_positive_complete_searchabsentnonunitidentitysecondimaginary) /\ (ge_balance_negative_complete_searchabsentnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_complete_searchabsentnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_complete_searchabsentnonunitidentitysecond) = 2 * ge_signed_half_complete_searchabsentnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_complete_searchabsentnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_complete_searchabsentnonunitidentitysecondimaginary) = S ge_signed_half_complete_searchabsentnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_complete_searchabsentnonunitidentity) + ge_balance_negative_complete_searchabsentnonunitidentitysecondimaginary = (ge_second_in_complete_searchabsentnonunitidentity) + ge_balance_positive_complete_searchabsentnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_complete_searchabsentnonunitidentityoutput ge_representation_imaginary_code_complete_searchabsentnonunitidentityoutput. (((6) = ((ge_representation_real_code_complete_searchabsentnonunitidentityoutput) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentityoutput)) * S ((ge_representation_real_code_complete_searchabsentnonunitidentityoutput) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentityoutput)) + ((ge_representation_imaginary_code_complete_searchabsentnonunitidentityoutput) + (ge_representation_imaginary_code_complete_searchabsentnonunitidentityoutput))) /\ ((exists ge_balance_positive_complete_searchabsentnonunitidentityoutputreal ge_balance_negative_complete_searchabsentnonunitidentityoutputreal. (((((ge_representation_real_code_complete_searchabsentnonunitidentityoutput) = 2 * (ge_balance_positive_complete_searchabsentnonunitidentityoutputreal) /\ (ge_balance_negative_complete_searchabsentnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_complete_searchabsentnonunitidentityoutputrealdecode. (((ge_representation_real_code_complete_searchabsentnonunitidentityoutput) = 2 * ge_signed_half_complete_searchabsentnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_complete_searchabsentnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_complete_searchabsentnonunitidentityoutputreal) = S ge_signed_half_complete_searchabsentnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_complete_searchabsentnonunitidentity) * (ge_second_rp_complete_searchabsentnonunitidentity))) + (((ge_first_rn_complete_searchabsentnonunitidentity) * (ge_second_rn_complete_searchabsentnonunitidentity))))) + (((((ge_first_ip_complete_searchabsentnonunitidentity) * (ge_second_in_complete_searchabsentnonunitidentity))) + (((ge_first_in_complete_searchabsentnonunitidentity) * (ge_second_ip_complete_searchabsentnonunitidentity))))))) + ge_balance_negative_complete_searchabsentnonunitidentityoutputreal = (((((((ge_first_rp_complete_searchabsentnonunitidentity) * (ge_second_rn_complete_searchabsentnonunitidentity))) + (((ge_first_rn_complete_searchabsentnonunitidentity) * (ge_second_rp_complete_searchabsentnonunitidentity))))) + (((((ge_first_ip_complete_searchabsentnonunitidentity) * (ge_second_ip_complete_searchabsentnonunitidentity))) + (((ge_first_in_complete_searchabsentnonunitidentity) * (ge_second_in_complete_searchabsentnonunitidentity))))))) + ge_balance_positive_complete_searchabsentnonunitidentityoutputreal))) /\ (exists ge_balance_positive_complete_searchabsentnonunitidentityoutputimaginary ge_balance_negative_complete_searchabsentnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_complete_searchabsentnonunitidentityoutput) = 2 * (ge_balance_positive_complete_searchabsentnonunitidentityoutputimaginary) /\ (ge_balance_negative_complete_searchabsentnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_complete_searchabsentnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_complete_searchabsentnonunitidentityoutput) = 2 * ge_signed_half_complete_searchabsentnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_complete_searchabsentnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_complete_searchabsentnonunitidentityoutputimaginary) = S ge_signed_half_complete_searchabsentnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_complete_searchabsentnonunitidentity) * (ge_second_ip_complete_searchabsentnonunitidentity))) + (((ge_first_rn_complete_searchabsentnonunitidentity) * (ge_second_in_complete_searchabsentnonunitidentity))))) + (((((ge_first_ip_complete_searchabsentnonunitidentity) * (ge_second_rp_complete_searchabsentnonunitidentity))) + (((ge_first_in_complete_searchabsentnonunitidentity) * (ge_second_rn_complete_searchabsentnonunitidentity))))))) + ge_balance_negative_complete_searchabsentnonunitidentityoutputimaginary = (((((((ge_first_rp_complete_searchabsentnonunitidentity) * (ge_second_in_complete_searchabsentnonunitidentity))) + (((ge_first_rn_complete_searchabsentnonunitidentity) * (ge_second_ip_complete_searchabsentnonunitidentity))))) + (((((ge_first_ip_complete_searchabsentnonunitidentity) * (ge_second_rn_complete_searchabsentnonunitidentity))) + (((ge_first_in_complete_searchabsentnonunitidentity) * (ge_second_rp_complete_searchabsentnonunitidentity))))))) + ge_balance_positive_complete_searchabsentnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_complete_searchabsentquotient. (exists ge_first_rp_complete_searchabsentquotientproduct ge_first_rn_complete_searchabsentquotientproduct ge_first_ip_complete_searchabsentquotientproduct ge_first_in_complete_searchabsentquotientproduct ge_second_rp_complete_searchabsentquotientproduct ge_second_rn_complete_searchabsentquotientproduct ge_second_ip_complete_searchabsentquotientproduct ge_second_in_complete_searchabsentquotientproduct. ((exists ge_representation_real_code_complete_searchabsentquotientproductfirst ge_representation_imaginary_code_complete_searchabsentquotientproductfirst. (((gr_complete_divisor_complete_search) = ((ge_representation_real_code_complete_searchabsentquotientproductfirst) + (ge_representation_imaginary_code_complete_searchabsentquotientproductfirst)) * S ((ge_representation_real_code_complete_searchabsentquotientproductfirst) + (ge_representation_imaginary_code_complete_searchabsentquotientproductfirst)) + ((ge_representation_imaginary_code_complete_searchabsentquotientproductfirst) + (ge_representation_imaginary_code_complete_searchabsentquotientproductfirst))) /\ ((exists ge_balance_positive_complete_searchabsentquotientproductfirstreal ge_balance_negative_complete_searchabsentquotientproductfirstreal. (((((ge_representation_real_code_complete_searchabsentquotientproductfirst) = 2 * (ge_balance_positive_complete_searchabsentquotientproductfirstreal) /\ (ge_balance_negative_complete_searchabsentquotientproductfirstreal) = 0) \/ exists ge_signed_half_complete_searchabsentquotientproductfirstrealdecode. (((ge_representation_real_code_complete_searchabsentquotientproductfirst) = 2 * ge_signed_half_complete_searchabsentquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_complete_searchabsentquotientproductfirstreal) = 0) /\ (ge_balance_negative_complete_searchabsentquotientproductfirstreal) = S ge_signed_half_complete_searchabsentquotientproductfirstrealdecode))) /\ ((ge_first_rp_complete_searchabsentquotientproduct) + ge_balance_negative_complete_searchabsentquotientproductfirstreal = (ge_first_rn_complete_searchabsentquotientproduct) + ge_balance_positive_complete_searchabsentquotientproductfirstreal))) /\ (exists ge_balance_positive_complete_searchabsentquotientproductfirstimaginary ge_balance_negative_complete_searchabsentquotientproductfirstimaginary. (((((ge_representation_imaginary_code_complete_searchabsentquotientproductfirst) = 2 * (ge_balance_positive_complete_searchabsentquotientproductfirstimaginary) /\ (ge_balance_negative_complete_searchabsentquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_complete_searchabsentquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_complete_searchabsentquotientproductfirst) = 2 * ge_signed_half_complete_searchabsentquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_complete_searchabsentquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_complete_searchabsentquotientproductfirstimaginary) = S ge_signed_half_complete_searchabsentquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_complete_searchabsentquotientproduct) + ge_balance_negative_complete_searchabsentquotientproductfirstimaginary = (ge_first_in_complete_searchabsentquotientproduct) + ge_balance_positive_complete_searchabsentquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_complete_searchabsentquotientproductsecond ge_representation_imaginary_code_complete_searchabsentquotientproductsecond. (((gr_quotient_complete_searchabsentquotient) = ((ge_representation_real_code_complete_searchabsentquotientproductsecond) + (ge_representation_imaginary_code_complete_searchabsentquotientproductsecond)) * S ((ge_representation_real_code_complete_searchabsentquotientproductsecond) + (ge_representation_imaginary_code_complete_searchabsentquotientproductsecond)) + ((ge_representation_imaginary_code_complete_searchabsentquotientproductsecond) + (ge_representation_imaginary_code_complete_searchabsentquotientproductsecond))) /\ ((exists ge_balance_positive_complete_searchabsentquotientproductsecondreal ge_balance_negative_complete_searchabsentquotientproductsecondreal. (((((ge_representation_real_code_complete_searchabsentquotientproductsecond) = 2 * (ge_balance_positive_complete_searchabsentquotientproductsecondreal) /\ (ge_balance_negative_complete_searchabsentquotientproductsecondreal) = 0) \/ exists ge_signed_half_complete_searchabsentquotientproductsecondrealdecode. (((ge_representation_real_code_complete_searchabsentquotientproductsecond) = 2 * ge_signed_half_complete_searchabsentquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_complete_searchabsentquotientproductsecondreal) = 0) /\ (ge_balance_negative_complete_searchabsentquotientproductsecondreal) = S ge_signed_half_complete_searchabsentquotientproductsecondrealdecode))) /\ ((ge_second_rp_complete_searchabsentquotientproduct) + ge_balance_negative_complete_searchabsentquotientproductsecondreal = (ge_second_rn_complete_searchabsentquotientproduct) + ge_balance_positive_complete_searchabsentquotientproductsecondreal))) /\ (exists ge_balance_positive_complete_searchabsentquotientproductsecondimaginary ge_balance_negative_complete_searchabsentquotientproductsecondimaginary. (((((ge_representation_imaginary_code_complete_searchabsentquotientproductsecond) = 2 * (ge_balance_positive_complete_searchabsentquotientproductsecondimaginary) /\ (ge_balance_negative_complete_searchabsentquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_complete_searchabsentquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_complete_searchabsentquotientproductsecond) = 2 * ge_signed_half_complete_searchabsentquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_complete_searchabsentquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_complete_searchabsentquotientproductsecondimaginary) = S ge_signed_half_complete_searchabsentquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_complete_searchabsentquotientproduct) + ge_balance_negative_complete_searchabsentquotientproductsecondimaginary = (ge_second_in_complete_searchabsentquotientproduct) + ge_balance_positive_complete_searchabsentquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_complete_searchabsentquotientproductoutput ge_representation_imaginary_code_complete_searchabsentquotientproductoutput. (((z) = ((ge_representation_real_code_complete_searchabsentquotientproductoutput) + (ge_representation_imaginary_code_complete_searchabsentquotientproductoutput)) * S ((ge_representation_real_code_complete_searchabsentquotientproductoutput) + (ge_representation_imaginary_code_complete_searchabsentquotientproductoutput)) + ((ge_representation_imaginary_code_complete_searchabsentquotientproductoutput) + (ge_representation_imaginary_code_complete_searchabsentquotientproductoutput))) /\ ((exists ge_balance_positive_complete_searchabsentquotientproductoutputreal ge_balance_negative_complete_searchabsentquotientproductoutputreal. (((((ge_representation_real_code_complete_searchabsentquotientproductoutput) = 2 * (ge_balance_positive_complete_searchabsentquotientproductoutputreal) /\ (ge_balance_negative_complete_searchabsentquotientproductoutputreal) = 0) \/ exists ge_signed_half_complete_searchabsentquotientproductoutputrealdecode. (((ge_representation_real_code_complete_searchabsentquotientproductoutput) = 2 * ge_signed_half_complete_searchabsentquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_complete_searchabsentquotientproductoutputreal) = 0) /\ (ge_balance_negative_complete_searchabsentquotientproductoutputreal) = S ge_signed_half_complete_searchabsentquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_complete_searchabsentquotientproduct) * (ge_second_rp_complete_searchabsentquotientproduct))) + (((ge_first_rn_complete_searchabsentquotientproduct) * (ge_second_rn_complete_searchabsentquotientproduct))))) + (((((ge_first_ip_complete_searchabsentquotientproduct) * (ge_second_in_complete_searchabsentquotientproduct))) + (((ge_first_in_complete_searchabsentquotientproduct) * (ge_second_ip_complete_searchabsentquotientproduct))))))) + ge_balance_negative_complete_searchabsentquotientproductoutputreal = (((((((ge_first_rp_complete_searchabsentquotientproduct) * (ge_second_rn_complete_searchabsentquotientproduct))) + (((ge_first_rn_complete_searchabsentquotientproduct) * (ge_second_rp_complete_searchabsentquotientproduct))))) + (((((ge_first_ip_complete_searchabsentquotientproduct) * (ge_second_ip_complete_searchabsentquotientproduct))) + (((ge_first_in_complete_searchabsentquotientproduct) * (ge_second_in_complete_searchabsentquotientproduct))))))) + ge_balance_positive_complete_searchabsentquotientproductoutputreal))) /\ (exists ge_balance_positive_complete_searchabsentquotientproductoutputimaginary ge_balance_negative_complete_searchabsentquotientproductoutputimaginary. (((((ge_representation_imaginary_code_complete_searchabsentquotientproductoutput) = 2 * (ge_balance_positive_complete_searchabsentquotientproductoutputimaginary) /\ (ge_balance_negative_complete_searchabsentquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_complete_searchabsentquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_complete_searchabsentquotientproductoutput) = 2 * ge_signed_half_complete_searchabsentquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_complete_searchabsentquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_complete_searchabsentquotientproductoutputimaginary) = S ge_signed_half_complete_searchabsentquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_complete_searchabsentquotientproduct) * (ge_second_ip_complete_searchabsentquotientproduct))) + (((ge_first_rn_complete_searchabsentquotientproduct) * (ge_second_in_complete_searchabsentquotientproduct))))) + (((((ge_first_ip_complete_searchabsentquotientproduct) * (ge_second_rp_complete_searchabsentquotientproduct))) + (((ge_first_in_complete_searchabsentquotientproduct) * (ge_second_rn_complete_searchabsentquotientproduct))))))) + ge_balance_negative_complete_searchabsentquotientproductoutputimaginary = (((((((ge_first_rp_complete_searchabsentquotientproduct) * (ge_second_in_complete_searchabsentquotientproduct))) + (((ge_first_rn_complete_searchabsentquotientproduct) * (ge_second_ip_complete_searchabsentquotientproduct))))) + (((((ge_first_ip_complete_searchabsentquotientproduct) * (ge_second_rn_complete_searchabsentquotientproduct))) + (((ge_first_in_complete_searchabsentquotientproduct) * (ge_second_rp_complete_searchabsentquotientproduct))))))) + ge_balance_positive_complete_searchabsentquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_complete_searchabsent. ((exists ge_norm_rp_complete_searchabsentnorm ge_norm_rn_complete_searchabsentnorm ge_norm_ip_complete_searchabsentnorm ge_norm_in_complete_searchabsentnorm. ((exists ge_representation_real_code_complete_searchabsentnormrepresentation ge_representation_imaginary_code_complete_searchabsentnormrepresentation. (((gr_complete_divisor_complete_search) = ((ge_representation_real_code_complete_searchabsentnormrepresentation) + (ge_representation_imaginary_code_complete_searchabsentnormrepresentation)) * S ((ge_representation_real_code_complete_searchabsentnormrepresentation) + (ge_representation_imaginary_code_complete_searchabsentnormrepresentation)) + ((ge_representation_imaginary_code_complete_searchabsentnormrepresentation) + (ge_representation_imaginary_code_complete_searchabsentnormrepresentation))) /\ ((exists ge_balance_positive_complete_searchabsentnormrepresentationreal ge_balance_negative_complete_searchabsentnormrepresentationreal. (((((ge_representation_real_code_complete_searchabsentnormrepresentation) = 2 * (ge_balance_positive_complete_searchabsentnormrepresentationreal) /\ (ge_balance_negative_complete_searchabsentnormrepresentationreal) = 0) \/ exists ge_signed_half_complete_searchabsentnormrepresentationrealdecode. (((ge_representation_real_code_complete_searchabsentnormrepresentation) = 2 * ge_signed_half_complete_searchabsentnormrepresentationrealdecode + 1 /\ (ge_balance_positive_complete_searchabsentnormrepresentationreal) = 0) /\ (ge_balance_negative_complete_searchabsentnormrepresentationreal) = S ge_signed_half_complete_searchabsentnormrepresentationrealdecode))) /\ ((ge_norm_rp_complete_searchabsentnorm) + ge_balance_negative_complete_searchabsentnormrepresentationreal = (ge_norm_rn_complete_searchabsentnorm) + ge_balance_positive_complete_searchabsentnormrepresentationreal))) /\ (exists ge_balance_positive_complete_searchabsentnormrepresentationimaginary ge_balance_negative_complete_searchabsentnormrepresentationimaginary. (((((ge_representation_imaginary_code_complete_searchabsentnormrepresentation) = 2 * (ge_balance_positive_complete_searchabsentnormrepresentationimaginary) /\ (ge_balance_negative_complete_searchabsentnormrepresentationimaginary) = 0) \/ exists ge_signed_half_complete_searchabsentnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_complete_searchabsentnormrepresentation) = 2 * ge_signed_half_complete_searchabsentnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_complete_searchabsentnormrepresentationimaginary) = 0) /\ (ge_balance_negative_complete_searchabsentnormrepresentationimaginary) = S ge_signed_half_complete_searchabsentnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_complete_searchabsentnorm) + ge_balance_negative_complete_searchabsentnormrepresentationimaginary = (ge_norm_in_complete_searchabsentnorm) + ge_balance_positive_complete_searchabsentnormrepresentationimaginary)))))) /\ (exists ge_real_square_complete_searchabsentnormsquare ge_imaginary_square_complete_searchabsentnormsquare. ((((((ge_norm_rp_complete_searchabsentnorm) * (ge_norm_rp_complete_searchabsentnorm))) + (((ge_norm_rn_complete_searchabsentnorm) * (ge_norm_rn_complete_searchabsentnorm)))) = ((ge_real_square_complete_searchabsentnormsquare) + (((((ge_norm_rp_complete_searchabsentnorm) * (ge_norm_rn_complete_searchabsentnorm))) + (((ge_norm_rn_complete_searchabsentnorm) * (ge_norm_rp_complete_searchabsentnorm))))))) /\ ((((((ge_norm_ip_complete_searchabsentnorm) * (ge_norm_ip_complete_searchabsentnorm))) + (((ge_norm_in_complete_searchabsentnorm) * (ge_norm_in_complete_searchabsentnorm)))) = ((ge_imaginary_square_complete_searchabsentnormsquare) + (((((ge_norm_ip_complete_searchabsentnorm) * (ge_norm_in_complete_searchabsentnorm))) + (((ge_norm_in_complete_searchabsentnorm) * (ge_norm_ip_complete_searchabsentnorm))))))) /\ ((gr_proper_divisor_norm_complete_searchabsent) = ge_real_square_complete_searchabsentnormsquare + ge_imaginary_square_complete_searchabsentnormsquare)))))) /\ (exists ge_gap_complete_searchabsentstrict. ge_gap_complete_searchabsentstrict + S (gr_proper_divisor_norm_complete_searchabsent) = (N)))))))))