gaussian_prime_factorizations_unique

Exact expanded first-order arithmetic statement

forall z u b c l v d e m. (((exists gr_inverse_unique_first_prime_factorizationunit. (exists ge_first_rp_unique_first_prime_factorizationunitidentity ge_first_rn_unique_first_prime_factorizationunitidentity ge_first_ip_unique_first_prime_factorizationunitidentity ge_first_in_unique_first_prime_factorizationunitidentity ge_second_rp_unique_first_prime_factorizationunitidentity ge_second_rn_unique_first_prime_factorizationunitidentity ge_second_ip_unique_first_prime_factorizationunitidentity ge_second_in_unique_first_prime_factorizationunitidentity. ((exists ge_representation_real_code_unique_first_prime_factorizationunitidentityfirst ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityfirst. (((u) = ((ge_representation_real_code_unique_first_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityfirst)) * S ((ge_representation_real_code_unique_first_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityfirst)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityfirst))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationunitidentityfirstreal ge_balance_negative_unique_first_prime_factorizationunitidentityfirstreal. (((((ge_representation_real_code_unique_first_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationunitidentityfirstreal) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationunitidentityfirstrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_unique_first_prime_factorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentityfirstreal) = S ge_signed_half_unique_first_prime_factorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_first_prime_factorizationunitidentity) + ge_balance_negative_unique_first_prime_factorizationunitidentityfirstreal = (ge_first_rn_unique_first_prime_factorizationunitidentity) + ge_balance_positive_unique_first_prime_factorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationunitidentityfirstimaginary ge_balance_negative_unique_first_prime_factorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationunitidentityfirstimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_unique_first_prime_factorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentityfirstimaginary) = S ge_signed_half_unique_first_prime_factorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_prime_factorizationunitidentity) + ge_balance_negative_unique_first_prime_factorizationunitidentityfirstimaginary = (ge_first_in_unique_first_prime_factorizationunitidentity) + ge_balance_positive_unique_first_prime_factorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_prime_factorizationunitidentitysecond ge_representation_imaginary_code_unique_first_prime_factorizationunitidentitysecond. (((gr_inverse_unique_first_prime_factorizationunit) = ((ge_representation_real_code_unique_first_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentitysecond)) * S ((ge_representation_real_code_unique_first_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentitysecond)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentitysecond))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationunitidentitysecondreal ge_balance_negative_unique_first_prime_factorizationunitidentitysecondreal. (((((ge_representation_real_code_unique_first_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationunitidentitysecondreal) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationunitidentitysecondrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_unique_first_prime_factorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentitysecondreal) = S ge_signed_half_unique_first_prime_factorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_first_prime_factorizationunitidentity) + ge_balance_negative_unique_first_prime_factorizationunitidentitysecondreal = (ge_second_rn_unique_first_prime_factorizationunitidentity) + ge_balance_positive_unique_first_prime_factorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationunitidentitysecondimaginary ge_balance_negative_unique_first_prime_factorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationunitidentitysecondimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_unique_first_prime_factorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentitysecondimaginary) = S ge_signed_half_unique_first_prime_factorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_first_prime_factorizationunitidentity) + ge_balance_negative_unique_first_prime_factorizationunitidentitysecondimaginary = (ge_second_in_unique_first_prime_factorizationunitidentity) + ge_balance_positive_unique_first_prime_factorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_prime_factorizationunitidentityoutput ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityoutput. (((6) = ((ge_representation_real_code_unique_first_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityoutput)) * S ((ge_representation_real_code_unique_first_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityoutput)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityoutput))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationunitidentityoutputreal ge_balance_negative_unique_first_prime_factorizationunitidentityoutputreal. (((((ge_representation_real_code_unique_first_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationunitidentityoutputreal) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationunitidentityoutputrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_unique_first_prime_factorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentityoutputreal) = S ge_signed_half_unique_first_prime_factorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationunitidentity) * (ge_second_rp_unique_first_prime_factorizationunitidentity))) + (((ge_first_rn_unique_first_prime_factorizationunitidentity) * (ge_second_rn_unique_first_prime_factorizationunitidentity))))) + (((((ge_first_ip_unique_first_prime_factorizationunitidentity) * (ge_second_in_unique_first_prime_factorizationunitidentity))) + (((ge_first_in_unique_first_prime_factorizationunitidentity) * (ge_second_ip_unique_first_prime_factorizationunitidentity))))))) + ge_balance_negative_unique_first_prime_factorizationunitidentityoutputreal = (((((((ge_first_rp_unique_first_prime_factorizationunitidentity) * (ge_second_rn_unique_first_prime_factorizationunitidentity))) + (((ge_first_rn_unique_first_prime_factorizationunitidentity) * (ge_second_rp_unique_first_prime_factorizationunitidentity))))) + (((((ge_first_ip_unique_first_prime_factorizationunitidentity) * (ge_second_ip_unique_first_prime_factorizationunitidentity))) + (((ge_first_in_unique_first_prime_factorizationunitidentity) * (ge_second_in_unique_first_prime_factorizationunitidentity))))))) + ge_balance_positive_unique_first_prime_factorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationunitidentityoutputimaginary ge_balance_negative_unique_first_prime_factorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationunitidentityoutputimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_unique_first_prime_factorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationunitidentityoutputimaginary) = S ge_signed_half_unique_first_prime_factorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationunitidentity) * (ge_second_ip_unique_first_prime_factorizationunitidentity))) + (((ge_first_rn_unique_first_prime_factorizationunitidentity) * (ge_second_in_unique_first_prime_factorizationunitidentity))))) + (((((ge_first_ip_unique_first_prime_factorizationunitidentity) * (ge_second_rp_unique_first_prime_factorizationunitidentity))) + (((ge_first_in_unique_first_prime_factorizationunitidentity) * (ge_second_rn_unique_first_prime_factorizationunitidentity))))))) + ge_balance_negative_unique_first_prime_factorizationunitidentityoutputimaginary = (((((((ge_first_rp_unique_first_prime_factorizationunitidentity) * (ge_second_in_unique_first_prime_factorizationunitidentity))) + (((ge_first_rn_unique_first_prime_factorizationunitidentity) * (ge_second_ip_unique_first_prime_factorizationunitidentity))))) + (((((ge_first_ip_unique_first_prime_factorizationunitidentity) * (ge_second_rn_unique_first_prime_factorizationunitidentity))) + (((ge_first_in_unique_first_prime_factorizationunitidentity) * (ge_second_rp_unique_first_prime_factorizationunitidentity))))))) + ge_balance_positive_unique_first_prime_factorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_unique_first_prime_factorizationprimes gr_prime_factor_value_unique_first_prime_factorizationprimes. (exists ge_gap_unique_first_prime_factorizationprimesindex. ge_gap_unique_first_prime_factorizationprimesindex + S (gr_prime_factor_index_unique_first_prime_factorizationprimes) = (l)) -> (((exists ff_h_gprod_unique_first_prime_factorizationprimesentry. ff_h_gprod_unique_first_prime_factorizationprimesentry + S (gr_prime_factor_value_unique_first_prime_factorizationprimes) = S ((S (gr_prime_factor_index_unique_first_prime_factorizationprimes)) * c)) /\ exists ff_q_gprod_unique_first_prime_factorizationprimesentry. b = ff_q_gprod_unique_first_prime_factorizationprimesentry * S ((S (gr_prime_factor_index_unique_first_prime_factorizationprimes)) * c) + (gr_prime_factor_value_unique_first_prime_factorizationprimes))) -> (((exists ge_real_positive_unique_first_prime_factorizationprimesprimecarrier ge_real_negative_unique_first_prime_factorizationprimesprimecarrier ge_imaginary_positive_unique_first_prime_factorizationprimesprimecarrier ge_imaginary_negative_unique_first_prime_factorizationprimesprimecarrier. (exists ge_real_code_unique_first_prime_factorizationprimesprimecarrierdecode ge_imaginary_code_unique_first_prime_factorizationprimesprimecarrierdecode. (((gr_prime_factor_value_unique_first_prime_factorizationprimes) = ((ge_real_code_unique_first_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unique_first_prime_factorizationprimesprimecarrierdecode)) * S ((ge_real_code_unique_first_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unique_first_prime_factorizationprimesprimecarrierdecode)) + ((ge_imaginary_code_unique_first_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unique_first_prime_factorizationprimesprimecarrierdecode))) /\ (((((ge_real_code_unique_first_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_real_positive_unique_first_prime_factorizationprimesprimecarrier) /\ (ge_real_negative_unique_first_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_unique_first_prime_factorizationprimesprimecarrierdecode_real. (((ge_real_code_unique_first_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_unique_first_prime_factorizationprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_unique_first_prime_factorizationprimesprimecarrier) = 0) /\ (ge_real_negative_unique_first_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_unique_first_prime_factorizationprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_unique_first_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_unique_first_prime_factorizationprimesprimecarrier) /\ (ge_imaginary_negative_unique_first_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_unique_first_prime_factorizationprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_unique_first_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_unique_first_prime_factorizationprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unique_first_prime_factorizationprimesprimecarrier) = 0) /\ (ge_imaginary_negative_unique_first_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_unique_first_prime_factorizationprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_unique_first_prime_factorizationprimes)=0)) /\ ((~(exists gr_inverse_unique_first_prime_factorizationprimesprimenonunit. (exists ge_first_rp_unique_first_prime_factorizationprimesprimenonunitidentity ge_first_rn_unique_first_prime_factorizationprimesprimenonunitidentity ge_first_ip_unique_first_prime_factorizationprimesprimenonunitidentity ge_first_in_unique_first_prime_factorizationprimesprimenonunitidentity ge_second_rp_unique_first_prime_factorizationprimesprimenonunitidentity ge_second_rn_unique_first_prime_factorizationprimesprimenonunitidentity ge_second_ip_unique_first_prime_factorizationprimesprimenonunitidentity ge_second_in_unique_first_prime_factorizationprimesprimenonunitidentity. ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst. (((gr_prime_factor_value_unique_first_prime_factorizationprimes) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityfirstreal ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityfirstreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_first_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityfirstreal = (ge_first_rn_unique_first_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginary = (ge_first_in_unique_first_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond. (((gr_inverse_unique_first_prime_factorizationprimesprimenonunit) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentitysecondreal ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentitysecondreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_first_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentitysecondreal = (ge_second_rn_unique_first_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_first_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginary = (ge_second_in_unique_first_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityoutputreal ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityoutputreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unique_first_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unique_first_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unique_first_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unique_first_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unique_first_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unique_first_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unique_first_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unique_first_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unique_first_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unique_first_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unique_first_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unique_first_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unique_first_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unique_first_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unique_first_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unique_first_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unique_first_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unique_first_prime_factorizationprimesprime gr_second_factor_unique_first_prime_factorizationprimesprime gr_product_unique_first_prime_factorizationprimesprime. (exists ge_first_rp_unique_first_prime_factorizationprimesprimeproduct ge_first_rn_unique_first_prime_factorizationprimesprimeproduct ge_first_ip_unique_first_prime_factorizationprimesprimeproduct ge_first_in_unique_first_prime_factorizationprimesprimeproduct ge_second_rp_unique_first_prime_factorizationprimesprimeproduct ge_second_rn_unique_first_prime_factorizationprimesprimeproduct ge_second_ip_unique_first_prime_factorizationprimesprimeproduct ge_second_in_unique_first_prime_factorizationprimesprimeproduct. ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductfirst ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductfirst. (((gr_first_factor_unique_first_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductfirst)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductfirst)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductfirst))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimeproductfirstreal ge_balance_negative_unique_first_prime_factorizationprimesprimeproductfirstreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductfirstreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimeproductfirstrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductfirstreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_unique_first_prime_factorizationprimesprimeproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimeproductfirstreal = (ge_first_rn_unique_first_prime_factorizationprimesprimeproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimeproductfirstimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductfirstimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductfirstimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_prime_factorizationprimesprimeproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimeproductfirstimaginary = (ge_first_in_unique_first_prime_factorizationprimesprimeproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductsecond ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductsecond. (((gr_second_factor_unique_first_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductsecond)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductsecond)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductsecond))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimeproductsecondreal ge_balance_negative_unique_first_prime_factorizationprimesprimeproductsecondreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductsecondreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimeproductsecondrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductsecondreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_unique_first_prime_factorizationprimesprimeproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimeproductsecondreal = (ge_second_rn_unique_first_prime_factorizationprimesprimeproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimeproductsecondimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductsecondimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductsecondimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_unique_first_prime_factorizationprimesprimeproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimeproductsecondimaginary = (ge_second_in_unique_first_prime_factorizationprimesprimeproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductoutput ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductoutput. (((gr_product_unique_first_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductoutput)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductoutput)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductoutput))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimeproductoutputreal ge_balance_negative_unique_first_prime_factorizationprimesprimeproductoutputreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductoutputreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimeproductoutputrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductoutputreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimeproductoutputreal = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimeproductoutputimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductoutputimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimeproductoutputimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimeproductoutputimaginary = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimeproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_unique_first_prime_factorizationprimesprimedivisor. (exists ge_first_rp_unique_first_prime_factorizationprimesprimedivisorproduct ge_first_rn_unique_first_prime_factorizationprimesprimedivisorproduct ge_first_ip_unique_first_prime_factorizationprimesprimedivisorproduct ge_first_in_unique_first_prime_factorizationprimesprimedivisorproduct ge_second_rp_unique_first_prime_factorizationprimesprimedivisorproduct ge_second_rn_unique_first_prime_factorizationprimesprimedivisorproduct ge_second_ip_unique_first_prime_factorizationprimesprimedivisorproduct ge_second_in_unique_first_prime_factorizationprimesprimedivisorproduct. ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductfirst ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductfirst. (((gr_prime_factor_value_unique_first_prime_factorizationprimes) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductfirstreal ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductfirstreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_unique_first_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductfirstreal = (ge_first_rn_unique_first_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginary = (ge_first_in_unique_first_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductsecond ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductsecond. (((gr_quotient_unique_first_prime_factorizationprimesprimedivisor) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductsecondreal ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductsecondreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_unique_first_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductsecondreal = (ge_second_rn_unique_first_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unique_first_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginary = (ge_second_in_unique_first_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductoutput ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductoutput. (((gr_product_unique_first_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductoutputreal ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductoutputreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductoutputreal = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_unique_first_prime_factorizationprimesprimefirst_divisor. (exists ge_first_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct ge_first_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct ge_first_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct ge_first_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct ge_second_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct ge_second_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct ge_second_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct ge_second_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_unique_first_prime_factorizationprimes) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstreal ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstreal = (ge_first_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond. (((gr_quotient_unique_first_prime_factorizationprimesprimefirst_divisor) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondreal ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondreal = (ge_second_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput. (((gr_first_factor_unique_first_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputreal ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_unique_first_prime_factorizationprimesprimesecond_divisor. (exists ge_first_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct ge_first_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct ge_first_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct ge_first_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct ge_second_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct ge_second_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct ge_second_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct ge_second_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_unique_first_prime_factorizationprimes) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstreal ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstreal = (ge_first_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond. (((gr_quotient_unique_first_prime_factorizationprimesprimesecond_divisor) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondreal ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondreal = (ge_second_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput. (((gr_second_factor_unique_first_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputreal ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unique_first_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unique_first_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unique_first_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_unique_first_prime_factorizationprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_unique_first_prime_factorization. ((exists gr_product_trace_unique_first_prime_factorizationtrace gr_product_scale_unique_first_prime_factorizationtrace. ((((exists ff_h_gprod_unique_first_prime_factorizationtracestart. ff_h_gprod_unique_first_prime_factorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_unique_first_prime_factorizationtrace)) /\ exists ff_q_gprod_unique_first_prime_factorizationtracestart. gr_product_trace_unique_first_prime_factorizationtrace = ff_q_gprod_unique_first_prime_factorizationtracestart * S ((S (0)) * gr_product_scale_unique_first_prime_factorizationtrace) + (6))) /\ ((((exists ff_h_gprod_unique_first_prime_factorizationtraceend. ff_h_gprod_unique_first_prime_factorizationtraceend + S (gr_prime_factor_product_unique_first_prime_factorization) = S ((S (l)) * gr_product_scale_unique_first_prime_factorizationtrace)) /\ exists ff_q_gprod_unique_first_prime_factorizationtraceend. gr_product_trace_unique_first_prime_factorizationtrace = ff_q_gprod_unique_first_prime_factorizationtraceend * S ((S (l)) * gr_product_scale_unique_first_prime_factorizationtrace) + (gr_prime_factor_product_unique_first_prime_factorization))) /\ (forall gr_product_index_unique_first_prime_factorizationtracesteps. (exists ge_gap_unique_first_prime_factorizationtracestepsindex_bound. ge_gap_unique_first_prime_factorizationtracestepsindex_bound + S (gr_product_index_unique_first_prime_factorizationtracesteps) = (l)) -> exists gr_product_factor_unique_first_prime_factorizationtracesteps gr_product_before_unique_first_prime_factorizationtracesteps gr_product_after_unique_first_prime_factorizationtracesteps. ((((exists ff_h_gprod_unique_first_prime_factorizationtracestepsfactor. ff_h_gprod_unique_first_prime_factorizationtracestepsfactor + S (gr_product_factor_unique_first_prime_factorizationtracesteps) = S ((S (gr_product_index_unique_first_prime_factorizationtracesteps)) * c)) /\ exists ff_q_gprod_unique_first_prime_factorizationtracestepsfactor. b = ff_q_gprod_unique_first_prime_factorizationtracestepsfactor * S ((S (gr_product_index_unique_first_prime_factorizationtracesteps)) * c) + (gr_product_factor_unique_first_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unique_first_prime_factorizationtracestepsbefore. ff_h_gprod_unique_first_prime_factorizationtracestepsbefore + S (gr_product_before_unique_first_prime_factorizationtracesteps) = S ((S (gr_product_index_unique_first_prime_factorizationtracesteps)) * gr_product_scale_unique_first_prime_factorizationtrace)) /\ exists ff_q_gprod_unique_first_prime_factorizationtracestepsbefore. gr_product_trace_unique_first_prime_factorizationtrace = ff_q_gprod_unique_first_prime_factorizationtracestepsbefore * S ((S (gr_product_index_unique_first_prime_factorizationtracesteps)) * gr_product_scale_unique_first_prime_factorizationtrace) + (gr_product_before_unique_first_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unique_first_prime_factorizationtracestepsafter. ff_h_gprod_unique_first_prime_factorizationtracestepsafter + S (gr_product_after_unique_first_prime_factorizationtracesteps) = S ((S (S (gr_product_index_unique_first_prime_factorizationtracesteps))) * gr_product_scale_unique_first_prime_factorizationtrace)) /\ exists ff_q_gprod_unique_first_prime_factorizationtracestepsafter. gr_product_trace_unique_first_prime_factorizationtrace = ff_q_gprod_unique_first_prime_factorizationtracestepsafter * S ((S (S (gr_product_index_unique_first_prime_factorizationtracesteps))) * gr_product_scale_unique_first_prime_factorizationtrace) + (gr_product_after_unique_first_prime_factorizationtracesteps))) /\ (exists ge_first_rp_unique_first_prime_factorizationtracestepsmultiply ge_first_rn_unique_first_prime_factorizationtracestepsmultiply ge_first_ip_unique_first_prime_factorizationtracestepsmultiply ge_first_in_unique_first_prime_factorizationtracestepsmultiply ge_second_rp_unique_first_prime_factorizationtracestepsmultiply ge_second_rn_unique_first_prime_factorizationtracestepsmultiply ge_second_ip_unique_first_prime_factorizationtracestepsmultiply ge_second_in_unique_first_prime_factorizationtracestepsmultiply. ((exists ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyfirst ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyfirst. (((gr_product_before_unique_first_prime_factorizationtracesteps) = ((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyfirstreal ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyfirstreal) = S ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unique_first_prime_factorizationtracestepsmultiply) + ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyfirstreal = (ge_first_rn_unique_first_prime_factorizationtracestepsmultiply) + ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyfirstimaginary ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_prime_factorizationtracestepsmultiply) + ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyfirstimaginary = (ge_first_in_unique_first_prime_factorizationtracestepsmultiply) + ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplysecond ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplysecond. (((gr_product_factor_unique_first_prime_factorizationtracesteps) = ((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplysecondreal ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unique_first_prime_factorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplysecondreal) = S ge_signed_half_unique_first_prime_factorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unique_first_prime_factorizationtracestepsmultiply) + ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplysecondreal = (ge_second_rn_unique_first_prime_factorizationtracestepsmultiply) + ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplysecondimaginary ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unique_first_prime_factorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_unique_first_prime_factorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unique_first_prime_factorizationtracestepsmultiply) + ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplysecondimaginary = (ge_second_in_unique_first_prime_factorizationtracestepsmultiply) + ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyoutput ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyoutput. (((gr_product_after_unique_first_prime_factorizationtracesteps) = ((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyoutputreal ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyoutputreal) = S ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_rp_unique_first_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_rn_unique_first_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_in_unique_first_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_ip_unique_first_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_rn_unique_first_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_rp_unique_first_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_ip_unique_first_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_in_unique_first_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyoutputimaginary ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_unique_first_prime_factorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_ip_unique_first_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_in_unique_first_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_rp_unique_first_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_rn_unique_first_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_unique_first_prime_factorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_in_unique_first_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_ip_unique_first_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_rn_unique_first_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unique_first_prime_factorizationtracestepsmultiply) * (ge_second_rp_unique_first_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_unique_first_prime_factorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_unique_first_prime_factorizationreconstruct ge_first_rn_unique_first_prime_factorizationreconstruct ge_first_ip_unique_first_prime_factorizationreconstruct ge_first_in_unique_first_prime_factorizationreconstruct ge_second_rp_unique_first_prime_factorizationreconstruct ge_second_rn_unique_first_prime_factorizationreconstruct ge_second_ip_unique_first_prime_factorizationreconstruct ge_second_in_unique_first_prime_factorizationreconstruct. ((exists ge_representation_real_code_unique_first_prime_factorizationreconstructfirst ge_representation_imaginary_code_unique_first_prime_factorizationreconstructfirst. (((u) = ((ge_representation_real_code_unique_first_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructfirst)) * S ((ge_representation_real_code_unique_first_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructfirst)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructfirst))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationreconstructfirstreal ge_balance_negative_unique_first_prime_factorizationreconstructfirstreal. (((((ge_representation_real_code_unique_first_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationreconstructfirstreal) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationreconstructfirstrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationreconstructfirst) = 2 * ge_signed_half_unique_first_prime_factorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructfirstreal) = S ge_signed_half_unique_first_prime_factorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_unique_first_prime_factorizationreconstruct) + ge_balance_negative_unique_first_prime_factorizationreconstructfirstreal = (ge_first_rn_unique_first_prime_factorizationreconstruct) + ge_balance_positive_unique_first_prime_factorizationreconstructfirstreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationreconstructfirstimaginary ge_balance_negative_unique_first_prime_factorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_unique_first_prime_factorizationreconstructfirstimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructfirst) = 2 * ge_signed_half_unique_first_prime_factorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructfirstimaginary) = S ge_signed_half_unique_first_prime_factorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_unique_first_prime_factorizationreconstruct) + ge_balance_negative_unique_first_prime_factorizationreconstructfirstimaginary = (ge_first_in_unique_first_prime_factorizationreconstruct) + ge_balance_positive_unique_first_prime_factorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_first_prime_factorizationreconstructsecond ge_representation_imaginary_code_unique_first_prime_factorizationreconstructsecond. (((gr_prime_factor_product_unique_first_prime_factorization) = ((ge_representation_real_code_unique_first_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructsecond)) * S ((ge_representation_real_code_unique_first_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructsecond)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructsecond))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationreconstructsecondreal ge_balance_negative_unique_first_prime_factorizationreconstructsecondreal. (((((ge_representation_real_code_unique_first_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationreconstructsecondreal) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationreconstructsecondrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationreconstructsecond) = 2 * ge_signed_half_unique_first_prime_factorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructsecondreal) = S ge_signed_half_unique_first_prime_factorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_unique_first_prime_factorizationreconstruct) + ge_balance_negative_unique_first_prime_factorizationreconstructsecondreal = (ge_second_rn_unique_first_prime_factorizationreconstruct) + ge_balance_positive_unique_first_prime_factorizationreconstructsecondreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationreconstructsecondimaginary ge_balance_negative_unique_first_prime_factorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_unique_first_prime_factorizationreconstructsecondimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructsecond) = 2 * ge_signed_half_unique_first_prime_factorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructsecondimaginary) = S ge_signed_half_unique_first_prime_factorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_unique_first_prime_factorizationreconstruct) + ge_balance_negative_unique_first_prime_factorizationreconstructsecondimaginary = (ge_second_in_unique_first_prime_factorizationreconstruct) + ge_balance_positive_unique_first_prime_factorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_first_prime_factorizationreconstructoutput ge_representation_imaginary_code_unique_first_prime_factorizationreconstructoutput. (((z) = ((ge_representation_real_code_unique_first_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructoutput)) * S ((ge_representation_real_code_unique_first_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructoutput)) + ((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_first_prime_factorizationreconstructoutput))) /\ ((exists ge_balance_positive_unique_first_prime_factorizationreconstructoutputreal ge_balance_negative_unique_first_prime_factorizationreconstructoutputreal. (((((ge_representation_real_code_unique_first_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationreconstructoutputreal) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationreconstructoutputrealdecode. (((ge_representation_real_code_unique_first_prime_factorizationreconstructoutput) = 2 * ge_signed_half_unique_first_prime_factorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructoutputreal) = S ge_signed_half_unique_first_prime_factorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationreconstruct) * (ge_second_rp_unique_first_prime_factorizationreconstruct))) + (((ge_first_rn_unique_first_prime_factorizationreconstruct) * (ge_second_rn_unique_first_prime_factorizationreconstruct))))) + (((((ge_first_ip_unique_first_prime_factorizationreconstruct) * (ge_second_in_unique_first_prime_factorizationreconstruct))) + (((ge_first_in_unique_first_prime_factorizationreconstruct) * (ge_second_ip_unique_first_prime_factorizationreconstruct))))))) + ge_balance_negative_unique_first_prime_factorizationreconstructoutputreal = (((((((ge_first_rp_unique_first_prime_factorizationreconstruct) * (ge_second_rn_unique_first_prime_factorizationreconstruct))) + (((ge_first_rn_unique_first_prime_factorizationreconstruct) * (ge_second_rp_unique_first_prime_factorizationreconstruct))))) + (((((ge_first_ip_unique_first_prime_factorizationreconstruct) * (ge_second_ip_unique_first_prime_factorizationreconstruct))) + (((ge_first_in_unique_first_prime_factorizationreconstruct) * (ge_second_in_unique_first_prime_factorizationreconstruct))))))) + ge_balance_positive_unique_first_prime_factorizationreconstructoutputreal))) /\ (exists ge_balance_positive_unique_first_prime_factorizationreconstructoutputimaginary ge_balance_negative_unique_first_prime_factorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_unique_first_prime_factorizationreconstructoutputimaginary) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_unique_first_prime_factorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_unique_first_prime_factorizationreconstructoutput) = 2 * ge_signed_half_unique_first_prime_factorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_first_prime_factorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_unique_first_prime_factorizationreconstructoutputimaginary) = S ge_signed_half_unique_first_prime_factorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_first_prime_factorizationreconstruct) * (ge_second_ip_unique_first_prime_factorizationreconstruct))) + (((ge_first_rn_unique_first_prime_factorizationreconstruct) * (ge_second_in_unique_first_prime_factorizationreconstruct))))) + (((((ge_first_ip_unique_first_prime_factorizationreconstruct) * (ge_second_rp_unique_first_prime_factorizationreconstruct))) + (((ge_first_in_unique_first_prime_factorizationreconstruct) * (ge_second_rn_unique_first_prime_factorizationreconstruct))))))) + ge_balance_negative_unique_first_prime_factorizationreconstructoutputimaginary = (((((((ge_first_rp_unique_first_prime_factorizationreconstruct) * (ge_second_in_unique_first_prime_factorizationreconstruct))) + (((ge_first_rn_unique_first_prime_factorizationreconstruct) * (ge_second_ip_unique_first_prime_factorizationreconstruct))))) + (((((ge_first_ip_unique_first_prime_factorizationreconstruct) * (ge_second_rn_unique_first_prime_factorizationreconstruct))) + (((ge_first_in_unique_first_prime_factorizationreconstruct) * (ge_second_rp_unique_first_prime_factorizationreconstruct))))))) + ge_balance_positive_unique_first_prime_factorizationreconstructoutputimaginary)))))))))))))) -> (((exists gr_inverse_unique_second_prime_factorizationunit. (exists ge_first_rp_unique_second_prime_factorizationunitidentity ge_first_rn_unique_second_prime_factorizationunitidentity ge_first_ip_unique_second_prime_factorizationunitidentity ge_first_in_unique_second_prime_factorizationunitidentity ge_second_rp_unique_second_prime_factorizationunitidentity ge_second_rn_unique_second_prime_factorizationunitidentity ge_second_ip_unique_second_prime_factorizationunitidentity ge_second_in_unique_second_prime_factorizationunitidentity. ((exists ge_representation_real_code_unique_second_prime_factorizationunitidentityfirst ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityfirst. (((v) = ((ge_representation_real_code_unique_second_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityfirst)) * S ((ge_representation_real_code_unique_second_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityfirst)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityfirst))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationunitidentityfirstreal ge_balance_negative_unique_second_prime_factorizationunitidentityfirstreal. (((((ge_representation_real_code_unique_second_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationunitidentityfirstreal) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationunitidentityfirstrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_unique_second_prime_factorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentityfirstreal) = S ge_signed_half_unique_second_prime_factorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_second_prime_factorizationunitidentity) + ge_balance_negative_unique_second_prime_factorizationunitidentityfirstreal = (ge_first_rn_unique_second_prime_factorizationunitidentity) + ge_balance_positive_unique_second_prime_factorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationunitidentityfirstimaginary ge_balance_negative_unique_second_prime_factorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationunitidentityfirstimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityfirst) = 2 * ge_signed_half_unique_second_prime_factorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentityfirstimaginary) = S ge_signed_half_unique_second_prime_factorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_prime_factorizationunitidentity) + ge_balance_negative_unique_second_prime_factorizationunitidentityfirstimaginary = (ge_first_in_unique_second_prime_factorizationunitidentity) + ge_balance_positive_unique_second_prime_factorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_prime_factorizationunitidentitysecond ge_representation_imaginary_code_unique_second_prime_factorizationunitidentitysecond. (((gr_inverse_unique_second_prime_factorizationunit) = ((ge_representation_real_code_unique_second_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentitysecond)) * S ((ge_representation_real_code_unique_second_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentitysecond)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentitysecond))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationunitidentitysecondreal ge_balance_negative_unique_second_prime_factorizationunitidentitysecondreal. (((((ge_representation_real_code_unique_second_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationunitidentitysecondreal) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationunitidentitysecondrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_unique_second_prime_factorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentitysecondreal) = S ge_signed_half_unique_second_prime_factorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_second_prime_factorizationunitidentity) + ge_balance_negative_unique_second_prime_factorizationunitidentitysecondreal = (ge_second_rn_unique_second_prime_factorizationunitidentity) + ge_balance_positive_unique_second_prime_factorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationunitidentitysecondimaginary ge_balance_negative_unique_second_prime_factorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationunitidentitysecondimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentitysecond) = 2 * ge_signed_half_unique_second_prime_factorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentitysecondimaginary) = S ge_signed_half_unique_second_prime_factorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_second_prime_factorizationunitidentity) + ge_balance_negative_unique_second_prime_factorizationunitidentitysecondimaginary = (ge_second_in_unique_second_prime_factorizationunitidentity) + ge_balance_positive_unique_second_prime_factorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_prime_factorizationunitidentityoutput ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityoutput. (((6) = ((ge_representation_real_code_unique_second_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityoutput)) * S ((ge_representation_real_code_unique_second_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityoutput)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityoutput))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationunitidentityoutputreal ge_balance_negative_unique_second_prime_factorizationunitidentityoutputreal. (((((ge_representation_real_code_unique_second_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationunitidentityoutputreal) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationunitidentityoutputrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_unique_second_prime_factorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentityoutputreal) = S ge_signed_half_unique_second_prime_factorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationunitidentity) * (ge_second_rp_unique_second_prime_factorizationunitidentity))) + (((ge_first_rn_unique_second_prime_factorizationunitidentity) * (ge_second_rn_unique_second_prime_factorizationunitidentity))))) + (((((ge_first_ip_unique_second_prime_factorizationunitidentity) * (ge_second_in_unique_second_prime_factorizationunitidentity))) + (((ge_first_in_unique_second_prime_factorizationunitidentity) * (ge_second_ip_unique_second_prime_factorizationunitidentity))))))) + ge_balance_negative_unique_second_prime_factorizationunitidentityoutputreal = (((((((ge_first_rp_unique_second_prime_factorizationunitidentity) * (ge_second_rn_unique_second_prime_factorizationunitidentity))) + (((ge_first_rn_unique_second_prime_factorizationunitidentity) * (ge_second_rp_unique_second_prime_factorizationunitidentity))))) + (((((ge_first_ip_unique_second_prime_factorizationunitidentity) * (ge_second_ip_unique_second_prime_factorizationunitidentity))) + (((ge_first_in_unique_second_prime_factorizationunitidentity) * (ge_second_in_unique_second_prime_factorizationunitidentity))))))) + ge_balance_positive_unique_second_prime_factorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationunitidentityoutputimaginary ge_balance_negative_unique_second_prime_factorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationunitidentityoutputimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationunitidentityoutput) = 2 * ge_signed_half_unique_second_prime_factorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationunitidentityoutputimaginary) = S ge_signed_half_unique_second_prime_factorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationunitidentity) * (ge_second_ip_unique_second_prime_factorizationunitidentity))) + (((ge_first_rn_unique_second_prime_factorizationunitidentity) * (ge_second_in_unique_second_prime_factorizationunitidentity))))) + (((((ge_first_ip_unique_second_prime_factorizationunitidentity) * (ge_second_rp_unique_second_prime_factorizationunitidentity))) + (((ge_first_in_unique_second_prime_factorizationunitidentity) * (ge_second_rn_unique_second_prime_factorizationunitidentity))))))) + ge_balance_negative_unique_second_prime_factorizationunitidentityoutputimaginary = (((((((ge_first_rp_unique_second_prime_factorizationunitidentity) * (ge_second_in_unique_second_prime_factorizationunitidentity))) + (((ge_first_rn_unique_second_prime_factorizationunitidentity) * (ge_second_ip_unique_second_prime_factorizationunitidentity))))) + (((((ge_first_ip_unique_second_prime_factorizationunitidentity) * (ge_second_rn_unique_second_prime_factorizationunitidentity))) + (((ge_first_in_unique_second_prime_factorizationunitidentity) * (ge_second_rp_unique_second_prime_factorizationunitidentity))))))) + ge_balance_positive_unique_second_prime_factorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_unique_second_prime_factorizationprimes gr_prime_factor_value_unique_second_prime_factorizationprimes. (exists ge_gap_unique_second_prime_factorizationprimesindex. ge_gap_unique_second_prime_factorizationprimesindex + S (gr_prime_factor_index_unique_second_prime_factorizationprimes) = (m)) -> (((exists ff_h_gprod_unique_second_prime_factorizationprimesentry. ff_h_gprod_unique_second_prime_factorizationprimesentry + S (gr_prime_factor_value_unique_second_prime_factorizationprimes) = S ((S (gr_prime_factor_index_unique_second_prime_factorizationprimes)) * e)) /\ exists ff_q_gprod_unique_second_prime_factorizationprimesentry. d = ff_q_gprod_unique_second_prime_factorizationprimesentry * S ((S (gr_prime_factor_index_unique_second_prime_factorizationprimes)) * e) + (gr_prime_factor_value_unique_second_prime_factorizationprimes))) -> (((exists ge_real_positive_unique_second_prime_factorizationprimesprimecarrier ge_real_negative_unique_second_prime_factorizationprimesprimecarrier ge_imaginary_positive_unique_second_prime_factorizationprimesprimecarrier ge_imaginary_negative_unique_second_prime_factorizationprimesprimecarrier. (exists ge_real_code_unique_second_prime_factorizationprimesprimecarrierdecode ge_imaginary_code_unique_second_prime_factorizationprimesprimecarrierdecode. (((gr_prime_factor_value_unique_second_prime_factorizationprimes) = ((ge_real_code_unique_second_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unique_second_prime_factorizationprimesprimecarrierdecode)) * S ((ge_real_code_unique_second_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unique_second_prime_factorizationprimesprimecarrierdecode)) + ((ge_imaginary_code_unique_second_prime_factorizationprimesprimecarrierdecode) + (ge_imaginary_code_unique_second_prime_factorizationprimesprimecarrierdecode))) /\ (((((ge_real_code_unique_second_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_real_positive_unique_second_prime_factorizationprimesprimecarrier) /\ (ge_real_negative_unique_second_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_unique_second_prime_factorizationprimesprimecarrierdecode_real. (((ge_real_code_unique_second_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_unique_second_prime_factorizationprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_unique_second_prime_factorizationprimesprimecarrier) = 0) /\ (ge_real_negative_unique_second_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_unique_second_prime_factorizationprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_unique_second_prime_factorizationprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_unique_second_prime_factorizationprimesprimecarrier) /\ (ge_imaginary_negative_unique_second_prime_factorizationprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_unique_second_prime_factorizationprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_unique_second_prime_factorizationprimesprimecarrierdecode) = 2 * ge_signed_half_ge_unique_second_prime_factorizationprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unique_second_prime_factorizationprimesprimecarrier) = 0) /\ (ge_imaginary_negative_unique_second_prime_factorizationprimesprimecarrier) = S ge_signed_half_ge_unique_second_prime_factorizationprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_unique_second_prime_factorizationprimes)=0)) /\ ((~(exists gr_inverse_unique_second_prime_factorizationprimesprimenonunit. (exists ge_first_rp_unique_second_prime_factorizationprimesprimenonunitidentity ge_first_rn_unique_second_prime_factorizationprimesprimenonunitidentity ge_first_ip_unique_second_prime_factorizationprimesprimenonunitidentity ge_first_in_unique_second_prime_factorizationprimesprimenonunitidentity ge_second_rp_unique_second_prime_factorizationprimesprimenonunitidentity ge_second_rn_unique_second_prime_factorizationprimesprimenonunitidentity ge_second_ip_unique_second_prime_factorizationprimesprimenonunitidentity ge_second_in_unique_second_prime_factorizationprimesprimenonunitidentity. ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst. (((gr_prime_factor_value_unique_second_prime_factorizationprimes) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityfirstreal ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityfirstreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_second_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityfirstreal = (ge_first_rn_unique_second_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginary = (ge_first_in_unique_second_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond. (((gr_inverse_unique_second_prime_factorizationprimesprimenonunit) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentitysecondreal ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentitysecondreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_second_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentitysecondreal = (ge_second_rn_unique_second_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentitysecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_second_prime_factorizationprimesprimenonunitidentity) + ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginary = (ge_second_in_unique_second_prime_factorizationprimesprimenonunitidentity) + ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityoutputreal ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityoutputreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unique_second_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unique_second_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unique_second_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unique_second_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unique_second_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unique_second_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unique_second_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unique_second_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimenonunitidentityoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unique_second_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unique_second_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unique_second_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unique_second_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_in_unique_second_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_ip_unique_second_prime_factorizationprimesprimenonunitidentity))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_rn_unique_second_prime_factorizationprimesprimenonunitidentity))) + (((ge_first_in_unique_second_prime_factorizationprimesprimenonunitidentity) * (ge_second_rp_unique_second_prime_factorizationprimesprimenonunitidentity))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unique_second_prime_factorizationprimesprime gr_second_factor_unique_second_prime_factorizationprimesprime gr_product_unique_second_prime_factorizationprimesprime. (exists ge_first_rp_unique_second_prime_factorizationprimesprimeproduct ge_first_rn_unique_second_prime_factorizationprimesprimeproduct ge_first_ip_unique_second_prime_factorizationprimesprimeproduct ge_first_in_unique_second_prime_factorizationprimesprimeproduct ge_second_rp_unique_second_prime_factorizationprimesprimeproduct ge_second_rn_unique_second_prime_factorizationprimesprimeproduct ge_second_ip_unique_second_prime_factorizationprimesprimeproduct ge_second_in_unique_second_prime_factorizationprimesprimeproduct. ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductfirst ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductfirst. (((gr_first_factor_unique_second_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductfirst)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductfirst)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductfirst))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimeproductfirstreal ge_balance_negative_unique_second_prime_factorizationprimesprimeproductfirstreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductfirstreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimeproductfirstrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductfirstreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_unique_second_prime_factorizationprimesprimeproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimeproductfirstreal = (ge_first_rn_unique_second_prime_factorizationprimesprimeproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimeproductfirstimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductfirstimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductfirstimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_prime_factorizationprimesprimeproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimeproductfirstimaginary = (ge_first_in_unique_second_prime_factorizationprimesprimeproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductsecond ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductsecond. (((gr_second_factor_unique_second_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductsecond)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductsecond)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductsecond))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimeproductsecondreal ge_balance_negative_unique_second_prime_factorizationprimesprimeproductsecondreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductsecondreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimeproductsecondrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductsecondreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_unique_second_prime_factorizationprimesprimeproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimeproductsecondreal = (ge_second_rn_unique_second_prime_factorizationprimesprimeproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimeproductsecondimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductsecondimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductsecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductsecondimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_unique_second_prime_factorizationprimesprimeproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimeproductsecondimaginary = (ge_second_in_unique_second_prime_factorizationprimesprimeproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductoutput ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductoutput. (((gr_product_unique_second_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductoutput)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductoutput)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductoutput))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimeproductoutputreal ge_balance_negative_unique_second_prime_factorizationprimesprimeproductoutputreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductoutputreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimeproductoutputrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductoutputreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimeproductoutputreal = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimeproductoutputimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductoutputimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimeproductoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimeproductoutputimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimeproduct))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimeproductoutputimaginary = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimeproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimeproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimeproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimeproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimeproduct))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_unique_second_prime_factorizationprimesprimedivisor. (exists ge_first_rp_unique_second_prime_factorizationprimesprimedivisorproduct ge_first_rn_unique_second_prime_factorizationprimesprimedivisorproduct ge_first_ip_unique_second_prime_factorizationprimesprimedivisorproduct ge_first_in_unique_second_prime_factorizationprimesprimedivisorproduct ge_second_rp_unique_second_prime_factorizationprimesprimedivisorproduct ge_second_rn_unique_second_prime_factorizationprimesprimedivisorproduct ge_second_ip_unique_second_prime_factorizationprimesprimedivisorproduct ge_second_in_unique_second_prime_factorizationprimesprimedivisorproduct. ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductfirst ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductfirst. (((gr_prime_factor_value_unique_second_prime_factorizationprimes) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductfirstreal ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductfirstreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_unique_second_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductfirstreal = (ge_first_rn_unique_second_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginary = (ge_first_in_unique_second_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductsecond ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductsecond. (((gr_quotient_unique_second_prime_factorizationprimesprimedivisor) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductsecondreal ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductsecondreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_unique_second_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductsecondreal = (ge_second_rn_unique_second_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductsecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unique_second_prime_factorizationprimesprimedivisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginary = (ge_second_in_unique_second_prime_factorizationprimesprimedivisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductoutput ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductoutput. (((gr_product_unique_second_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductoutputreal ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductoutputreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductoutputreal = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimedivisorproductoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimedivisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimedivisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimedivisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimedivisorproduct))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_unique_second_prime_factorizationprimesprimefirst_divisor. (exists ge_first_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct ge_first_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct ge_first_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct ge_first_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct ge_second_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct ge_second_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct ge_second_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct ge_second_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_unique_second_prime_factorizationprimes) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstreal ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstreal = (ge_first_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond. (((gr_quotient_unique_second_prime_factorizationprimesprimefirst_divisor) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondreal ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondreal = (ge_second_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput. (((gr_first_factor_unique_second_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputreal ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimefirst_divisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimefirst_divisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimefirst_divisorproduct))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_unique_second_prime_factorizationprimesprimesecond_divisor. (exists ge_first_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct ge_first_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct ge_first_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct ge_first_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct ge_second_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct ge_second_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct ge_second_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct ge_second_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_unique_second_prime_factorizationprimes) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstreal ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstreal = (ge_first_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond. (((gr_quotient_unique_second_prime_factorizationprimesprimesecond_divisor) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondreal ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondreal = (ge_second_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct) + ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput. (((gr_second_factor_unique_second_prime_factorizationprimesprime) = ((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputreal ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_negative_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rn_unique_second_prime_factorizationprimesprimesecond_divisorproduct))) + (((ge_first_in_unique_second_prime_factorizationprimesprimesecond_divisorproduct) * (ge_second_rp_unique_second_prime_factorizationprimesprimesecond_divisorproduct))))))) + ge_balance_positive_unique_second_prime_factorizationprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_unique_second_prime_factorization. ((exists gr_product_trace_unique_second_prime_factorizationtrace gr_product_scale_unique_second_prime_factorizationtrace. ((((exists ff_h_gprod_unique_second_prime_factorizationtracestart. ff_h_gprod_unique_second_prime_factorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_unique_second_prime_factorizationtrace)) /\ exists ff_q_gprod_unique_second_prime_factorizationtracestart. gr_product_trace_unique_second_prime_factorizationtrace = ff_q_gprod_unique_second_prime_factorizationtracestart * S ((S (0)) * gr_product_scale_unique_second_prime_factorizationtrace) + (6))) /\ ((((exists ff_h_gprod_unique_second_prime_factorizationtraceend. ff_h_gprod_unique_second_prime_factorizationtraceend + S (gr_prime_factor_product_unique_second_prime_factorization) = S ((S (m)) * gr_product_scale_unique_second_prime_factorizationtrace)) /\ exists ff_q_gprod_unique_second_prime_factorizationtraceend. gr_product_trace_unique_second_prime_factorizationtrace = ff_q_gprod_unique_second_prime_factorizationtraceend * S ((S (m)) * gr_product_scale_unique_second_prime_factorizationtrace) + (gr_prime_factor_product_unique_second_prime_factorization))) /\ (forall gr_product_index_unique_second_prime_factorizationtracesteps. (exists ge_gap_unique_second_prime_factorizationtracestepsindex_bound. ge_gap_unique_second_prime_factorizationtracestepsindex_bound + S (gr_product_index_unique_second_prime_factorizationtracesteps) = (m)) -> exists gr_product_factor_unique_second_prime_factorizationtracesteps gr_product_before_unique_second_prime_factorizationtracesteps gr_product_after_unique_second_prime_factorizationtracesteps. ((((exists ff_h_gprod_unique_second_prime_factorizationtracestepsfactor. ff_h_gprod_unique_second_prime_factorizationtracestepsfactor + S (gr_product_factor_unique_second_prime_factorizationtracesteps) = S ((S (gr_product_index_unique_second_prime_factorizationtracesteps)) * e)) /\ exists ff_q_gprod_unique_second_prime_factorizationtracestepsfactor. d = ff_q_gprod_unique_second_prime_factorizationtracestepsfactor * S ((S (gr_product_index_unique_second_prime_factorizationtracesteps)) * e) + (gr_product_factor_unique_second_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unique_second_prime_factorizationtracestepsbefore. ff_h_gprod_unique_second_prime_factorizationtracestepsbefore + S (gr_product_before_unique_second_prime_factorizationtracesteps) = S ((S (gr_product_index_unique_second_prime_factorizationtracesteps)) * gr_product_scale_unique_second_prime_factorizationtrace)) /\ exists ff_q_gprod_unique_second_prime_factorizationtracestepsbefore. gr_product_trace_unique_second_prime_factorizationtrace = ff_q_gprod_unique_second_prime_factorizationtracestepsbefore * S ((S (gr_product_index_unique_second_prime_factorizationtracesteps)) * gr_product_scale_unique_second_prime_factorizationtrace) + (gr_product_before_unique_second_prime_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unique_second_prime_factorizationtracestepsafter. ff_h_gprod_unique_second_prime_factorizationtracestepsafter + S (gr_product_after_unique_second_prime_factorizationtracesteps) = S ((S (S (gr_product_index_unique_second_prime_factorizationtracesteps))) * gr_product_scale_unique_second_prime_factorizationtrace)) /\ exists ff_q_gprod_unique_second_prime_factorizationtracestepsafter. gr_product_trace_unique_second_prime_factorizationtrace = ff_q_gprod_unique_second_prime_factorizationtracestepsafter * S ((S (S (gr_product_index_unique_second_prime_factorizationtracesteps))) * gr_product_scale_unique_second_prime_factorizationtrace) + (gr_product_after_unique_second_prime_factorizationtracesteps))) /\ (exists ge_first_rp_unique_second_prime_factorizationtracestepsmultiply ge_first_rn_unique_second_prime_factorizationtracestepsmultiply ge_first_ip_unique_second_prime_factorizationtracestepsmultiply ge_first_in_unique_second_prime_factorizationtracestepsmultiply ge_second_rp_unique_second_prime_factorizationtracestepsmultiply ge_second_rn_unique_second_prime_factorizationtracestepsmultiply ge_second_ip_unique_second_prime_factorizationtracestepsmultiply ge_second_in_unique_second_prime_factorizationtracestepsmultiply. ((exists ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyfirst ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyfirst. (((gr_product_before_unique_second_prime_factorizationtracesteps) = ((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyfirstreal ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyfirstreal) = S ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unique_second_prime_factorizationtracestepsmultiply) + ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyfirstreal = (ge_first_rn_unique_second_prime_factorizationtracestepsmultiply) + ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyfirstimaginary ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_prime_factorizationtracestepsmultiply) + ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyfirstimaginary = (ge_first_in_unique_second_prime_factorizationtracestepsmultiply) + ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplysecond ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplysecond. (((gr_product_factor_unique_second_prime_factorizationtracesteps) = ((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplysecondreal ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unique_second_prime_factorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplysecondreal) = S ge_signed_half_unique_second_prime_factorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unique_second_prime_factorizationtracestepsmultiply) + ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplysecondreal = (ge_second_rn_unique_second_prime_factorizationtracestepsmultiply) + ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplysecondimaginary ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unique_second_prime_factorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_unique_second_prime_factorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unique_second_prime_factorizationtracestepsmultiply) + ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplysecondimaginary = (ge_second_in_unique_second_prime_factorizationtracestepsmultiply) + ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyoutput ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyoutput. (((gr_product_after_unique_second_prime_factorizationtracesteps) = ((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyoutputreal ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyoutputreal) = S ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_rp_unique_second_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_rn_unique_second_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_in_unique_second_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_ip_unique_second_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_rn_unique_second_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_rp_unique_second_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_ip_unique_second_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_in_unique_second_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyoutputimaginary ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_unique_second_prime_factorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_ip_unique_second_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_in_unique_second_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_rp_unique_second_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_rn_unique_second_prime_factorizationtracestepsmultiply))))))) + ge_balance_negative_unique_second_prime_factorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_in_unique_second_prime_factorizationtracestepsmultiply))) + (((ge_first_rn_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_ip_unique_second_prime_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_rn_unique_second_prime_factorizationtracestepsmultiply))) + (((ge_first_in_unique_second_prime_factorizationtracestepsmultiply) * (ge_second_rp_unique_second_prime_factorizationtracestepsmultiply))))))) + ge_balance_positive_unique_second_prime_factorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_unique_second_prime_factorizationreconstruct ge_first_rn_unique_second_prime_factorizationreconstruct ge_first_ip_unique_second_prime_factorizationreconstruct ge_first_in_unique_second_prime_factorizationreconstruct ge_second_rp_unique_second_prime_factorizationreconstruct ge_second_rn_unique_second_prime_factorizationreconstruct ge_second_ip_unique_second_prime_factorizationreconstruct ge_second_in_unique_second_prime_factorizationreconstruct. ((exists ge_representation_real_code_unique_second_prime_factorizationreconstructfirst ge_representation_imaginary_code_unique_second_prime_factorizationreconstructfirst. (((v) = ((ge_representation_real_code_unique_second_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructfirst)) * S ((ge_representation_real_code_unique_second_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructfirst)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructfirst) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructfirst))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationreconstructfirstreal ge_balance_negative_unique_second_prime_factorizationreconstructfirstreal. (((((ge_representation_real_code_unique_second_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationreconstructfirstreal) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationreconstructfirstrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationreconstructfirst) = 2 * ge_signed_half_unique_second_prime_factorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructfirstreal) = S ge_signed_half_unique_second_prime_factorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_unique_second_prime_factorizationreconstruct) + ge_balance_negative_unique_second_prime_factorizationreconstructfirstreal = (ge_first_rn_unique_second_prime_factorizationreconstruct) + ge_balance_positive_unique_second_prime_factorizationreconstructfirstreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationreconstructfirstimaginary ge_balance_negative_unique_second_prime_factorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructfirst) = 2 * (ge_balance_positive_unique_second_prime_factorizationreconstructfirstimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructfirst) = 2 * ge_signed_half_unique_second_prime_factorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructfirstimaginary) = S ge_signed_half_unique_second_prime_factorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_unique_second_prime_factorizationreconstruct) + ge_balance_negative_unique_second_prime_factorizationreconstructfirstimaginary = (ge_first_in_unique_second_prime_factorizationreconstruct) + ge_balance_positive_unique_second_prime_factorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_second_prime_factorizationreconstructsecond ge_representation_imaginary_code_unique_second_prime_factorizationreconstructsecond. (((gr_prime_factor_product_unique_second_prime_factorization) = ((ge_representation_real_code_unique_second_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructsecond)) * S ((ge_representation_real_code_unique_second_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructsecond)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructsecond) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructsecond))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationreconstructsecondreal ge_balance_negative_unique_second_prime_factorizationreconstructsecondreal. (((((ge_representation_real_code_unique_second_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationreconstructsecondreal) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationreconstructsecondrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationreconstructsecond) = 2 * ge_signed_half_unique_second_prime_factorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructsecondreal) = S ge_signed_half_unique_second_prime_factorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_unique_second_prime_factorizationreconstruct) + ge_balance_negative_unique_second_prime_factorizationreconstructsecondreal = (ge_second_rn_unique_second_prime_factorizationreconstruct) + ge_balance_positive_unique_second_prime_factorizationreconstructsecondreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationreconstructsecondimaginary ge_balance_negative_unique_second_prime_factorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructsecond) = 2 * (ge_balance_positive_unique_second_prime_factorizationreconstructsecondimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructsecond) = 2 * ge_signed_half_unique_second_prime_factorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructsecondimaginary) = S ge_signed_half_unique_second_prime_factorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_unique_second_prime_factorizationreconstruct) + ge_balance_negative_unique_second_prime_factorizationreconstructsecondimaginary = (ge_second_in_unique_second_prime_factorizationreconstruct) + ge_balance_positive_unique_second_prime_factorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_second_prime_factorizationreconstructoutput ge_representation_imaginary_code_unique_second_prime_factorizationreconstructoutput. (((z) = ((ge_representation_real_code_unique_second_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructoutput)) * S ((ge_representation_real_code_unique_second_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructoutput)) + ((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructoutput) + (ge_representation_imaginary_code_unique_second_prime_factorizationreconstructoutput))) /\ ((exists ge_balance_positive_unique_second_prime_factorizationreconstructoutputreal ge_balance_negative_unique_second_prime_factorizationreconstructoutputreal. (((((ge_representation_real_code_unique_second_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationreconstructoutputreal) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationreconstructoutputrealdecode. (((ge_representation_real_code_unique_second_prime_factorizationreconstructoutput) = 2 * ge_signed_half_unique_second_prime_factorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructoutputreal) = S ge_signed_half_unique_second_prime_factorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationreconstruct) * (ge_second_rp_unique_second_prime_factorizationreconstruct))) + (((ge_first_rn_unique_second_prime_factorizationreconstruct) * (ge_second_rn_unique_second_prime_factorizationreconstruct))))) + (((((ge_first_ip_unique_second_prime_factorizationreconstruct) * (ge_second_in_unique_second_prime_factorizationreconstruct))) + (((ge_first_in_unique_second_prime_factorizationreconstruct) * (ge_second_ip_unique_second_prime_factorizationreconstruct))))))) + ge_balance_negative_unique_second_prime_factorizationreconstructoutputreal = (((((((ge_first_rp_unique_second_prime_factorizationreconstruct) * (ge_second_rn_unique_second_prime_factorizationreconstruct))) + (((ge_first_rn_unique_second_prime_factorizationreconstruct) * (ge_second_rp_unique_second_prime_factorizationreconstruct))))) + (((((ge_first_ip_unique_second_prime_factorizationreconstruct) * (ge_second_ip_unique_second_prime_factorizationreconstruct))) + (((ge_first_in_unique_second_prime_factorizationreconstruct) * (ge_second_in_unique_second_prime_factorizationreconstruct))))))) + ge_balance_positive_unique_second_prime_factorizationreconstructoutputreal))) /\ (exists ge_balance_positive_unique_second_prime_factorizationreconstructoutputimaginary ge_balance_negative_unique_second_prime_factorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructoutput) = 2 * (ge_balance_positive_unique_second_prime_factorizationreconstructoutputimaginary) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_unique_second_prime_factorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_unique_second_prime_factorizationreconstructoutput) = 2 * ge_signed_half_unique_second_prime_factorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_second_prime_factorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_unique_second_prime_factorizationreconstructoutputimaginary) = S ge_signed_half_unique_second_prime_factorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_second_prime_factorizationreconstruct) * (ge_second_ip_unique_second_prime_factorizationreconstruct))) + (((ge_first_rn_unique_second_prime_factorizationreconstruct) * (ge_second_in_unique_second_prime_factorizationreconstruct))))) + (((((ge_first_ip_unique_second_prime_factorizationreconstruct) * (ge_second_rp_unique_second_prime_factorizationreconstruct))) + (((ge_first_in_unique_second_prime_factorizationreconstruct) * (ge_second_rn_unique_second_prime_factorizationreconstruct))))))) + ge_balance_negative_unique_second_prime_factorizationreconstructoutputimaginary = (((((((ge_first_rp_unique_second_prime_factorizationreconstruct) * (ge_second_in_unique_second_prime_factorizationreconstruct))) + (((ge_first_rn_unique_second_prime_factorizationreconstruct) * (ge_second_ip_unique_second_prime_factorizationreconstruct))))) + (((((ge_first_ip_unique_second_prime_factorizationreconstruct) * (ge_second_rn_unique_second_prime_factorizationreconstruct))) + (((ge_first_in_unique_second_prime_factorizationreconstruct) * (ge_second_rp_unique_second_prime_factorizationreconstruct))))))) + ge_balance_positive_unique_second_prime_factorizationreconstructoutputimaginary)))))))))))))) -> ((((l)=(m)) /\ (exists gr_unique_map_unique_prime_factorizations gr_unique_scale_unique_prime_factorizations. (((((forall pfp_i_unique_prime_factorizationsmatchingbijectionbounded. (exists pfp_gap_unique_prime_factorizationsmatchingbijectionboundedindex. pfp_gap_unique_prime_factorizationsmatchingbijectionboundedindex + S (pfp_i_unique_prime_factorizationsmatchingbijectionbounded) = (l)) -> exists pfp_a_unique_prime_factorizationsmatchingbijectionbounded. (((exists ff_h_pfp_unique_prime_factorizationsmatchingbijectionboundedentry. ff_h_pfp_unique_prime_factorizationsmatchingbijectionboundedentry + S (pfp_a_unique_prime_factorizationsmatchingbijectionbounded) = S ((S (pfp_i_unique_prime_factorizationsmatchingbijectionbounded)) * gr_unique_scale_unique_prime_factorizations)) /\ exists ff_q_pfp_unique_prime_factorizationsmatchingbijectionboundedentry. gr_unique_map_unique_prime_factorizations = ff_q_pfp_unique_prime_factorizationsmatchingbijectionboundedentry * S ((S (pfp_i_unique_prime_factorizationsmatchingbijectionbounded)) * gr_unique_scale_unique_prime_factorizations) + (pfp_a_unique_prime_factorizationsmatchingbijectionbounded))) /\ (exists pfp_gap_unique_prime_factorizationsmatchingbijectionboundedvalue. pfp_gap_unique_prime_factorizationsmatchingbijectionboundedvalue + S (pfp_a_unique_prime_factorizationsmatchingbijectionbounded) = (l))) /\ (((forall pfp_i_unique_prime_factorizationsmatchingbijectioninjective pfp_j_unique_prime_factorizationsmatchingbijectioninjective pfp_a_unique_prime_factorizationsmatchingbijectioninjective. (exists pfp_gap_unique_prime_factorizationsmatchingbijectioninjectivefirst. pfp_gap_unique_prime_factorizationsmatchingbijectioninjectivefirst + S (pfp_i_unique_prime_factorizationsmatchingbijectioninjective) = (l)) -> (exists pfp_gap_unique_prime_factorizationsmatchingbijectioninjectivesecond. pfp_gap_unique_prime_factorizationsmatchingbijectioninjectivesecond + S (pfp_j_unique_prime_factorizationsmatchingbijectioninjective) = (l)) -> (((exists ff_h_pfp_unique_prime_factorizationsmatchingbijectioninjectiveleft. ff_h_pfp_unique_prime_factorizationsmatchingbijectioninjectiveleft + S (pfp_a_unique_prime_factorizationsmatchingbijectioninjective) = S ((S (pfp_i_unique_prime_factorizationsmatchingbijectioninjective)) * gr_unique_scale_unique_prime_factorizations)) /\ exists ff_q_pfp_unique_prime_factorizationsmatchingbijectioninjectiveleft. gr_unique_map_unique_prime_factorizations = ff_q_pfp_unique_prime_factorizationsmatchingbijectioninjectiveleft * S ((S (pfp_i_unique_prime_factorizationsmatchingbijectioninjective)) * gr_unique_scale_unique_prime_factorizations) + (pfp_a_unique_prime_factorizationsmatchingbijectioninjective))) -> (((exists ff_h_pfp_unique_prime_factorizationsmatchingbijectioninjectiveright. ff_h_pfp_unique_prime_factorizationsmatchingbijectioninjectiveright + S (pfp_a_unique_prime_factorizationsmatchingbijectioninjective) = S ((S (pfp_j_unique_prime_factorizationsmatchingbijectioninjective)) * gr_unique_scale_unique_prime_factorizations)) /\ exists ff_q_pfp_unique_prime_factorizationsmatchingbijectioninjectiveright. gr_unique_map_unique_prime_factorizations = ff_q_pfp_unique_prime_factorizationsmatchingbijectioninjectiveright * S ((S (pfp_j_unique_prime_factorizationsmatchingbijectioninjective)) * gr_unique_scale_unique_prime_factorizations) + (pfp_a_unique_prime_factorizationsmatchingbijectioninjective))) -> pfp_i_unique_prime_factorizationsmatchingbijectioninjective = pfp_j_unique_prime_factorizationsmatchingbijectioninjective) /\ (forall pfp_a_unique_prime_factorizationsmatchingbijectionsurjective. (exists pfp_gap_unique_prime_factorizationsmatchingbijectionsurjectivevalue. pfp_gap_unique_prime_factorizationsmatchingbijectionsurjectivevalue + S (pfp_a_unique_prime_factorizationsmatchingbijectionsurjective) = (l)) -> exists pfp_i_unique_prime_factorizationsmatchingbijectionsurjective. (exists pfp_gap_unique_prime_factorizationsmatchingbijectionsurjectiveindex. pfp_gap_unique_prime_factorizationsmatchingbijectionsurjectiveindex + S (pfp_i_unique_prime_factorizationsmatchingbijectionsurjective) = (l)) /\ (((exists ff_h_pfp_unique_prime_factorizationsmatchingbijectionsurjectiveentry. ff_h_pfp_unique_prime_factorizationsmatchingbijectionsurjectiveentry + S (pfp_a_unique_prime_factorizationsmatchingbijectionsurjective) = S ((S (pfp_i_unique_prime_factorizationsmatchingbijectionsurjective)) * gr_unique_scale_unique_prime_factorizations)) /\ exists ff_q_pfp_unique_prime_factorizationsmatchingbijectionsurjectiveentry. gr_unique_map_unique_prime_factorizations = ff_q_pfp_unique_prime_factorizationsmatchingbijectionsurjectiveentry * S ((S (pfp_i_unique_prime_factorizationsmatchingbijectionsurjective)) * gr_unique_scale_unique_prime_factorizations) + (pfp_a_unique_prime_factorizationsmatchingbijectionsurjective)))))))) /\ (forall gr_match_index_unique_prime_factorizationsmatchingmatching gr_match_image_unique_prime_factorizationsmatchingmatching gr_match_source_unique_prime_factorizationsmatchingmatching gr_match_target_unique_prime_factorizationsmatchingmatching. (exists ge_gap_unique_prime_factorizationsmatchingmatchingindex. ge_gap_unique_prime_factorizationsmatchingmatchingindex + S (gr_match_index_unique_prime_factorizationsmatchingmatching) = (l)) -> (((exists ff_h_gprod_unique_prime_factorizationsmatchingmatchingmap. ff_h_gprod_unique_prime_factorizationsmatchingmatchingmap + S (gr_match_image_unique_prime_factorizationsmatchingmatching) = S ((S (gr_match_index_unique_prime_factorizationsmatchingmatching)) * gr_unique_scale_unique_prime_factorizations)) /\ exists ff_q_gprod_unique_prime_factorizationsmatchingmatchingmap. gr_unique_map_unique_prime_factorizations = ff_q_gprod_unique_prime_factorizationsmatchingmatchingmap * S ((S (gr_match_index_unique_prime_factorizationsmatchingmatching)) * gr_unique_scale_unique_prime_factorizations) + (gr_match_image_unique_prime_factorizationsmatchingmatching))) -> (((exists ff_h_gprod_unique_prime_factorizationsmatchingmatchingsource. ff_h_gprod_unique_prime_factorizationsmatchingmatchingsource + S (gr_match_source_unique_prime_factorizationsmatchingmatching) = S ((S (gr_match_index_unique_prime_factorizationsmatchingmatching)) * c)) /\ exists ff_q_gprod_unique_prime_factorizationsmatchingmatchingsource. b = ff_q_gprod_unique_prime_factorizationsmatchingmatchingsource * S ((S (gr_match_index_unique_prime_factorizationsmatchingmatching)) * c) + (gr_match_source_unique_prime_factorizationsmatchingmatching))) -> (((exists ff_h_gprod_unique_prime_factorizationsmatchingmatchingtarget. ff_h_gprod_unique_prime_factorizationsmatchingmatchingtarget + S (gr_match_target_unique_prime_factorizationsmatchingmatching) = S ((S (gr_match_image_unique_prime_factorizationsmatchingmatching)) * e)) /\ exists ff_q_gprod_unique_prime_factorizationsmatchingmatchingtarget. d = ff_q_gprod_unique_prime_factorizationsmatchingmatchingtarget * S ((S (gr_match_image_unique_prime_factorizationsmatchingmatching)) * e) + (gr_match_target_unique_prime_factorizationsmatchingmatching))) -> (exists gr_unit_unique_prime_factorizationsmatchingmatchingunit_witness. ((exists gr_inverse_unique_prime_factorizationsmatchingmatchingunit_witnessunit. (exists ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst. (((gr_unit_unique_prime_factorizationsmatchingmatchingunit_witness) = ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond. (((gr_inverse_unique_prime_factorizationsmatchingmatchingunit_witnessunit) = ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))) + (((ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity) * (ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport. ((exists ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst. (((gr_unit_unique_prime_factorizationsmatchingmatchingunit_witness) = ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstreal ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstreal) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstreal = (ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary = (ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond. (((gr_match_source_unique_prime_factorizationsmatchingmatching) = ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondreal ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondreal) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondreal = (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary = (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput. (((gr_match_target_unique_prime_factorizationsmatchingmatching) = ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputreal ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputreal) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))))))) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))))))) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))))))) + ge_balance_negative_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rn_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))) + (((ge_first_in_unique_prime_factorizationsmatchingmatchingunit_witnesstransport) * (ge_second_rp_unique_prime_factorizationsmatchingmatchingunit_witnesstransport))))))) + ge_balance_positive_unique_prime_factorizationsmatchingmatchingunit_witnesstransportoutputimaginary)))))))))))))))))