gaussian_irreducible_divisor_bounded_norm

Exact expanded first-order arithmetic statement

forall k z N. (exists ge_gap_prime_divisor_bound. ge_gap_prime_divisor_bound + (N) = (k)) -> (exists ge_norm_rp_prime_divisor_norm ge_norm_rn_prime_divisor_norm ge_norm_ip_prime_divisor_norm ge_norm_in_prime_divisor_norm. ((exists ge_representation_real_code_prime_divisor_normrepresentation ge_representation_imaginary_code_prime_divisor_normrepresentation. (((z) = ((ge_representation_real_code_prime_divisor_normrepresentation) + (ge_representation_imaginary_code_prime_divisor_normrepresentation)) * S ((ge_representation_real_code_prime_divisor_normrepresentation) + (ge_representation_imaginary_code_prime_divisor_normrepresentation)) + ((ge_representation_imaginary_code_prime_divisor_normrepresentation) + (ge_representation_imaginary_code_prime_divisor_normrepresentation))) /\ ((exists ge_balance_positive_prime_divisor_normrepresentationreal ge_balance_negative_prime_divisor_normrepresentationreal. (((((ge_representation_real_code_prime_divisor_normrepresentation) = 2 * (ge_balance_positive_prime_divisor_normrepresentationreal) /\ (ge_balance_negative_prime_divisor_normrepresentationreal) = 0) \/ exists ge_signed_half_prime_divisor_normrepresentationrealdecode. (((ge_representation_real_code_prime_divisor_normrepresentation) = 2 * ge_signed_half_prime_divisor_normrepresentationrealdecode + 1 /\ (ge_balance_positive_prime_divisor_normrepresentationreal) = 0) /\ (ge_balance_negative_prime_divisor_normrepresentationreal) = S ge_signed_half_prime_divisor_normrepresentationrealdecode))) /\ ((ge_norm_rp_prime_divisor_norm) + ge_balance_negative_prime_divisor_normrepresentationreal = (ge_norm_rn_prime_divisor_norm) + ge_balance_positive_prime_divisor_normrepresentationreal))) /\ (exists ge_balance_positive_prime_divisor_normrepresentationimaginary ge_balance_negative_prime_divisor_normrepresentationimaginary. (((((ge_representation_imaginary_code_prime_divisor_normrepresentation) = 2 * (ge_balance_positive_prime_divisor_normrepresentationimaginary) /\ (ge_balance_negative_prime_divisor_normrepresentationimaginary) = 0) \/ exists ge_signed_half_prime_divisor_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_normrepresentation) = 2 * ge_signed_half_prime_divisor_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_normrepresentationimaginary) = 0) /\ (ge_balance_negative_prime_divisor_normrepresentationimaginary) = S ge_signed_half_prime_divisor_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_prime_divisor_norm) + ge_balance_negative_prime_divisor_normrepresentationimaginary = (ge_norm_in_prime_divisor_norm) + ge_balance_positive_prime_divisor_normrepresentationimaginary)))))) /\ (exists ge_real_square_prime_divisor_normsquare ge_imaginary_square_prime_divisor_normsquare. ((((((ge_norm_rp_prime_divisor_norm) * (ge_norm_rp_prime_divisor_norm))) + (((ge_norm_rn_prime_divisor_norm) * (ge_norm_rn_prime_divisor_norm)))) = ((ge_real_square_prime_divisor_normsquare) + (((((ge_norm_rp_prime_divisor_norm) * (ge_norm_rn_prime_divisor_norm))) + (((ge_norm_rn_prime_divisor_norm) * (ge_norm_rp_prime_divisor_norm))))))) /\ ((((((ge_norm_ip_prime_divisor_norm) * (ge_norm_ip_prime_divisor_norm))) + (((ge_norm_in_prime_divisor_norm) * (ge_norm_in_prime_divisor_norm)))) = ((ge_imaginary_square_prime_divisor_normsquare) + (((((ge_norm_ip_prime_divisor_norm) * (ge_norm_in_prime_divisor_norm))) + (((ge_norm_in_prime_divisor_norm) * (ge_norm_ip_prime_divisor_norm))))))) /\ ((N) = ge_real_square_prime_divisor_normsquare + ge_imaginary_square_prime_divisor_normsquare)))))) -> ~(z=0) -> ~(exists gr_inverse_prime_divisor_nonunit. (exists ge_first_rp_prime_divisor_nonunitidentity ge_first_rn_prime_divisor_nonunitidentity ge_first_ip_prime_divisor_nonunitidentity ge_first_in_prime_divisor_nonunitidentity ge_second_rp_prime_divisor_nonunitidentity ge_second_rn_prime_divisor_nonunitidentity ge_second_ip_prime_divisor_nonunitidentity ge_second_in_prime_divisor_nonunitidentity. ((exists ge_representation_real_code_prime_divisor_nonunitidentityfirst ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst. (((z) = ((ge_representation_real_code_prime_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst)) * S ((ge_representation_real_code_prime_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_divisor_nonunitidentityfirstreal ge_balance_negative_prime_divisor_nonunitidentityfirstreal. (((((ge_representation_real_code_prime_divisor_nonunitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_nonunitidentityfirstreal) /\ (ge_balance_negative_prime_divisor_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_divisor_nonunitidentityfirst) = 2 * ge_signed_half_prime_divisor_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentityfirstreal) = S ge_signed_half_prime_divisor_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_divisor_nonunitidentity) + ge_balance_negative_prime_divisor_nonunitidentityfirstreal = (ge_first_rn_prime_divisor_nonunitidentity) + ge_balance_positive_prime_divisor_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_divisor_nonunitidentityfirstimaginary ge_balance_negative_prime_divisor_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst) = 2 * (ge_balance_positive_prime_divisor_nonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_divisor_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_nonunitidentityfirst) = 2 * ge_signed_half_prime_divisor_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentityfirstimaginary) = S ge_signed_half_prime_divisor_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisor_nonunitidentity) + ge_balance_negative_prime_divisor_nonunitidentityfirstimaginary = (ge_first_in_prime_divisor_nonunitidentity) + ge_balance_positive_prime_divisor_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisor_nonunitidentitysecond ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond. (((gr_inverse_prime_divisor_nonunit) = ((ge_representation_real_code_prime_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond)) * S ((ge_representation_real_code_prime_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond) + (ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_divisor_nonunitidentitysecondreal ge_balance_negative_prime_divisor_nonunitidentitysecondreal. (((((ge_representation_real_code_prime_divisor_nonunitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_nonunitidentitysecondreal) /\ (ge_balance_negative_prime_divisor_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_divisor_nonunitidentitysecond) = 2 * ge_signed_half_prime_divisor_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentitysecondreal) = S ge_signed_half_prime_divisor_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_divisor_nonunitidentity) + ge_balance_negative_prime_divisor_nonunitidentitysecondreal = (ge_second_rn_prime_divisor_nonunitidentity) + ge_balance_positive_prime_divisor_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_divisor_nonunitidentitysecondimaginary ge_balance_negative_prime_divisor_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond) = 2 * (ge_balance_positive_prime_divisor_nonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_divisor_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_nonunitidentitysecond) = 2 * ge_signed_half_prime_divisor_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentitysecondimaginary) = S ge_signed_half_prime_divisor_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_divisor_nonunitidentity) + ge_balance_negative_prime_divisor_nonunitidentitysecondimaginary = (ge_second_in_prime_divisor_nonunitidentity) + ge_balance_positive_prime_divisor_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisor_nonunitidentityoutput ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput)) * S ((ge_representation_real_code_prime_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput) + (ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_divisor_nonunitidentityoutputreal ge_balance_negative_prime_divisor_nonunitidentityoutputreal. (((((ge_representation_real_code_prime_divisor_nonunitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_nonunitidentityoutputreal) /\ (ge_balance_negative_prime_divisor_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_divisor_nonunitidentityoutput) = 2 * ge_signed_half_prime_divisor_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentityoutputreal) = S ge_signed_half_prime_divisor_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisor_nonunitidentity) * (ge_second_rp_prime_divisor_nonunitidentity))) + (((ge_first_rn_prime_divisor_nonunitidentity) * (ge_second_rn_prime_divisor_nonunitidentity))))) + (((((ge_first_ip_prime_divisor_nonunitidentity) * (ge_second_in_prime_divisor_nonunitidentity))) + (((ge_first_in_prime_divisor_nonunitidentity) * (ge_second_ip_prime_divisor_nonunitidentity))))))) + ge_balance_negative_prime_divisor_nonunitidentityoutputreal = (((((((ge_first_rp_prime_divisor_nonunitidentity) * (ge_second_rn_prime_divisor_nonunitidentity))) + (((ge_first_rn_prime_divisor_nonunitidentity) * (ge_second_rp_prime_divisor_nonunitidentity))))) + (((((ge_first_ip_prime_divisor_nonunitidentity) * (ge_second_ip_prime_divisor_nonunitidentity))) + (((ge_first_in_prime_divisor_nonunitidentity) * (ge_second_in_prime_divisor_nonunitidentity))))))) + ge_balance_positive_prime_divisor_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_divisor_nonunitidentityoutputimaginary ge_balance_negative_prime_divisor_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput) = 2 * (ge_balance_positive_prime_divisor_nonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_divisor_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisor_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisor_nonunitidentityoutput) = 2 * ge_signed_half_prime_divisor_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisor_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisor_nonunitidentityoutputimaginary) = S ge_signed_half_prime_divisor_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisor_nonunitidentity) * (ge_second_ip_prime_divisor_nonunitidentity))) + (((ge_first_rn_prime_divisor_nonunitidentity) * (ge_second_in_prime_divisor_nonunitidentity))))) + (((((ge_first_ip_prime_divisor_nonunitidentity) * (ge_second_rp_prime_divisor_nonunitidentity))) + (((ge_first_in_prime_divisor_nonunitidentity) * (ge_second_rn_prime_divisor_nonunitidentity))))))) + ge_balance_negative_prime_divisor_nonunitidentityoutputimaginary = (((((((ge_first_rp_prime_divisor_nonunitidentity) * (ge_second_in_prime_divisor_nonunitidentity))) + (((ge_first_rn_prime_divisor_nonunitidentity) * (ge_second_ip_prime_divisor_nonunitidentity))))) + (((((ge_first_ip_prime_divisor_nonunitidentity) * (ge_second_rn_prime_divisor_nonunitidentity))) + (((ge_first_in_prime_divisor_nonunitidentity) * (ge_second_rp_prime_divisor_nonunitidentity))))))) + ge_balance_positive_prime_divisor_nonunitidentityoutputimaginary)))))))))) -> (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))))))))))))