gaussian_irreducible_factor_reduction

Exact expanded first-order arithmetic statement

forall z N. (exists ge_norm_rp_reduction_actual_norm ge_norm_rn_reduction_actual_norm ge_norm_ip_reduction_actual_norm ge_norm_in_reduction_actual_norm. ((exists ge_representation_real_code_reduction_actual_normrepresentation ge_representation_imaginary_code_reduction_actual_normrepresentation. (((z) = ((ge_representation_real_code_reduction_actual_normrepresentation) + (ge_representation_imaginary_code_reduction_actual_normrepresentation)) * S ((ge_representation_real_code_reduction_actual_normrepresentation) + (ge_representation_imaginary_code_reduction_actual_normrepresentation)) + ((ge_representation_imaginary_code_reduction_actual_normrepresentation) + (ge_representation_imaginary_code_reduction_actual_normrepresentation))) /\ ((exists ge_balance_positive_reduction_actual_normrepresentationreal ge_balance_negative_reduction_actual_normrepresentationreal. (((((ge_representation_real_code_reduction_actual_normrepresentation) = 2 * (ge_balance_positive_reduction_actual_normrepresentationreal) /\ (ge_balance_negative_reduction_actual_normrepresentationreal) = 0) \/ exists ge_signed_half_reduction_actual_normrepresentationrealdecode. (((ge_representation_real_code_reduction_actual_normrepresentation) = 2 * ge_signed_half_reduction_actual_normrepresentationrealdecode + 1 /\ (ge_balance_positive_reduction_actual_normrepresentationreal) = 0) /\ (ge_balance_negative_reduction_actual_normrepresentationreal) = S ge_signed_half_reduction_actual_normrepresentationrealdecode))) /\ ((ge_norm_rp_reduction_actual_norm) + ge_balance_negative_reduction_actual_normrepresentationreal = (ge_norm_rn_reduction_actual_norm) + ge_balance_positive_reduction_actual_normrepresentationreal))) /\ (exists ge_balance_positive_reduction_actual_normrepresentationimaginary ge_balance_negative_reduction_actual_normrepresentationimaginary. (((((ge_representation_imaginary_code_reduction_actual_normrepresentation) = 2 * (ge_balance_positive_reduction_actual_normrepresentationimaginary) /\ (ge_balance_negative_reduction_actual_normrepresentationimaginary) = 0) \/ exists ge_signed_half_reduction_actual_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_reduction_actual_normrepresentation) = 2 * ge_signed_half_reduction_actual_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_reduction_actual_normrepresentationimaginary) = 0) /\ (ge_balance_negative_reduction_actual_normrepresentationimaginary) = S ge_signed_half_reduction_actual_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_reduction_actual_norm) + ge_balance_negative_reduction_actual_normrepresentationimaginary = (ge_norm_in_reduction_actual_norm) + ge_balance_positive_reduction_actual_normrepresentationimaginary)))))) /\ (exists ge_real_square_reduction_actual_normsquare ge_imaginary_square_reduction_actual_normsquare. ((((((ge_norm_rp_reduction_actual_norm) * (ge_norm_rp_reduction_actual_norm))) + (((ge_norm_rn_reduction_actual_norm) * (ge_norm_rn_reduction_actual_norm)))) = ((ge_real_square_reduction_actual_normsquare) + (((((ge_norm_rp_reduction_actual_norm) * (ge_norm_rn_reduction_actual_norm))) + (((ge_norm_rn_reduction_actual_norm) * (ge_norm_rp_reduction_actual_norm))))))) /\ ((((((ge_norm_ip_reduction_actual_norm) * (ge_norm_ip_reduction_actual_norm))) + (((ge_norm_in_reduction_actual_norm) * (ge_norm_in_reduction_actual_norm)))) = ((ge_imaginary_square_reduction_actual_normsquare) + (((((ge_norm_ip_reduction_actual_norm) * (ge_norm_in_reduction_actual_norm))) + (((ge_norm_in_reduction_actual_norm) * (ge_norm_ip_reduction_actual_norm))))))) /\ ((N) = ge_real_square_reduction_actual_normsquare + ge_imaginary_square_reduction_actual_normsquare)))))) -> ~(z=0) -> ~(exists gr_inverse_reduction_nonunit. (exists ge_first_rp_reduction_nonunitidentity ge_first_rn_reduction_nonunitidentity ge_first_ip_reduction_nonunitidentity ge_first_in_reduction_nonunitidentity ge_second_rp_reduction_nonunitidentity ge_second_rn_reduction_nonunitidentity ge_second_ip_reduction_nonunitidentity ge_second_in_reduction_nonunitidentity. ((exists ge_representation_real_code_reduction_nonunitidentityfirst ge_representation_imaginary_code_reduction_nonunitidentityfirst. (((z) = ((ge_representation_real_code_reduction_nonunitidentityfirst) + (ge_representation_imaginary_code_reduction_nonunitidentityfirst)) * S ((ge_representation_real_code_reduction_nonunitidentityfirst) + (ge_representation_imaginary_code_reduction_nonunitidentityfirst)) + ((ge_representation_imaginary_code_reduction_nonunitidentityfirst) + (ge_representation_imaginary_code_reduction_nonunitidentityfirst))) /\ ((exists ge_balance_positive_reduction_nonunitidentityfirstreal ge_balance_negative_reduction_nonunitidentityfirstreal. (((((ge_representation_real_code_reduction_nonunitidentityfirst) = 2 * (ge_balance_positive_reduction_nonunitidentityfirstreal) /\ (ge_balance_negative_reduction_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_reduction_nonunitidentityfirstrealdecode. (((ge_representation_real_code_reduction_nonunitidentityfirst) = 2 * ge_signed_half_reduction_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_reduction_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_reduction_nonunitidentityfirstreal) = S ge_signed_half_reduction_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_reduction_nonunitidentity) + ge_balance_negative_reduction_nonunitidentityfirstreal = (ge_first_rn_reduction_nonunitidentity) + ge_balance_positive_reduction_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_reduction_nonunitidentityfirstimaginary ge_balance_negative_reduction_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_reduction_nonunitidentityfirst) = 2 * (ge_balance_positive_reduction_nonunitidentityfirstimaginary) /\ (ge_balance_negative_reduction_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_reduction_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_reduction_nonunitidentityfirst) = 2 * ge_signed_half_reduction_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_reduction_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_reduction_nonunitidentityfirstimaginary) = S ge_signed_half_reduction_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_reduction_nonunitidentity) + ge_balance_negative_reduction_nonunitidentityfirstimaginary = (ge_first_in_reduction_nonunitidentity) + ge_balance_positive_reduction_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_reduction_nonunitidentitysecond ge_representation_imaginary_code_reduction_nonunitidentitysecond. (((gr_inverse_reduction_nonunit) = ((ge_representation_real_code_reduction_nonunitidentitysecond) + (ge_representation_imaginary_code_reduction_nonunitidentitysecond)) * S ((ge_representation_real_code_reduction_nonunitidentitysecond) + (ge_representation_imaginary_code_reduction_nonunitidentitysecond)) + ((ge_representation_imaginary_code_reduction_nonunitidentitysecond) + (ge_representation_imaginary_code_reduction_nonunitidentitysecond))) /\ ((exists ge_balance_positive_reduction_nonunitidentitysecondreal ge_balance_negative_reduction_nonunitidentitysecondreal. (((((ge_representation_real_code_reduction_nonunitidentitysecond) = 2 * (ge_balance_positive_reduction_nonunitidentitysecondreal) /\ (ge_balance_negative_reduction_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_reduction_nonunitidentitysecondrealdecode. (((ge_representation_real_code_reduction_nonunitidentitysecond) = 2 * ge_signed_half_reduction_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_reduction_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_reduction_nonunitidentitysecondreal) = S ge_signed_half_reduction_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_reduction_nonunitidentity) + ge_balance_negative_reduction_nonunitidentitysecondreal = (ge_second_rn_reduction_nonunitidentity) + ge_balance_positive_reduction_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_reduction_nonunitidentitysecondimaginary ge_balance_negative_reduction_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_reduction_nonunitidentitysecond) = 2 * (ge_balance_positive_reduction_nonunitidentitysecondimaginary) /\ (ge_balance_negative_reduction_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_reduction_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_reduction_nonunitidentitysecond) = 2 * ge_signed_half_reduction_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_reduction_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_reduction_nonunitidentitysecondimaginary) = S ge_signed_half_reduction_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_reduction_nonunitidentity) + ge_balance_negative_reduction_nonunitidentitysecondimaginary = (ge_second_in_reduction_nonunitidentity) + ge_balance_positive_reduction_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_reduction_nonunitidentityoutput ge_representation_imaginary_code_reduction_nonunitidentityoutput. (((6) = ((ge_representation_real_code_reduction_nonunitidentityoutput) + (ge_representation_imaginary_code_reduction_nonunitidentityoutput)) * S ((ge_representation_real_code_reduction_nonunitidentityoutput) + (ge_representation_imaginary_code_reduction_nonunitidentityoutput)) + ((ge_representation_imaginary_code_reduction_nonunitidentityoutput) + (ge_representation_imaginary_code_reduction_nonunitidentityoutput))) /\ ((exists ge_balance_positive_reduction_nonunitidentityoutputreal ge_balance_negative_reduction_nonunitidentityoutputreal. (((((ge_representation_real_code_reduction_nonunitidentityoutput) = 2 * (ge_balance_positive_reduction_nonunitidentityoutputreal) /\ (ge_balance_negative_reduction_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_reduction_nonunitidentityoutputrealdecode. (((ge_representation_real_code_reduction_nonunitidentityoutput) = 2 * ge_signed_half_reduction_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_reduction_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_reduction_nonunitidentityoutputreal) = S ge_signed_half_reduction_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_reduction_nonunitidentity) * (ge_second_rp_reduction_nonunitidentity))) + (((ge_first_rn_reduction_nonunitidentity) * (ge_second_rn_reduction_nonunitidentity))))) + (((((ge_first_ip_reduction_nonunitidentity) * (ge_second_in_reduction_nonunitidentity))) + (((ge_first_in_reduction_nonunitidentity) * (ge_second_ip_reduction_nonunitidentity))))))) + ge_balance_negative_reduction_nonunitidentityoutputreal = (((((((ge_first_rp_reduction_nonunitidentity) * (ge_second_rn_reduction_nonunitidentity))) + (((ge_first_rn_reduction_nonunitidentity) * (ge_second_rp_reduction_nonunitidentity))))) + (((((ge_first_ip_reduction_nonunitidentity) * (ge_second_ip_reduction_nonunitidentity))) + (((ge_first_in_reduction_nonunitidentity) * (ge_second_in_reduction_nonunitidentity))))))) + ge_balance_positive_reduction_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_reduction_nonunitidentityoutputimaginary ge_balance_negative_reduction_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_reduction_nonunitidentityoutput) = 2 * (ge_balance_positive_reduction_nonunitidentityoutputimaginary) /\ (ge_balance_negative_reduction_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_reduction_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_reduction_nonunitidentityoutput) = 2 * ge_signed_half_reduction_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_reduction_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_reduction_nonunitidentityoutputimaginary) = S ge_signed_half_reduction_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_reduction_nonunitidentity) * (ge_second_ip_reduction_nonunitidentity))) + (((ge_first_rn_reduction_nonunitidentity) * (ge_second_in_reduction_nonunitidentity))))) + (((((ge_first_ip_reduction_nonunitidentity) * (ge_second_rp_reduction_nonunitidentity))) + (((ge_first_in_reduction_nonunitidentity) * (ge_second_rn_reduction_nonunitidentity))))))) + ge_balance_negative_reduction_nonunitidentityoutputimaginary = (((((((ge_first_rp_reduction_nonunitidentity) * (ge_second_in_reduction_nonunitidentity))) + (((ge_first_rn_reduction_nonunitidentity) * (ge_second_ip_reduction_nonunitidentity))))) + (((((ge_first_ip_reduction_nonunitidentity) * (ge_second_rn_reduction_nonunitidentity))) + (((ge_first_in_reduction_nonunitidentity) * (ge_second_rp_reduction_nonunitidentity))))))) + ge_balance_positive_reduction_nonunitidentityoutputimaginary)))))))))) -> exists p q Q. ((((exists ge_real_positive_reduction_irreduciblecarrier ge_real_negative_reduction_irreduciblecarrier ge_imaginary_positive_reduction_irreduciblecarrier ge_imaginary_negative_reduction_irreduciblecarrier. (exists ge_real_code_reduction_irreduciblecarrierdecode ge_imaginary_code_reduction_irreduciblecarrierdecode. (((p) = ((ge_real_code_reduction_irreduciblecarrierdecode) + (ge_imaginary_code_reduction_irreduciblecarrierdecode)) * S ((ge_real_code_reduction_irreduciblecarrierdecode) + (ge_imaginary_code_reduction_irreduciblecarrierdecode)) + ((ge_imaginary_code_reduction_irreduciblecarrierdecode) + (ge_imaginary_code_reduction_irreduciblecarrierdecode))) /\ (((((ge_real_code_reduction_irreduciblecarrierdecode) = 2 * (ge_real_positive_reduction_irreduciblecarrier) /\ (ge_real_negative_reduction_irreduciblecarrier) = 0) \/ exists ge_signed_half_ge_reduction_irreduciblecarrierdecode_real. (((ge_real_code_reduction_irreduciblecarrierdecode) = 2 * ge_signed_half_ge_reduction_irreduciblecarrierdecode_real + 1 /\ (ge_real_positive_reduction_irreduciblecarrier) = 0) /\ (ge_real_negative_reduction_irreduciblecarrier) = S ge_signed_half_ge_reduction_irreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_reduction_irreduciblecarrierdecode) = 2 * (ge_imaginary_positive_reduction_irreduciblecarrier) /\ (ge_imaginary_negative_reduction_irreduciblecarrier) = 0) \/ exists ge_signed_half_ge_reduction_irreduciblecarrierdecode_imaginary. (((ge_imaginary_code_reduction_irreduciblecarrierdecode) = 2 * ge_signed_half_ge_reduction_irreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_reduction_irreduciblecarrier) = 0) /\ (ge_imaginary_negative_reduction_irreduciblecarrier) = S ge_signed_half_ge_reduction_irreduciblecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_reduction_irreduciblenonunit. (exists ge_first_rp_reduction_irreduciblenonunitidentity ge_first_rn_reduction_irreduciblenonunitidentity ge_first_ip_reduction_irreduciblenonunitidentity ge_first_in_reduction_irreduciblenonunitidentity ge_second_rp_reduction_irreduciblenonunitidentity ge_second_rn_reduction_irreduciblenonunitidentity ge_second_ip_reduction_irreduciblenonunitidentity ge_second_in_reduction_irreduciblenonunitidentity. ((exists ge_representation_real_code_reduction_irreduciblenonunitidentityfirst ge_representation_imaginary_code_reduction_irreduciblenonunitidentityfirst. (((p) = ((ge_representation_real_code_reduction_irreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_reduction_irreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_reduction_irreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_reduction_irreduciblenonunitidentityfirstreal ge_balance_negative_reduction_irreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_reduction_irreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_reduction_irreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_reduction_irreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_reduction_irreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_reduction_irreduciblenonunitidentityfirst) = 2 * ge_signed_half_reduction_irreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_reduction_irreduciblenonunitidentityfirstreal) = S ge_signed_half_reduction_irreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_reduction_irreduciblenonunitidentity) + ge_balance_negative_reduction_irreduciblenonunitidentityfirstreal = (ge_first_rn_reduction_irreduciblenonunitidentity) + ge_balance_positive_reduction_irreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_reduction_irreduciblenonunitidentityfirstimaginary ge_balance_negative_reduction_irreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_reduction_irreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_reduction_irreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblenonunitidentityfirst) = 2 * ge_signed_half_reduction_irreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblenonunitidentityfirstimaginary) = S ge_signed_half_reduction_irreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_reduction_irreduciblenonunitidentity) + ge_balance_negative_reduction_irreduciblenonunitidentityfirstimaginary = (ge_first_in_reduction_irreduciblenonunitidentity) + ge_balance_positive_reduction_irreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_reduction_irreduciblenonunitidentitysecond ge_representation_imaginary_code_reduction_irreduciblenonunitidentitysecond. (((gr_inverse_reduction_irreduciblenonunit) = ((ge_representation_real_code_reduction_irreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_reduction_irreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_reduction_irreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_reduction_irreduciblenonunitidentitysecondreal ge_balance_negative_reduction_irreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_reduction_irreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_reduction_irreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_reduction_irreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_reduction_irreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_reduction_irreduciblenonunitidentitysecond) = 2 * ge_signed_half_reduction_irreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_reduction_irreduciblenonunitidentitysecondreal) = S ge_signed_half_reduction_irreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_reduction_irreduciblenonunitidentity) + ge_balance_negative_reduction_irreduciblenonunitidentitysecondreal = (ge_second_rn_reduction_irreduciblenonunitidentity) + ge_balance_positive_reduction_irreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_reduction_irreduciblenonunitidentitysecondimaginary ge_balance_negative_reduction_irreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_reduction_irreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_reduction_irreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblenonunitidentitysecond) = 2 * ge_signed_half_reduction_irreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblenonunitidentitysecondimaginary) = S ge_signed_half_reduction_irreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_reduction_irreduciblenonunitidentity) + ge_balance_negative_reduction_irreduciblenonunitidentitysecondimaginary = (ge_second_in_reduction_irreduciblenonunitidentity) + ge_balance_positive_reduction_irreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_reduction_irreduciblenonunitidentityoutput ge_representation_imaginary_code_reduction_irreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_reduction_irreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_reduction_irreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_reduction_irreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_reduction_irreduciblenonunitidentityoutputreal ge_balance_negative_reduction_irreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_reduction_irreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_reduction_irreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_reduction_irreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_reduction_irreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_reduction_irreduciblenonunitidentityoutput) = 2 * ge_signed_half_reduction_irreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_reduction_irreduciblenonunitidentityoutputreal) = S ge_signed_half_reduction_irreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_reduction_irreduciblenonunitidentity) * (ge_second_rp_reduction_irreduciblenonunitidentity))) + (((ge_first_rn_reduction_irreduciblenonunitidentity) * (ge_second_rn_reduction_irreduciblenonunitidentity))))) + (((((ge_first_ip_reduction_irreduciblenonunitidentity) * (ge_second_in_reduction_irreduciblenonunitidentity))) + (((ge_first_in_reduction_irreduciblenonunitidentity) * (ge_second_ip_reduction_irreduciblenonunitidentity))))))) + ge_balance_negative_reduction_irreduciblenonunitidentityoutputreal = (((((((ge_first_rp_reduction_irreduciblenonunitidentity) * (ge_second_rn_reduction_irreduciblenonunitidentity))) + (((ge_first_rn_reduction_irreduciblenonunitidentity) * (ge_second_rp_reduction_irreduciblenonunitidentity))))) + (((((ge_first_ip_reduction_irreduciblenonunitidentity) * (ge_second_ip_reduction_irreduciblenonunitidentity))) + (((ge_first_in_reduction_irreduciblenonunitidentity) * (ge_second_in_reduction_irreduciblenonunitidentity))))))) + ge_balance_positive_reduction_irreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_reduction_irreduciblenonunitidentityoutputimaginary ge_balance_negative_reduction_irreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_reduction_irreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_reduction_irreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblenonunitidentityoutput) = 2 * ge_signed_half_reduction_irreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblenonunitidentityoutputimaginary) = S ge_signed_half_reduction_irreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_reduction_irreduciblenonunitidentity) * (ge_second_ip_reduction_irreduciblenonunitidentity))) + (((ge_first_rn_reduction_irreduciblenonunitidentity) * (ge_second_in_reduction_irreduciblenonunitidentity))))) + (((((ge_first_ip_reduction_irreduciblenonunitidentity) * (ge_second_rp_reduction_irreduciblenonunitidentity))) + (((ge_first_in_reduction_irreduciblenonunitidentity) * (ge_second_rn_reduction_irreduciblenonunitidentity))))))) + ge_balance_negative_reduction_irreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_reduction_irreduciblenonunitidentity) * (ge_second_in_reduction_irreduciblenonunitidentity))) + (((ge_first_rn_reduction_irreduciblenonunitidentity) * (ge_second_ip_reduction_irreduciblenonunitidentity))))) + (((((ge_first_ip_reduction_irreduciblenonunitidentity) * (ge_second_rn_reduction_irreduciblenonunitidentity))) + (((ge_first_in_reduction_irreduciblenonunitidentity) * (ge_second_rp_reduction_irreduciblenonunitidentity))))))) + ge_balance_positive_reduction_irreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_reduction_irreducible gr_second_factor_reduction_irreducible. (exists ge_first_rp_reduction_irreduciblefactorization ge_first_rn_reduction_irreduciblefactorization ge_first_ip_reduction_irreduciblefactorization ge_first_in_reduction_irreduciblefactorization ge_second_rp_reduction_irreduciblefactorization ge_second_rn_reduction_irreduciblefactorization ge_second_ip_reduction_irreduciblefactorization ge_second_in_reduction_irreduciblefactorization. ((exists ge_representation_real_code_reduction_irreduciblefactorizationfirst ge_representation_imaginary_code_reduction_irreduciblefactorizationfirst. (((gr_first_factor_reduction_irreducible) = ((ge_representation_real_code_reduction_irreduciblefactorizationfirst) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationfirst)) * S ((ge_representation_real_code_reduction_irreduciblefactorizationfirst) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_reduction_irreduciblefactorizationfirst) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_reduction_irreduciblefactorizationfirstreal ge_balance_negative_reduction_irreduciblefactorizationfirstreal. (((((ge_representation_real_code_reduction_irreduciblefactorizationfirst) = 2 * (ge_balance_positive_reduction_irreduciblefactorizationfirstreal) /\ (ge_balance_negative_reduction_irreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_reduction_irreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_reduction_irreduciblefactorizationfirst) = 2 * ge_signed_half_reduction_irreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_reduction_irreduciblefactorizationfirstreal) = S ge_signed_half_reduction_irreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_reduction_irreduciblefactorization) + ge_balance_negative_reduction_irreduciblefactorizationfirstreal = (ge_first_rn_reduction_irreduciblefactorization) + ge_balance_positive_reduction_irreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_reduction_irreduciblefactorizationfirstimaginary ge_balance_negative_reduction_irreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblefactorizationfirst) = 2 * (ge_balance_positive_reduction_irreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_reduction_irreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblefactorizationfirst) = 2 * ge_signed_half_reduction_irreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblefactorizationfirstimaginary) = S ge_signed_half_reduction_irreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_reduction_irreduciblefactorization) + ge_balance_negative_reduction_irreduciblefactorizationfirstimaginary = (ge_first_in_reduction_irreduciblefactorization) + ge_balance_positive_reduction_irreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_reduction_irreduciblefactorizationsecond ge_representation_imaginary_code_reduction_irreduciblefactorizationsecond. (((gr_second_factor_reduction_irreducible) = ((ge_representation_real_code_reduction_irreduciblefactorizationsecond) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationsecond)) * S ((ge_representation_real_code_reduction_irreduciblefactorizationsecond) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_reduction_irreduciblefactorizationsecond) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_reduction_irreduciblefactorizationsecondreal ge_balance_negative_reduction_irreduciblefactorizationsecondreal. (((((ge_representation_real_code_reduction_irreduciblefactorizationsecond) = 2 * (ge_balance_positive_reduction_irreduciblefactorizationsecondreal) /\ (ge_balance_negative_reduction_irreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_reduction_irreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_reduction_irreduciblefactorizationsecond) = 2 * ge_signed_half_reduction_irreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_reduction_irreduciblefactorizationsecondreal) = S ge_signed_half_reduction_irreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_reduction_irreduciblefactorization) + ge_balance_negative_reduction_irreduciblefactorizationsecondreal = (ge_second_rn_reduction_irreduciblefactorization) + ge_balance_positive_reduction_irreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_reduction_irreduciblefactorizationsecondimaginary ge_balance_negative_reduction_irreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblefactorizationsecond) = 2 * (ge_balance_positive_reduction_irreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_reduction_irreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblefactorizationsecond) = 2 * ge_signed_half_reduction_irreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblefactorizationsecondimaginary) = S ge_signed_half_reduction_irreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_reduction_irreduciblefactorization) + ge_balance_negative_reduction_irreduciblefactorizationsecondimaginary = (ge_second_in_reduction_irreduciblefactorization) + ge_balance_positive_reduction_irreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_reduction_irreduciblefactorizationoutput ge_representation_imaginary_code_reduction_irreduciblefactorizationoutput. (((p) = ((ge_representation_real_code_reduction_irreduciblefactorizationoutput) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationoutput)) * S ((ge_representation_real_code_reduction_irreduciblefactorizationoutput) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_reduction_irreduciblefactorizationoutput) + (ge_representation_imaginary_code_reduction_irreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_reduction_irreduciblefactorizationoutputreal ge_balance_negative_reduction_irreduciblefactorizationoutputreal. (((((ge_representation_real_code_reduction_irreduciblefactorizationoutput) = 2 * (ge_balance_positive_reduction_irreduciblefactorizationoutputreal) /\ (ge_balance_negative_reduction_irreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_reduction_irreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_reduction_irreduciblefactorizationoutput) = 2 * ge_signed_half_reduction_irreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_reduction_irreduciblefactorizationoutputreal) = S ge_signed_half_reduction_irreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_reduction_irreduciblefactorization) * (ge_second_rp_reduction_irreduciblefactorization))) + (((ge_first_rn_reduction_irreduciblefactorization) * (ge_second_rn_reduction_irreduciblefactorization))))) + (((((ge_first_ip_reduction_irreduciblefactorization) * (ge_second_in_reduction_irreduciblefactorization))) + (((ge_first_in_reduction_irreduciblefactorization) * (ge_second_ip_reduction_irreduciblefactorization))))))) + ge_balance_negative_reduction_irreduciblefactorizationoutputreal = (((((((ge_first_rp_reduction_irreduciblefactorization) * (ge_second_rn_reduction_irreduciblefactorization))) + (((ge_first_rn_reduction_irreduciblefactorization) * (ge_second_rp_reduction_irreduciblefactorization))))) + (((((ge_first_ip_reduction_irreduciblefactorization) * (ge_second_ip_reduction_irreduciblefactorization))) + (((ge_first_in_reduction_irreduciblefactorization) * (ge_second_in_reduction_irreduciblefactorization))))))) + ge_balance_positive_reduction_irreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_reduction_irreduciblefactorizationoutputimaginary ge_balance_negative_reduction_irreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblefactorizationoutput) = 2 * (ge_balance_positive_reduction_irreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_reduction_irreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblefactorizationoutput) = 2 * ge_signed_half_reduction_irreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblefactorizationoutputimaginary) = S ge_signed_half_reduction_irreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_reduction_irreduciblefactorization) * (ge_second_ip_reduction_irreduciblefactorization))) + (((ge_first_rn_reduction_irreduciblefactorization) * (ge_second_in_reduction_irreduciblefactorization))))) + (((((ge_first_ip_reduction_irreduciblefactorization) * (ge_second_rp_reduction_irreduciblefactorization))) + (((ge_first_in_reduction_irreduciblefactorization) * (ge_second_rn_reduction_irreduciblefactorization))))))) + ge_balance_negative_reduction_irreduciblefactorizationoutputimaginary = (((((((ge_first_rp_reduction_irreduciblefactorization) * (ge_second_in_reduction_irreduciblefactorization))) + (((ge_first_rn_reduction_irreduciblefactorization) * (ge_second_ip_reduction_irreduciblefactorization))))) + (((((ge_first_ip_reduction_irreduciblefactorization) * (ge_second_rn_reduction_irreduciblefactorization))) + (((ge_first_in_reduction_irreduciblefactorization) * (ge_second_rp_reduction_irreduciblefactorization))))))) + ge_balance_positive_reduction_irreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_reduction_irreduciblefirst_unit. (exists ge_first_rp_reduction_irreduciblefirst_unitidentity ge_first_rn_reduction_irreduciblefirst_unitidentity ge_first_ip_reduction_irreduciblefirst_unitidentity ge_first_in_reduction_irreduciblefirst_unitidentity ge_second_rp_reduction_irreduciblefirst_unitidentity ge_second_rn_reduction_irreduciblefirst_unitidentity ge_second_ip_reduction_irreduciblefirst_unitidentity ge_second_in_reduction_irreduciblefirst_unitidentity. ((exists ge_representation_real_code_reduction_irreduciblefirst_unitidentityfirst ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityfirst. (((gr_first_factor_reduction_irreducible) = ((ge_representation_real_code_reduction_irreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_reduction_irreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_reduction_irreduciblefirst_unitidentityfirstreal ge_balance_negative_reduction_irreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_reduction_irreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_reduction_irreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_reduction_irreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_reduction_irreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_reduction_irreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentityfirstreal) = S ge_signed_half_reduction_irreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_reduction_irreduciblefirst_unitidentity) + ge_balance_negative_reduction_irreduciblefirst_unitidentityfirstreal = (ge_first_rn_reduction_irreduciblefirst_unitidentity) + ge_balance_positive_reduction_irreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_reduction_irreduciblefirst_unitidentityfirstimaginary ge_balance_negative_reduction_irreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_reduction_irreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_reduction_irreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_reduction_irreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_reduction_irreduciblefirst_unitidentity) + ge_balance_negative_reduction_irreduciblefirst_unitidentityfirstimaginary = (ge_first_in_reduction_irreduciblefirst_unitidentity) + ge_balance_positive_reduction_irreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_reduction_irreduciblefirst_unitidentitysecond ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentitysecond. (((gr_inverse_reduction_irreduciblefirst_unit) = ((ge_representation_real_code_reduction_irreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_reduction_irreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_reduction_irreduciblefirst_unitidentitysecondreal ge_balance_negative_reduction_irreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_reduction_irreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_reduction_irreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_reduction_irreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_reduction_irreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_reduction_irreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentitysecondreal) = S ge_signed_half_reduction_irreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_reduction_irreduciblefirst_unitidentity) + ge_balance_negative_reduction_irreduciblefirst_unitidentitysecondreal = (ge_second_rn_reduction_irreduciblefirst_unitidentity) + ge_balance_positive_reduction_irreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_reduction_irreduciblefirst_unitidentitysecondimaginary ge_balance_negative_reduction_irreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_reduction_irreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_reduction_irreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_reduction_irreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_reduction_irreduciblefirst_unitidentity) + ge_balance_negative_reduction_irreduciblefirst_unitidentitysecondimaginary = (ge_second_in_reduction_irreduciblefirst_unitidentity) + ge_balance_positive_reduction_irreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_reduction_irreduciblefirst_unitidentityoutput ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_reduction_irreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_reduction_irreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_reduction_irreduciblefirst_unitidentityoutputreal ge_balance_negative_reduction_irreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_reduction_irreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_reduction_irreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_reduction_irreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_reduction_irreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_reduction_irreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentityoutputreal) = S ge_signed_half_reduction_irreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_reduction_irreduciblefirst_unitidentity) * (ge_second_rp_reduction_irreduciblefirst_unitidentity))) + (((ge_first_rn_reduction_irreduciblefirst_unitidentity) * (ge_second_rn_reduction_irreduciblefirst_unitidentity))))) + (((((ge_first_ip_reduction_irreduciblefirst_unitidentity) * (ge_second_in_reduction_irreduciblefirst_unitidentity))) + (((ge_first_in_reduction_irreduciblefirst_unitidentity) * (ge_second_ip_reduction_irreduciblefirst_unitidentity))))))) + ge_balance_negative_reduction_irreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_reduction_irreduciblefirst_unitidentity) * (ge_second_rn_reduction_irreduciblefirst_unitidentity))) + (((ge_first_rn_reduction_irreduciblefirst_unitidentity) * (ge_second_rp_reduction_irreduciblefirst_unitidentity))))) + (((((ge_first_ip_reduction_irreduciblefirst_unitidentity) * (ge_second_ip_reduction_irreduciblefirst_unitidentity))) + (((ge_first_in_reduction_irreduciblefirst_unitidentity) * (ge_second_in_reduction_irreduciblefirst_unitidentity))))))) + ge_balance_positive_reduction_irreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_reduction_irreduciblefirst_unitidentityoutputimaginary ge_balance_negative_reduction_irreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_reduction_irreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_reduction_irreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_reduction_irreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_reduction_irreduciblefirst_unitidentity) * (ge_second_ip_reduction_irreduciblefirst_unitidentity))) + (((ge_first_rn_reduction_irreduciblefirst_unitidentity) * (ge_second_in_reduction_irreduciblefirst_unitidentity))))) + (((((ge_first_ip_reduction_irreduciblefirst_unitidentity) * (ge_second_rp_reduction_irreduciblefirst_unitidentity))) + (((ge_first_in_reduction_irreduciblefirst_unitidentity) * (ge_second_rn_reduction_irreduciblefirst_unitidentity))))))) + ge_balance_negative_reduction_irreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_reduction_irreduciblefirst_unitidentity) * (ge_second_in_reduction_irreduciblefirst_unitidentity))) + (((ge_first_rn_reduction_irreduciblefirst_unitidentity) * (ge_second_ip_reduction_irreduciblefirst_unitidentity))))) + (((((ge_first_ip_reduction_irreduciblefirst_unitidentity) * (ge_second_rn_reduction_irreduciblefirst_unitidentity))) + (((ge_first_in_reduction_irreduciblefirst_unitidentity) * (ge_second_rp_reduction_irreduciblefirst_unitidentity))))))) + ge_balance_positive_reduction_irreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_reduction_irreduciblesecond_unit. (exists ge_first_rp_reduction_irreduciblesecond_unitidentity ge_first_rn_reduction_irreduciblesecond_unitidentity ge_first_ip_reduction_irreduciblesecond_unitidentity ge_first_in_reduction_irreduciblesecond_unitidentity ge_second_rp_reduction_irreduciblesecond_unitidentity ge_second_rn_reduction_irreduciblesecond_unitidentity ge_second_ip_reduction_irreduciblesecond_unitidentity ge_second_in_reduction_irreduciblesecond_unitidentity. ((exists ge_representation_real_code_reduction_irreduciblesecond_unitidentityfirst ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityfirst. (((gr_second_factor_reduction_irreducible) = ((ge_representation_real_code_reduction_irreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_reduction_irreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_reduction_irreduciblesecond_unitidentityfirstreal ge_balance_negative_reduction_irreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_reduction_irreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_reduction_irreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_reduction_irreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_reduction_irreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_reduction_irreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentityfirstreal) = S ge_signed_half_reduction_irreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_reduction_irreduciblesecond_unitidentity) + ge_balance_negative_reduction_irreduciblesecond_unitidentityfirstreal = (ge_first_rn_reduction_irreduciblesecond_unitidentity) + ge_balance_positive_reduction_irreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_reduction_irreduciblesecond_unitidentityfirstimaginary ge_balance_negative_reduction_irreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_reduction_irreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_reduction_irreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_reduction_irreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_reduction_irreduciblesecond_unitidentity) + ge_balance_negative_reduction_irreduciblesecond_unitidentityfirstimaginary = (ge_first_in_reduction_irreduciblesecond_unitidentity) + ge_balance_positive_reduction_irreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_reduction_irreduciblesecond_unitidentitysecond ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentitysecond. (((gr_inverse_reduction_irreduciblesecond_unit) = ((ge_representation_real_code_reduction_irreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_reduction_irreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_reduction_irreduciblesecond_unitidentitysecondreal ge_balance_negative_reduction_irreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_reduction_irreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_reduction_irreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_reduction_irreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_reduction_irreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_reduction_irreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentitysecondreal) = S ge_signed_half_reduction_irreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_reduction_irreduciblesecond_unitidentity) + ge_balance_negative_reduction_irreduciblesecond_unitidentitysecondreal = (ge_second_rn_reduction_irreduciblesecond_unitidentity) + ge_balance_positive_reduction_irreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_reduction_irreduciblesecond_unitidentitysecondimaginary ge_balance_negative_reduction_irreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_reduction_irreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_reduction_irreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_reduction_irreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_reduction_irreduciblesecond_unitidentity) + ge_balance_negative_reduction_irreduciblesecond_unitidentitysecondimaginary = (ge_second_in_reduction_irreduciblesecond_unitidentity) + ge_balance_positive_reduction_irreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_reduction_irreduciblesecond_unitidentityoutput ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_reduction_irreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_reduction_irreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_reduction_irreduciblesecond_unitidentityoutputreal ge_balance_negative_reduction_irreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_reduction_irreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_reduction_irreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_reduction_irreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_reduction_irreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_reduction_irreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_reduction_irreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentityoutputreal) = S ge_signed_half_reduction_irreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_reduction_irreduciblesecond_unitidentity) * (ge_second_rp_reduction_irreduciblesecond_unitidentity))) + (((ge_first_rn_reduction_irreduciblesecond_unitidentity) * (ge_second_rn_reduction_irreduciblesecond_unitidentity))))) + (((((ge_first_ip_reduction_irreduciblesecond_unitidentity) * (ge_second_in_reduction_irreduciblesecond_unitidentity))) + (((ge_first_in_reduction_irreduciblesecond_unitidentity) * (ge_second_ip_reduction_irreduciblesecond_unitidentity))))))) + ge_balance_negative_reduction_irreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_reduction_irreduciblesecond_unitidentity) * (ge_second_rn_reduction_irreduciblesecond_unitidentity))) + (((ge_first_rn_reduction_irreduciblesecond_unitidentity) * (ge_second_rp_reduction_irreduciblesecond_unitidentity))))) + (((((ge_first_ip_reduction_irreduciblesecond_unitidentity) * (ge_second_ip_reduction_irreduciblesecond_unitidentity))) + (((ge_first_in_reduction_irreduciblesecond_unitidentity) * (ge_second_in_reduction_irreduciblesecond_unitidentity))))))) + ge_balance_positive_reduction_irreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_reduction_irreduciblesecond_unitidentityoutputimaginary ge_balance_negative_reduction_irreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_reduction_irreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_reduction_irreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_reduction_irreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_reduction_irreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_reduction_irreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_reduction_irreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_reduction_irreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_reduction_irreduciblesecond_unitidentity) * (ge_second_ip_reduction_irreduciblesecond_unitidentity))) + (((ge_first_rn_reduction_irreduciblesecond_unitidentity) * (ge_second_in_reduction_irreduciblesecond_unitidentity))))) + (((((ge_first_ip_reduction_irreduciblesecond_unitidentity) * (ge_second_rp_reduction_irreduciblesecond_unitidentity))) + (((ge_first_in_reduction_irreduciblesecond_unitidentity) * (ge_second_rn_reduction_irreduciblesecond_unitidentity))))))) + ge_balance_negative_reduction_irreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_reduction_irreduciblesecond_unitidentity) * (ge_second_in_reduction_irreduciblesecond_unitidentity))) + (((ge_first_rn_reduction_irreduciblesecond_unitidentity) * (ge_second_ip_reduction_irreduciblesecond_unitidentity))))) + (((((ge_first_ip_reduction_irreduciblesecond_unitidentity) * (ge_second_rn_reduction_irreduciblesecond_unitidentity))) + (((ge_first_in_reduction_irreduciblesecond_unitidentity) * (ge_second_rp_reduction_irreduciblesecond_unitidentity))))))) + ge_balance_positive_reduction_irreduciblesecond_unitidentityoutputimaginary))))))))))))))) /\ ((exists ge_first_rp_reduction_product ge_first_rn_reduction_product ge_first_ip_reduction_product ge_first_in_reduction_product ge_second_rp_reduction_product ge_second_rn_reduction_product ge_second_ip_reduction_product ge_second_in_reduction_product. ((exists ge_representation_real_code_reduction_productfirst ge_representation_imaginary_code_reduction_productfirst. (((p) = ((ge_representation_real_code_reduction_productfirst) + (ge_representation_imaginary_code_reduction_productfirst)) * S ((ge_representation_real_code_reduction_productfirst) + (ge_representation_imaginary_code_reduction_productfirst)) + ((ge_representation_imaginary_code_reduction_productfirst) + (ge_representation_imaginary_code_reduction_productfirst))) /\ ((exists ge_balance_positive_reduction_productfirstreal ge_balance_negative_reduction_productfirstreal. (((((ge_representation_real_code_reduction_productfirst) = 2 * (ge_balance_positive_reduction_productfirstreal) /\ (ge_balance_negative_reduction_productfirstreal) = 0) \/ exists ge_signed_half_reduction_productfirstrealdecode. (((ge_representation_real_code_reduction_productfirst) = 2 * ge_signed_half_reduction_productfirstrealdecode + 1 /\ (ge_balance_positive_reduction_productfirstreal) = 0) /\ (ge_balance_negative_reduction_productfirstreal) = S ge_signed_half_reduction_productfirstrealdecode))) /\ ((ge_first_rp_reduction_product) + ge_balance_negative_reduction_productfirstreal = (ge_first_rn_reduction_product) + ge_balance_positive_reduction_productfirstreal))) /\ (exists ge_balance_positive_reduction_productfirstimaginary ge_balance_negative_reduction_productfirstimaginary. (((((ge_representation_imaginary_code_reduction_productfirst) = 2 * (ge_balance_positive_reduction_productfirstimaginary) /\ (ge_balance_negative_reduction_productfirstimaginary) = 0) \/ exists ge_signed_half_reduction_productfirstimaginarydecode. (((ge_representation_imaginary_code_reduction_productfirst) = 2 * ge_signed_half_reduction_productfirstimaginarydecode + 1 /\ (ge_balance_positive_reduction_productfirstimaginary) = 0) /\ (ge_balance_negative_reduction_productfirstimaginary) = S ge_signed_half_reduction_productfirstimaginarydecode))) /\ ((ge_first_ip_reduction_product) + ge_balance_negative_reduction_productfirstimaginary = (ge_first_in_reduction_product) + ge_balance_positive_reduction_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_reduction_productsecond ge_representation_imaginary_code_reduction_productsecond. (((q) = ((ge_representation_real_code_reduction_productsecond) + (ge_representation_imaginary_code_reduction_productsecond)) * S ((ge_representation_real_code_reduction_productsecond) + (ge_representation_imaginary_code_reduction_productsecond)) + ((ge_representation_imaginary_code_reduction_productsecond) + (ge_representation_imaginary_code_reduction_productsecond))) /\ ((exists ge_balance_positive_reduction_productsecondreal ge_balance_negative_reduction_productsecondreal. (((((ge_representation_real_code_reduction_productsecond) = 2 * (ge_balance_positive_reduction_productsecondreal) /\ (ge_balance_negative_reduction_productsecondreal) = 0) \/ exists ge_signed_half_reduction_productsecondrealdecode. (((ge_representation_real_code_reduction_productsecond) = 2 * ge_signed_half_reduction_productsecondrealdecode + 1 /\ (ge_balance_positive_reduction_productsecondreal) = 0) /\ (ge_balance_negative_reduction_productsecondreal) = S ge_signed_half_reduction_productsecondrealdecode))) /\ ((ge_second_rp_reduction_product) + ge_balance_negative_reduction_productsecondreal = (ge_second_rn_reduction_product) + ge_balance_positive_reduction_productsecondreal))) /\ (exists ge_balance_positive_reduction_productsecondimaginary ge_balance_negative_reduction_productsecondimaginary. (((((ge_representation_imaginary_code_reduction_productsecond) = 2 * (ge_balance_positive_reduction_productsecondimaginary) /\ (ge_balance_negative_reduction_productsecondimaginary) = 0) \/ exists ge_signed_half_reduction_productsecondimaginarydecode. (((ge_representation_imaginary_code_reduction_productsecond) = 2 * ge_signed_half_reduction_productsecondimaginarydecode + 1 /\ (ge_balance_positive_reduction_productsecondimaginary) = 0) /\ (ge_balance_negative_reduction_productsecondimaginary) = S ge_signed_half_reduction_productsecondimaginarydecode))) /\ ((ge_second_ip_reduction_product) + ge_balance_negative_reduction_productsecondimaginary = (ge_second_in_reduction_product) + ge_balance_positive_reduction_productsecondimaginary)))))) /\ (exists ge_representation_real_code_reduction_productoutput ge_representation_imaginary_code_reduction_productoutput. (((z) = ((ge_representation_real_code_reduction_productoutput) + (ge_representation_imaginary_code_reduction_productoutput)) * S ((ge_representation_real_code_reduction_productoutput) + (ge_representation_imaginary_code_reduction_productoutput)) + ((ge_representation_imaginary_code_reduction_productoutput) + (ge_representation_imaginary_code_reduction_productoutput))) /\ ((exists ge_balance_positive_reduction_productoutputreal ge_balance_negative_reduction_productoutputreal. (((((ge_representation_real_code_reduction_productoutput) = 2 * (ge_balance_positive_reduction_productoutputreal) /\ (ge_balance_negative_reduction_productoutputreal) = 0) \/ exists ge_signed_half_reduction_productoutputrealdecode. (((ge_representation_real_code_reduction_productoutput) = 2 * ge_signed_half_reduction_productoutputrealdecode + 1 /\ (ge_balance_positive_reduction_productoutputreal) = 0) /\ (ge_balance_negative_reduction_productoutputreal) = S ge_signed_half_reduction_productoutputrealdecode))) /\ ((((((((ge_first_rp_reduction_product) * (ge_second_rp_reduction_product))) + (((ge_first_rn_reduction_product) * (ge_second_rn_reduction_product))))) + (((((ge_first_ip_reduction_product) * (ge_second_in_reduction_product))) + (((ge_first_in_reduction_product) * (ge_second_ip_reduction_product))))))) + ge_balance_negative_reduction_productoutputreal = (((((((ge_first_rp_reduction_product) * (ge_second_rn_reduction_product))) + (((ge_first_rn_reduction_product) * (ge_second_rp_reduction_product))))) + (((((ge_first_ip_reduction_product) * (ge_second_ip_reduction_product))) + (((ge_first_in_reduction_product) * (ge_second_in_reduction_product))))))) + ge_balance_positive_reduction_productoutputreal))) /\ (exists ge_balance_positive_reduction_productoutputimaginary ge_balance_negative_reduction_productoutputimaginary. (((((ge_representation_imaginary_code_reduction_productoutput) = 2 * (ge_balance_positive_reduction_productoutputimaginary) /\ (ge_balance_negative_reduction_productoutputimaginary) = 0) \/ exists ge_signed_half_reduction_productoutputimaginarydecode. (((ge_representation_imaginary_code_reduction_productoutput) = 2 * ge_signed_half_reduction_productoutputimaginarydecode + 1 /\ (ge_balance_positive_reduction_productoutputimaginary) = 0) /\ (ge_balance_negative_reduction_productoutputimaginary) = S ge_signed_half_reduction_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_reduction_product) * (ge_second_ip_reduction_product))) + (((ge_first_rn_reduction_product) * (ge_second_in_reduction_product))))) + (((((ge_first_ip_reduction_product) * (ge_second_rp_reduction_product))) + (((ge_first_in_reduction_product) * (ge_second_rn_reduction_product))))))) + ge_balance_negative_reduction_productoutputimaginary = (((((((ge_first_rp_reduction_product) * (ge_second_in_reduction_product))) + (((ge_first_rn_reduction_product) * (ge_second_ip_reduction_product))))) + (((((ge_first_ip_reduction_product) * (ge_second_rn_reduction_product))) + (((ge_first_in_reduction_product) * (ge_second_rp_reduction_product))))))) + ge_balance_positive_reduction_productoutputimaginary))))))))) /\ ((exists ge_norm_rp_reduction_quotient_norm ge_norm_rn_reduction_quotient_norm ge_norm_ip_reduction_quotient_norm ge_norm_in_reduction_quotient_norm. ((exists ge_representation_real_code_reduction_quotient_normrepresentation ge_representation_imaginary_code_reduction_quotient_normrepresentation. (((q) = ((ge_representation_real_code_reduction_quotient_normrepresentation) + (ge_representation_imaginary_code_reduction_quotient_normrepresentation)) * S ((ge_representation_real_code_reduction_quotient_normrepresentation) + (ge_representation_imaginary_code_reduction_quotient_normrepresentation)) + ((ge_representation_imaginary_code_reduction_quotient_normrepresentation) + (ge_representation_imaginary_code_reduction_quotient_normrepresentation))) /\ ((exists ge_balance_positive_reduction_quotient_normrepresentationreal ge_balance_negative_reduction_quotient_normrepresentationreal. (((((ge_representation_real_code_reduction_quotient_normrepresentation) = 2 * (ge_balance_positive_reduction_quotient_normrepresentationreal) /\ (ge_balance_negative_reduction_quotient_normrepresentationreal) = 0) \/ exists ge_signed_half_reduction_quotient_normrepresentationrealdecode. (((ge_representation_real_code_reduction_quotient_normrepresentation) = 2 * ge_signed_half_reduction_quotient_normrepresentationrealdecode + 1 /\ (ge_balance_positive_reduction_quotient_normrepresentationreal) = 0) /\ (ge_balance_negative_reduction_quotient_normrepresentationreal) = S ge_signed_half_reduction_quotient_normrepresentationrealdecode))) /\ ((ge_norm_rp_reduction_quotient_norm) + ge_balance_negative_reduction_quotient_normrepresentationreal = (ge_norm_rn_reduction_quotient_norm) + ge_balance_positive_reduction_quotient_normrepresentationreal))) /\ (exists ge_balance_positive_reduction_quotient_normrepresentationimaginary ge_balance_negative_reduction_quotient_normrepresentationimaginary. (((((ge_representation_imaginary_code_reduction_quotient_normrepresentation) = 2 * (ge_balance_positive_reduction_quotient_normrepresentationimaginary) /\ (ge_balance_negative_reduction_quotient_normrepresentationimaginary) = 0) \/ exists ge_signed_half_reduction_quotient_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_reduction_quotient_normrepresentation) = 2 * ge_signed_half_reduction_quotient_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_reduction_quotient_normrepresentationimaginary) = 0) /\ (ge_balance_negative_reduction_quotient_normrepresentationimaginary) = S ge_signed_half_reduction_quotient_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_reduction_quotient_norm) + ge_balance_negative_reduction_quotient_normrepresentationimaginary = (ge_norm_in_reduction_quotient_norm) + ge_balance_positive_reduction_quotient_normrepresentationimaginary)))))) /\ (exists ge_real_square_reduction_quotient_normsquare ge_imaginary_square_reduction_quotient_normsquare. ((((((ge_norm_rp_reduction_quotient_norm) * (ge_norm_rp_reduction_quotient_norm))) + (((ge_norm_rn_reduction_quotient_norm) * (ge_norm_rn_reduction_quotient_norm)))) = ((ge_real_square_reduction_quotient_normsquare) + (((((ge_norm_rp_reduction_quotient_norm) * (ge_norm_rn_reduction_quotient_norm))) + (((ge_norm_rn_reduction_quotient_norm) * (ge_norm_rp_reduction_quotient_norm))))))) /\ ((((((ge_norm_ip_reduction_quotient_norm) * (ge_norm_ip_reduction_quotient_norm))) + (((ge_norm_in_reduction_quotient_norm) * (ge_norm_in_reduction_quotient_norm)))) = ((ge_imaginary_square_reduction_quotient_normsquare) + (((((ge_norm_ip_reduction_quotient_norm) * (ge_norm_in_reduction_quotient_norm))) + (((ge_norm_in_reduction_quotient_norm) * (ge_norm_ip_reduction_quotient_norm))))))) /\ ((Q) = ge_real_square_reduction_quotient_normsquare + ge_imaginary_square_reduction_quotient_normsquare)))))) /\ ((exists ge_gap_reduction_quotient_strict. ge_gap_reduction_quotient_strict + S (Q) = (N)) /\ (~(q=0))))))