gaussian_irreducible_divisor_exists

Exact expanded first-order arithmetic statement

forall z. (exists ge_real_positive_prime_divisor_domain ge_real_negative_prime_divisor_domain ge_imaginary_positive_prime_divisor_domain ge_imaginary_negative_prime_divisor_domain. (exists ge_real_code_prime_divisor_domaindecode ge_imaginary_code_prime_divisor_domaindecode. (((z) = ((ge_real_code_prime_divisor_domaindecode) + (ge_imaginary_code_prime_divisor_domaindecode)) * S ((ge_real_code_prime_divisor_domaindecode) + (ge_imaginary_code_prime_divisor_domaindecode)) + ((ge_imaginary_code_prime_divisor_domaindecode) + (ge_imaginary_code_prime_divisor_domaindecode))) /\ (((((ge_real_code_prime_divisor_domaindecode) = 2 * (ge_real_positive_prime_divisor_domain) /\ (ge_real_negative_prime_divisor_domain) = 0) \/ exists ge_signed_half_ge_prime_divisor_domaindecode_real. (((ge_real_code_prime_divisor_domaindecode) = 2 * ge_signed_half_ge_prime_divisor_domaindecode_real + 1 /\ (ge_real_positive_prime_divisor_domain) = 0) /\ (ge_real_negative_prime_divisor_domain) = S ge_signed_half_ge_prime_divisor_domaindecode_real))) /\ ((((ge_imaginary_code_prime_divisor_domaindecode) = 2 * (ge_imaginary_positive_prime_divisor_domain) /\ (ge_imaginary_negative_prime_divisor_domain) = 0) \/ exists ge_signed_half_ge_prime_divisor_domaindecode_imaginary. (((ge_imaginary_code_prime_divisor_domaindecode) = 2 * ge_signed_half_ge_prime_divisor_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_prime_divisor_domain) = 0) /\ (ge_imaginary_negative_prime_divisor_domain) = S ge_signed_half_ge_prime_divisor_domaindecode_imaginary))))))) -> ~(z=0) -> ~(exists gr_inverse_prime_divisor_not_unit. (exists ge_first_rp_prime_divisor_not_unitidentity ge_first_rn_prime_divisor_not_unitidentity ge_first_ip_prime_divisor_not_unitidentity ge_first_in_prime_divisor_not_unitidentity ge_second_rp_prime_divisor_not_unitidentity ge_second_rn_prime_divisor_not_unitidentity ge_second_ip_prime_divisor_not_unitidentity ge_second_in_prime_divisor_not_unitidentity. ((exists ge_representation_real_code_prime_divisor_not_unitidentityfirst ge_representation_imaginary_code_prime_divisor_not_unitidentityfirst. (((z) = ((ge_representation_real_code_prime_divisor_not_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_not_unitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_not_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_not_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_not_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_not_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_not_unitidentityfirstreal ge_balance_negative_prime_divisor_not_unitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_not_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_not_unitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_not_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_not_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_not_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_not_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_not_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_not_unitidentityfirstreal) = S ge_signed_half_prime_divisor_not_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_not_unitidentity) + ge_balance_negative_prime_divisor_not_unitidentityfirstreal = (ge_first_rn_prime_divisor_not_unitidentity) + ge_balance_positive_prime_divisor_not_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_not_unitidentityfirstimaginary ge_balance_negative_prime_divisor_not_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_not_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_not_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_not_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_not_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_not_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_not_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_not_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_not_unitidentityfirstimaginary) = S ge_signed_half_prime_divisor_not_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_not_unitidentity) + ge_balance_negative_prime_divisor_not_unitidentityfirstimaginary = (ge_first_in_prime_divisor_not_unitidentity) + ge_balance_positive_prime_divisor_not_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_not_unitidentitysecond ge_representation_imaginary_code_prime_divisor_not_unitidentitysecond. (((gr_inverse_prime_divisor_not_unit) = ((ge_representation_real_code_prime_divisor_not_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_not_unitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_not_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_not_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_not_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_not_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_not_unitidentitysecondreal ge_balance_negative_prime_divisor_not_unitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_not_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_not_unitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_not_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_not_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_not_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_not_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_not_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_not_unitidentitysecondreal) = S ge_signed_half_prime_divisor_not_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_not_unitidentity) + ge_balance_negative_prime_divisor_not_unitidentitysecondreal = (ge_second_rn_prime_divisor_not_unitidentity) + ge_balance_positive_prime_divisor_not_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_not_unitidentitysecondimaginary ge_balance_negative_prime_divisor_not_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_not_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_not_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_not_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_not_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_not_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_not_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_not_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_not_unitidentitysecondimaginary) = S ge_signed_half_prime_divisor_not_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_not_unitidentity) + ge_balance_negative_prime_divisor_not_unitidentitysecondimaginary = (ge_second_in_prime_divisor_not_unitidentity) + ge_balance_positive_prime_divisor_not_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_not_unitidentityoutput ge_representation_imaginary_code_prime_divisor_not_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_not_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_not_unitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_not_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_not_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_not_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_not_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_not_unitidentityoutputreal ge_balance_negative_prime_divisor_not_unitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_not_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_not_unitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_not_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_not_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_not_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_not_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_not_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_not_unitidentityoutputreal) = S ge_signed_half_prime_divisor_not_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_not_unitidentity) * (ge_second_rp_prime_divisor_not_unitidentity))) + (((ge_first_rn_prime_divisor_not_unitidentity) * (ge_second_rn_prime_divisor_not_unitidentity))))) + (((((ge_first_ip_prime_divisor_not_unitidentity) * (ge_second_in_prime_divisor_not_unitidentity))) + (((ge_first_in_prime_divisor_not_unitidentity) * (ge_second_ip_prime_divisor_not_unitidentity))))))) + ge_balance_negative_prime_divisor_not_unitidentityoutputreal = (((((((ge_first_rp_prime_divisor_not_unitidentity) * (ge_second_rn_prime_divisor_not_unitidentity))) + (((ge_first_rn_prime_divisor_not_unitidentity) * (ge_second_rp_prime_divisor_not_unitidentity))))) + (((((ge_first_ip_prime_divisor_not_unitidentity) * (ge_second_ip_prime_divisor_not_unitidentity))) + (((ge_first_in_prime_divisor_not_unitidentity) * (ge_second_in_prime_divisor_not_unitidentity))))))) + ge_balance_positive_prime_divisor_not_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_not_unitidentityoutputimaginary ge_balance_negative_prime_divisor_not_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_not_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_not_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_not_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_not_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_not_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_not_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_not_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_not_unitidentityoutputimaginary) = S ge_signed_half_prime_divisor_not_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_not_unitidentity) * (ge_second_ip_prime_divisor_not_unitidentity))) + (((ge_first_rn_prime_divisor_not_unitidentity) * (ge_second_in_prime_divisor_not_unitidentity))))) + (((((ge_first_ip_prime_divisor_not_unitidentity) * (ge_second_rp_prime_divisor_not_unitidentity))) + (((ge_first_in_prime_divisor_not_unitidentity) * (ge_second_rn_prime_divisor_not_unitidentity))))))) + ge_balance_negative_prime_divisor_not_unitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_not_unitidentity) * (ge_second_in_prime_divisor_not_unitidentity))) + (((ge_first_rn_prime_divisor_not_unitidentity) * (ge_second_ip_prime_divisor_not_unitidentity))))) + (((((ge_first_ip_prime_divisor_not_unitidentity) * (ge_second_rn_prime_divisor_not_unitidentity))) + (((ge_first_in_prime_divisor_not_unitidentity) * (ge_second_rp_prime_divisor_not_unitidentity))))))) + ge_balance_positive_prime_divisor_not_unitidentityoutputimaginary)))))))))) -> (exists p. ((((exists ge_real_positive_prime_divisor_resultirreduciblecarrier ge_real_negative_prime_divisor_resultirreduciblecarrier ge_imaginary_positive_prime_divisor_resultirreduciblecarrier ge_imaginary_negative_prime_divisor_resultirreduciblecarrier. (exists ge_real_code_prime_divisor_resultirreduciblecarrierdecode ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode. (((p) = ((ge_real_code_prime_divisor_resultirreduciblecarrierdecode) + (ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode)) * S ((ge_real_code_prime_divisor_resultirreduciblecarrierdecode) + (ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode)) + ((ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode) + (ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode))) /\ (((((ge_real_code_prime_divisor_resultirreduciblecarrierdecode) = 2 * (ge_real_positive_prime_divisor_resultirreduciblecarrier) /\ (ge_real_negative_prime_divisor_resultirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_real. (((ge_real_code_prime_divisor_resultirreduciblecarrierdecode) = 2 * ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_prime_divisor_resultirreduciblecarrier) = 0) /\ (ge_real_negative_prime_divisor_resultirreduciblecarrier) = S ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_prime_divisor_resultirreduciblecarrier) /\ (ge_imaginary_negative_prime_divisor_resultirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_prime_divisor_resultirreduciblecarrierdecode) = 2 * ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_divisor_resultirreduciblecarrier) = 0) /\ (ge_imaginary_negative_prime_divisor_resultirreduciblecarrier) = S ge_signed_half_ge_prime_divisor_resultirreduciblecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_prime_divisor_resultirreduciblenonunit. (exists ge_first_rp_prime_divisor_resultirreduciblenonunitidentity ge_first_rn_prime_divisor_resultirreduciblenonunitidentity ge_first_ip_prime_divisor_resultirreduciblenonunitidentity ge_first_in_prime_divisor_resultirreduciblenonunitidentity ge_second_rp_prime_divisor_resultirreduciblenonunitidentity ge_second_rn_prime_divisor_resultirreduciblenonunitidentity ge_second_ip_prime_divisor_resultirreduciblenonunitidentity ge_second_in_prime_divisor_resultirreduciblenonunitidentity. ((exists ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst. (((p) = ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstreal ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstreal) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstreal = (ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstimaginary ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityfirstimaginary = (ge_first_in_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond. (((gr_inverse_prime_divisor_resultirreduciblenonunit) = ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondreal ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondreal) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondreal = (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondimaginary ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentitysecondimaginary = (ge_second_in_prime_divisor_resultirreduciblenonunitidentity) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputreal ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblenonunitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputreal) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rp_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_in_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_ip_prime_divisor_resultirreduciblenonunitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rp_prime_divisor_resultirreduciblenonunitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_ip_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_in_prime_divisor_resultirreduciblenonunitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputimaginary ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblenonunitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_prime_divisor_resultirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_ip_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_in_prime_divisor_resultirreduciblenonunitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rp_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_in_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_ip_prime_divisor_resultirreduciblenonunitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rn_prime_divisor_resultirreduciblenonunitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblenonunitidentity) * (ge_second_rp_prime_divisor_resultirreduciblenonunitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_divisor_resultirreducible gr_second_factor_prime_divisor_resultirreducible. (exists ge_first_rp_prime_divisor_resultirreduciblefactorization ge_first_rn_prime_divisor_resultirreduciblefactorization ge_first_ip_prime_divisor_resultirreduciblefactorization ge_first_in_prime_divisor_resultirreduciblefactorization ge_second_rp_prime_divisor_resultirreduciblefactorization ge_second_rn_prime_divisor_resultirreduciblefactorization ge_second_ip_prime_divisor_resultirreduciblefactorization ge_second_in_prime_divisor_resultirreduciblefactorization. ((exists ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst. (((gr_first_factor_prime_divisor_resultirreducible) = ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstreal ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstreal) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultirreduciblefactorization) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstreal = (ge_first_rn_prime_divisor_resultirreduciblefactorization) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstimaginary ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultirreduciblefactorization) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationfirstimaginary = (ge_first_in_prime_divisor_resultirreduciblefactorization) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond. (((gr_second_factor_prime_divisor_resultirreducible) = ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondreal ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationsecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondreal) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultirreduciblefactorization) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondreal = (ge_second_rn_prime_divisor_resultirreduciblefactorization) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondimaginary ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationsecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultirreduciblefactorization) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationsecondimaginary = (ge_second_in_prime_divisor_resultirreduciblefactorization) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput. (((p) = ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputreal ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefactorizationoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputreal) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblefactorization) * (ge_second_rp_prime_divisor_resultirreduciblefactorization))) + (((ge_first_rn_prime_divisor_resultirreduciblefactorization) * (ge_second_rn_prime_divisor_resultirreduciblefactorization))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefactorization) * (ge_second_in_prime_divisor_resultirreduciblefactorization))) + (((ge_first_in_prime_divisor_resultirreduciblefactorization) * (ge_second_ip_prime_divisor_resultirreduciblefactorization))))))) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputreal = (((((((ge_first_rp_prime_divisor_resultirreduciblefactorization) * (ge_second_rn_prime_divisor_resultirreduciblefactorization))) + (((ge_first_rn_prime_divisor_resultirreduciblefactorization) * (ge_second_rp_prime_divisor_resultirreduciblefactorization))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefactorization) * (ge_second_ip_prime_divisor_resultirreduciblefactorization))) + (((ge_first_in_prime_divisor_resultirreduciblefactorization) * (ge_second_in_prime_divisor_resultirreduciblefactorization))))))) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputimaginary ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefactorizationoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblefactorization) * (ge_second_ip_prime_divisor_resultirreduciblefactorization))) + (((ge_first_rn_prime_divisor_resultirreduciblefactorization) * (ge_second_in_prime_divisor_resultirreduciblefactorization))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefactorization) * (ge_second_rp_prime_divisor_resultirreduciblefactorization))) + (((ge_first_in_prime_divisor_resultirreduciblefactorization) * (ge_second_rn_prime_divisor_resultirreduciblefactorization))))))) + ge_balance_negative_prime_divisor_resultirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_prime_divisor_resultirreduciblefactorization) * (ge_second_in_prime_divisor_resultirreduciblefactorization))) + (((ge_first_rn_prime_divisor_resultirreduciblefactorization) * (ge_second_ip_prime_divisor_resultirreduciblefactorization))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefactorization) * (ge_second_rn_prime_divisor_resultirreduciblefactorization))) + (((ge_first_in_prime_divisor_resultirreduciblefactorization) * (ge_second_rp_prime_divisor_resultirreduciblefactorization))))))) + ge_balance_positive_prime_divisor_resultirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_prime_divisor_resultirreduciblefirst_unit. (exists ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity. ((exists ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst. (((gr_first_factor_prime_divisor_resultirreducible) = ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstreal ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstreal = (ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond. (((gr_inverse_prime_divisor_resultirreduciblefirst_unit) = ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondreal ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondreal = (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputreal ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblefirst_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblefirst_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblefirst_unitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_prime_divisor_resultirreduciblesecond_unit. (exists ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity. ((exists ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst. (((gr_second_factor_prime_divisor_resultirreducible) = ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstreal ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstreal = (ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond. (((gr_inverse_prime_divisor_resultirreduciblesecond_unit) = ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondreal ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondreal = (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputreal ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity))))))) + ge_balance_negative_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_in_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_rn_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_ip_prime_divisor_resultirreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rn_prime_divisor_resultirreduciblesecond_unitidentity))) + (((ge_first_in_prime_divisor_resultirreduciblesecond_unitidentity) * (ge_second_rp_prime_divisor_resultirreduciblesecond_unitidentity))))))) + ge_balance_positive_prime_divisor_resultirreduciblesecond_unitidentityoutputimaginary))))))))))))))) /\ (exists gr_quotient_prime_divisor_resultdivisor. (exists ge_first_rp_prime_divisor_resultdivisorproduct ge_first_rn_prime_divisor_resultdivisorproduct ge_first_ip_prime_divisor_resultdivisorproduct ge_first_in_prime_divisor_resultdivisorproduct ge_second_rp_prime_divisor_resultdivisorproduct ge_second_rn_prime_divisor_resultdivisorproduct ge_second_ip_prime_divisor_resultdivisorproduct ge_second_in_prime_divisor_resultdivisorproduct. ((exists ge_representation_real_code_prime_divisor_resultdivisorproductfirst ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst. (((p) = ((ge_representation_real_code_prime_divisor_resultdivisorproductfirst) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst)) * S ((ge_representation_real_code_prime_divisor_resultdivisorproductfirst) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst)) + ((ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst))) /\ ((exists ge_balance_positive_prime_divisor_resultdivisorproductfirstreal ge_balance_negative_prime_divisor_resultdivisorproductfirstreal. (((((ge_representation_real_code_prime_divisor_resultdivisorproductfirst) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductfirstreal) /\ (ge_balance_negative_prime_divisor_resultdivisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductfirstrealdecode. (((ge_representation_real_code_prime_divisor_resultdivisorproductfirst) = 2 * ge_signed_half_prime_divisor_resultdivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductfirstreal) = S ge_signed_half_prime_divisor_resultdivisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_resultdivisorproduct) + ge_balance_negative_prime_divisor_resultdivisorproductfirstreal = (ge_first_rn_prime_divisor_resultdivisorproduct) + ge_balance_positive_prime_divisor_resultdivisorproductfirstreal))) /\ (exists ge_balance_positive_prime_divisor_resultdivisorproductfirstimaginary ge_balance_negative_prime_divisor_resultdivisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductfirstimaginary) /\ (ge_balance_negative_prime_divisor_resultdivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultdivisorproductfirst) = 2 * ge_signed_half_prime_divisor_resultdivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductfirstimaginary) = S ge_signed_half_prime_divisor_resultdivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_resultdivisorproduct) + ge_balance_negative_prime_divisor_resultdivisorproductfirstimaginary = (ge_first_in_prime_divisor_resultdivisorproduct) + ge_balance_positive_prime_divisor_resultdivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_resultdivisorproductsecond ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond. (((gr_quotient_prime_divisor_resultdivisor) = ((ge_representation_real_code_prime_divisor_resultdivisorproductsecond) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond)) * S ((ge_representation_real_code_prime_divisor_resultdivisorproductsecond) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond)) + ((ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond))) /\ ((exists ge_balance_positive_prime_divisor_resultdivisorproductsecondreal ge_balance_negative_prime_divisor_resultdivisorproductsecondreal. (((((ge_representation_real_code_prime_divisor_resultdivisorproductsecond) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductsecondreal) /\ (ge_balance_negative_prime_divisor_resultdivisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductsecondrealdecode. (((ge_representation_real_code_prime_divisor_resultdivisorproductsecond) = 2 * ge_signed_half_prime_divisor_resultdivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductsecondreal) = S ge_signed_half_prime_divisor_resultdivisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_divisor_resultdivisorproduct) + ge_balance_negative_prime_divisor_resultdivisorproductsecondreal = (ge_second_rn_prime_divisor_resultdivisorproduct) + ge_balance_positive_prime_divisor_resultdivisorproductsecondreal))) /\ (exists ge_balance_positive_prime_divisor_resultdivisorproductsecondimaginary ge_balance_negative_prime_divisor_resultdivisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductsecondimaginary) /\ (ge_balance_negative_prime_divisor_resultdivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultdivisorproductsecond) = 2 * ge_signed_half_prime_divisor_resultdivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductsecondimaginary) = S ge_signed_half_prime_divisor_resultdivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_resultdivisorproduct) + ge_balance_negative_prime_divisor_resultdivisorproductsecondimaginary = (ge_second_in_prime_divisor_resultdivisorproduct) + ge_balance_positive_prime_divisor_resultdivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_resultdivisorproductoutput ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput. (((z) = ((ge_representation_real_code_prime_divisor_resultdivisorproductoutput) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput)) * S ((ge_representation_real_code_prime_divisor_resultdivisorproductoutput) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput)) + ((ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput) + (ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput))) /\ ((exists ge_balance_positive_prime_divisor_resultdivisorproductoutputreal ge_balance_negative_prime_divisor_resultdivisorproductoutputreal. (((((ge_representation_real_code_prime_divisor_resultdivisorproductoutput) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductoutputreal) /\ (ge_balance_negative_prime_divisor_resultdivisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductoutputrealdecode. (((ge_representation_real_code_prime_divisor_resultdivisorproductoutput) = 2 * ge_signed_half_prime_divisor_resultdivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductoutputreal) = S ge_signed_half_prime_divisor_resultdivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_resultdivisorproduct) * (ge_second_rp_prime_divisor_resultdivisorproduct))) + (((ge_first_rn_prime_divisor_resultdivisorproduct) * (ge_second_rn_prime_divisor_resultdivisorproduct))))) + (((((ge_first_ip_prime_divisor_resultdivisorproduct) * (ge_second_in_prime_divisor_resultdivisorproduct))) + (((ge_first_in_prime_divisor_resultdivisorproduct) * (ge_second_ip_prime_divisor_resultdivisorproduct))))))) + ge_balance_negative_prime_divisor_resultdivisorproductoutputreal = (((((((ge_first_rp_prime_divisor_resultdivisorproduct) * (ge_second_rn_prime_divisor_resultdivisorproduct))) + (((ge_first_rn_prime_divisor_resultdivisorproduct) * (ge_second_rp_prime_divisor_resultdivisorproduct))))) + (((((ge_first_ip_prime_divisor_resultdivisorproduct) * (ge_second_ip_prime_divisor_resultdivisorproduct))) + (((ge_first_in_prime_divisor_resultdivisorproduct) * (ge_second_in_prime_divisor_resultdivisorproduct))))))) + ge_balance_positive_prime_divisor_resultdivisorproductoutputreal))) /\ (exists ge_balance_positive_prime_divisor_resultdivisorproductoutputimaginary ge_balance_negative_prime_divisor_resultdivisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput) = 2 * (ge_balance_positive_prime_divisor_resultdivisorproductoutputimaginary) /\ (ge_balance_negative_prime_divisor_resultdivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_resultdivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_resultdivisorproductoutput) = 2 * ge_signed_half_prime_divisor_resultdivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_resultdivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_resultdivisorproductoutputimaginary) = S ge_signed_half_prime_divisor_resultdivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_resultdivisorproduct) * (ge_second_ip_prime_divisor_resultdivisorproduct))) + (((ge_first_rn_prime_divisor_resultdivisorproduct) * (ge_second_in_prime_divisor_resultdivisorproduct))))) + (((((ge_first_ip_prime_divisor_resultdivisorproduct) * (ge_second_rp_prime_divisor_resultdivisorproduct))) + (((ge_first_in_prime_divisor_resultdivisorproduct) * (ge_second_rn_prime_divisor_resultdivisorproduct))))))) + ge_balance_negative_prime_divisor_resultdivisorproductoutputimaginary = (((((((ge_first_rp_prime_divisor_resultdivisorproduct) * (ge_second_in_prime_divisor_resultdivisorproduct))) + (((ge_first_rn_prime_divisor_resultdivisorproduct) * (ge_second_ip_prime_divisor_resultdivisorproduct))))) + (((((ge_first_ip_prime_divisor_resultdivisorproduct) * (ge_second_rn_prime_divisor_resultdivisorproduct))) + (((ge_first_in_prime_divisor_resultdivisorproduct) * (ge_second_rp_prime_divisor_resultdivisorproduct))))))) + ge_balance_positive_prime_divisor_resultdivisorproductoutputimaginary))))))))))))