gaussian_prime_factorization_exists

Exact expanded first-order arithmetic statement

forall z. (exists ge_real_positive_prime_factorization_domain ge_real_negative_prime_factorization_domain ge_imaginary_positive_prime_factorization_domain ge_imaginary_negative_prime_factorization_domain. (exists ge_real_code_prime_factorization_domaindecode ge_imaginary_code_prime_factorization_domaindecode. (((z) = ((ge_real_code_prime_factorization_domaindecode) + (ge_imaginary_code_prime_factorization_domaindecode)) * S ((ge_real_code_prime_factorization_domaindecode) + (ge_imaginary_code_prime_factorization_domaindecode)) + ((ge_imaginary_code_prime_factorization_domaindecode) + (ge_imaginary_code_prime_factorization_domaindecode))) /\ (((((ge_real_code_prime_factorization_domaindecode) = 2 * (ge_real_positive_prime_factorization_domain) /\ (ge_real_negative_prime_factorization_domain) = 0) \/ exists ge_signed_half_ge_prime_factorization_domaindecode_real. (((ge_real_code_prime_factorization_domaindecode) = 2 * ge_signed_half_ge_prime_factorization_domaindecode_real + 1 /\ (ge_real_positive_prime_factorization_domain) = 0) /\ (ge_real_negative_prime_factorization_domain) = S ge_signed_half_ge_prime_factorization_domaindecode_real))) /\ ((((ge_imaginary_code_prime_factorization_domaindecode) = 2 * (ge_imaginary_positive_prime_factorization_domain) /\ (ge_imaginary_negative_prime_factorization_domain) = 0) \/ exists ge_signed_half_ge_prime_factorization_domaindecode_imaginary. (((ge_imaginary_code_prime_factorization_domaindecode) = 2 * ge_signed_half_ge_prime_factorization_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_prime_factorization_domain) = 0) /\ (ge_imaginary_negative_prime_factorization_domain) = S ge_signed_half_ge_prime_factorization_domaindecode_imaginary))))))) -> ~(z=0) -> exists u b c l. (((exists gr_inverse_prime_factorization_existsunit. (exists ge_first_rp_prime_factorization_existsunitidentity ge_first_rn_prime_factorization_existsunitidentity ge_first_ip_prime_factorization_existsunitidentity ge_first_in_prime_factorization_existsunitidentity ge_second_rp_prime_factorization_existsunitidentity ge_second_rn_prime_factorization_existsunitidentity ge_second_ip_prime_factorization_existsunitidentity ge_second_in_prime_factorization_existsunitidentity. ((exists ge_representation_real_code_prime_factorization_existsunitidentityfirst ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst. (((u) = ((ge_representation_real_code_prime_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst)) * S ((ge_representation_real_code_prime_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsunitidentityfirstreal ge_balance_negative_prime_factorization_existsunitidentityfirstreal. (((((ge_representation_real_code_prime_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_existsunitidentityfirstreal) /\ (ge_balance_negative_prime_factorization_existsunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentityfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsunitidentityfirst) = 2 * ge_signed_half_prime_factorization_existsunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentityfirstreal) = S ge_signed_half_prime_factorization_existsunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsunitidentity) + ge_balance_negative_prime_factorization_existsunitidentityfirstreal = (ge_first_rn_prime_factorization_existsunitidentity) + ge_balance_positive_prime_factorization_existsunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsunitidentityfirstimaginary ge_balance_negative_prime_factorization_existsunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_existsunitidentityfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsunitidentityfirst) = 2 * ge_signed_half_prime_factorization_existsunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentityfirstimaginary) = S ge_signed_half_prime_factorization_existsunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsunitidentity) + ge_balance_negative_prime_factorization_existsunitidentityfirstimaginary = (ge_first_in_prime_factorization_existsunitidentity) + ge_balance_positive_prime_factorization_existsunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsunitidentitysecond ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond. (((gr_inverse_prime_factorization_existsunit) = ((ge_representation_real_code_prime_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond)) * S ((ge_representation_real_code_prime_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond)) + ((ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond))) /\ ((exists ge_balance_positive_prime_factorization_existsunitidentitysecondreal ge_balance_negative_prime_factorization_existsunitidentitysecondreal. (((((ge_representation_real_code_prime_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_existsunitidentitysecondreal) /\ (ge_balance_negative_prime_factorization_existsunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentitysecondrealdecode. (((ge_representation_real_code_prime_factorization_existsunitidentitysecond) = 2 * ge_signed_half_prime_factorization_existsunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentitysecondreal) = S ge_signed_half_prime_factorization_existsunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsunitidentity) + ge_balance_negative_prime_factorization_existsunitidentitysecondreal = (ge_second_rn_prime_factorization_existsunitidentity) + ge_balance_positive_prime_factorization_existsunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsunitidentitysecondimaginary ge_balance_negative_prime_factorization_existsunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_existsunitidentitysecondimaginary) /\ (ge_balance_negative_prime_factorization_existsunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsunitidentitysecond) = 2 * ge_signed_half_prime_factorization_existsunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentitysecondimaginary) = S ge_signed_half_prime_factorization_existsunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsunitidentity) + ge_balance_negative_prime_factorization_existsunitidentitysecondimaginary = (ge_second_in_prime_factorization_existsunitidentity) + ge_balance_positive_prime_factorization_existsunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsunitidentityoutput ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput. (((6) = ((ge_representation_real_code_prime_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput)) * S ((ge_representation_real_code_prime_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsunitidentityoutputreal ge_balance_negative_prime_factorization_existsunitidentityoutputreal. (((((ge_representation_real_code_prime_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_existsunitidentityoutputreal) /\ (ge_balance_negative_prime_factorization_existsunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentityoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsunitidentityoutput) = 2 * ge_signed_half_prime_factorization_existsunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentityoutputreal) = S ge_signed_half_prime_factorization_existsunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsunitidentity) * (ge_second_rp_prime_factorization_existsunitidentity))) + (((ge_first_rn_prime_factorization_existsunitidentity) * (ge_second_rn_prime_factorization_existsunitidentity))))) + (((((ge_first_ip_prime_factorization_existsunitidentity) * (ge_second_in_prime_factorization_existsunitidentity))) + (((ge_first_in_prime_factorization_existsunitidentity) * (ge_second_ip_prime_factorization_existsunitidentity))))))) + ge_balance_negative_prime_factorization_existsunitidentityoutputreal = (((((((ge_first_rp_prime_factorization_existsunitidentity) * (ge_second_rn_prime_factorization_existsunitidentity))) + (((ge_first_rn_prime_factorization_existsunitidentity) * (ge_second_rp_prime_factorization_existsunitidentity))))) + (((((ge_first_ip_prime_factorization_existsunitidentity) * (ge_second_ip_prime_factorization_existsunitidentity))) + (((ge_first_in_prime_factorization_existsunitidentity) * (ge_second_in_prime_factorization_existsunitidentity))))))) + ge_balance_positive_prime_factorization_existsunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsunitidentityoutputimaginary ge_balance_negative_prime_factorization_existsunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_existsunitidentityoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsunitidentityoutput) = 2 * ge_signed_half_prime_factorization_existsunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsunitidentityoutputimaginary) = S ge_signed_half_prime_factorization_existsunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsunitidentity) * (ge_second_ip_prime_factorization_existsunitidentity))) + (((ge_first_rn_prime_factorization_existsunitidentity) * (ge_second_in_prime_factorization_existsunitidentity))))) + (((((ge_first_ip_prime_factorization_existsunitidentity) * (ge_second_rp_prime_factorization_existsunitidentity))) + (((ge_first_in_prime_factorization_existsunitidentity) * (ge_second_rn_prime_factorization_existsunitidentity))))))) + ge_balance_negative_prime_factorization_existsunitidentityoutputimaginary = (((((((ge_first_rp_prime_factorization_existsunitidentity) * (ge_second_in_prime_factorization_existsunitidentity))) + (((ge_first_rn_prime_factorization_existsunitidentity) * (ge_second_ip_prime_factorization_existsunitidentity))))) + (((((ge_first_ip_prime_factorization_existsunitidentity) * (ge_second_rn_prime_factorization_existsunitidentity))) + (((ge_first_in_prime_factorization_existsunitidentity) * (ge_second_rp_prime_factorization_existsunitidentity))))))) + ge_balance_positive_prime_factorization_existsunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_prime_factorization_existsprimes gr_prime_factor_value_prime_factorization_existsprimes. (exists ge_gap_prime_factorization_existsprimesindex. ge_gap_prime_factorization_existsprimesindex + S (gr_prime_factor_index_prime_factorization_existsprimes) = (l)) -> (((exists ff_h_gprod_prime_factorization_existsprimesentry. ff_h_gprod_prime_factorization_existsprimesentry + S (gr_prime_factor_value_prime_factorization_existsprimes) = S ((S (gr_prime_factor_index_prime_factorization_existsprimes)) * c)) /\ exists ff_q_gprod_prime_factorization_existsprimesentry. b = ff_q_gprod_prime_factorization_existsprimesentry * S ((S (gr_prime_factor_index_prime_factorization_existsprimes)) * c) + (gr_prime_factor_value_prime_factorization_existsprimes))) -> (((exists ge_real_positive_prime_factorization_existsprimesprimecarrier ge_real_negative_prime_factorization_existsprimesprimecarrier ge_imaginary_positive_prime_factorization_existsprimesprimecarrier ge_imaginary_negative_prime_factorization_existsprimesprimecarrier. (exists ge_real_code_prime_factorization_existsprimesprimecarrierdecode ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_real_code_prime_factorization_existsprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode)) * S ((ge_real_code_prime_factorization_existsprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode)) + ((ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode))) /\ (((((ge_real_code_prime_factorization_existsprimesprimecarrierdecode) = 2 * (ge_real_positive_prime_factorization_existsprimesprimecarrier) /\ (ge_real_negative_prime_factorization_existsprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_real. (((ge_real_code_prime_factorization_existsprimesprimecarrierdecode) = 2 * ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_prime_factorization_existsprimesprimecarrier) = 0) /\ (ge_real_negative_prime_factorization_existsprimesprimecarrier) = S ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_prime_factorization_existsprimesprimecarrier) /\ (ge_imaginary_negative_prime_factorization_existsprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_prime_factorization_existsprimesprimecarrierdecode) = 2 * ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_factorization_existsprimesprimecarrier) = 0) /\ (ge_imaginary_negative_prime_factorization_existsprimesprimecarrier) = S ge_signed_half_ge_prime_factorization_existsprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_prime_factorization_existsprimes)=0)) /\ ((~(exists gr_inverse_prime_factorization_existsprimesprimenonunit. (exists ge_first_rp_prime_factorization_existsprimesprimenonunitidentity ge_first_rn_prime_factorization_existsprimesprimenonunitidentity ge_first_ip_prime_factorization_existsprimesprimenonunitidentity ge_first_in_prime_factorization_existsprimesprimenonunitidentity ge_second_rp_prime_factorization_existsprimesprimenonunitidentity ge_second_rn_prime_factorization_existsprimesprimenonunitidentity ge_second_ip_prime_factorization_existsprimesprimenonunitidentity ge_second_in_prime_factorization_existsprimesprimenonunitidentity. ((exists ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstreal ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstreal = (ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond. (((gr_inverse_prime_factorization_existsprimesprimenonunit) = ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondreal ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentitysecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondreal) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondreal = (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondimaginary ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentitysecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentitysecondimaginary = (ge_second_in_prime_factorization_existsprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputreal ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimenonunitidentityoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_in_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_existsprimesprimenonunitidentity))))))) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_existsprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_in_prime_factorization_existsprimesprimenonunitidentity))))))) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimenonunitidentityoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_in_prime_factorization_existsprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity))))))) + ge_balance_negative_prime_factorization_existsprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_in_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_existsprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_existsprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_existsprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_existsprimesprimenonunitidentity))))))) + ge_balance_positive_prime_factorization_existsprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_factorization_existsprimesprime gr_second_factor_prime_factorization_existsprimesprime gr_product_prime_factorization_existsprimesprime. (exists ge_first_rp_prime_factorization_existsprimesprimeproduct ge_first_rn_prime_factorization_existsprimesprimeproduct ge_first_ip_prime_factorization_existsprimesprimeproduct ge_first_in_prime_factorization_existsprimesprimeproduct ge_second_rp_prime_factorization_existsprimesprimeproduct ge_second_rn_prime_factorization_existsprimesprimeproduct ge_second_ip_prime_factorization_existsprimesprimeproduct ge_second_in_prime_factorization_existsprimesprimeproduct. ((exists ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst. (((gr_first_factor_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimeproductfirstreal ge_balance_negative_prime_factorization_existsprimesprimeproductfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimeproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimeproduct) + ge_balance_negative_prime_factorization_existsprimesprimeproductfirstreal = (ge_first_rn_prime_factorization_existsprimesprimeproduct) + ge_balance_positive_prime_factorization_existsprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimeproductfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimeproduct) + ge_balance_negative_prime_factorization_existsprimesprimeproductfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimeproduct) + ge_balance_positive_prime_factorization_existsprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond. (((gr_second_factor_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimeproductsecondreal ge_balance_negative_prime_factorization_existsprimesprimeproductsecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductsecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimeproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductsecondreal) = S ge_signed_half_prime_factorization_existsprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimeproduct) + ge_balance_negative_prime_factorization_existsprimesprimeproductsecondreal = (ge_second_rn_prime_factorization_existsprimesprimeproduct) + ge_balance_positive_prime_factorization_existsprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimeproductsecondimaginary ge_balance_negative_prime_factorization_existsprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductsecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimeproduct) + ge_balance_negative_prime_factorization_existsprimesprimeproductsecondimaginary = (ge_second_in_prime_factorization_existsprimesprimeproduct) + ge_balance_positive_prime_factorization_existsprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput. (((gr_product_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimeproductoutputreal ge_balance_negative_prime_factorization_existsprimesprimeproductoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimeproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimeproduct) * (ge_second_rp_prime_factorization_existsprimesprimeproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimeproduct) * (ge_second_rn_prime_factorization_existsprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimeproduct) * (ge_second_in_prime_factorization_existsprimesprimeproduct))) + (((ge_first_in_prime_factorization_existsprimesprimeproduct) * (ge_second_ip_prime_factorization_existsprimesprimeproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimeproductoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimeproduct) * (ge_second_rn_prime_factorization_existsprimesprimeproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimeproduct) * (ge_second_rp_prime_factorization_existsprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimeproduct) * (ge_second_ip_prime_factorization_existsprimesprimeproduct))) + (((ge_first_in_prime_factorization_existsprimesprimeproduct) * (ge_second_in_prime_factorization_existsprimesprimeproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimeproductoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimeproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimeproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimeproductoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimeproduct) * (ge_second_ip_prime_factorization_existsprimesprimeproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimeproduct) * (ge_second_in_prime_factorization_existsprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimeproduct) * (ge_second_rp_prime_factorization_existsprimesprimeproduct))) + (((ge_first_in_prime_factorization_existsprimesprimeproduct) * (ge_second_rn_prime_factorization_existsprimesprimeproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimeproductoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimeproduct) * (ge_second_in_prime_factorization_existsprimesprimeproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimeproduct) * (ge_second_ip_prime_factorization_existsprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimeproduct) * (ge_second_rn_prime_factorization_existsprimesprimeproduct))) + (((ge_first_in_prime_factorization_existsprimesprimeproduct) * (ge_second_rp_prime_factorization_existsprimesprimeproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_prime_factorization_existsprimesprimedivisor. (exists ge_first_rp_prime_factorization_existsprimesprimedivisorproduct ge_first_rn_prime_factorization_existsprimesprimedivisorproduct ge_first_ip_prime_factorization_existsprimesprimedivisorproduct ge_first_in_prime_factorization_existsprimesprimedivisorproduct ge_second_rp_prime_factorization_existsprimesprimedivisorproduct ge_second_rn_prime_factorization_existsprimesprimedivisorproduct ge_second_ip_prime_factorization_existsprimesprimedivisorproduct ge_second_in_prime_factorization_existsprimesprimedivisorproduct. ((exists ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstreal ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstreal = (ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond. (((gr_quotient_prime_factorization_existsprimesprimedivisor) = ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondreal ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondreal) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondreal = (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondimaginary ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductsecondimaginary = (ge_second_in_prime_factorization_existsprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput. (((gr_product_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputreal ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimedivisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_in_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimedivisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_in_prime_factorization_existsprimesprimedivisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimedivisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_in_prime_factorization_existsprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_in_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimedivisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_prime_factorization_existsprimesprimefirst_divisor. (exists ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstreal ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstreal = (ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond. (((gr_quotient_prime_factorization_existsprimesprimefirst_divisor) = ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondreal ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondreal = (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput. (((gr_first_factor_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputreal ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimefirst_divisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_prime_factorization_existsprimesprimesecond_divisor. (exists ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_prime_factorization_existsprimes) = ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstreal ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstreal = (ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond. (((gr_quotient_prime_factorization_existsprimesprimesecond_divisor) = ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondreal ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondreal = (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput. (((gr_second_factor_prime_factorization_existsprimesprime) = ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputreal ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct))))))) + ge_balance_negative_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_existsprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_existsprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_existsprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_existsprimesprimesecond_divisorproduct))))))) + ge_balance_positive_prime_factorization_existsprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_prime_factorization_exists. ((exists gr_product_trace_prime_factorization_existstrace gr_product_scale_prime_factorization_existstrace. ((((exists ff_h_gprod_prime_factorization_existstracestart. ff_h_gprod_prime_factorization_existstracestart + S (6) = S ((S (0)) * gr_product_scale_prime_factorization_existstrace)) /\ exists ff_q_gprod_prime_factorization_existstracestart. gr_product_trace_prime_factorization_existstrace = ff_q_gprod_prime_factorization_existstracestart * S ((S (0)) * gr_product_scale_prime_factorization_existstrace) + (6))) /\ ((((exists ff_h_gprod_prime_factorization_existstraceend. ff_h_gprod_prime_factorization_existstraceend + S (gr_prime_factor_product_prime_factorization_exists) = S ((S (l)) * gr_product_scale_prime_factorization_existstrace)) /\ exists ff_q_gprod_prime_factorization_existstraceend. gr_product_trace_prime_factorization_existstrace = ff_q_gprod_prime_factorization_existstraceend * S ((S (l)) * gr_product_scale_prime_factorization_existstrace) + (gr_prime_factor_product_prime_factorization_exists))) /\ (forall gr_product_index_prime_factorization_existstracesteps. (exists ge_gap_prime_factorization_existstracestepsindex_bound. ge_gap_prime_factorization_existstracestepsindex_bound + S (gr_product_index_prime_factorization_existstracesteps) = (l)) -> exists gr_product_factor_prime_factorization_existstracesteps gr_product_before_prime_factorization_existstracesteps gr_product_after_prime_factorization_existstracesteps. ((((exists ff_h_gprod_prime_factorization_existstracestepsfactor. ff_h_gprod_prime_factorization_existstracestepsfactor + S (gr_product_factor_prime_factorization_existstracesteps) = S ((S (gr_product_index_prime_factorization_existstracesteps)) * c)) /\ exists ff_q_gprod_prime_factorization_existstracestepsfactor. b = ff_q_gprod_prime_factorization_existstracestepsfactor * S ((S (gr_product_index_prime_factorization_existstracesteps)) * c) + (gr_product_factor_prime_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_prime_factorization_existstracestepsbefore. ff_h_gprod_prime_factorization_existstracestepsbefore + S (gr_product_before_prime_factorization_existstracesteps) = S ((S (gr_product_index_prime_factorization_existstracesteps)) * gr_product_scale_prime_factorization_existstrace)) /\ exists ff_q_gprod_prime_factorization_existstracestepsbefore. gr_product_trace_prime_factorization_existstrace = ff_q_gprod_prime_factorization_existstracestepsbefore * S ((S (gr_product_index_prime_factorization_existstracesteps)) * gr_product_scale_prime_factorization_existstrace) + (gr_product_before_prime_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_prime_factorization_existstracestepsafter. ff_h_gprod_prime_factorization_existstracestepsafter + S (gr_product_after_prime_factorization_existstracesteps) = S ((S (S (gr_product_index_prime_factorization_existstracesteps))) * gr_product_scale_prime_factorization_existstrace)) /\ exists ff_q_gprod_prime_factorization_existstracestepsafter. gr_product_trace_prime_factorization_existstrace = ff_q_gprod_prime_factorization_existstracestepsafter * S ((S (S (gr_product_index_prime_factorization_existstracesteps))) * gr_product_scale_prime_factorization_existstrace) + (gr_product_after_prime_factorization_existstracesteps))) /\ (exists ge_first_rp_prime_factorization_existstracestepsmultiply ge_first_rn_prime_factorization_existstracestepsmultiply ge_first_ip_prime_factorization_existstracestepsmultiply ge_first_in_prime_factorization_existstracestepsmultiply ge_second_rp_prime_factorization_existstracestepsmultiply ge_second_rn_prime_factorization_existstracestepsmultiply ge_second_ip_prime_factorization_existstracestepsmultiply ge_second_in_prime_factorization_existstracestepsmultiply. ((exists ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst. (((gr_product_before_prime_factorization_existstracesteps) = ((ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst)) * S ((ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstreal ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstreal. (((((ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstreal) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_prime_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstreal) = S ge_signed_half_prime_factorization_existstracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existstracestepsmultiply) + ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstreal = (ge_first_rn_prime_factorization_existstracestepsmultiply) + ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstimaginary ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstimaginary) = S ge_signed_half_prime_factorization_existstracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existstracestepsmultiply) + ge_balance_negative_prime_factorization_existstracestepsmultiplyfirstimaginary = (ge_first_in_prime_factorization_existstracestepsmultiply) + ge_balance_positive_prime_factorization_existstracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond. (((gr_product_factor_prime_factorization_existstracesteps) = ((ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond)) * S ((ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond)) + ((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond))) /\ ((exists ge_balance_positive_prime_factorization_existstracestepsmultiplysecondreal ge_balance_negative_prime_factorization_existstracestepsmultiplysecondreal. (((((ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplysecondreal) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplysecondrealdecode. (((ge_representation_real_code_prime_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplysecondreal) = S ge_signed_half_prime_factorization_existstracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existstracestepsmultiply) + ge_balance_negative_prime_factorization_existstracestepsmultiplysecondreal = (ge_second_rn_prime_factorization_existstracestepsmultiply) + ge_balance_positive_prime_factorization_existstracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_prime_factorization_existstracestepsmultiplysecondimaginary ge_balance_negative_prime_factorization_existstracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplysecondimaginary) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplysecondimaginary) = S ge_signed_half_prime_factorization_existstracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existstracestepsmultiply) + ge_balance_negative_prime_factorization_existstracestepsmultiplysecondimaginary = (ge_second_in_prime_factorization_existstracestepsmultiply) + ge_balance_positive_prime_factorization_existstracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput. (((gr_product_after_prime_factorization_existstracesteps) = ((ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput)) * S ((ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputreal ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputreal. (((((ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputreal) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_prime_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputreal) = S ge_signed_half_prime_factorization_existstracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existstracestepsmultiply) * (ge_second_rp_prime_factorization_existstracestepsmultiply))) + (((ge_first_rn_prime_factorization_existstracestepsmultiply) * (ge_second_rn_prime_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_existstracestepsmultiply) * (ge_second_in_prime_factorization_existstracestepsmultiply))) + (((ge_first_in_prime_factorization_existstracestepsmultiply) * (ge_second_ip_prime_factorization_existstracestepsmultiply))))))) + ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputreal = (((((((ge_first_rp_prime_factorization_existstracestepsmultiply) * (ge_second_rn_prime_factorization_existstracestepsmultiply))) + (((ge_first_rn_prime_factorization_existstracestepsmultiply) * (ge_second_rp_prime_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_existstracestepsmultiply) * (ge_second_ip_prime_factorization_existstracestepsmultiply))) + (((ge_first_in_prime_factorization_existstracestepsmultiply) * (ge_second_in_prime_factorization_existstracestepsmultiply))))))) + ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputimaginary ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existstracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_prime_factorization_existstracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputimaginary) = S ge_signed_half_prime_factorization_existstracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existstracestepsmultiply) * (ge_second_ip_prime_factorization_existstracestepsmultiply))) + (((ge_first_rn_prime_factorization_existstracestepsmultiply) * (ge_second_in_prime_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_existstracestepsmultiply) * (ge_second_rp_prime_factorization_existstracestepsmultiply))) + (((ge_first_in_prime_factorization_existstracestepsmultiply) * (ge_second_rn_prime_factorization_existstracestepsmultiply))))))) + ge_balance_negative_prime_factorization_existstracestepsmultiplyoutputimaginary = (((((((ge_first_rp_prime_factorization_existstracestepsmultiply) * (ge_second_in_prime_factorization_existstracestepsmultiply))) + (((ge_first_rn_prime_factorization_existstracestepsmultiply) * (ge_second_ip_prime_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_existstracestepsmultiply) * (ge_second_rn_prime_factorization_existstracestepsmultiply))) + (((ge_first_in_prime_factorization_existstracestepsmultiply) * (ge_second_rp_prime_factorization_existstracestepsmultiply))))))) + ge_balance_positive_prime_factorization_existstracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_prime_factorization_existsreconstruct ge_first_rn_prime_factorization_existsreconstruct ge_first_ip_prime_factorization_existsreconstruct ge_first_in_prime_factorization_existsreconstruct ge_second_rp_prime_factorization_existsreconstruct ge_second_rn_prime_factorization_existsreconstruct ge_second_ip_prime_factorization_existsreconstruct ge_second_in_prime_factorization_existsreconstruct. ((exists ge_representation_real_code_prime_factorization_existsreconstructfirst ge_representation_imaginary_code_prime_factorization_existsreconstructfirst. (((u) = ((ge_representation_real_code_prime_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_existsreconstructfirst)) * S ((ge_representation_real_code_prime_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_existsreconstructfirst)) + ((ge_representation_imaginary_code_prime_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_existsreconstructfirst))) /\ ((exists ge_balance_positive_prime_factorization_existsreconstructfirstreal ge_balance_negative_prime_factorization_existsreconstructfirstreal. (((((ge_representation_real_code_prime_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_prime_factorization_existsreconstructfirstreal) /\ (ge_balance_negative_prime_factorization_existsreconstructfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructfirstrealdecode. (((ge_representation_real_code_prime_factorization_existsreconstructfirst) = 2 * ge_signed_half_prime_factorization_existsreconstructfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructfirstreal) = S ge_signed_half_prime_factorization_existsreconstructfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_existsreconstruct) + ge_balance_negative_prime_factorization_existsreconstructfirstreal = (ge_first_rn_prime_factorization_existsreconstruct) + ge_balance_positive_prime_factorization_existsreconstructfirstreal))) /\ (exists ge_balance_positive_prime_factorization_existsreconstructfirstimaginary ge_balance_negative_prime_factorization_existsreconstructfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_prime_factorization_existsreconstructfirstimaginary) /\ (ge_balance_negative_prime_factorization_existsreconstructfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsreconstructfirst) = 2 * ge_signed_half_prime_factorization_existsreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructfirstimaginary) = S ge_signed_half_prime_factorization_existsreconstructfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_existsreconstruct) + ge_balance_negative_prime_factorization_existsreconstructfirstimaginary = (ge_first_in_prime_factorization_existsreconstruct) + ge_balance_positive_prime_factorization_existsreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_existsreconstructsecond ge_representation_imaginary_code_prime_factorization_existsreconstructsecond. (((gr_prime_factor_product_prime_factorization_exists) = ((ge_representation_real_code_prime_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_existsreconstructsecond)) * S ((ge_representation_real_code_prime_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_existsreconstructsecond)) + ((ge_representation_imaginary_code_prime_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_existsreconstructsecond))) /\ ((exists ge_balance_positive_prime_factorization_existsreconstructsecondreal ge_balance_negative_prime_factorization_existsreconstructsecondreal. (((((ge_representation_real_code_prime_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_prime_factorization_existsreconstructsecondreal) /\ (ge_balance_negative_prime_factorization_existsreconstructsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructsecondrealdecode. (((ge_representation_real_code_prime_factorization_existsreconstructsecond) = 2 * ge_signed_half_prime_factorization_existsreconstructsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructsecondreal) = S ge_signed_half_prime_factorization_existsreconstructsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_existsreconstruct) + ge_balance_negative_prime_factorization_existsreconstructsecondreal = (ge_second_rn_prime_factorization_existsreconstruct) + ge_balance_positive_prime_factorization_existsreconstructsecondreal))) /\ (exists ge_balance_positive_prime_factorization_existsreconstructsecondimaginary ge_balance_negative_prime_factorization_existsreconstructsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_prime_factorization_existsreconstructsecondimaginary) /\ (ge_balance_negative_prime_factorization_existsreconstructsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsreconstructsecond) = 2 * ge_signed_half_prime_factorization_existsreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructsecondimaginary) = S ge_signed_half_prime_factorization_existsreconstructsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_existsreconstruct) + ge_balance_negative_prime_factorization_existsreconstructsecondimaginary = (ge_second_in_prime_factorization_existsreconstruct) + ge_balance_positive_prime_factorization_existsreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_existsreconstructoutput ge_representation_imaginary_code_prime_factorization_existsreconstructoutput. (((z) = ((ge_representation_real_code_prime_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_existsreconstructoutput)) * S ((ge_representation_real_code_prime_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_existsreconstructoutput)) + ((ge_representation_imaginary_code_prime_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_existsreconstructoutput))) /\ ((exists ge_balance_positive_prime_factorization_existsreconstructoutputreal ge_balance_negative_prime_factorization_existsreconstructoutputreal. (((((ge_representation_real_code_prime_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_prime_factorization_existsreconstructoutputreal) /\ (ge_balance_negative_prime_factorization_existsreconstructoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructoutputrealdecode. (((ge_representation_real_code_prime_factorization_existsreconstructoutput) = 2 * ge_signed_half_prime_factorization_existsreconstructoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructoutputreal) = S ge_signed_half_prime_factorization_existsreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_existsreconstruct) * (ge_second_rp_prime_factorization_existsreconstruct))) + (((ge_first_rn_prime_factorization_existsreconstruct) * (ge_second_rn_prime_factorization_existsreconstruct))))) + (((((ge_first_ip_prime_factorization_existsreconstruct) * (ge_second_in_prime_factorization_existsreconstruct))) + (((ge_first_in_prime_factorization_existsreconstruct) * (ge_second_ip_prime_factorization_existsreconstruct))))))) + ge_balance_negative_prime_factorization_existsreconstructoutputreal = (((((((ge_first_rp_prime_factorization_existsreconstruct) * (ge_second_rn_prime_factorization_existsreconstruct))) + (((ge_first_rn_prime_factorization_existsreconstruct) * (ge_second_rp_prime_factorization_existsreconstruct))))) + (((((ge_first_ip_prime_factorization_existsreconstruct) * (ge_second_ip_prime_factorization_existsreconstruct))) + (((ge_first_in_prime_factorization_existsreconstruct) * (ge_second_in_prime_factorization_existsreconstruct))))))) + ge_balance_positive_prime_factorization_existsreconstructoutputreal))) /\ (exists ge_balance_positive_prime_factorization_existsreconstructoutputimaginary ge_balance_negative_prime_factorization_existsreconstructoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_prime_factorization_existsreconstructoutputimaginary) /\ (ge_balance_negative_prime_factorization_existsreconstructoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_existsreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_existsreconstructoutput) = 2 * ge_signed_half_prime_factorization_existsreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_existsreconstructoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_existsreconstructoutputimaginary) = S ge_signed_half_prime_factorization_existsreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_existsreconstruct) * (ge_second_ip_prime_factorization_existsreconstruct))) + (((ge_first_rn_prime_factorization_existsreconstruct) * (ge_second_in_prime_factorization_existsreconstruct))))) + (((((ge_first_ip_prime_factorization_existsreconstruct) * (ge_second_rp_prime_factorization_existsreconstruct))) + (((ge_first_in_prime_factorization_existsreconstruct) * (ge_second_rn_prime_factorization_existsreconstruct))))))) + ge_balance_negative_prime_factorization_existsreconstructoutputimaginary = (((((((ge_first_rp_prime_factorization_existsreconstruct) * (ge_second_in_prime_factorization_existsreconstruct))) + (((ge_first_rn_prime_factorization_existsreconstruct) * (ge_second_ip_prime_factorization_existsreconstruct))))) + (((((ge_first_ip_prime_factorization_existsreconstruct) * (ge_second_rn_prime_factorization_existsreconstruct))) + (((ge_first_in_prime_factorization_existsreconstruct) * (ge_second_rp_prime_factorization_existsreconstruct))))))) + ge_balance_positive_prime_factorization_existsreconstructoutputimaginary))))))))))))))