gaussian_zero_has_no_prime_factorization

Exact expanded first-order arithmetic statement

forall u b c l. ~(((exists gr_inverse_zero_prime_factorizationunit. (exists ge_first_rp_zero_prime_factorizationunitidentity ge_first_rn_zero_prime_factorizationunitidentity ge_first_ip_zero_prime_factorizationunitidentity ge_first_in_zero_prime_factorizationunitidentity ge_second_rp_zero_prime_factorizationunitidentity ge_second_rn_zero_prime_factorizationunitidentity ge_second_ip_zero_prime_factorizationunitidentity ge_second_in_zero_prime_factorizationunitidentity. ((exists ge_representation_real_code_zero_prime_factorizationunitidentityfirst ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst. (((u) = ((ge_representation_real_code_zero_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst)) * S ((ge_representation_real_code_zero_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationunitidentityfirstreal ge_balance_negative_zero_prime_factorizationunitidentityfirstreal. (((((ge_representation_real_code_zero_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentityfirstreal) /\ (ge_balance_negative_zero_prime_factorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentityfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_zero_prime_factorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentityfirstreal) = S ge_signed_half_zero_prime_factorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationunitidentity) + ge_balance_negative_zero_prime_factorizationunitidentityfirstreal = (ge_first_rn_zero_prime_factorizationunitidentity) + ge_balance_positive_zero_prime_factorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationunitidentityfirstimaginary ge_balance_negative_zero_prime_factorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentityfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_zero_prime_factorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentityfirstimaginary) = S ge_signed_half_zero_prime_factorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationunitidentity) + ge_balance_negative_zero_prime_factorizationunitidentityfirstimaginary = (ge_first_in_zero_prime_factorizationunitidentity) + ge_balance_positive_zero_prime_factorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationunitidentitysecond ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond. (((gr_inverse_zero_prime_factorizationunit) = ((ge_representation_real_code_zero_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond)) * S ((ge_representation_real_code_zero_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationunitidentitysecondreal ge_balance_negative_zero_prime_factorizationunitidentitysecondreal. (((((ge_representation_real_code_zero_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentitysecondreal) /\ (ge_balance_negative_zero_prime_factorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentitysecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_zero_prime_factorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentitysecondreal) = S ge_signed_half_zero_prime_factorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationunitidentity) + ge_balance_negative_zero_prime_factorizationunitidentitysecondreal = (ge_second_rn_zero_prime_factorizationunitidentity) + ge_balance_positive_zero_prime_factorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationunitidentitysecondimaginary ge_balance_negative_zero_prime_factorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentitysecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_zero_prime_factorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentitysecondimaginary) = S ge_signed_half_zero_prime_factorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationunitidentity) + ge_balance_negative_zero_prime_factorizationunitidentitysecondimaginary = (ge_second_in_zero_prime_factorizationunitidentity) + ge_balance_positive_zero_prime_factorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationunitidentityoutput ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput. (((6) = ((ge_representation_real_code_zero_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput)) * S ((ge_representation_real_code_zero_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationunitidentityoutputreal ge_balance_negative_zero_prime_factorizationunitidentityoutputreal. (((((ge_representation_real_code_zero_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentityoutputreal) /\ (ge_balance_negative_zero_prime_factorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentityoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_zero_prime_factorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentityoutputreal) = S ge_signed_half_zero_prime_factorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationunitidentity) * (ge_second_rp_zero_prime_factorizationunitidentity))) + (((ge_first_rn_zero_prime_factorizationunitidentity) * (ge_second_rn_zero_prime_factorizationunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationunitidentity) * (ge_second_in_zero_prime_factorizationunitidentity))) + (((ge_first_in_zero_prime_factorizationunitidentity) * (ge_second_ip_zero_prime_factorizationunitidentity))))))) + ge_balance_negative_zero_prime_factorizationunitidentityoutputreal = (((((((ge_first_rp_zero_prime_factorizationunitidentity) * (ge_second_rn_zero_prime_factorizationunitidentity))) + (((ge_first_rn_zero_prime_factorizationunitidentity) * (ge_second_rp_zero_prime_factorizationunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationunitidentity) * (ge_second_ip_zero_prime_factorizationunitidentity))) + (((ge_first_in_zero_prime_factorizationunitidentity) * (ge_second_in_zero_prime_factorizationunitidentity))))))) + ge_balance_positive_zero_prime_factorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationunitidentityoutputimaginary ge_balance_negative_zero_prime_factorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_zero_prime_factorizationunitidentityoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_zero_prime_factorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationunitidentityoutputimaginary) = S ge_signed_half_zero_prime_factorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationunitidentity) * (ge_second_ip_zero_prime_factorizationunitidentity))) + (((ge_first_rn_zero_prime_factorizationunitidentity) * (ge_second_in_zero_prime_factorizationunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationunitidentity) * (ge_second_rp_zero_prime_factorizationunitidentity))) + (((ge_first_in_zero_prime_factorizationunitidentity) * (ge_second_rn_zero_prime_factorizationunitidentity))))))) + ge_balance_negative_zero_prime_factorizationunitidentityoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationunitidentity) * (ge_second_in_zero_prime_factorizationunitidentity))) + (((ge_first_rn_zero_prime_factorizationunitidentity) * (ge_second_ip_zero_prime_factorizationunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationunitidentity) * (ge_second_rn_zero_prime_factorizationunitidentity))) + (((ge_first_in_zero_prime_factorizationunitidentity) * (ge_second_rp_zero_prime_factorizationunitidentity))))))) + ge_balance_positive_zero_prime_factorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_zero_prime_factorizationprimes gr_prime_factor_value_zero_prime_factorizationprimes. (exists ge_gap_zero_prime_factorizationprimesindex. ge_gap_zero_prime_factorizationprimesindex + S (gr_prime_factor_index_zero_prime_factorizationprimes) = (l)) -> (((exists ff_h_gprod_zero_prime_factorizationprimesentry. ff_h_gprod_zero_prime_factorizationprimesentry + S (gr_prime_factor_value_zero_prime_factorizationprimes) = S ((S (gr_prime_factor_index_zero_prime_factorizationprimes)) * c)) /\ exists ff_q_gprod_zero_prime_factorizationprimesentry. b = ff_q_gprod_zero_prime_factorizationprimesentry * S ((S (gr_prime_factor_index_zero_prime_factorizationprimes)) * c) + (gr_prime_factor_value_zero_prime_factorizationprimes))) -> (((exists ge_real_positive_zero_prime_factorizationprimesprimecarrier ge_real_negative_zero_prime_factorizationprimesprimecarrier ge_imaginary_positive_zero_prime_factorizationprimesprimecarrier ge_imaginary_negative_zero_prime_factorizationprimesprimecarrier. (exists ge_real_code_zero_prime_factorizationprimesprimecarrierdecode ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_real_code_zero_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode)) * S ((ge_real_code_zero_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode)) + ((ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode))) /\ (((((ge_real_code_zero_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_real_positive_zero_prime_factorizationprimesprimecarrier) /\ (ge_real_negative_zero_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_real. (((ge_real_code_zero_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_zero_prime_factorizationprimesprimecarrier) = 0) /\ (ge_real_negative_zero_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_zero_prime_factorizationprimesprimecarrier) /\ (ge_imaginary_negative_zero_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_zero_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_zero_prime_factorizationprimesprimecarrier) = 0) /\ (ge_imaginary_negative_zero_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_zero_prime_factorizationprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_zero_prime_factorizationprimes)=0)) /\ ((~(exists gr_inverse_zero_prime_factorizationprimesprimenonunit. (exists ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity ge_first_in_zero_prime_factorizationprimesprimenonunitidentity ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity ge_second_in_zero_prime_factorizationprimesprimenonunitidentity. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstreal ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond. (((gr_inverse_zero_prime_factorizationprimesprimenonunit) = ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondreal ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondreal = (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputreal ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_zero_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_zero_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_zero_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_zero_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_zero_prime_factorizationprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_zero_prime_factorizationprimesprime gr_second_factor_zero_prime_factorizationprimesprime gr_product_zero_prime_factorizationprimesprime. (exists ge_first_rp_zero_prime_factorizationprimesprimeproduct ge_first_rn_zero_prime_factorizationprimesprimeproduct ge_first_ip_zero_prime_factorizationprimesprimeproduct ge_first_in_zero_prime_factorizationprimesprimeproduct ge_second_rp_zero_prime_factorizationprimesprimeproduct ge_second_rn_zero_prime_factorizationprimesprimeproduct ge_second_ip_zero_prime_factorizationprimesprimeproduct ge_second_in_zero_prime_factorizationprimesprimeproduct. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst. (((gr_first_factor_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstreal ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimeproduct) + ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimeproduct) + ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimeproduct) + ge_balance_negative_zero_prime_factorizationprimesprimeproductfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimeproduct) + ge_balance_positive_zero_prime_factorizationprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond. (((gr_second_factor_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondreal ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimeproduct) + ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondreal = (ge_second_rn_zero_prime_factorizationprimesprimeproduct) + ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimeproduct) + ge_balance_negative_zero_prime_factorizationprimesprimeproductsecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimeproduct) + ge_balance_positive_zero_prime_factorizationprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput. (((gr_product_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputreal ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimeproduct) * (ge_second_rp_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimeproduct) * (ge_second_rn_zero_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimeproduct) * (ge_second_in_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimeproduct) * (ge_second_ip_zero_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimeproduct) * (ge_second_rn_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimeproduct) * (ge_second_rp_zero_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimeproduct) * (ge_second_ip_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimeproduct) * (ge_second_in_zero_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimeproduct) * (ge_second_ip_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimeproduct) * (ge_second_in_zero_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimeproduct) * (ge_second_rp_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimeproduct) * (ge_second_rn_zero_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimeproductoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimeproduct) * (ge_second_in_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimeproduct) * (ge_second_ip_zero_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimeproduct) * (ge_second_rn_zero_prime_factorizationprimesprimeproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimeproduct) * (ge_second_rp_zero_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_zero_prime_factorizationprimesprimedivisor. (exists ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct ge_first_in_zero_prime_factorizationprimesprimedivisorproduct ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct ge_second_in_zero_prime_factorizationprimesprimedivisorproduct. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstreal ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond. (((gr_quotient_zero_prime_factorizationprimesprimedivisor) = ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondreal ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondreal = (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductsecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput. (((gr_product_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputreal ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_zero_prime_factorizationprimesprimefirst_divisor. (exists ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond. (((gr_quotient_zero_prime_factorizationprimesprimefirst_divisor) = ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal = (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput. (((gr_first_factor_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_zero_prime_factorizationprimesprimesecond_divisor. (exists ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_zero_prime_factorizationprimes) = ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal = (ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond. (((gr_quotient_zero_prime_factorizationprimesprimesecond_divisor) = ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal = (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput. (((gr_second_factor_zero_prime_factorizationprimesprime) = ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_zero_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_zero_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_zero_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_zero_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_zero_prime_factorizationprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_zero_prime_factorization. ((exists gr_product_trace_zero_prime_factorizationtrace gr_product_scale_zero_prime_factorizationtrace. ((((exists ff_h_gprod_zero_prime_factorizationtracestart. ff_h_gprod_zero_prime_factorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_zero_prime_factorizationtrace)) /\ exists ff_q_gprod_zero_prime_factorizationtracestart. gr_product_trace_zero_prime_factorizationtrace = ff_q_gprod_zero_prime_factorizationtracestart * S ((S (0)) * gr_product_scale_zero_prime_factorizationtrace) + (6))) /\ ((((exists ff_h_gprod_zero_prime_factorizationtraceend. ff_h_gprod_zero_prime_factorizationtraceend + S (gr_prime_factor_product_zero_prime_factorization) = S ((S (l)) * gr_product_scale_zero_prime_factorizationtrace)) /\ exists ff_q_gprod_zero_prime_factorizationtraceend. gr_product_trace_zero_prime_factorizationtrace = ff_q_gprod_zero_prime_factorizationtraceend * S ((S (l)) * gr_product_scale_zero_prime_factorizationtrace) + (gr_prime_factor_product_zero_prime_factorization))) /\ (forall gr_product_index_zero_prime_factorizationtracesteps. (exists ge_gap_zero_prime_factorizationtracestepsindex_bound. ge_gap_zero_prime_factorizationtracestepsindex_bound + S (gr_product_index_zero_prime_factorizationtracesteps) = (l)) -> exists gr_product_factor_zero_prime_factorizationtracesteps gr_product_before_zero_prime_factorizationtracesteps gr_product_after_zero_prime_factorizationtracesteps. ((((exists ff_h_gprod_zero_prime_factorizationtracestepsfactor. ff_h_gprod_zero_prime_factorizationtracestepsfactor + S (gr_product_factor_zero_prime_factorizationtracesteps) = S ((S (gr_product_index_zero_prime_factorizationtracesteps)) * c)) /\ exists ff_q_gprod_zero_prime_factorizationtracestepsfactor. b = ff_q_gprod_zero_prime_factorizationtracestepsfactor * S ((S (gr_product_index_zero_prime_factorizationtracesteps)) * c) + (gr_product_factor_zero_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_zero_prime_factorizationtracestepsbefore. ff_h_gprod_zero_prime_factorizationtracestepsbefore + S (gr_product_before_zero_prime_factorizationtracesteps) = S ((S (gr_product_index_zero_prime_factorizationtracesteps)) * gr_product_scale_zero_prime_factorizationtrace)) /\ exists ff_q_gprod_zero_prime_factorizationtracestepsbefore. gr_product_trace_zero_prime_factorizationtrace = ff_q_gprod_zero_prime_factorizationtracestepsbefore * S ((S (gr_product_index_zero_prime_factorizationtracesteps)) * gr_product_scale_zero_prime_factorizationtrace) + (gr_product_before_zero_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_zero_prime_factorizationtracestepsafter. ff_h_gprod_zero_prime_factorizationtracestepsafter + S (gr_product_after_zero_prime_factorizationtracesteps) = S ((S (S (gr_product_index_zero_prime_factorizationtracesteps))) * gr_product_scale_zero_prime_factorizationtrace)) /\ exists ff_q_gprod_zero_prime_factorizationtracestepsafter. gr_product_trace_zero_prime_factorizationtrace = ff_q_gprod_zero_prime_factorizationtracestepsafter * S ((S (S (gr_product_index_zero_prime_factorizationtracesteps))) * gr_product_scale_zero_prime_factorizationtrace) + (gr_product_after_zero_prime_factorizationtracesteps))) /\ (exists ge_first_rp_zero_prime_factorizationtracestepsmultiply ge_first_rn_zero_prime_factorizationtracestepsmultiply ge_first_ip_zero_prime_factorizationtracestepsmultiply ge_first_in_zero_prime_factorizationtracestepsmultiply ge_second_rp_zero_prime_factorizationtracestepsmultiply ge_second_rn_zero_prime_factorizationtracestepsmultiply ge_second_ip_zero_prime_factorizationtracestepsmultiply ge_second_in_zero_prime_factorizationtracestepsmultiply. ((exists ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst. (((gr_product_before_zero_prime_factorizationtracesteps) = ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstreal ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstreal) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationtracestepsmultiply) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstreal = (ge_first_rn_zero_prime_factorizationtracestepsmultiply) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstimaginary ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationtracestepsmultiply) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplyfirstimaginary = (ge_first_in_zero_prime_factorizationtracestepsmultiply) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond. (((gr_product_factor_zero_prime_factorizationtracesteps) = ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondreal ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondreal) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationtracestepsmultiply) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondreal = (ge_second_rn_zero_prime_factorizationtracestepsmultiply) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondimaginary ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationtracestepsmultiply) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplysecondimaginary = (ge_second_in_zero_prime_factorizationtracestepsmultiply) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput. (((gr_product_after_zero_prime_factorizationtracesteps) = ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputreal ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputreal) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationtracestepsmultiply) * (ge_second_rp_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_zero_prime_factorizationtracestepsmultiply) * (ge_second_rn_zero_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_zero_prime_factorizationtracestepsmultiply) * (ge_second_in_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_in_zero_prime_factorizationtracestepsmultiply) * (ge_second_ip_zero_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_zero_prime_factorizationtracestepsmultiply) * (ge_second_rn_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_zero_prime_factorizationtracestepsmultiply) * (ge_second_rp_zero_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_zero_prime_factorizationtracestepsmultiply) * (ge_second_ip_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_in_zero_prime_factorizationtracestepsmultiply) * (ge_second_in_zero_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputimaginary ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_zero_prime_factorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationtracestepsmultiply) * (ge_second_ip_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_zero_prime_factorizationtracestepsmultiply) * (ge_second_in_zero_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_zero_prime_factorizationtracestepsmultiply) * (ge_second_rp_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_in_zero_prime_factorizationtracestepsmultiply) * (ge_second_rn_zero_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_zero_prime_factorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationtracestepsmultiply) * (ge_second_in_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_zero_prime_factorizationtracestepsmultiply) * (ge_second_ip_zero_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_zero_prime_factorizationtracestepsmultiply) * (ge_second_rn_zero_prime_factorizationtracestepsmultiply))) + (((ge_first_in_zero_prime_factorizationtracestepsmultiply) * (ge_second_rp_zero_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_zero_prime_factorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_zero_prime_factorizationreconstruct ge_first_rn_zero_prime_factorizationreconstruct ge_first_ip_zero_prime_factorizationreconstruct ge_first_in_zero_prime_factorizationreconstruct ge_second_rp_zero_prime_factorizationreconstruct ge_second_rn_zero_prime_factorizationreconstruct ge_second_ip_zero_prime_factorizationreconstruct ge_second_in_zero_prime_factorizationreconstruct. ((exists ge_representation_real_code_zero_prime_factorizationreconstructfirst ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst. (((u) = ((ge_representation_real_code_zero_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst)) * S ((ge_representation_real_code_zero_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst)) + ((ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst))) /\ ((exists ge_balance_positive_zero_prime_factorizationreconstructfirstreal ge_balance_negative_zero_prime_factorizationreconstructfirstreal. (((((ge_representation_real_code_zero_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructfirstreal) /\ (ge_balance_negative_zero_prime_factorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructfirstrealdecode. (((ge_representation_real_code_zero_prime_factorizationreconstructfirst) = 2 * ge_signed_half_zero_prime_factorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructfirstreal) = S ge_signed_half_zero_prime_factorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_zero_prime_factorizationreconstruct) + ge_balance_negative_zero_prime_factorizationreconstructfirstreal = (ge_first_rn_zero_prime_factorizationreconstruct) + ge_balance_positive_zero_prime_factorizationreconstructfirstreal))) /\ (exists ge_balance_positive_zero_prime_factorizationreconstructfirstimaginary ge_balance_negative_zero_prime_factorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructfirstimaginary) /\ (ge_balance_negative_zero_prime_factorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationreconstructfirst) = 2 * ge_signed_half_zero_prime_factorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructfirstimaginary) = S ge_signed_half_zero_prime_factorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_zero_prime_factorizationreconstruct) + ge_balance_negative_zero_prime_factorizationreconstructfirstimaginary = (ge_first_in_zero_prime_factorizationreconstruct) + ge_balance_positive_zero_prime_factorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_prime_factorizationreconstructsecond ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond. (((gr_prime_factor_product_zero_prime_factorization) = ((ge_representation_real_code_zero_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond)) * S ((ge_representation_real_code_zero_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond)) + ((ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond))) /\ ((exists ge_balance_positive_zero_prime_factorizationreconstructsecondreal ge_balance_negative_zero_prime_factorizationreconstructsecondreal. (((((ge_representation_real_code_zero_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructsecondreal) /\ (ge_balance_negative_zero_prime_factorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructsecondrealdecode. (((ge_representation_real_code_zero_prime_factorizationreconstructsecond) = 2 * ge_signed_half_zero_prime_factorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructsecondreal) = S ge_signed_half_zero_prime_factorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_zero_prime_factorizationreconstruct) + ge_balance_negative_zero_prime_factorizationreconstructsecondreal = (ge_second_rn_zero_prime_factorizationreconstruct) + ge_balance_positive_zero_prime_factorizationreconstructsecondreal))) /\ (exists ge_balance_positive_zero_prime_factorizationreconstructsecondimaginary ge_balance_negative_zero_prime_factorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructsecondimaginary) /\ (ge_balance_negative_zero_prime_factorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationreconstructsecond) = 2 * ge_signed_half_zero_prime_factorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructsecondimaginary) = S ge_signed_half_zero_prime_factorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_zero_prime_factorizationreconstruct) + ge_balance_negative_zero_prime_factorizationreconstructsecondimaginary = (ge_second_in_zero_prime_factorizationreconstruct) + ge_balance_positive_zero_prime_factorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_prime_factorizationreconstructoutput ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput. (((0) = ((ge_representation_real_code_zero_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput)) * S ((ge_representation_real_code_zero_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput)) + ((ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput))) /\ ((exists ge_balance_positive_zero_prime_factorizationreconstructoutputreal ge_balance_negative_zero_prime_factorizationreconstructoutputreal. (((((ge_representation_real_code_zero_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructoutputreal) /\ (ge_balance_negative_zero_prime_factorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructoutputrealdecode. (((ge_representation_real_code_zero_prime_factorizationreconstructoutput) = 2 * ge_signed_half_zero_prime_factorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructoutputreal) = S ge_signed_half_zero_prime_factorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationreconstruct) * (ge_second_rp_zero_prime_factorizationreconstruct))) + (((ge_first_rn_zero_prime_factorizationreconstruct) * (ge_second_rn_zero_prime_factorizationreconstruct))))) + (((((ge_first_ip_zero_prime_factorizationreconstruct) * (ge_second_in_zero_prime_factorizationreconstruct))) + (((ge_first_in_zero_prime_factorizationreconstruct) * (ge_second_ip_zero_prime_factorizationreconstruct))))))) + ge_balance_negative_zero_prime_factorizationreconstructoutputreal = (((((((ge_first_rp_zero_prime_factorizationreconstruct) * (ge_second_rn_zero_prime_factorizationreconstruct))) + (((ge_first_rn_zero_prime_factorizationreconstruct) * (ge_second_rp_zero_prime_factorizationreconstruct))))) + (((((ge_first_ip_zero_prime_factorizationreconstruct) * (ge_second_ip_zero_prime_factorizationreconstruct))) + (((ge_first_in_zero_prime_factorizationreconstruct) * (ge_second_in_zero_prime_factorizationreconstruct))))))) + ge_balance_positive_zero_prime_factorizationreconstructoutputreal))) /\ (exists ge_balance_positive_zero_prime_factorizationreconstructoutputimaginary ge_balance_negative_zero_prime_factorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_zero_prime_factorizationreconstructoutputimaginary) /\ (ge_balance_negative_zero_prime_factorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_zero_prime_factorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_zero_prime_factorizationreconstructoutput) = 2 * ge_signed_half_zero_prime_factorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_prime_factorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_zero_prime_factorizationreconstructoutputimaginary) = S ge_signed_half_zero_prime_factorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_prime_factorizationreconstruct) * (ge_second_ip_zero_prime_factorizationreconstruct))) + (((ge_first_rn_zero_prime_factorizationreconstruct) * (ge_second_in_zero_prime_factorizationreconstruct))))) + (((((ge_first_ip_zero_prime_factorizationreconstruct) * (ge_second_rp_zero_prime_factorizationreconstruct))) + (((ge_first_in_zero_prime_factorizationreconstruct) * (ge_second_rn_zero_prime_factorizationreconstruct))))))) + ge_balance_negative_zero_prime_factorizationreconstructoutputimaginary = (((((((ge_first_rp_zero_prime_factorizationreconstruct) * (ge_second_in_zero_prime_factorizationreconstruct))) + (((ge_first_rn_zero_prime_factorizationreconstruct) * (ge_second_ip_zero_prime_factorizationreconstruct))))) + (((((ge_first_ip_zero_prime_factorizationreconstruct) * (ge_second_rn_zero_prime_factorizationreconstruct))) + (((ge_first_in_zero_prime_factorizationreconstruct) * (ge_second_rp_zero_prime_factorizationreconstruct))))))) + ge_balance_positive_zero_prime_factorizationreconstructoutputimaginary))))))))))))))