GAllPrime(b,c,l)

forall gr_prime_factor_index_gaussianfactorization gr_prime_factor_value_gaussianfactorization. (exists ge_gap_gaussianfactorizationindex. ge_gap_gaussianfactorizationindex + S (gr_prime_factor_index_gaussianfactorization) = ((l))) -> (((exists ff_h_gprod_gaussianfactorizationentry. ff_h_gprod_gaussianfactorizationentry + S (gr_prime_factor_value_gaussianfactorization) = S ((S (gr_prime_factor_index_gaussianfactorization)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationentry. (b) = ff_q_gprod_gaussianfactorizationentry * S ((S (gr_prime_factor_index_gaussianfactorization)) * (c)) + (gr_prime_factor_value_gaussianfactorization))) -> (((exists ge_real_positive_gaussianfactorizationprimecarrier ge_real_negative_gaussianfactorizationprimecarrier ge_imaginary_positive_gaussianfactorizationprimecarrier ge_imaginary_negative_gaussianfactorizationprimecarrier. (exists ge_real_code_gaussianfactorizationprimecarrierdecode ge_imaginary_code_gaussianfactorizationprimecarrierdecode. (((gr_prime_factor_value_gaussianfactorization) = ((ge_real_code_gaussianfactorizationprimecarrierdecode) + (ge_imaginary_code_gaussianfactorizationprimecarrierdecode)) * S ((ge_real_code_gaussianfactorizationprimecarrierdecode) + (ge_imaginary_code_gaussianfactorizationprimecarrierdecode)) + ((ge_imaginary_code_gaussianfactorizationprimecarrierdecode) + (ge_imaginary_code_gaussianfactorizationprimecarrierdecode))) /\ (((((ge_real_code_gaussianfactorizationprimecarrierdecode) = 2 * (ge_real_positive_gaussianfactorizationprimecarrier) /\ (ge_real_negative_gaussianfactorizationprimecarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationprimecarrierdecode_real. (((ge_real_code_gaussianfactorizationprimecarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationprimecarrierdecode_real + 1 /\ (ge_real_positive_gaussianfactorizationprimecarrier) = 0) /\ (ge_real_negative_gaussianfactorizationprimecarrier) = S ge_signed_half_ge_gaussianfactorizationprimecarrierdecode_real))) /\ ((((ge_imaginary_code_gaussianfactorizationprimecarrierdecode) = 2 * (ge_imaginary_positive_gaussianfactorizationprimecarrier) /\ (ge_imaginary_negative_gaussianfactorizationprimecarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationprimecarrierdecode_imaginary. (((ge_imaginary_code_gaussianfactorizationprimecarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_gaussianfactorizationprimecarrier) = 0) /\ (ge_imaginary_negative_gaussianfactorizationprimecarrier) = S ge_signed_half_ge_gaussianfactorizationprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_gaussianfactorization)=0)) /\ ((~(exists gr_inverse_gaussianfactorizationprimenonunit. (exists ge_first_rp_gaussianfactorizationprimenonunitidentity ge_first_rn_gaussianfactorizationprimenonunitidentity ge_first_ip_gaussianfactorizationprimenonunitidentity ge_first_in_gaussianfactorizationprimenonunitidentity ge_second_rp_gaussianfactorizationprimenonunitidentity ge_second_rn_gaussianfactorizationprimenonunitidentity ge_second_ip_gaussianfactorizationprimenonunitidentity ge_second_in_gaussianfactorizationprimenonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationprimenonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityfirst. (((gr_prime_factor_value_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationprimenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimenonunitidentityfirstreal ge_balance_negative_gaussianfactorizationprimenonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimenonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimenonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimenonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimenonunitidentity) + ge_balance_negative_gaussianfactorizationprimenonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationprimenonunitidentity) + ge_balance_positive_gaussianfactorizationprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimenonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimenonunitidentity) + ge_balance_negative_gaussianfactorizationprimenonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationprimenonunitidentity) + ge_balance_positive_gaussianfactorizationprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimenonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentitysecond. (((gr_inverse_gaussianfactorizationprimenonunit) = ((ge_representation_real_code_gaussianfactorizationprimenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationprimenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimenonunitidentitysecondreal ge_balance_negative_gaussianfactorizationprimenonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationprimenonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationprimenonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimenonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimenonunitidentity) + ge_balance_negative_gaussianfactorizationprimenonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationprimenonunitidentity) + ge_balance_positive_gaussianfactorizationprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimenonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimenonunitidentity) + ge_balance_negative_gaussianfactorizationprimenonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationprimenonunitidentity) + ge_balance_positive_gaussianfactorizationprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimenonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationprimenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimenonunitidentityoutputreal ge_balance_negative_gaussianfactorizationprimenonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimenonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimenonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimenonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimenonunitidentity) * (ge_second_rp_gaussianfactorizationprimenonunitidentity))) + (((ge_first_rn_gaussianfactorizationprimenonunitidentity) * (ge_second_rn_gaussianfactorizationprimenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationprimenonunitidentity) * (ge_second_in_gaussianfactorizationprimenonunitidentity))) + (((ge_first_in_gaussianfactorizationprimenonunitidentity) * (ge_second_ip_gaussianfactorizationprimenonunitidentity))))))) + ge_balance_negative_gaussianfactorizationprimenonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationprimenonunitidentity) * (ge_second_rn_gaussianfactorizationprimenonunitidentity))) + (((ge_first_rn_gaussianfactorizationprimenonunitidentity) * (ge_second_rp_gaussianfactorizationprimenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationprimenonunitidentity) * (ge_second_ip_gaussianfactorizationprimenonunitidentity))) + (((ge_first_in_gaussianfactorizationprimenonunitidentity) * (ge_second_in_gaussianfactorizationprimenonunitidentity))))))) + ge_balance_positive_gaussianfactorizationprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimenonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimenonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimenonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimenonunitidentity) * (ge_second_ip_gaussianfactorizationprimenonunitidentity))) + (((ge_first_rn_gaussianfactorizationprimenonunitidentity) * (ge_second_in_gaussianfactorizationprimenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationprimenonunitidentity) * (ge_second_rp_gaussianfactorizationprimenonunitidentity))) + (((ge_first_in_gaussianfactorizationprimenonunitidentity) * (ge_second_rn_gaussianfactorizationprimenonunitidentity))))))) + ge_balance_negative_gaussianfactorizationprimenonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimenonunitidentity) * (ge_second_in_gaussianfactorizationprimenonunitidentity))) + (((ge_first_rn_gaussianfactorizationprimenonunitidentity) * (ge_second_ip_gaussianfactorizationprimenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationprimenonunitidentity) * (ge_second_rn_gaussianfactorizationprimenonunitidentity))) + (((ge_first_in_gaussianfactorizationprimenonunitidentity) * (ge_second_rp_gaussianfactorizationprimenonunitidentity))))))) + ge_balance_positive_gaussianfactorizationprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_gaussianfactorizationprime gr_second_factor_gaussianfactorizationprime gr_product_gaussianfactorizationprime. (exists ge_first_rp_gaussianfactorizationprimeproduct ge_first_rn_gaussianfactorizationprimeproduct ge_first_ip_gaussianfactorizationprimeproduct ge_first_in_gaussianfactorizationprimeproduct ge_second_rp_gaussianfactorizationprimeproduct ge_second_rn_gaussianfactorizationprimeproduct ge_second_ip_gaussianfactorizationprimeproduct ge_second_in_gaussianfactorizationprimeproduct. ((exists ge_representation_real_code_gaussianfactorizationprimeproductfirst ge_representation_imaginary_code_gaussianfactorizationprimeproductfirst. (((gr_first_factor_gaussianfactorizationprime) = ((ge_representation_real_code_gaussianfactorizationprimeproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimeproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimeproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimeproductfirstreal ge_balance_negative_gaussianfactorizationprimeproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimeproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimeproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimeproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimeproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimeproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimeproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimeproductfirstreal) = S ge_signed_half_gaussianfactorizationprimeproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimeproduct) + ge_balance_negative_gaussianfactorizationprimeproductfirstreal = (ge_first_rn_gaussianfactorizationprimeproduct) + ge_balance_positive_gaussianfactorizationprimeproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimeproductfirstimaginary ge_balance_negative_gaussianfactorizationprimeproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimeproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimeproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimeproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimeproductfirstimaginary) = S ge_signed_half_gaussianfactorizationprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimeproduct) + ge_balance_negative_gaussianfactorizationprimeproductfirstimaginary = (ge_first_in_gaussianfactorizationprimeproduct) + ge_balance_positive_gaussianfactorizationprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimeproductsecond ge_representation_imaginary_code_gaussianfactorizationprimeproductsecond. (((gr_second_factor_gaussianfactorizationprime) = ((ge_representation_real_code_gaussianfactorizationprimeproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationprimeproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimeproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimeproductsecondreal ge_balance_negative_gaussianfactorizationprimeproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationprimeproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimeproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationprimeproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimeproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimeproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimeproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimeproductsecondreal) = S ge_signed_half_gaussianfactorizationprimeproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimeproduct) + ge_balance_negative_gaussianfactorizationprimeproductsecondreal = (ge_second_rn_gaussianfactorizationprimeproduct) + ge_balance_positive_gaussianfactorizationprimeproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimeproductsecondimaginary ge_balance_negative_gaussianfactorizationprimeproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimeproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimeproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimeproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimeproductsecondimaginary) = S ge_signed_half_gaussianfactorizationprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimeproduct) + ge_balance_negative_gaussianfactorizationprimeproductsecondimaginary = (ge_second_in_gaussianfactorizationprimeproduct) + ge_balance_positive_gaussianfactorizationprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimeproductoutput ge_representation_imaginary_code_gaussianfactorizationprimeproductoutput. (((gr_product_gaussianfactorizationprime) = ((ge_representation_real_code_gaussianfactorizationprimeproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimeproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimeproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimeproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimeproductoutputreal ge_balance_negative_gaussianfactorizationprimeproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimeproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimeproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimeproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimeproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimeproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimeproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimeproductoutputreal) = S ge_signed_half_gaussianfactorizationprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimeproduct) * (ge_second_rp_gaussianfactorizationprimeproduct))) + (((ge_first_rn_gaussianfactorizationprimeproduct) * (ge_second_rn_gaussianfactorizationprimeproduct))))) + (((((ge_first_ip_gaussianfactorizationprimeproduct) * (ge_second_in_gaussianfactorizationprimeproduct))) + (((ge_first_in_gaussianfactorizationprimeproduct) * (ge_second_ip_gaussianfactorizationprimeproduct))))))) + ge_balance_negative_gaussianfactorizationprimeproductoutputreal = (((((((ge_first_rp_gaussianfactorizationprimeproduct) * (ge_second_rn_gaussianfactorizationprimeproduct))) + (((ge_first_rn_gaussianfactorizationprimeproduct) * (ge_second_rp_gaussianfactorizationprimeproduct))))) + (((((ge_first_ip_gaussianfactorizationprimeproduct) * (ge_second_ip_gaussianfactorizationprimeproduct))) + (((ge_first_in_gaussianfactorizationprimeproduct) * (ge_second_in_gaussianfactorizationprimeproduct))))))) + ge_balance_positive_gaussianfactorizationprimeproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimeproductoutputimaginary ge_balance_negative_gaussianfactorizationprimeproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimeproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimeproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimeproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimeproductoutputimaginary) = S ge_signed_half_gaussianfactorizationprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimeproduct) * (ge_second_ip_gaussianfactorizationprimeproduct))) + (((ge_first_rn_gaussianfactorizationprimeproduct) * (ge_second_in_gaussianfactorizationprimeproduct))))) + (((((ge_first_ip_gaussianfactorizationprimeproduct) * (ge_second_rp_gaussianfactorizationprimeproduct))) + (((ge_first_in_gaussianfactorizationprimeproduct) * (ge_second_rn_gaussianfactorizationprimeproduct))))))) + ge_balance_negative_gaussianfactorizationprimeproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimeproduct) * (ge_second_in_gaussianfactorizationprimeproduct))) + (((ge_first_rn_gaussianfactorizationprimeproduct) * (ge_second_ip_gaussianfactorizationprimeproduct))))) + (((((ge_first_ip_gaussianfactorizationprimeproduct) * (ge_second_rn_gaussianfactorizationprimeproduct))) + (((ge_first_in_gaussianfactorizationprimeproduct) * (ge_second_rp_gaussianfactorizationprimeproduct))))))) + ge_balance_positive_gaussianfactorizationprimeproductoutputimaginary))))))))) -> (exists gr_quotient_gaussianfactorizationprimedivisor. (exists ge_first_rp_gaussianfactorizationprimedivisorproduct ge_first_rn_gaussianfactorizationprimedivisorproduct ge_first_ip_gaussianfactorizationprimedivisorproduct ge_first_in_gaussianfactorizationprimedivisorproduct ge_second_rp_gaussianfactorizationprimedivisorproduct ge_second_rn_gaussianfactorizationprimedivisorproduct ge_second_ip_gaussianfactorizationprimedivisorproduct ge_second_in_gaussianfactorizationprimedivisorproduct. ((exists ge_representation_real_code_gaussianfactorizationprimedivisorproductfirst ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductfirst. (((gr_prime_factor_value_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationprimedivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimedivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimedivisorproductfirstreal ge_balance_negative_gaussianfactorizationprimedivisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimedivisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimedivisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimedivisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimedivisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductfirstreal) = S ge_signed_half_gaussianfactorizationprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimedivisorproduct) + ge_balance_negative_gaussianfactorizationprimedivisorproductfirstreal = (ge_first_rn_gaussianfactorizationprimedivisorproduct) + ge_balance_positive_gaussianfactorizationprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimedivisorproductfirstimaginary ge_balance_negative_gaussianfactorizationprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimedivisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimedivisorproduct) + ge_balance_negative_gaussianfactorizationprimedivisorproductfirstimaginary = (ge_first_in_gaussianfactorizationprimedivisorproduct) + ge_balance_positive_gaussianfactorizationprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimedivisorproductsecond ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductsecond. (((gr_quotient_gaussianfactorizationprimedivisor) = ((ge_representation_real_code_gaussianfactorizationprimedivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationprimedivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimedivisorproductsecondreal ge_balance_negative_gaussianfactorizationprimedivisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationprimedivisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimedivisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimedivisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimedivisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductsecondreal) = S ge_signed_half_gaussianfactorizationprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimedivisorproduct) + ge_balance_negative_gaussianfactorizationprimedivisorproductsecondreal = (ge_second_rn_gaussianfactorizationprimedivisorproduct) + ge_balance_positive_gaussianfactorizationprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimedivisorproductsecondimaginary ge_balance_negative_gaussianfactorizationprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimedivisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimedivisorproduct) + ge_balance_negative_gaussianfactorizationprimedivisorproductsecondimaginary = (ge_second_in_gaussianfactorizationprimedivisorproduct) + ge_balance_positive_gaussianfactorizationprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimedivisorproductoutput ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductoutput. (((gr_product_gaussianfactorizationprime) = ((ge_representation_real_code_gaussianfactorizationprimedivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimedivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimedivisorproductoutputreal ge_balance_negative_gaussianfactorizationprimedivisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimedivisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimedivisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimedivisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimedivisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductoutputreal) = S ge_signed_half_gaussianfactorizationprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimedivisorproduct) * (ge_second_rp_gaussianfactorizationprimedivisorproduct))) + (((ge_first_rn_gaussianfactorizationprimedivisorproduct) * (ge_second_rn_gaussianfactorizationprimedivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimedivisorproduct) * (ge_second_in_gaussianfactorizationprimedivisorproduct))) + (((ge_first_in_gaussianfactorizationprimedivisorproduct) * (ge_second_ip_gaussianfactorizationprimedivisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimedivisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationprimedivisorproduct) * (ge_second_rn_gaussianfactorizationprimedivisorproduct))) + (((ge_first_rn_gaussianfactorizationprimedivisorproduct) * (ge_second_rp_gaussianfactorizationprimedivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimedivisorproduct) * (ge_second_ip_gaussianfactorizationprimedivisorproduct))) + (((ge_first_in_gaussianfactorizationprimedivisorproduct) * (ge_second_in_gaussianfactorizationprimedivisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimedivisorproductoutputimaginary ge_balance_negative_gaussianfactorizationprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimedivisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimedivisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimedivisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimedivisorproduct) * (ge_second_ip_gaussianfactorizationprimedivisorproduct))) + (((ge_first_rn_gaussianfactorizationprimedivisorproduct) * (ge_second_in_gaussianfactorizationprimedivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimedivisorproduct) * (ge_second_rp_gaussianfactorizationprimedivisorproduct))) + (((ge_first_in_gaussianfactorizationprimedivisorproduct) * (ge_second_rn_gaussianfactorizationprimedivisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimedivisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimedivisorproduct) * (ge_second_in_gaussianfactorizationprimedivisorproduct))) + (((ge_first_rn_gaussianfactorizationprimedivisorproduct) * (ge_second_ip_gaussianfactorizationprimedivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimedivisorproduct) * (ge_second_rn_gaussianfactorizationprimedivisorproduct))) + (((ge_first_in_gaussianfactorizationprimedivisorproduct) * (ge_second_rp_gaussianfactorizationprimedivisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_gaussianfactorizationprimefirst_divisor. (exists ge_first_rp_gaussianfactorizationprimefirst_divisorproduct ge_first_rn_gaussianfactorizationprimefirst_divisorproduct ge_first_ip_gaussianfactorizationprimefirst_divisorproduct ge_first_in_gaussianfactorizationprimefirst_divisorproduct ge_second_rp_gaussianfactorizationprimefirst_divisorproduct ge_second_rn_gaussianfactorizationprimefirst_divisorproduct ge_second_ip_gaussianfactorizationprimefirst_divisorproduct ge_second_in_gaussianfactorizationprimefirst_divisorproduct. ((exists ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductfirst ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductfirst. (((gr_prime_factor_value_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimefirst_divisorproductfirstreal ge_balance_negative_gaussianfactorizationprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductfirstreal) = S ge_signed_half_gaussianfactorizationprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimefirst_divisorproduct) + ge_balance_negative_gaussianfactorizationprimefirst_divisorproductfirstreal = (ge_first_rn_gaussianfactorizationprimefirst_divisorproduct) + ge_balance_positive_gaussianfactorizationprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimefirst_divisorproductfirstimaginary ge_balance_negative_gaussianfactorizationprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimefirst_divisorproduct) + ge_balance_negative_gaussianfactorizationprimefirst_divisorproductfirstimaginary = (ge_first_in_gaussianfactorizationprimefirst_divisorproduct) + ge_balance_positive_gaussianfactorizationprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductsecond ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductsecond. (((gr_quotient_gaussianfactorizationprimefirst_divisor) = ((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimefirst_divisorproductsecondreal ge_balance_negative_gaussianfactorizationprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductsecondreal) = S ge_signed_half_gaussianfactorizationprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimefirst_divisorproduct) + ge_balance_negative_gaussianfactorizationprimefirst_divisorproductsecondreal = (ge_second_rn_gaussianfactorizationprimefirst_divisorproduct) + ge_balance_positive_gaussianfactorizationprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimefirst_divisorproductsecondimaginary ge_balance_negative_gaussianfactorizationprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimefirst_divisorproduct) + ge_balance_negative_gaussianfactorizationprimefirst_divisorproductsecondimaginary = (ge_second_in_gaussianfactorizationprimefirst_divisorproduct) + ge_balance_positive_gaussianfactorizationprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductoutput ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductoutput. (((gr_first_factor_gaussianfactorizationprime) = ((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimefirst_divisorproductoutputreal ge_balance_negative_gaussianfactorizationprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimefirst_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductoutputreal) = S ge_signed_half_gaussianfactorizationprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_rp_gaussianfactorizationprimefirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_rn_gaussianfactorizationprimefirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_in_gaussianfactorizationprimefirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_ip_gaussianfactorizationprimefirst_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimefirst_divisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_rn_gaussianfactorizationprimefirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_rp_gaussianfactorizationprimefirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_ip_gaussianfactorizationprimefirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_in_gaussianfactorizationprimefirst_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimefirst_divisorproductoutputimaginary ge_balance_negative_gaussianfactorizationprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimefirst_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimefirst_divisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_ip_gaussianfactorizationprimefirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_in_gaussianfactorizationprimefirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_rp_gaussianfactorizationprimefirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_rn_gaussianfactorizationprimefirst_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_in_gaussianfactorizationprimefirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_ip_gaussianfactorizationprimefirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_rn_gaussianfactorizationprimefirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimefirst_divisorproduct) * (ge_second_rp_gaussianfactorizationprimefirst_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_gaussianfactorizationprimesecond_divisor. (exists ge_first_rp_gaussianfactorizationprimesecond_divisorproduct ge_first_rn_gaussianfactorizationprimesecond_divisorproduct ge_first_ip_gaussianfactorizationprimesecond_divisorproduct ge_first_in_gaussianfactorizationprimesecond_divisorproduct ge_second_rp_gaussianfactorizationprimesecond_divisorproduct ge_second_rn_gaussianfactorizationprimesecond_divisorproduct ge_second_ip_gaussianfactorizationprimesecond_divisorproduct ge_second_in_gaussianfactorizationprimesecond_divisorproduct. ((exists ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductfirst ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductfirst. (((gr_prime_factor_value_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesecond_divisorproductfirstreal ge_balance_negative_gaussianfactorizationprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductfirstreal) = S ge_signed_half_gaussianfactorizationprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationprimesecond_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesecond_divisorproductfirstreal = (ge_first_rn_gaussianfactorizationprimesecond_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesecond_divisorproductfirstimaginary ge_balance_negative_gaussianfactorizationprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationprimesecond_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesecond_divisorproductfirstimaginary = (ge_first_in_gaussianfactorizationprimesecond_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductsecond ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductsecond. (((gr_quotient_gaussianfactorizationprimesecond_divisor) = ((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesecond_divisorproductsecondreal ge_balance_negative_gaussianfactorizationprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductsecondreal) = S ge_signed_half_gaussianfactorizationprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationprimesecond_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesecond_divisorproductsecondreal = (ge_second_rn_gaussianfactorizationprimesecond_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesecond_divisorproductsecondimaginary ge_balance_negative_gaussianfactorizationprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationprimesecond_divisorproduct) + ge_balance_negative_gaussianfactorizationprimesecond_divisorproductsecondimaginary = (ge_second_in_gaussianfactorizationprimesecond_divisorproduct) + ge_balance_positive_gaussianfactorizationprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductoutput ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductoutput. (((gr_second_factor_gaussianfactorizationprime) = ((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationprimesecond_divisorproductoutputreal ge_balance_negative_gaussianfactorizationprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationprimesecond_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductoutputreal) = S ge_signed_half_gaussianfactorizationprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_in_gaussianfactorizationprimesecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesecond_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimesecond_divisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_in_gaussianfactorizationprimesecond_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationprimesecond_divisorproductoutputimaginary ge_balance_negative_gaussianfactorizationprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationprimesecond_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationprimesecond_divisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_in_gaussianfactorizationprimesecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesecond_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_in_gaussianfactorizationprimesecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_ip_gaussianfactorizationprimesecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_rn_gaussianfactorizationprimesecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationprimesecond_divisorproduct) * (ge_second_rp_gaussianfactorizationprimesecond_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationprimesecond_divisorproductoutputimaginary)))))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.