gaussian_prime_factorization_is_irreducible

Exact expanded first-order arithmetic statement

forall z u b c l. (((exists gr_inverse_prime_factorization_givenunit. (exists ge_first_rp_prime_factorization_givenunitidentity ge_first_rn_prime_factorization_givenunitidentity ge_first_ip_prime_factorization_givenunitidentity ge_first_in_prime_factorization_givenunitidentity ge_second_rp_prime_factorization_givenunitidentity ge_second_rn_prime_factorization_givenunitidentity ge_second_ip_prime_factorization_givenunitidentity ge_second_in_prime_factorization_givenunitidentity. ((exists ge_representation_real_code_prime_factorization_givenunitidentityfirst ge_representation_imaginary_code_prime_factorization_givenunitidentityfirst. (((u) = ((ge_representation_real_code_prime_factorization_givenunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_givenunitidentityfirst)) * S ((ge_representation_real_code_prime_factorization_givenunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_givenunitidentityfirst)) + ((ge_representation_imaginary_code_prime_factorization_givenunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_givenunitidentityfirst))) /\ ((exists ge_balance_positive_prime_factorization_givenunitidentityfirstreal ge_balance_negative_prime_factorization_givenunitidentityfirstreal. (((((ge_representation_real_code_prime_factorization_givenunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_givenunitidentityfirstreal) /\ (ge_balance_negative_prime_factorization_givenunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_givenunitidentityfirstrealdecode. (((ge_representation_real_code_prime_factorization_givenunitidentityfirst) = 2 * ge_signed_half_prime_factorization_givenunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_givenunitidentityfirstreal) = S ge_signed_half_prime_factorization_givenunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_givenunitidentity) + ge_balance_negative_prime_factorization_givenunitidentityfirstreal = (ge_first_rn_prime_factorization_givenunitidentity) + ge_balance_positive_prime_factorization_givenunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_factorization_givenunitidentityfirstimaginary ge_balance_negative_prime_factorization_givenunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_givenunitidentityfirstimaginary) /\ (ge_balance_negative_prime_factorization_givenunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenunitidentityfirst) = 2 * ge_signed_half_prime_factorization_givenunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenunitidentityfirstimaginary) = S ge_signed_half_prime_factorization_givenunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_givenunitidentity) + ge_balance_negative_prime_factorization_givenunitidentityfirstimaginary = (ge_first_in_prime_factorization_givenunitidentity) + ge_balance_positive_prime_factorization_givenunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_givenunitidentitysecond ge_representation_imaginary_code_prime_factorization_givenunitidentitysecond. (((gr_inverse_prime_factorization_givenunit) = ((ge_representation_real_code_prime_factorization_givenunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_givenunitidentitysecond)) * S ((ge_representation_real_code_prime_factorization_givenunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_givenunitidentitysecond)) + ((ge_representation_imaginary_code_prime_factorization_givenunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_givenunitidentitysecond))) /\ ((exists ge_balance_positive_prime_factorization_givenunitidentitysecondreal ge_balance_negative_prime_factorization_givenunitidentitysecondreal. (((((ge_representation_real_code_prime_factorization_givenunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_givenunitidentitysecondreal) /\ (ge_balance_negative_prime_factorization_givenunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_givenunitidentitysecondrealdecode. (((ge_representation_real_code_prime_factorization_givenunitidentitysecond) = 2 * ge_signed_half_prime_factorization_givenunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_givenunitidentitysecondreal) = S ge_signed_half_prime_factorization_givenunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_givenunitidentity) + ge_balance_negative_prime_factorization_givenunitidentitysecondreal = (ge_second_rn_prime_factorization_givenunitidentity) + ge_balance_positive_prime_factorization_givenunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_factorization_givenunitidentitysecondimaginary ge_balance_negative_prime_factorization_givenunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_givenunitidentitysecondimaginary) /\ (ge_balance_negative_prime_factorization_givenunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenunitidentitysecond) = 2 * ge_signed_half_prime_factorization_givenunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenunitidentitysecondimaginary) = S ge_signed_half_prime_factorization_givenunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_givenunitidentity) + ge_balance_negative_prime_factorization_givenunitidentitysecondimaginary = (ge_second_in_prime_factorization_givenunitidentity) + ge_balance_positive_prime_factorization_givenunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_givenunitidentityoutput ge_representation_imaginary_code_prime_factorization_givenunitidentityoutput. (((6) = ((ge_representation_real_code_prime_factorization_givenunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_givenunitidentityoutput)) * S ((ge_representation_real_code_prime_factorization_givenunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_givenunitidentityoutput)) + ((ge_representation_imaginary_code_prime_factorization_givenunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_givenunitidentityoutput))) /\ ((exists ge_balance_positive_prime_factorization_givenunitidentityoutputreal ge_balance_negative_prime_factorization_givenunitidentityoutputreal. (((((ge_representation_real_code_prime_factorization_givenunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_givenunitidentityoutputreal) /\ (ge_balance_negative_prime_factorization_givenunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_givenunitidentityoutputrealdecode. (((ge_representation_real_code_prime_factorization_givenunitidentityoutput) = 2 * ge_signed_half_prime_factorization_givenunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_givenunitidentityoutputreal) = S ge_signed_half_prime_factorization_givenunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_givenunitidentity) * (ge_second_rp_prime_factorization_givenunitidentity))) + (((ge_first_rn_prime_factorization_givenunitidentity) * (ge_second_rn_prime_factorization_givenunitidentity))))) + (((((ge_first_ip_prime_factorization_givenunitidentity) * (ge_second_in_prime_factorization_givenunitidentity))) + (((ge_first_in_prime_factorization_givenunitidentity) * (ge_second_ip_prime_factorization_givenunitidentity))))))) + ge_balance_negative_prime_factorization_givenunitidentityoutputreal = (((((((ge_first_rp_prime_factorization_givenunitidentity) * (ge_second_rn_prime_factorization_givenunitidentity))) + (((ge_first_rn_prime_factorization_givenunitidentity) * (ge_second_rp_prime_factorization_givenunitidentity))))) + (((((ge_first_ip_prime_factorization_givenunitidentity) * (ge_second_ip_prime_factorization_givenunitidentity))) + (((ge_first_in_prime_factorization_givenunitidentity) * (ge_second_in_prime_factorization_givenunitidentity))))))) + ge_balance_positive_prime_factorization_givenunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_factorization_givenunitidentityoutputimaginary ge_balance_negative_prime_factorization_givenunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_givenunitidentityoutputimaginary) /\ (ge_balance_negative_prime_factorization_givenunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenunitidentityoutput) = 2 * ge_signed_half_prime_factorization_givenunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenunitidentityoutputimaginary) = S ge_signed_half_prime_factorization_givenunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_givenunitidentity) * (ge_second_ip_prime_factorization_givenunitidentity))) + (((ge_first_rn_prime_factorization_givenunitidentity) * (ge_second_in_prime_factorization_givenunitidentity))))) + (((((ge_first_ip_prime_factorization_givenunitidentity) * (ge_second_rp_prime_factorization_givenunitidentity))) + (((ge_first_in_prime_factorization_givenunitidentity) * (ge_second_rn_prime_factorization_givenunitidentity))))))) + ge_balance_negative_prime_factorization_givenunitidentityoutputimaginary = (((((((ge_first_rp_prime_factorization_givenunitidentity) * (ge_second_in_prime_factorization_givenunitidentity))) + (((ge_first_rn_prime_factorization_givenunitidentity) * (ge_second_ip_prime_factorization_givenunitidentity))))) + (((((ge_first_ip_prime_factorization_givenunitidentity) * (ge_second_rn_prime_factorization_givenunitidentity))) + (((ge_first_in_prime_factorization_givenunitidentity) * (ge_second_rp_prime_factorization_givenunitidentity))))))) + ge_balance_positive_prime_factorization_givenunitidentityoutputimaginary)))))))))) /\ ((forall gr_prime_factor_index_prime_factorization_givenprimes gr_prime_factor_value_prime_factorization_givenprimes. (exists ge_gap_prime_factorization_givenprimesindex. ge_gap_prime_factorization_givenprimesindex + S (gr_prime_factor_index_prime_factorization_givenprimes) = (l)) -> (((exists ff_h_gprod_prime_factorization_givenprimesentry. ff_h_gprod_prime_factorization_givenprimesentry + S (gr_prime_factor_value_prime_factorization_givenprimes) = S ((S (gr_prime_factor_index_prime_factorization_givenprimes)) * c)) /\ exists ff_q_gprod_prime_factorization_givenprimesentry. b = ff_q_gprod_prime_factorization_givenprimesentry * S ((S (gr_prime_factor_index_prime_factorization_givenprimes)) * c) + (gr_prime_factor_value_prime_factorization_givenprimes))) -> (((exists ge_real_positive_prime_factorization_givenprimesprimecarrier ge_real_negative_prime_factorization_givenprimesprimecarrier ge_imaginary_positive_prime_factorization_givenprimesprimecarrier ge_imaginary_negative_prime_factorization_givenprimesprimecarrier. (exists ge_real_code_prime_factorization_givenprimesprimecarrierdecode ge_imaginary_code_prime_factorization_givenprimesprimecarrierdecode. (((gr_prime_factor_value_prime_factorization_givenprimes) = ((ge_real_code_prime_factorization_givenprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_givenprimesprimecarrierdecode)) * S ((ge_real_code_prime_factorization_givenprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_givenprimesprimecarrierdecode)) + ((ge_imaginary_code_prime_factorization_givenprimesprimecarrierdecode) + (ge_imaginary_code_prime_factorization_givenprimesprimecarrierdecode))) /\ (((((ge_real_code_prime_factorization_givenprimesprimecarrierdecode) = 2 * (ge_real_positive_prime_factorization_givenprimesprimecarrier) /\ (ge_real_negative_prime_factorization_givenprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_prime_factorization_givenprimesprimecarrierdecode_real. (((ge_real_code_prime_factorization_givenprimesprimecarrierdecode) = 2 * ge_signed_half_ge_prime_factorization_givenprimesprimecarrierdecode_real + 1 /\ (ge_real_positive_prime_factorization_givenprimesprimecarrier) = 0) /\ (ge_real_negative_prime_factorization_givenprimesprimecarrier) = S ge_signed_half_ge_prime_factorization_givenprimesprimecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_factorization_givenprimesprimecarrierdecode) = 2 * (ge_imaginary_positive_prime_factorization_givenprimesprimecarrier) /\ (ge_imaginary_negative_prime_factorization_givenprimesprimecarrier) = 0) \/ exists ge_signed_half_ge_prime_factorization_givenprimesprimecarrierdecode_imaginary. (((ge_imaginary_code_prime_factorization_givenprimesprimecarrierdecode) = 2 * ge_signed_half_ge_prime_factorization_givenprimesprimecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_factorization_givenprimesprimecarrier) = 0) /\ (ge_imaginary_negative_prime_factorization_givenprimesprimecarrier) = S ge_signed_half_ge_prime_factorization_givenprimesprimecarrierdecode_imaginary))))))) /\ ((~((gr_prime_factor_value_prime_factorization_givenprimes)=0)) /\ ((~(exists gr_inverse_prime_factorization_givenprimesprimenonunit. (exists ge_first_rp_prime_factorization_givenprimesprimenonunitidentity ge_first_rn_prime_factorization_givenprimesprimenonunitidentity ge_first_ip_prime_factorization_givenprimesprimenonunitidentity ge_first_in_prime_factorization_givenprimesprimenonunitidentity ge_second_rp_prime_factorization_givenprimesprimenonunitidentity ge_second_rn_prime_factorization_givenprimesprimenonunitidentity ge_second_ip_prime_factorization_givenprimesprimenonunitidentity ge_second_in_prime_factorization_givenprimesprimenonunitidentity. ((exists ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityfirst ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityfirst. (((gr_prime_factor_value_prime_factorization_givenprimes) = ((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityfirst)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityfirstreal ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityfirstreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityfirstreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityfirstreal) = S ge_signed_half_prime_factorization_givenprimesprimenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_givenprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityfirstreal = (ge_first_rn_prime_factorization_givenprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityfirstimaginary ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityfirstimaginary) = S ge_signed_half_prime_factorization_givenprimesprimenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_givenprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityfirstimaginary = (ge_first_in_prime_factorization_givenprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentitysecond ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentitysecond. (((gr_inverse_prime_factorization_givenprimesprimenonunit) = ((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentitysecond)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentitysecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimenonunitidentitysecondreal ge_balance_negative_prime_factorization_givenprimesprimenonunitidentitysecondreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentitysecondreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentitysecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentitysecondreal) = S ge_signed_half_prime_factorization_givenprimesprimenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_givenprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_givenprimesprimenonunitidentitysecondreal = (ge_second_rn_prime_factorization_givenprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_givenprimesprimenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimenonunitidentitysecondimaginary ge_balance_negative_prime_factorization_givenprimesprimenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentitysecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentitysecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentitysecondimaginary) = S ge_signed_half_prime_factorization_givenprimesprimenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_givenprimesprimenonunitidentity) + ge_balance_negative_prime_factorization_givenprimesprimenonunitidentitysecondimaginary = (ge_second_in_prime_factorization_givenprimesprimenonunitidentity) + ge_balance_positive_prime_factorization_givenprimesprimenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityoutput ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityoutput)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityoutputreal ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityoutputreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityoutputreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimenonunitidentityoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityoutputreal) = S ge_signed_half_prime_factorization_givenprimesprimenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_givenprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_givenprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_in_prime_factorization_givenprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_givenprimesprimenonunitidentity))))))) + ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityoutputreal = (((((((ge_first_rp_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_givenprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_givenprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_givenprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_in_prime_factorization_givenprimesprimenonunitidentity))))))) + ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityoutputimaginary ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimenonunitidentityoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityoutputimaginary) = S ge_signed_half_prime_factorization_givenprimesprimenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_givenprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_in_prime_factorization_givenprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_givenprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_givenprimesprimenonunitidentity))))))) + ge_balance_negative_prime_factorization_givenprimesprimenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_in_prime_factorization_givenprimesprimenonunitidentity))) + (((ge_first_rn_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_ip_prime_factorization_givenprimesprimenonunitidentity))))) + (((((ge_first_ip_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_rn_prime_factorization_givenprimesprimenonunitidentity))) + (((ge_first_in_prime_factorization_givenprimesprimenonunitidentity) * (ge_second_rp_prime_factorization_givenprimesprimenonunitidentity))))))) + ge_balance_positive_prime_factorization_givenprimesprimenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_factorization_givenprimesprime gr_second_factor_prime_factorization_givenprimesprime gr_product_prime_factorization_givenprimesprime. (exists ge_first_rp_prime_factorization_givenprimesprimeproduct ge_first_rn_prime_factorization_givenprimesprimeproduct ge_first_ip_prime_factorization_givenprimesprimeproduct ge_first_in_prime_factorization_givenprimesprimeproduct ge_second_rp_prime_factorization_givenprimesprimeproduct ge_second_rn_prime_factorization_givenprimesprimeproduct ge_second_ip_prime_factorization_givenprimesprimeproduct ge_second_in_prime_factorization_givenprimesprimeproduct. ((exists ge_representation_real_code_prime_factorization_givenprimesprimeproductfirst ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductfirst. (((gr_first_factor_prime_factorization_givenprimesprime) = ((ge_representation_real_code_prime_factorization_givenprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductfirst)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimeproductfirstreal ge_balance_negative_prime_factorization_givenprimesprimeproductfirstreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimeproductfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimeproductfirstreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimeproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimeproductfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimeproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimeproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductfirstreal) = S ge_signed_half_prime_factorization_givenprimesprimeproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_givenprimesprimeproduct) + ge_balance_negative_prime_factorization_givenprimesprimeproductfirstreal = (ge_first_rn_prime_factorization_givenprimesprimeproduct) + ge_balance_positive_prime_factorization_givenprimesprimeproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimeproductfirstimaginary ge_balance_negative_prime_factorization_givenprimesprimeproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimeproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimeproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimeproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimeproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductfirstimaginary) = S ge_signed_half_prime_factorization_givenprimesprimeproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_givenprimesprimeproduct) + ge_balance_negative_prime_factorization_givenprimesprimeproductfirstimaginary = (ge_first_in_prime_factorization_givenprimesprimeproduct) + ge_balance_positive_prime_factorization_givenprimesprimeproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_givenprimesprimeproductsecond ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductsecond. (((gr_second_factor_prime_factorization_givenprimesprime) = ((ge_representation_real_code_prime_factorization_givenprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductsecond)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimeproductsecondreal ge_balance_negative_prime_factorization_givenprimesprimeproductsecondreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimeproductsecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimeproductsecondreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimeproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimeproductsecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimeproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimeproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductsecondreal) = S ge_signed_half_prime_factorization_givenprimesprimeproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_givenprimesprimeproduct) + ge_balance_negative_prime_factorization_givenprimesprimeproductsecondreal = (ge_second_rn_prime_factorization_givenprimesprimeproduct) + ge_balance_positive_prime_factorization_givenprimesprimeproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimeproductsecondimaginary ge_balance_negative_prime_factorization_givenprimesprimeproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductsecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimeproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimeproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductsecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimeproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimeproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductsecondimaginary) = S ge_signed_half_prime_factorization_givenprimesprimeproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_givenprimesprimeproduct) + ge_balance_negative_prime_factorization_givenprimesprimeproductsecondimaginary = (ge_second_in_prime_factorization_givenprimesprimeproduct) + ge_balance_positive_prime_factorization_givenprimesprimeproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_givenprimesprimeproductoutput ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductoutput. (((gr_product_prime_factorization_givenprimesprime) = ((ge_representation_real_code_prime_factorization_givenprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductoutput)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimeproductoutputreal ge_balance_negative_prime_factorization_givenprimesprimeproductoutputreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimeproductoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimeproductoutputreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimeproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimeproductoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimeproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimeproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductoutputreal) = S ge_signed_half_prime_factorization_givenprimesprimeproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimeproduct) * (ge_second_rp_prime_factorization_givenprimesprimeproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimeproduct) * (ge_second_rn_prime_factorization_givenprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimeproduct) * (ge_second_in_prime_factorization_givenprimesprimeproduct))) + (((ge_first_in_prime_factorization_givenprimesprimeproduct) * (ge_second_ip_prime_factorization_givenprimesprimeproduct))))))) + ge_balance_negative_prime_factorization_givenprimesprimeproductoutputreal = (((((((ge_first_rp_prime_factorization_givenprimesprimeproduct) * (ge_second_rn_prime_factorization_givenprimesprimeproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimeproduct) * (ge_second_rp_prime_factorization_givenprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimeproduct) * (ge_second_ip_prime_factorization_givenprimesprimeproduct))) + (((ge_first_in_prime_factorization_givenprimesprimeproduct) * (ge_second_in_prime_factorization_givenprimesprimeproduct))))))) + ge_balance_positive_prime_factorization_givenprimesprimeproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimeproductoutputimaginary ge_balance_negative_prime_factorization_givenprimesprimeproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimeproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimeproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimeproductoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimeproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimeproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimeproductoutputimaginary) = S ge_signed_half_prime_factorization_givenprimesprimeproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimeproduct) * (ge_second_ip_prime_factorization_givenprimesprimeproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimeproduct) * (ge_second_in_prime_factorization_givenprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimeproduct) * (ge_second_rp_prime_factorization_givenprimesprimeproduct))) + (((ge_first_in_prime_factorization_givenprimesprimeproduct) * (ge_second_rn_prime_factorization_givenprimesprimeproduct))))))) + ge_balance_negative_prime_factorization_givenprimesprimeproductoutputimaginary = (((((((ge_first_rp_prime_factorization_givenprimesprimeproduct) * (ge_second_in_prime_factorization_givenprimesprimeproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimeproduct) * (ge_second_ip_prime_factorization_givenprimesprimeproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimeproduct) * (ge_second_rn_prime_factorization_givenprimesprimeproduct))) + (((ge_first_in_prime_factorization_givenprimesprimeproduct) * (ge_second_rp_prime_factorization_givenprimesprimeproduct))))))) + ge_balance_positive_prime_factorization_givenprimesprimeproductoutputimaginary))))))))) -> (exists gr_quotient_prime_factorization_givenprimesprimedivisor. (exists ge_first_rp_prime_factorization_givenprimesprimedivisorproduct ge_first_rn_prime_factorization_givenprimesprimedivisorproduct ge_first_ip_prime_factorization_givenprimesprimedivisorproduct ge_first_in_prime_factorization_givenprimesprimedivisorproduct ge_second_rp_prime_factorization_givenprimesprimedivisorproduct ge_second_rn_prime_factorization_givenprimesprimedivisorproduct ge_second_ip_prime_factorization_givenprimesprimedivisorproduct ge_second_in_prime_factorization_givenprimesprimedivisorproduct. ((exists ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductfirst ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductfirst. (((gr_prime_factor_value_prime_factorization_givenprimes) = ((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimedivisorproductfirstreal ge_balance_negative_prime_factorization_givenprimesprimedivisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimedivisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimedivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductfirstreal) = S ge_signed_half_prime_factorization_givenprimesprimedivisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_givenprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimedivisorproductfirstreal = (ge_first_rn_prime_factorization_givenprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimedivisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimedivisorproductfirstimaginary ge_balance_negative_prime_factorization_givenprimesprimedivisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimedivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimedivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductfirstimaginary) = S ge_signed_half_prime_factorization_givenprimesprimedivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_givenprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimedivisorproductfirstimaginary = (ge_first_in_prime_factorization_givenprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimedivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductsecond ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductsecond. (((gr_quotient_prime_factorization_givenprimesprimedivisor) = ((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimedivisorproductsecondreal ge_balance_negative_prime_factorization_givenprimesprimedivisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimedivisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductsecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimedivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductsecondreal) = S ge_signed_half_prime_factorization_givenprimesprimedivisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_givenprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimedivisorproductsecondreal = (ge_second_rn_prime_factorization_givenprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimedivisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimedivisorproductsecondimaginary ge_balance_negative_prime_factorization_givenprimesprimedivisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimedivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductsecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimedivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductsecondimaginary) = S ge_signed_half_prime_factorization_givenprimesprimedivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_givenprimesprimedivisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimedivisorproductsecondimaginary = (ge_second_in_prime_factorization_givenprimesprimedivisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimedivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductoutput ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductoutput. (((gr_product_prime_factorization_givenprimesprime) = ((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimedivisorproductoutputreal ge_balance_negative_prime_factorization_givenprimesprimedivisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimedivisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimedivisorproductoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimedivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductoutputreal) = S ge_signed_half_prime_factorization_givenprimesprimedivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_in_prime_factorization_givenprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimedivisorproduct))))))) + ge_balance_negative_prime_factorization_givenprimesprimedivisorproductoutputreal = (((((((ge_first_rp_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_in_prime_factorization_givenprimesprimedivisorproduct))))))) + ge_balance_positive_prime_factorization_givenprimesprimedivisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimedivisorproductoutputimaginary ge_balance_negative_prime_factorization_givenprimesprimedivisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimedivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimedivisorproductoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimedivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimedivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimedivisorproductoutputimaginary) = S ge_signed_half_prime_factorization_givenprimesprimedivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_in_prime_factorization_givenprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimedivisorproduct))))))) + ge_balance_negative_prime_factorization_givenprimesprimedivisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_in_prime_factorization_givenprimesprimedivisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimedivisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimedivisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimedivisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimedivisorproduct))))))) + ge_balance_positive_prime_factorization_givenprimesprimedivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_prime_factorization_givenprimesprimefirst_divisor. (exists ge_first_rp_prime_factorization_givenprimesprimefirst_divisorproduct ge_first_rn_prime_factorization_givenprimesprimefirst_divisorproduct ge_first_ip_prime_factorization_givenprimesprimefirst_divisorproduct ge_first_in_prime_factorization_givenprimesprimefirst_divisorproduct ge_second_rp_prime_factorization_givenprimesprimefirst_divisorproduct ge_second_rn_prime_factorization_givenprimesprimefirst_divisorproduct ge_second_ip_prime_factorization_givenprimesprimefirst_divisorproduct ge_second_in_prime_factorization_givenprimesprimefirst_divisorproduct. ((exists ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductfirst ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductfirst. (((gr_prime_factor_value_prime_factorization_givenprimes) = ((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductfirstreal ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductfirstreal) = S ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_givenprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductfirstreal = (ge_first_rn_prime_factorization_givenprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginary ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginary) = S ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_givenprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginary = (ge_first_in_prime_factorization_givenprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductsecond ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductsecond. (((gr_quotient_prime_factorization_givenprimesprimefirst_divisor) = ((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductsecondreal ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductsecondreal) = S ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_givenprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductsecondreal = (ge_second_rn_prime_factorization_givenprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginary ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginary) = S ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_givenprimesprimefirst_divisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginary = (ge_second_in_prime_factorization_givenprimesprimefirst_divisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductoutput ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductoutput. (((gr_first_factor_prime_factorization_givenprimesprime) = ((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductoutputreal ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductoutputreal) = S ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_givenprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimefirst_divisorproduct))))))) + ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductoutputreal = (((((((ge_first_rp_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_givenprimesprimefirst_divisorproduct))))))) + ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginary ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimefirst_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginary) = S ge_signed_half_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_givenprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimefirst_divisorproduct))))))) + ge_balance_negative_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_in_prime_factorization_givenprimesprimefirst_divisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimefirst_divisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimefirst_divisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimefirst_divisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimefirst_divisorproduct))))))) + ge_balance_positive_prime_factorization_givenprimesprimefirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_prime_factorization_givenprimesprimesecond_divisor. (exists ge_first_rp_prime_factorization_givenprimesprimesecond_divisorproduct ge_first_rn_prime_factorization_givenprimesprimesecond_divisorproduct ge_first_ip_prime_factorization_givenprimesprimesecond_divisorproduct ge_first_in_prime_factorization_givenprimesprimesecond_divisorproduct ge_second_rp_prime_factorization_givenprimesprimesecond_divisorproduct ge_second_rn_prime_factorization_givenprimesprimesecond_divisorproduct ge_second_ip_prime_factorization_givenprimesprimesecond_divisorproduct ge_second_in_prime_factorization_givenprimesprimesecond_divisorproduct. ((exists ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductfirst ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductfirst. (((gr_prime_factor_value_prime_factorization_givenprimes) = ((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductfirst)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductfirst) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductfirstreal ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductfirstreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductfirstreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductfirstreal) = S ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_givenprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductfirstreal = (ge_first_rn_prime_factorization_givenprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginary ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductfirst) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductfirst) = 2 * ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginary) = S ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_givenprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginary = (ge_first_in_prime_factorization_givenprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductsecond ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductsecond. (((gr_quotient_prime_factorization_givenprimesprimesecond_divisor) = ((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductsecond)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductsecond) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductsecondreal ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductsecondreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductsecondreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductsecondreal) = S ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_givenprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductsecondreal = (ge_second_rn_prime_factorization_givenprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginary ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductsecond) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductsecond) = 2 * ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginary) = S ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_givenprimesprimesecond_divisorproduct) + ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginary = (ge_second_in_prime_factorization_givenprimesprimesecond_divisorproduct) + ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductoutput ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductoutput. (((gr_second_factor_prime_factorization_givenprimesprime) = ((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductoutput)) * S ((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductoutput) + (ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductoutputreal ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductoutputreal. (((((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductoutputreal) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_factorization_givenprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductoutputreal) = S ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_givenprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimesecond_divisorproduct))))))) + ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductoutputreal = (((((((ge_first_rp_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_givenprimesprimesecond_divisorproduct))))))) + ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginary ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductoutput) = 2 * (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenprimesprimesecond_divisorproductoutput) = 2 * ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginary) = S ge_signed_half_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_givenprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimesecond_divisorproduct))))))) + ge_balance_negative_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginary = (((((((ge_first_rp_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_in_prime_factorization_givenprimesprimesecond_divisorproduct))) + (((ge_first_rn_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_ip_prime_factorization_givenprimesprimesecond_divisorproduct))))) + (((((ge_first_ip_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_rn_prime_factorization_givenprimesprimesecond_divisorproduct))) + (((ge_first_in_prime_factorization_givenprimesprimesecond_divisorproduct) * (ge_second_rp_prime_factorization_givenprimesprimesecond_divisorproduct))))))) + ge_balance_positive_prime_factorization_givenprimesprimesecond_divisorproductoutputimaginary)))))))))))))))) /\ (exists gr_prime_factor_product_prime_factorization_given. ((exists gr_product_trace_prime_factorization_giventrace gr_product_scale_prime_factorization_giventrace. ((((exists ff_h_gprod_prime_factorization_giventracestart. ff_h_gprod_prime_factorization_giventracestart + S (6) = S ((S (0)) * gr_product_scale_prime_factorization_giventrace)) /\ exists ff_q_gprod_prime_factorization_giventracestart. gr_product_trace_prime_factorization_giventrace = ff_q_gprod_prime_factorization_giventracestart * S ((S (0)) * gr_product_scale_prime_factorization_giventrace) + (6))) /\ ((((exists ff_h_gprod_prime_factorization_giventraceend. ff_h_gprod_prime_factorization_giventraceend + S (gr_prime_factor_product_prime_factorization_given) = S ((S (l)) * gr_product_scale_prime_factorization_giventrace)) /\ exists ff_q_gprod_prime_factorization_giventraceend. gr_product_trace_prime_factorization_giventrace = ff_q_gprod_prime_factorization_giventraceend * S ((S (l)) * gr_product_scale_prime_factorization_giventrace) + (gr_prime_factor_product_prime_factorization_given))) /\ (forall gr_product_index_prime_factorization_giventracesteps. (exists ge_gap_prime_factorization_giventracestepsindex_bound. ge_gap_prime_factorization_giventracestepsindex_bound + S (gr_product_index_prime_factorization_giventracesteps) = (l)) -> exists gr_product_factor_prime_factorization_giventracesteps gr_product_before_prime_factorization_giventracesteps gr_product_after_prime_factorization_giventracesteps. ((((exists ff_h_gprod_prime_factorization_giventracestepsfactor. ff_h_gprod_prime_factorization_giventracestepsfactor + S (gr_product_factor_prime_factorization_giventracesteps) = S ((S (gr_product_index_prime_factorization_giventracesteps)) * c)) /\ exists ff_q_gprod_prime_factorization_giventracestepsfactor. b = ff_q_gprod_prime_factorization_giventracestepsfactor * S ((S (gr_product_index_prime_factorization_giventracesteps)) * c) + (gr_product_factor_prime_factorization_giventracesteps))) /\ ((((exists ff_h_gprod_prime_factorization_giventracestepsbefore. ff_h_gprod_prime_factorization_giventracestepsbefore + S (gr_product_before_prime_factorization_giventracesteps) = S ((S (gr_product_index_prime_factorization_giventracesteps)) * gr_product_scale_prime_factorization_giventrace)) /\ exists ff_q_gprod_prime_factorization_giventracestepsbefore. gr_product_trace_prime_factorization_giventrace = ff_q_gprod_prime_factorization_giventracestepsbefore * S ((S (gr_product_index_prime_factorization_giventracesteps)) * gr_product_scale_prime_factorization_giventrace) + (gr_product_before_prime_factorization_giventracesteps))) /\ ((((exists ff_h_gprod_prime_factorization_giventracestepsafter. ff_h_gprod_prime_factorization_giventracestepsafter + S (gr_product_after_prime_factorization_giventracesteps) = S ((S (S (gr_product_index_prime_factorization_giventracesteps))) * gr_product_scale_prime_factorization_giventrace)) /\ exists ff_q_gprod_prime_factorization_giventracestepsafter. gr_product_trace_prime_factorization_giventrace = ff_q_gprod_prime_factorization_giventracestepsafter * S ((S (S (gr_product_index_prime_factorization_giventracesteps))) * gr_product_scale_prime_factorization_giventrace) + (gr_product_after_prime_factorization_giventracesteps))) /\ (exists ge_first_rp_prime_factorization_giventracestepsmultiply ge_first_rn_prime_factorization_giventracestepsmultiply ge_first_ip_prime_factorization_giventracestepsmultiply ge_first_in_prime_factorization_giventracestepsmultiply ge_second_rp_prime_factorization_giventracestepsmultiply ge_second_rn_prime_factorization_giventracestepsmultiply ge_second_ip_prime_factorization_giventracestepsmultiply ge_second_in_prime_factorization_giventracestepsmultiply. ((exists ge_representation_real_code_prime_factorization_giventracestepsmultiplyfirst ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyfirst. (((gr_product_before_prime_factorization_giventracesteps) = ((ge_representation_real_code_prime_factorization_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyfirst)) * S ((ge_representation_real_code_prime_factorization_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_prime_factorization_giventracestepsmultiplyfirstreal ge_balance_negative_prime_factorization_giventracestepsmultiplyfirstreal. (((((ge_representation_real_code_prime_factorization_giventracestepsmultiplyfirst) = 2 * (ge_balance_positive_prime_factorization_giventracestepsmultiplyfirstreal) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_giventracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_prime_factorization_giventracestepsmultiplyfirst) = 2 * ge_signed_half_prime_factorization_giventracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_giventracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplyfirstreal) = S ge_signed_half_prime_factorization_giventracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_giventracestepsmultiply) + ge_balance_negative_prime_factorization_giventracestepsmultiplyfirstreal = (ge_first_rn_prime_factorization_giventracestepsmultiply) + ge_balance_positive_prime_factorization_giventracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_prime_factorization_giventracestepsmultiplyfirstimaginary ge_balance_negative_prime_factorization_giventracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyfirst) = 2 * (ge_balance_positive_prime_factorization_giventracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_giventracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyfirst) = 2 * ge_signed_half_prime_factorization_giventracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_giventracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplyfirstimaginary) = S ge_signed_half_prime_factorization_giventracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_giventracestepsmultiply) + ge_balance_negative_prime_factorization_giventracestepsmultiplyfirstimaginary = (ge_first_in_prime_factorization_giventracestepsmultiply) + ge_balance_positive_prime_factorization_giventracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_giventracestepsmultiplysecond ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplysecond. (((gr_product_factor_prime_factorization_giventracesteps) = ((ge_representation_real_code_prime_factorization_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplysecond)) * S ((ge_representation_real_code_prime_factorization_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplysecond)) + ((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplysecond))) /\ ((exists ge_balance_positive_prime_factorization_giventracestepsmultiplysecondreal ge_balance_negative_prime_factorization_giventracestepsmultiplysecondreal. (((((ge_representation_real_code_prime_factorization_giventracestepsmultiplysecond) = 2 * (ge_balance_positive_prime_factorization_giventracestepsmultiplysecondreal) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_prime_factorization_giventracestepsmultiplysecondrealdecode. (((ge_representation_real_code_prime_factorization_giventracestepsmultiplysecond) = 2 * ge_signed_half_prime_factorization_giventracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_giventracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplysecondreal) = S ge_signed_half_prime_factorization_giventracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_prime_factorization_giventracestepsmultiply) + ge_balance_negative_prime_factorization_giventracestepsmultiplysecondreal = (ge_second_rn_prime_factorization_giventracestepsmultiply) + ge_balance_positive_prime_factorization_giventracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_prime_factorization_giventracestepsmultiplysecondimaginary ge_balance_negative_prime_factorization_giventracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplysecond) = 2 * (ge_balance_positive_prime_factorization_giventracestepsmultiplysecondimaginary) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_giventracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplysecond) = 2 * ge_signed_half_prime_factorization_giventracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_giventracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplysecondimaginary) = S ge_signed_half_prime_factorization_giventracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_giventracestepsmultiply) + ge_balance_negative_prime_factorization_giventracestepsmultiplysecondimaginary = (ge_second_in_prime_factorization_giventracestepsmultiply) + ge_balance_positive_prime_factorization_giventracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_giventracestepsmultiplyoutput ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyoutput. (((gr_product_after_prime_factorization_giventracesteps) = ((ge_representation_real_code_prime_factorization_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyoutput)) * S ((ge_representation_real_code_prime_factorization_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_prime_factorization_giventracestepsmultiplyoutputreal ge_balance_negative_prime_factorization_giventracestepsmultiplyoutputreal. (((((ge_representation_real_code_prime_factorization_giventracestepsmultiplyoutput) = 2 * (ge_balance_positive_prime_factorization_giventracestepsmultiplyoutputreal) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_giventracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_prime_factorization_giventracestepsmultiplyoutput) = 2 * ge_signed_half_prime_factorization_giventracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_giventracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplyoutputreal) = S ge_signed_half_prime_factorization_giventracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_giventracestepsmultiply) * (ge_second_rp_prime_factorization_giventracestepsmultiply))) + (((ge_first_rn_prime_factorization_giventracestepsmultiply) * (ge_second_rn_prime_factorization_giventracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_giventracestepsmultiply) * (ge_second_in_prime_factorization_giventracestepsmultiply))) + (((ge_first_in_prime_factorization_giventracestepsmultiply) * (ge_second_ip_prime_factorization_giventracestepsmultiply))))))) + ge_balance_negative_prime_factorization_giventracestepsmultiplyoutputreal = (((((((ge_first_rp_prime_factorization_giventracestepsmultiply) * (ge_second_rn_prime_factorization_giventracestepsmultiply))) + (((ge_first_rn_prime_factorization_giventracestepsmultiply) * (ge_second_rp_prime_factorization_giventracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_giventracestepsmultiply) * (ge_second_ip_prime_factorization_giventracestepsmultiply))) + (((ge_first_in_prime_factorization_giventracestepsmultiply) * (ge_second_in_prime_factorization_giventracestepsmultiply))))))) + ge_balance_positive_prime_factorization_giventracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_prime_factorization_giventracestepsmultiplyoutputimaginary ge_balance_negative_prime_factorization_giventracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyoutput) = 2 * (ge_balance_positive_prime_factorization_giventracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_giventracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_giventracestepsmultiplyoutput) = 2 * ge_signed_half_prime_factorization_giventracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_giventracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_giventracestepsmultiplyoutputimaginary) = S ge_signed_half_prime_factorization_giventracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_giventracestepsmultiply) * (ge_second_ip_prime_factorization_giventracestepsmultiply))) + (((ge_first_rn_prime_factorization_giventracestepsmultiply) * (ge_second_in_prime_factorization_giventracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_giventracestepsmultiply) * (ge_second_rp_prime_factorization_giventracestepsmultiply))) + (((ge_first_in_prime_factorization_giventracestepsmultiply) * (ge_second_rn_prime_factorization_giventracestepsmultiply))))))) + ge_balance_negative_prime_factorization_giventracestepsmultiplyoutputimaginary = (((((((ge_first_rp_prime_factorization_giventracestepsmultiply) * (ge_second_in_prime_factorization_giventracestepsmultiply))) + (((ge_first_rn_prime_factorization_giventracestepsmultiply) * (ge_second_ip_prime_factorization_giventracestepsmultiply))))) + (((((ge_first_ip_prime_factorization_giventracestepsmultiply) * (ge_second_rn_prime_factorization_giventracestepsmultiply))) + (((ge_first_in_prime_factorization_giventracestepsmultiply) * (ge_second_rp_prime_factorization_giventracestepsmultiply))))))) + ge_balance_positive_prime_factorization_giventracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_prime_factorization_givenreconstruct ge_first_rn_prime_factorization_givenreconstruct ge_first_ip_prime_factorization_givenreconstruct ge_first_in_prime_factorization_givenreconstruct ge_second_rp_prime_factorization_givenreconstruct ge_second_rn_prime_factorization_givenreconstruct ge_second_ip_prime_factorization_givenreconstruct ge_second_in_prime_factorization_givenreconstruct. ((exists ge_representation_real_code_prime_factorization_givenreconstructfirst ge_representation_imaginary_code_prime_factorization_givenreconstructfirst. (((u) = ((ge_representation_real_code_prime_factorization_givenreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_givenreconstructfirst)) * S ((ge_representation_real_code_prime_factorization_givenreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_givenreconstructfirst)) + ((ge_representation_imaginary_code_prime_factorization_givenreconstructfirst) + (ge_representation_imaginary_code_prime_factorization_givenreconstructfirst))) /\ ((exists ge_balance_positive_prime_factorization_givenreconstructfirstreal ge_balance_negative_prime_factorization_givenreconstructfirstreal. (((((ge_representation_real_code_prime_factorization_givenreconstructfirst) = 2 * (ge_balance_positive_prime_factorization_givenreconstructfirstreal) /\ (ge_balance_negative_prime_factorization_givenreconstructfirstreal) = 0) \/ exists ge_signed_half_prime_factorization_givenreconstructfirstrealdecode. (((ge_representation_real_code_prime_factorization_givenreconstructfirst) = 2 * ge_signed_half_prime_factorization_givenreconstructfirstrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenreconstructfirstreal) = 0) /\ (ge_balance_negative_prime_factorization_givenreconstructfirstreal) = S ge_signed_half_prime_factorization_givenreconstructfirstrealdecode))) /\ ((ge_first_rp_prime_factorization_givenreconstruct) + ge_balance_negative_prime_factorization_givenreconstructfirstreal = (ge_first_rn_prime_factorization_givenreconstruct) + ge_balance_positive_prime_factorization_givenreconstructfirstreal))) /\ (exists ge_balance_positive_prime_factorization_givenreconstructfirstimaginary ge_balance_negative_prime_factorization_givenreconstructfirstimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenreconstructfirst) = 2 * (ge_balance_positive_prime_factorization_givenreconstructfirstimaginary) /\ (ge_balance_negative_prime_factorization_givenreconstructfirstimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenreconstructfirst) = 2 * ge_signed_half_prime_factorization_givenreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenreconstructfirstimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenreconstructfirstimaginary) = S ge_signed_half_prime_factorization_givenreconstructfirstimaginarydecode))) /\ ((ge_first_ip_prime_factorization_givenreconstruct) + ge_balance_negative_prime_factorization_givenreconstructfirstimaginary = (ge_first_in_prime_factorization_givenreconstruct) + ge_balance_positive_prime_factorization_givenreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_factorization_givenreconstructsecond ge_representation_imaginary_code_prime_factorization_givenreconstructsecond. (((gr_prime_factor_product_prime_factorization_given) = ((ge_representation_real_code_prime_factorization_givenreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_givenreconstructsecond)) * S ((ge_representation_real_code_prime_factorization_givenreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_givenreconstructsecond)) + ((ge_representation_imaginary_code_prime_factorization_givenreconstructsecond) + (ge_representation_imaginary_code_prime_factorization_givenreconstructsecond))) /\ ((exists ge_balance_positive_prime_factorization_givenreconstructsecondreal ge_balance_negative_prime_factorization_givenreconstructsecondreal. (((((ge_representation_real_code_prime_factorization_givenreconstructsecond) = 2 * (ge_balance_positive_prime_factorization_givenreconstructsecondreal) /\ (ge_balance_negative_prime_factorization_givenreconstructsecondreal) = 0) \/ exists ge_signed_half_prime_factorization_givenreconstructsecondrealdecode. (((ge_representation_real_code_prime_factorization_givenreconstructsecond) = 2 * ge_signed_half_prime_factorization_givenreconstructsecondrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenreconstructsecondreal) = 0) /\ (ge_balance_negative_prime_factorization_givenreconstructsecondreal) = S ge_signed_half_prime_factorization_givenreconstructsecondrealdecode))) /\ ((ge_second_rp_prime_factorization_givenreconstruct) + ge_balance_negative_prime_factorization_givenreconstructsecondreal = (ge_second_rn_prime_factorization_givenreconstruct) + ge_balance_positive_prime_factorization_givenreconstructsecondreal))) /\ (exists ge_balance_positive_prime_factorization_givenreconstructsecondimaginary ge_balance_negative_prime_factorization_givenreconstructsecondimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenreconstructsecond) = 2 * (ge_balance_positive_prime_factorization_givenreconstructsecondimaginary) /\ (ge_balance_negative_prime_factorization_givenreconstructsecondimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenreconstructsecond) = 2 * ge_signed_half_prime_factorization_givenreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenreconstructsecondimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenreconstructsecondimaginary) = S ge_signed_half_prime_factorization_givenreconstructsecondimaginarydecode))) /\ ((ge_second_ip_prime_factorization_givenreconstruct) + ge_balance_negative_prime_factorization_givenreconstructsecondimaginary = (ge_second_in_prime_factorization_givenreconstruct) + ge_balance_positive_prime_factorization_givenreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_factorization_givenreconstructoutput ge_representation_imaginary_code_prime_factorization_givenreconstructoutput. (((z) = ((ge_representation_real_code_prime_factorization_givenreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_givenreconstructoutput)) * S ((ge_representation_real_code_prime_factorization_givenreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_givenreconstructoutput)) + ((ge_representation_imaginary_code_prime_factorization_givenreconstructoutput) + (ge_representation_imaginary_code_prime_factorization_givenreconstructoutput))) /\ ((exists ge_balance_positive_prime_factorization_givenreconstructoutputreal ge_balance_negative_prime_factorization_givenreconstructoutputreal. (((((ge_representation_real_code_prime_factorization_givenreconstructoutput) = 2 * (ge_balance_positive_prime_factorization_givenreconstructoutputreal) /\ (ge_balance_negative_prime_factorization_givenreconstructoutputreal) = 0) \/ exists ge_signed_half_prime_factorization_givenreconstructoutputrealdecode. (((ge_representation_real_code_prime_factorization_givenreconstructoutput) = 2 * ge_signed_half_prime_factorization_givenreconstructoutputrealdecode + 1 /\ (ge_balance_positive_prime_factorization_givenreconstructoutputreal) = 0) /\ (ge_balance_negative_prime_factorization_givenreconstructoutputreal) = S ge_signed_half_prime_factorization_givenreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_prime_factorization_givenreconstruct) * (ge_second_rp_prime_factorization_givenreconstruct))) + (((ge_first_rn_prime_factorization_givenreconstruct) * (ge_second_rn_prime_factorization_givenreconstruct))))) + (((((ge_first_ip_prime_factorization_givenreconstruct) * (ge_second_in_prime_factorization_givenreconstruct))) + (((ge_first_in_prime_factorization_givenreconstruct) * (ge_second_ip_prime_factorization_givenreconstruct))))))) + ge_balance_negative_prime_factorization_givenreconstructoutputreal = (((((((ge_first_rp_prime_factorization_givenreconstruct) * (ge_second_rn_prime_factorization_givenreconstruct))) + (((ge_first_rn_prime_factorization_givenreconstruct) * (ge_second_rp_prime_factorization_givenreconstruct))))) + (((((ge_first_ip_prime_factorization_givenreconstruct) * (ge_second_ip_prime_factorization_givenreconstruct))) + (((ge_first_in_prime_factorization_givenreconstruct) * (ge_second_in_prime_factorization_givenreconstruct))))))) + ge_balance_positive_prime_factorization_givenreconstructoutputreal))) /\ (exists ge_balance_positive_prime_factorization_givenreconstructoutputimaginary ge_balance_negative_prime_factorization_givenreconstructoutputimaginary. (((((ge_representation_imaginary_code_prime_factorization_givenreconstructoutput) = 2 * (ge_balance_positive_prime_factorization_givenreconstructoutputimaginary) /\ (ge_balance_negative_prime_factorization_givenreconstructoutputimaginary) = 0) \/ exists ge_signed_half_prime_factorization_givenreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_prime_factorization_givenreconstructoutput) = 2 * ge_signed_half_prime_factorization_givenreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_factorization_givenreconstructoutputimaginary) = 0) /\ (ge_balance_negative_prime_factorization_givenreconstructoutputimaginary) = S ge_signed_half_prime_factorization_givenreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_factorization_givenreconstruct) * (ge_second_ip_prime_factorization_givenreconstruct))) + (((ge_first_rn_prime_factorization_givenreconstruct) * (ge_second_in_prime_factorization_givenreconstruct))))) + (((((ge_first_ip_prime_factorization_givenreconstruct) * (ge_second_rp_prime_factorization_givenreconstruct))) + (((ge_first_in_prime_factorization_givenreconstruct) * (ge_second_rn_prime_factorization_givenreconstruct))))))) + ge_balance_negative_prime_factorization_givenreconstructoutputimaginary = (((((((ge_first_rp_prime_factorization_givenreconstruct) * (ge_second_in_prime_factorization_givenreconstruct))) + (((ge_first_rn_prime_factorization_givenreconstruct) * (ge_second_ip_prime_factorization_givenreconstruct))))) + (((((ge_first_ip_prime_factorization_givenreconstruct) * (ge_second_rn_prime_factorization_givenreconstruct))) + (((ge_first_in_prime_factorization_givenreconstruct) * (ge_second_rp_prime_factorization_givenreconstruct))))))) + ge_balance_positive_prime_factorization_givenreconstructoutputimaginary)))))))))))))) -> (((exists gr_inverse_irreducible_factorization_resultunit. (exists ge_first_rp_irreducible_factorization_resultunitidentity ge_first_rn_irreducible_factorization_resultunitidentity ge_first_ip_irreducible_factorization_resultunitidentity ge_first_in_irreducible_factorization_resultunitidentity ge_second_rp_irreducible_factorization_resultunitidentity ge_second_rn_irreducible_factorization_resultunitidentity ge_second_ip_irreducible_factorization_resultunitidentity ge_second_in_irreducible_factorization_resultunitidentity. ((exists ge_representation_real_code_irreducible_factorization_resultunitidentityfirst ge_representation_imaginary_code_irreducible_factorization_resultunitidentityfirst. (((u) = ((ge_representation_real_code_irreducible_factorization_resultunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentityfirst)) * S ((ge_representation_real_code_irreducible_factorization_resultunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_resultunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_resultunitidentityfirstreal ge_balance_negative_irreducible_factorization_resultunitidentityfirstreal. (((((ge_representation_real_code_irreducible_factorization_resultunitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultunitidentityfirstreal) /\ (ge_balance_negative_irreducible_factorization_resultunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_resultunitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_resultunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultunitidentityfirstreal) = S ge_signed_half_irreducible_factorization_resultunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_resultunitidentity) + ge_balance_negative_irreducible_factorization_resultunitidentityfirstreal = (ge_first_rn_irreducible_factorization_resultunitidentity) + ge_balance_positive_irreducible_factorization_resultunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultunitidentityfirstimaginary ge_balance_negative_irreducible_factorization_resultunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultunitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_resultunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultunitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_resultunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultunitidentityfirstimaginary) = S ge_signed_half_irreducible_factorization_resultunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_resultunitidentity) + ge_balance_negative_irreducible_factorization_resultunitidentityfirstimaginary = (ge_first_in_irreducible_factorization_resultunitidentity) + ge_balance_positive_irreducible_factorization_resultunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_resultunitidentitysecond ge_representation_imaginary_code_irreducible_factorization_resultunitidentitysecond. (((gr_inverse_irreducible_factorization_resultunit) = ((ge_representation_real_code_irreducible_factorization_resultunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentitysecond)) * S ((ge_representation_real_code_irreducible_factorization_resultunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_resultunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_resultunitidentitysecondreal ge_balance_negative_irreducible_factorization_resultunitidentitysecondreal. (((((ge_representation_real_code_irreducible_factorization_resultunitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_resultunitidentitysecondreal) /\ (ge_balance_negative_irreducible_factorization_resultunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_resultunitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_resultunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultunitidentitysecondreal) = S ge_signed_half_irreducible_factorization_resultunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_resultunitidentity) + ge_balance_negative_irreducible_factorization_resultunitidentitysecondreal = (ge_second_rn_irreducible_factorization_resultunitidentity) + ge_balance_positive_irreducible_factorization_resultunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultunitidentitysecondimaginary ge_balance_negative_irreducible_factorization_resultunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultunitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_resultunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_resultunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultunitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_resultunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultunitidentitysecondimaginary) = S ge_signed_half_irreducible_factorization_resultunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_resultunitidentity) + ge_balance_negative_irreducible_factorization_resultunitidentitysecondimaginary = (ge_second_in_irreducible_factorization_resultunitidentity) + ge_balance_positive_irreducible_factorization_resultunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_resultunitidentityoutput ge_representation_imaginary_code_irreducible_factorization_resultunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_factorization_resultunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentityoutput)) * S ((ge_representation_real_code_irreducible_factorization_resultunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_resultunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_resultunitidentityoutputreal ge_balance_negative_irreducible_factorization_resultunitidentityoutputreal. (((((ge_representation_real_code_irreducible_factorization_resultunitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultunitidentityoutputreal) /\ (ge_balance_negative_irreducible_factorization_resultunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_resultunitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_resultunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultunitidentityoutputreal) = S ge_signed_half_irreducible_factorization_resultunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultunitidentity) * (ge_second_rp_irreducible_factorization_resultunitidentity))) + (((ge_first_rn_irreducible_factorization_resultunitidentity) * (ge_second_rn_irreducible_factorization_resultunitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultunitidentity) * (ge_second_in_irreducible_factorization_resultunitidentity))) + (((ge_first_in_irreducible_factorization_resultunitidentity) * (ge_second_ip_irreducible_factorization_resultunitidentity))))))) + ge_balance_negative_irreducible_factorization_resultunitidentityoutputreal = (((((((ge_first_rp_irreducible_factorization_resultunitidentity) * (ge_second_rn_irreducible_factorization_resultunitidentity))) + (((ge_first_rn_irreducible_factorization_resultunitidentity) * (ge_second_rp_irreducible_factorization_resultunitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultunitidentity) * (ge_second_ip_irreducible_factorization_resultunitidentity))) + (((ge_first_in_irreducible_factorization_resultunitidentity) * (ge_second_in_irreducible_factorization_resultunitidentity))))))) + ge_balance_positive_irreducible_factorization_resultunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultunitidentityoutputimaginary ge_balance_negative_irreducible_factorization_resultunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultunitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_resultunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultunitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_resultunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultunitidentityoutputimaginary) = S ge_signed_half_irreducible_factorization_resultunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultunitidentity) * (ge_second_ip_irreducible_factorization_resultunitidentity))) + (((ge_first_rn_irreducible_factorization_resultunitidentity) * (ge_second_in_irreducible_factorization_resultunitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultunitidentity) * (ge_second_rp_irreducible_factorization_resultunitidentity))) + (((ge_first_in_irreducible_factorization_resultunitidentity) * (ge_second_rn_irreducible_factorization_resultunitidentity))))))) + ge_balance_negative_irreducible_factorization_resultunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_factorization_resultunitidentity) * (ge_second_in_irreducible_factorization_resultunitidentity))) + (((ge_first_rn_irreducible_factorization_resultunitidentity) * (ge_second_ip_irreducible_factorization_resultunitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultunitidentity) * (ge_second_rn_irreducible_factorization_resultunitidentity))) + (((ge_first_in_irreducible_factorization_resultunitidentity) * (ge_second_rp_irreducible_factorization_resultunitidentity))))))) + ge_balance_positive_irreducible_factorization_resultunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_irreducible_factorization_resultirreducible gr_factor_value_irreducible_factorization_resultirreducible. (exists ge_gap_irreducible_factorization_resultirreducibleindex. ge_gap_irreducible_factorization_resultirreducibleindex + S (gr_factor_index_irreducible_factorization_resultirreducible) = (l)) -> (((exists ff_h_gprod_irreducible_factorization_resultirreducibleentry. ff_h_gprod_irreducible_factorization_resultirreducibleentry + S (gr_factor_value_irreducible_factorization_resultirreducible) = S ((S (gr_factor_index_irreducible_factorization_resultirreducible)) * c)) /\ exists ff_q_gprod_irreducible_factorization_resultirreducibleentry. b = ff_q_gprod_irreducible_factorization_resultirreducibleentry * S ((S (gr_factor_index_irreducible_factorization_resultirreducible)) * c) + (gr_factor_value_irreducible_factorization_resultirreducible))) -> (((exists ge_real_positive_irreducible_factorization_resultirreducibleirreduciblecarrier ge_real_negative_irreducible_factorization_resultirreducibleirreduciblecarrier ge_imaginary_positive_irreducible_factorization_resultirreducibleirreduciblecarrier ge_imaginary_negative_irreducible_factorization_resultirreducibleirreduciblecarrier. (exists ge_real_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode ge_imaginary_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode. (((gr_factor_value_irreducible_factorization_resultirreducible) = ((ge_real_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_factorization_resultirreducibleirreduciblecarrier) /\ (ge_real_negative_irreducible_factorization_resultirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_factorization_resultirreducibleirreduciblecarrierdecode_real. (((ge_real_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_factorization_resultirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_factorization_resultirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_factorization_resultirreducibleirreduciblecarrier) = S ge_signed_half_ge_irreducible_factorization_resultirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_factorization_resultirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_factorization_resultirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_factorization_resultirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_factorization_resultirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_factorization_resultirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_factorization_resultirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_factorization_resultirreducibleirreduciblecarrier) = S ge_signed_half_ge_irreducible_factorization_resultirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_irreducible_factorization_resultirreducible)=0)) /\ ((~(exists gr_inverse_irreducible_factorization_resultirreducibleirreduciblenonunit. (exists ge_first_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity ge_first_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity ge_first_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity ge_first_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity ge_second_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity ge_second_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity ge_second_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity ge_second_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_irreducible_factorization_resultirreducible) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_factorization_resultirreducibleirreduciblenonunit) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblenonunitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_factorization_resultirreducibleirreducible gr_second_factor_irreducible_factorization_resultirreducibleirreducible. (exists ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefactorization ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefactorization ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefactorization ge_first_in_irreducible_factorization_resultirreducibleirreduciblefactorization ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefactorization ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefactorization ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefactorization ge_second_in_irreducible_factorization_resultirreducibleirreduciblefactorization. ((exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst. (((gr_first_factor_irreducible_factorization_resultirreducibleirreducible) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefactorization) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefactorization) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefactorization) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_factorization_resultirreducibleirreduciblefactorization) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond. (((gr_second_factor_irreducible_factorization_resultirreducibleirreducible) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefactorization) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefactorization) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefactorization) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefactorization) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput. (((gr_factor_value_irreducible_factorization_resultirreducible) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefactorization))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefactorization))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefactorization))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefactorization))))))) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefactorization))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefactorization))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefactorization))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefactorization))))))) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefactorization))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefactorization))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefactorization))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefactorization))))))) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefactorization))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefactorization))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefactorization))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblefactorization) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefactorization))))))) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_factorization_resultirreducibleirreduciblefirst_unit. (exists ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity ge_first_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity ge_second_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_factorization_resultirreducibleirreducible) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_factorization_resultirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_factorization_resultirreducibleirreduciblesecond_unit. (exists ge_first_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity ge_first_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity ge_first_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity ge_first_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity ge_second_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity ge_second_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity ge_second_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity ge_second_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_factorization_resultirreducibleirreducible) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_factorization_resultirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_factorization_resultirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_irreducible_factorization_result. ((exists gr_product_trace_irreducible_factorization_resulttrace gr_product_scale_irreducible_factorization_resulttrace. ((((exists ff_h_gprod_irreducible_factorization_resulttracestart. ff_h_gprod_irreducible_factorization_resulttracestart + S (6) = S ((S (0)) * gr_product_scale_irreducible_factorization_resulttrace)) /\ exists ff_q_gprod_irreducible_factorization_resulttracestart. gr_product_trace_irreducible_factorization_resulttrace = ff_q_gprod_irreducible_factorization_resulttracestart * S ((S (0)) * gr_product_scale_irreducible_factorization_resulttrace) + (6))) /\ ((((exists ff_h_gprod_irreducible_factorization_resulttraceend. ff_h_gprod_irreducible_factorization_resulttraceend + S (gr_factor_product_irreducible_factorization_result) = S ((S (l)) * gr_product_scale_irreducible_factorization_resulttrace)) /\ exists ff_q_gprod_irreducible_factorization_resulttraceend. gr_product_trace_irreducible_factorization_resulttrace = ff_q_gprod_irreducible_factorization_resulttraceend * S ((S (l)) * gr_product_scale_irreducible_factorization_resulttrace) + (gr_factor_product_irreducible_factorization_result))) /\ (forall gr_product_index_irreducible_factorization_resulttracesteps. (exists ge_gap_irreducible_factorization_resulttracestepsindex_bound. ge_gap_irreducible_factorization_resulttracestepsindex_bound + S (gr_product_index_irreducible_factorization_resulttracesteps) = (l)) -> exists gr_product_factor_irreducible_factorization_resulttracesteps gr_product_before_irreducible_factorization_resulttracesteps gr_product_after_irreducible_factorization_resulttracesteps. ((((exists ff_h_gprod_irreducible_factorization_resulttracestepsfactor. ff_h_gprod_irreducible_factorization_resulttracestepsfactor + S (gr_product_factor_irreducible_factorization_resulttracesteps) = S ((S (gr_product_index_irreducible_factorization_resulttracesteps)) * c)) /\ exists ff_q_gprod_irreducible_factorization_resulttracestepsfactor. b = ff_q_gprod_irreducible_factorization_resulttracestepsfactor * S ((S (gr_product_index_irreducible_factorization_resulttracesteps)) * c) + (gr_product_factor_irreducible_factorization_resulttracesteps))) /\ ((((exists ff_h_gprod_irreducible_factorization_resulttracestepsbefore. ff_h_gprod_irreducible_factorization_resulttracestepsbefore + S (gr_product_before_irreducible_factorization_resulttracesteps) = S ((S (gr_product_index_irreducible_factorization_resulttracesteps)) * gr_product_scale_irreducible_factorization_resulttrace)) /\ exists ff_q_gprod_irreducible_factorization_resulttracestepsbefore. gr_product_trace_irreducible_factorization_resulttrace = ff_q_gprod_irreducible_factorization_resulttracestepsbefore * S ((S (gr_product_index_irreducible_factorization_resulttracesteps)) * gr_product_scale_irreducible_factorization_resulttrace) + (gr_product_before_irreducible_factorization_resulttracesteps))) /\ ((((exists ff_h_gprod_irreducible_factorization_resulttracestepsafter. ff_h_gprod_irreducible_factorization_resulttracestepsafter + S (gr_product_after_irreducible_factorization_resulttracesteps) = S ((S (S (gr_product_index_irreducible_factorization_resulttracesteps))) * gr_product_scale_irreducible_factorization_resulttrace)) /\ exists ff_q_gprod_irreducible_factorization_resulttracestepsafter. gr_product_trace_irreducible_factorization_resulttrace = ff_q_gprod_irreducible_factorization_resulttracestepsafter * S ((S (S (gr_product_index_irreducible_factorization_resulttracesteps))) * gr_product_scale_irreducible_factorization_resulttrace) + (gr_product_after_irreducible_factorization_resulttracesteps))) /\ (exists ge_first_rp_irreducible_factorization_resulttracestepsmultiply ge_first_rn_irreducible_factorization_resulttracestepsmultiply ge_first_ip_irreducible_factorization_resulttracestepsmultiply ge_first_in_irreducible_factorization_resulttracestepsmultiply ge_second_rp_irreducible_factorization_resulttracestepsmultiply ge_second_rn_irreducible_factorization_resulttracestepsmultiply ge_second_ip_irreducible_factorization_resulttracestepsmultiply ge_second_in_irreducible_factorization_resulttracestepsmultiply. ((exists ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyfirst ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyfirst. (((gr_product_before_irreducible_factorization_resulttracesteps) = ((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyfirst) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyfirst)) * S ((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyfirst) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyfirst) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyfirstreal ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyfirstreal. (((((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyfirst) = 2 * (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyfirstreal) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resulttracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyfirst) = 2 * ge_signed_half_irreducible_factorization_resulttracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyfirstreal) = S ge_signed_half_irreducible_factorization_resulttracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_resulttracestepsmultiply) + ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyfirstreal = (ge_first_rn_irreducible_factorization_resulttracestepsmultiply) + ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyfirstimaginary ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyfirst) = 2 * (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resulttracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyfirst) = 2 * ge_signed_half_irreducible_factorization_resulttracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyfirstimaginary) = S ge_signed_half_irreducible_factorization_resulttracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_resulttracestepsmultiply) + ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyfirstimaginary = (ge_first_in_irreducible_factorization_resulttracestepsmultiply) + ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplysecond ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplysecond. (((gr_product_factor_irreducible_factorization_resulttracesteps) = ((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplysecond) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplysecond)) * S ((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplysecond) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplysecond)) + ((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplysecond) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplysecond))) /\ ((exists ge_balance_positive_irreducible_factorization_resulttracestepsmultiplysecondreal ge_balance_negative_irreducible_factorization_resulttracestepsmultiplysecondreal. (((((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplysecond) = 2 * (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplysecondreal) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resulttracestepsmultiplysecondrealdecode. (((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplysecond) = 2 * ge_signed_half_irreducible_factorization_resulttracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplysecondreal) = S ge_signed_half_irreducible_factorization_resulttracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_resulttracestepsmultiply) + ge_balance_negative_irreducible_factorization_resulttracestepsmultiplysecondreal = (ge_second_rn_irreducible_factorization_resulttracestepsmultiply) + ge_balance_positive_irreducible_factorization_resulttracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_resulttracestepsmultiplysecondimaginary ge_balance_negative_irreducible_factorization_resulttracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplysecond) = 2 * (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplysecondimaginary) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resulttracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplysecond) = 2 * ge_signed_half_irreducible_factorization_resulttracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplysecondimaginary) = S ge_signed_half_irreducible_factorization_resulttracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_resulttracestepsmultiply) + ge_balance_negative_irreducible_factorization_resulttracestepsmultiplysecondimaginary = (ge_second_in_irreducible_factorization_resulttracestepsmultiply) + ge_balance_positive_irreducible_factorization_resulttracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyoutput ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyoutput. (((gr_product_after_irreducible_factorization_resulttracesteps) = ((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyoutput) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyoutput)) * S ((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyoutput) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyoutput) + (ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyoutputreal ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyoutputreal. (((((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyoutput) = 2 * (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyoutputreal) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resulttracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_resulttracestepsmultiplyoutput) = 2 * ge_signed_half_irreducible_factorization_resulttracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyoutputreal) = S ge_signed_half_irreducible_factorization_resulttracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resulttracestepsmultiply) * (ge_second_rp_irreducible_factorization_resulttracestepsmultiply))) + (((ge_first_rn_irreducible_factorization_resulttracestepsmultiply) * (ge_second_rn_irreducible_factorization_resulttracestepsmultiply))))) + (((((ge_first_ip_irreducible_factorization_resulttracestepsmultiply) * (ge_second_in_irreducible_factorization_resulttracestepsmultiply))) + (((ge_first_in_irreducible_factorization_resulttracestepsmultiply) * (ge_second_ip_irreducible_factorization_resulttracestepsmultiply))))))) + ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyoutputreal = (((((((ge_first_rp_irreducible_factorization_resulttracestepsmultiply) * (ge_second_rn_irreducible_factorization_resulttracestepsmultiply))) + (((ge_first_rn_irreducible_factorization_resulttracestepsmultiply) * (ge_second_rp_irreducible_factorization_resulttracestepsmultiply))))) + (((((ge_first_ip_irreducible_factorization_resulttracestepsmultiply) * (ge_second_ip_irreducible_factorization_resulttracestepsmultiply))) + (((ge_first_in_irreducible_factorization_resulttracestepsmultiply) * (ge_second_in_irreducible_factorization_resulttracestepsmultiply))))))) + ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyoutputimaginary ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyoutput) = 2 * (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resulttracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resulttracestepsmultiplyoutput) = 2 * ge_signed_half_irreducible_factorization_resulttracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyoutputimaginary) = S ge_signed_half_irreducible_factorization_resulttracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resulttracestepsmultiply) * (ge_second_ip_irreducible_factorization_resulttracestepsmultiply))) + (((ge_first_rn_irreducible_factorization_resulttracestepsmultiply) * (ge_second_in_irreducible_factorization_resulttracestepsmultiply))))) + (((((ge_first_ip_irreducible_factorization_resulttracestepsmultiply) * (ge_second_rp_irreducible_factorization_resulttracestepsmultiply))) + (((ge_first_in_irreducible_factorization_resulttracestepsmultiply) * (ge_second_rn_irreducible_factorization_resulttracestepsmultiply))))))) + ge_balance_negative_irreducible_factorization_resulttracestepsmultiplyoutputimaginary = (((((((ge_first_rp_irreducible_factorization_resulttracestepsmultiply) * (ge_second_in_irreducible_factorization_resulttracestepsmultiply))) + (((ge_first_rn_irreducible_factorization_resulttracestepsmultiply) * (ge_second_ip_irreducible_factorization_resulttracestepsmultiply))))) + (((((ge_first_ip_irreducible_factorization_resulttracestepsmultiply) * (ge_second_rn_irreducible_factorization_resulttracestepsmultiply))) + (((ge_first_in_irreducible_factorization_resulttracestepsmultiply) * (ge_second_rp_irreducible_factorization_resulttracestepsmultiply))))))) + ge_balance_positive_irreducible_factorization_resulttracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_irreducible_factorization_resultreconstruct ge_first_rn_irreducible_factorization_resultreconstruct ge_first_ip_irreducible_factorization_resultreconstruct ge_first_in_irreducible_factorization_resultreconstruct ge_second_rp_irreducible_factorization_resultreconstruct ge_second_rn_irreducible_factorization_resultreconstruct ge_second_ip_irreducible_factorization_resultreconstruct ge_second_in_irreducible_factorization_resultreconstruct. ((exists ge_representation_real_code_irreducible_factorization_resultreconstructfirst ge_representation_imaginary_code_irreducible_factorization_resultreconstructfirst. (((u) = ((ge_representation_real_code_irreducible_factorization_resultreconstructfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructfirst)) * S ((ge_representation_real_code_irreducible_factorization_resultreconstructfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructfirst)) + ((ge_representation_imaginary_code_irreducible_factorization_resultreconstructfirst) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructfirst))) /\ ((exists ge_balance_positive_irreducible_factorization_resultreconstructfirstreal ge_balance_negative_irreducible_factorization_resultreconstructfirstreal. (((((ge_representation_real_code_irreducible_factorization_resultreconstructfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultreconstructfirstreal) /\ (ge_balance_negative_irreducible_factorization_resultreconstructfirstreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultreconstructfirstrealdecode. (((ge_representation_real_code_irreducible_factorization_resultreconstructfirst) = 2 * ge_signed_half_irreducible_factorization_resultreconstructfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultreconstructfirstreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultreconstructfirstreal) = S ge_signed_half_irreducible_factorization_resultreconstructfirstrealdecode))) /\ ((ge_first_rp_irreducible_factorization_resultreconstruct) + ge_balance_negative_irreducible_factorization_resultreconstructfirstreal = (ge_first_rn_irreducible_factorization_resultreconstruct) + ge_balance_positive_irreducible_factorization_resultreconstructfirstreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultreconstructfirstimaginary ge_balance_negative_irreducible_factorization_resultreconstructfirstimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultreconstructfirst) = 2 * (ge_balance_positive_irreducible_factorization_resultreconstructfirstimaginary) /\ (ge_balance_negative_irreducible_factorization_resultreconstructfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultreconstructfirst) = 2 * ge_signed_half_irreducible_factorization_resultreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultreconstructfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultreconstructfirstimaginary) = S ge_signed_half_irreducible_factorization_resultreconstructfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_factorization_resultreconstruct) + ge_balance_negative_irreducible_factorization_resultreconstructfirstimaginary = (ge_first_in_irreducible_factorization_resultreconstruct) + ge_balance_positive_irreducible_factorization_resultreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_factorization_resultreconstructsecond ge_representation_imaginary_code_irreducible_factorization_resultreconstructsecond. (((gr_factor_product_irreducible_factorization_result) = ((ge_representation_real_code_irreducible_factorization_resultreconstructsecond) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructsecond)) * S ((ge_representation_real_code_irreducible_factorization_resultreconstructsecond) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructsecond)) + ((ge_representation_imaginary_code_irreducible_factorization_resultreconstructsecond) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructsecond))) /\ ((exists ge_balance_positive_irreducible_factorization_resultreconstructsecondreal ge_balance_negative_irreducible_factorization_resultreconstructsecondreal. (((((ge_representation_real_code_irreducible_factorization_resultreconstructsecond) = 2 * (ge_balance_positive_irreducible_factorization_resultreconstructsecondreal) /\ (ge_balance_negative_irreducible_factorization_resultreconstructsecondreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultreconstructsecondrealdecode. (((ge_representation_real_code_irreducible_factorization_resultreconstructsecond) = 2 * ge_signed_half_irreducible_factorization_resultreconstructsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultreconstructsecondreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultreconstructsecondreal) = S ge_signed_half_irreducible_factorization_resultreconstructsecondrealdecode))) /\ ((ge_second_rp_irreducible_factorization_resultreconstruct) + ge_balance_negative_irreducible_factorization_resultreconstructsecondreal = (ge_second_rn_irreducible_factorization_resultreconstruct) + ge_balance_positive_irreducible_factorization_resultreconstructsecondreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultreconstructsecondimaginary ge_balance_negative_irreducible_factorization_resultreconstructsecondimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultreconstructsecond) = 2 * (ge_balance_positive_irreducible_factorization_resultreconstructsecondimaginary) /\ (ge_balance_negative_irreducible_factorization_resultreconstructsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultreconstructsecond) = 2 * ge_signed_half_irreducible_factorization_resultreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultreconstructsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultreconstructsecondimaginary) = S ge_signed_half_irreducible_factorization_resultreconstructsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_factorization_resultreconstruct) + ge_balance_negative_irreducible_factorization_resultreconstructsecondimaginary = (ge_second_in_irreducible_factorization_resultreconstruct) + ge_balance_positive_irreducible_factorization_resultreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_factorization_resultreconstructoutput ge_representation_imaginary_code_irreducible_factorization_resultreconstructoutput. (((z) = ((ge_representation_real_code_irreducible_factorization_resultreconstructoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructoutput)) * S ((ge_representation_real_code_irreducible_factorization_resultreconstructoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructoutput)) + ((ge_representation_imaginary_code_irreducible_factorization_resultreconstructoutput) + (ge_representation_imaginary_code_irreducible_factorization_resultreconstructoutput))) /\ ((exists ge_balance_positive_irreducible_factorization_resultreconstructoutputreal ge_balance_negative_irreducible_factorization_resultreconstructoutputreal. (((((ge_representation_real_code_irreducible_factorization_resultreconstructoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultreconstructoutputreal) /\ (ge_balance_negative_irreducible_factorization_resultreconstructoutputreal) = 0) \/ exists ge_signed_half_irreducible_factorization_resultreconstructoutputrealdecode. (((ge_representation_real_code_irreducible_factorization_resultreconstructoutput) = 2 * ge_signed_half_irreducible_factorization_resultreconstructoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultreconstructoutputreal) = 0) /\ (ge_balance_negative_irreducible_factorization_resultreconstructoutputreal) = S ge_signed_half_irreducible_factorization_resultreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultreconstruct) * (ge_second_rp_irreducible_factorization_resultreconstruct))) + (((ge_first_rn_irreducible_factorization_resultreconstruct) * (ge_second_rn_irreducible_factorization_resultreconstruct))))) + (((((ge_first_ip_irreducible_factorization_resultreconstruct) * (ge_second_in_irreducible_factorization_resultreconstruct))) + (((ge_first_in_irreducible_factorization_resultreconstruct) * (ge_second_ip_irreducible_factorization_resultreconstruct))))))) + ge_balance_negative_irreducible_factorization_resultreconstructoutputreal = (((((((ge_first_rp_irreducible_factorization_resultreconstruct) * (ge_second_rn_irreducible_factorization_resultreconstruct))) + (((ge_first_rn_irreducible_factorization_resultreconstruct) * (ge_second_rp_irreducible_factorization_resultreconstruct))))) + (((((ge_first_ip_irreducible_factorization_resultreconstruct) * (ge_second_ip_irreducible_factorization_resultreconstruct))) + (((ge_first_in_irreducible_factorization_resultreconstruct) * (ge_second_in_irreducible_factorization_resultreconstruct))))))) + ge_balance_positive_irreducible_factorization_resultreconstructoutputreal))) /\ (exists ge_balance_positive_irreducible_factorization_resultreconstructoutputimaginary ge_balance_negative_irreducible_factorization_resultreconstructoutputimaginary. (((((ge_representation_imaginary_code_irreducible_factorization_resultreconstructoutput) = 2 * (ge_balance_positive_irreducible_factorization_resultreconstructoutputimaginary) /\ (ge_balance_negative_irreducible_factorization_resultreconstructoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_factorization_resultreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_factorization_resultreconstructoutput) = 2 * ge_signed_half_irreducible_factorization_resultreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_factorization_resultreconstructoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_factorization_resultreconstructoutputimaginary) = S ge_signed_half_irreducible_factorization_resultreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_factorization_resultreconstruct) * (ge_second_ip_irreducible_factorization_resultreconstruct))) + (((ge_first_rn_irreducible_factorization_resultreconstruct) * (ge_second_in_irreducible_factorization_resultreconstruct))))) + (((((ge_first_ip_irreducible_factorization_resultreconstruct) * (ge_second_rp_irreducible_factorization_resultreconstruct))) + (((ge_first_in_irreducible_factorization_resultreconstruct) * (ge_second_rn_irreducible_factorization_resultreconstruct))))))) + ge_balance_negative_irreducible_factorization_resultreconstructoutputimaginary = (((((((ge_first_rp_irreducible_factorization_resultreconstruct) * (ge_second_in_irreducible_factorization_resultreconstruct))) + (((ge_first_rn_irreducible_factorization_resultreconstruct) * (ge_second_ip_irreducible_factorization_resultreconstruct))))) + (((((ge_first_ip_irreducible_factorization_resultreconstruct) * (ge_second_rn_irreducible_factorization_resultreconstruct))) + (((ge_first_in_irreducible_factorization_resultreconstruct) * (ge_second_rp_irreducible_factorization_resultreconstruct))))))) + ge_balance_positive_irreducible_factorization_resultreconstructoutputimaginary))))))))))))))