gaussian_irreducible_or_strict_nonunit_factorization

Exact expanded first-order arithmetic statement

forall z N. (exists ge_norm_rp_irreducible_split_norm ge_norm_rn_irreducible_split_norm ge_norm_ip_irreducible_split_norm ge_norm_in_irreducible_split_norm. ((exists ge_representation_real_code_irreducible_split_normrepresentation ge_representation_imaginary_code_irreducible_split_normrepresentation. (((z) = ((ge_representation_real_code_irreducible_split_normrepresentation) + (ge_representation_imaginary_code_irreducible_split_normrepresentation)) * S ((ge_representation_real_code_irreducible_split_normrepresentation) + (ge_representation_imaginary_code_irreducible_split_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_split_normrepresentation) + (ge_representation_imaginary_code_irreducible_split_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_split_normrepresentationreal ge_balance_negative_irreducible_split_normrepresentationreal. (((((ge_representation_real_code_irreducible_split_normrepresentation) = 2 * (ge_balance_positive_irreducible_split_normrepresentationreal) /\ (ge_balance_negative_irreducible_split_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_split_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_split_normrepresentation) = 2 * ge_signed_half_irreducible_split_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_split_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_split_normrepresentationreal) = S ge_signed_half_irreducible_split_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_split_norm) + ge_balance_negative_irreducible_split_normrepresentationreal = (ge_norm_rn_irreducible_split_norm) + ge_balance_positive_irreducible_split_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_split_normrepresentationimaginary ge_balance_negative_irreducible_split_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_split_normrepresentation) = 2 * (ge_balance_positive_irreducible_split_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_split_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_split_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_split_normrepresentation) = 2 * ge_signed_half_irreducible_split_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_split_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_split_normrepresentationimaginary) = S ge_signed_half_irreducible_split_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_split_norm) + ge_balance_negative_irreducible_split_normrepresentationimaginary = (ge_norm_in_irreducible_split_norm) + ge_balance_positive_irreducible_split_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_split_normsquare ge_imaginary_square_irreducible_split_normsquare. ((((((ge_norm_rp_irreducible_split_norm) * (ge_norm_rp_irreducible_split_norm))) + (((ge_norm_rn_irreducible_split_norm) * (ge_norm_rn_irreducible_split_norm)))) = ((ge_real_square_irreducible_split_normsquare) + (((((ge_norm_rp_irreducible_split_norm) * (ge_norm_rn_irreducible_split_norm))) + (((ge_norm_rn_irreducible_split_norm) * (ge_norm_rp_irreducible_split_norm))))))) /\ ((((((ge_norm_ip_irreducible_split_norm) * (ge_norm_ip_irreducible_split_norm))) + (((ge_norm_in_irreducible_split_norm) * (ge_norm_in_irreducible_split_norm)))) = ((ge_imaginary_square_irreducible_split_normsquare) + (((((ge_norm_ip_irreducible_split_norm) * (ge_norm_in_irreducible_split_norm))) + (((ge_norm_in_irreducible_split_norm) * (ge_norm_ip_irreducible_split_norm))))))) /\ ((N) = ge_real_square_irreducible_split_normsquare + ge_imaginary_square_irreducible_split_normsquare)))))) -> ~(z=0) -> ~(exists gr_inverse_irreducible_split_nonunit. (exists ge_first_rp_irreducible_split_nonunitidentity ge_first_rn_irreducible_split_nonunitidentity ge_first_ip_irreducible_split_nonunitidentity ge_first_in_irreducible_split_nonunitidentity ge_second_rp_irreducible_split_nonunitidentity ge_second_rn_irreducible_split_nonunitidentity ge_second_ip_irreducible_split_nonunitidentity ge_second_in_irreducible_split_nonunitidentity. ((exists ge_representation_real_code_irreducible_split_nonunitidentityfirst ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst. (((z) = ((ge_representation_real_code_irreducible_split_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_split_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_split_nonunitidentityfirstreal ge_balance_negative_irreducible_split_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_split_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_split_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_split_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_split_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_split_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentityfirstreal) = S ge_signed_half_irreducible_split_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_split_nonunitidentity) + ge_balance_negative_irreducible_split_nonunitidentityfirstreal = (ge_first_rn_irreducible_split_nonunitidentity) + ge_balance_positive_irreducible_split_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_split_nonunitidentityfirstimaginary ge_balance_negative_irreducible_split_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_split_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_split_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_split_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_split_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_split_nonunitidentity) + ge_balance_negative_irreducible_split_nonunitidentityfirstimaginary = (ge_first_in_irreducible_split_nonunitidentity) + ge_balance_positive_irreducible_split_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_split_nonunitidentitysecond ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond. (((gr_inverse_irreducible_split_nonunit) = ((ge_representation_real_code_irreducible_split_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_split_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_split_nonunitidentitysecondreal ge_balance_negative_irreducible_split_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_split_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_split_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_split_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_split_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_split_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentitysecondreal) = S ge_signed_half_irreducible_split_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_split_nonunitidentity) + ge_balance_negative_irreducible_split_nonunitidentitysecondreal = (ge_second_rn_irreducible_split_nonunitidentity) + ge_balance_positive_irreducible_split_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_split_nonunitidentitysecondimaginary ge_balance_negative_irreducible_split_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_split_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_split_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_split_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_split_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_split_nonunitidentity) + ge_balance_negative_irreducible_split_nonunitidentitysecondimaginary = (ge_second_in_irreducible_split_nonunitidentity) + ge_balance_positive_irreducible_split_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_split_nonunitidentityoutput ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_split_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_split_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_split_nonunitidentityoutputreal ge_balance_negative_irreducible_split_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_split_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_split_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_split_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_split_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_split_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentityoutputreal) = S ge_signed_half_irreducible_split_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_split_nonunitidentity) * (ge_second_rp_irreducible_split_nonunitidentity))) + (((ge_first_rn_irreducible_split_nonunitidentity) * (ge_second_rn_irreducible_split_nonunitidentity))))) + (((((ge_first_ip_irreducible_split_nonunitidentity) * (ge_second_in_irreducible_split_nonunitidentity))) + (((ge_first_in_irreducible_split_nonunitidentity) * (ge_second_ip_irreducible_split_nonunitidentity))))))) + ge_balance_negative_irreducible_split_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_split_nonunitidentity) * (ge_second_rn_irreducible_split_nonunitidentity))) + (((ge_first_rn_irreducible_split_nonunitidentity) * (ge_second_rp_irreducible_split_nonunitidentity))))) + (((((ge_first_ip_irreducible_split_nonunitidentity) * (ge_second_ip_irreducible_split_nonunitidentity))) + (((ge_first_in_irreducible_split_nonunitidentity) * (ge_second_in_irreducible_split_nonunitidentity))))))) + ge_balance_positive_irreducible_split_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_split_nonunitidentityoutputimaginary ge_balance_negative_irreducible_split_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_split_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_split_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_split_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_split_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_split_nonunitidentity) * (ge_second_ip_irreducible_split_nonunitidentity))) + (((ge_first_rn_irreducible_split_nonunitidentity) * (ge_second_in_irreducible_split_nonunitidentity))))) + (((((ge_first_ip_irreducible_split_nonunitidentity) * (ge_second_rp_irreducible_split_nonunitidentity))) + (((ge_first_in_irreducible_split_nonunitidentity) * (ge_second_rn_irreducible_split_nonunitidentity))))))) + ge_balance_negative_irreducible_split_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_split_nonunitidentity) * (ge_second_in_irreducible_split_nonunitidentity))) + (((ge_first_rn_irreducible_split_nonunitidentity) * (ge_second_ip_irreducible_split_nonunitidentity))))) + (((((ge_first_ip_irreducible_split_nonunitidentity) * (ge_second_rn_irreducible_split_nonunitidentity))) + (((ge_first_in_irreducible_split_nonunitidentity) * (ge_second_rp_irreducible_split_nonunitidentity))))))) + ge_balance_positive_irreducible_split_nonunitidentityoutputimaginary)))))))))) -> ((((exists ge_real_positive_irreducible_splitirreduciblecarrier ge_real_negative_irreducible_splitirreduciblecarrier ge_imaginary_positive_irreducible_splitirreduciblecarrier ge_imaginary_negative_irreducible_splitirreduciblecarrier. (exists ge_real_code_irreducible_splitirreduciblecarrierdecode ge_imaginary_code_irreducible_splitirreduciblecarrierdecode. (((z) = ((ge_real_code_irreducible_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_splitirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_splitirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_splitirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_splitirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_splitirreduciblecarrier) /\ (ge_real_negative_irreducible_splitirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_real. (((ge_real_code_irreducible_splitirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_splitirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_splitirreduciblecarrier) = S ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_splitirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_splitirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_splitirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_splitirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_splitirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_splitirreduciblecarrier) = S ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_imaginary))))))) /\ ((~((z)=0)) /\ ((~(exists gr_inverse_irreducible_splitirreduciblenonunit. (exists ge_first_rp_irreducible_splitirreduciblenonunitidentity ge_first_rn_irreducible_splitirreduciblenonunitidentity ge_first_ip_irreducible_splitirreduciblenonunitidentity ge_first_in_irreducible_splitirreduciblenonunitidentity ge_second_rp_irreducible_splitirreduciblenonunitidentity ge_second_rn_irreducible_splitirreduciblenonunitidentity ge_second_ip_irreducible_splitirreduciblenonunitidentity ge_second_in_irreducible_splitirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst. (((z) = ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_splitirreduciblenonunit) = ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_splitirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_splitirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_splitirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_splitirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_splitirreducible gr_second_factor_irreducible_splitirreducible. (exists ge_first_rp_irreducible_splitirreduciblefactorization ge_first_rn_irreducible_splitirreduciblefactorization ge_first_ip_irreducible_splitirreduciblefactorization ge_first_in_irreducible_splitirreduciblefactorization ge_second_rp_irreducible_splitirreduciblefactorization ge_second_rn_irreducible_splitirreduciblefactorization ge_second_ip_irreducible_splitirreduciblefactorization ge_second_in_irreducible_splitirreduciblefactorization. ((exists ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst. (((gr_first_factor_irreducible_splitirreducible) = ((ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefactorizationfirstreal ge_balance_negative_irreducible_splitirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_splitirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitirreduciblefactorization) + ge_balance_negative_irreducible_splitirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_splitirreduciblefactorization) + ge_balance_positive_irreducible_splitirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_splitirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_splitirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitirreduciblefactorization) + ge_balance_negative_irreducible_splitirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_splitirreduciblefactorization) + ge_balance_positive_irreducible_splitirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond. (((gr_second_factor_irreducible_splitirreducible) = ((ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefactorizationsecondreal ge_balance_negative_irreducible_splitirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_splitirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_splitirreduciblefactorization) + ge_balance_negative_irreducible_splitirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_splitirreduciblefactorization) + ge_balance_positive_irreducible_splitirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_splitirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_splitirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitirreduciblefactorization) + ge_balance_negative_irreducible_splitirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_splitirreduciblefactorization) + ge_balance_positive_irreducible_splitirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput. (((z) = ((ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefactorizationoutputreal ge_balance_negative_irreducible_splitirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_splitirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblefactorization) * (ge_second_rp_irreducible_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_splitirreduciblefactorization) * (ge_second_rn_irreducible_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_splitirreduciblefactorization) * (ge_second_in_irreducible_splitirreduciblefactorization))) + (((ge_first_in_irreducible_splitirreduciblefactorization) * (ge_second_ip_irreducible_splitirreduciblefactorization))))))) + ge_balance_negative_irreducible_splitirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_splitirreduciblefactorization) * (ge_second_rn_irreducible_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_splitirreduciblefactorization) * (ge_second_rp_irreducible_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_splitirreduciblefactorization) * (ge_second_ip_irreducible_splitirreduciblefactorization))) + (((ge_first_in_irreducible_splitirreduciblefactorization) * (ge_second_in_irreducible_splitirreduciblefactorization))))))) + ge_balance_positive_irreducible_splitirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_splitirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_splitirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblefactorization) * (ge_second_ip_irreducible_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_splitirreduciblefactorization) * (ge_second_in_irreducible_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_splitirreduciblefactorization) * (ge_second_rp_irreducible_splitirreduciblefactorization))) + (((ge_first_in_irreducible_splitirreduciblefactorization) * (ge_second_rn_irreducible_splitirreduciblefactorization))))))) + ge_balance_negative_irreducible_splitirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_splitirreduciblefactorization) * (ge_second_in_irreducible_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_splitirreduciblefactorization) * (ge_second_ip_irreducible_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_splitirreduciblefactorization) * (ge_second_rn_irreducible_splitirreduciblefactorization))) + (((ge_first_in_irreducible_splitirreduciblefactorization) * (ge_second_rp_irreducible_splitirreduciblefactorization))))))) + ge_balance_positive_irreducible_splitirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_splitirreduciblefirst_unit. (exists ge_first_rp_irreducible_splitirreduciblefirst_unitidentity ge_first_rn_irreducible_splitirreduciblefirst_unitidentity ge_first_ip_irreducible_splitirreduciblefirst_unitidentity ge_first_in_irreducible_splitirreduciblefirst_unitidentity ge_second_rp_irreducible_splitirreduciblefirst_unitidentity ge_second_rn_irreducible_splitirreduciblefirst_unitidentity ge_second_ip_irreducible_splitirreduciblefirst_unitidentity ge_second_in_irreducible_splitirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_splitirreducible) = ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_splitirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_splitirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_splitirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_splitirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_splitirreduciblesecond_unit. (exists ge_first_rp_irreducible_splitirreduciblesecond_unitidentity ge_first_rn_irreducible_splitirreduciblesecond_unitidentity ge_first_ip_irreducible_splitirreduciblesecond_unitidentity ge_first_in_irreducible_splitirreduciblesecond_unitidentity ge_second_rp_irreducible_splitirreduciblesecond_unitidentity ge_second_rn_irreducible_splitirreduciblesecond_unitidentity ge_second_ip_irreducible_splitirreduciblesecond_unitidentity ge_second_in_irreducible_splitirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_splitirreducible) = ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_splitirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_splitirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_splitirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_splitirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputimaginary))))))))))))))) \/ (exists gr_split_first_irreducible_split gr_split_second_irreducible_split gr_split_first_norm_irreducible_split gr_split_second_norm_irreducible_split. (((exists ge_first_rp_irreducible_splitsplitproduct ge_first_rn_irreducible_splitsplitproduct ge_first_ip_irreducible_splitsplitproduct ge_first_in_irreducible_splitsplitproduct ge_second_rp_irreducible_splitsplitproduct ge_second_rn_irreducible_splitsplitproduct ge_second_ip_irreducible_splitsplitproduct ge_second_in_irreducible_splitsplitproduct. ((exists ge_representation_real_code_irreducible_splitsplitproductfirst ge_representation_imaginary_code_irreducible_splitsplitproductfirst. (((gr_split_first_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_splitsplitproductfirst)) * S ((ge_representation_real_code_irreducible_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_splitsplitproductfirst)) + ((ge_representation_imaginary_code_irreducible_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_splitsplitproductfirst))) /\ ((exists ge_balance_positive_irreducible_splitsplitproductfirstreal ge_balance_negative_irreducible_splitsplitproductfirstreal. (((((ge_representation_real_code_irreducible_splitsplitproductfirst) = 2 * (ge_balance_positive_irreducible_splitsplitproductfirstreal) /\ (ge_balance_negative_irreducible_splitsplitproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductfirstrealdecode. (((ge_representation_real_code_irreducible_splitsplitproductfirst) = 2 * ge_signed_half_irreducible_splitsplitproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductfirstreal) = S ge_signed_half_irreducible_splitsplitproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitsplitproduct) + ge_balance_negative_irreducible_splitsplitproductfirstreal = (ge_first_rn_irreducible_splitsplitproduct) + ge_balance_positive_irreducible_splitsplitproductfirstreal))) /\ (exists ge_balance_positive_irreducible_splitsplitproductfirstimaginary ge_balance_negative_irreducible_splitsplitproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitproductfirst) = 2 * (ge_balance_positive_irreducible_splitsplitproductfirstimaginary) /\ (ge_balance_negative_irreducible_splitsplitproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitproductfirst) = 2 * ge_signed_half_irreducible_splitsplitproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductfirstimaginary) = S ge_signed_half_irreducible_splitsplitproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitsplitproduct) + ge_balance_negative_irreducible_splitsplitproductfirstimaginary = (ge_first_in_irreducible_splitsplitproduct) + ge_balance_positive_irreducible_splitsplitproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitsplitproductsecond ge_representation_imaginary_code_irreducible_splitsplitproductsecond. (((gr_split_second_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_splitsplitproductsecond)) * S ((ge_representation_real_code_irreducible_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_splitsplitproductsecond)) + ((ge_representation_imaginary_code_irreducible_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_splitsplitproductsecond))) /\ ((exists ge_balance_positive_irreducible_splitsplitproductsecondreal ge_balance_negative_irreducible_splitsplitproductsecondreal. (((((ge_representation_real_code_irreducible_splitsplitproductsecond) = 2 * (ge_balance_positive_irreducible_splitsplitproductsecondreal) /\ (ge_balance_negative_irreducible_splitsplitproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductsecondrealdecode. (((ge_representation_real_code_irreducible_splitsplitproductsecond) = 2 * ge_signed_half_irreducible_splitsplitproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductsecondreal) = S ge_signed_half_irreducible_splitsplitproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_splitsplitproduct) + ge_balance_negative_irreducible_splitsplitproductsecondreal = (ge_second_rn_irreducible_splitsplitproduct) + ge_balance_positive_irreducible_splitsplitproductsecondreal))) /\ (exists ge_balance_positive_irreducible_splitsplitproductsecondimaginary ge_balance_negative_irreducible_splitsplitproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitproductsecond) = 2 * (ge_balance_positive_irreducible_splitsplitproductsecondimaginary) /\ (ge_balance_negative_irreducible_splitsplitproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitproductsecond) = 2 * ge_signed_half_irreducible_splitsplitproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductsecondimaginary) = S ge_signed_half_irreducible_splitsplitproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitsplitproduct) + ge_balance_negative_irreducible_splitsplitproductsecondimaginary = (ge_second_in_irreducible_splitsplitproduct) + ge_balance_positive_irreducible_splitsplitproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitsplitproductoutput ge_representation_imaginary_code_irreducible_splitsplitproductoutput. (((z) = ((ge_representation_real_code_irreducible_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_splitsplitproductoutput)) * S ((ge_representation_real_code_irreducible_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_splitsplitproductoutput)) + ((ge_representation_imaginary_code_irreducible_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_splitsplitproductoutput))) /\ ((exists ge_balance_positive_irreducible_splitsplitproductoutputreal ge_balance_negative_irreducible_splitsplitproductoutputreal. (((((ge_representation_real_code_irreducible_splitsplitproductoutput) = 2 * (ge_balance_positive_irreducible_splitsplitproductoutputreal) /\ (ge_balance_negative_irreducible_splitsplitproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductoutputrealdecode. (((ge_representation_real_code_irreducible_splitsplitproductoutput) = 2 * ge_signed_half_irreducible_splitsplitproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductoutputreal) = S ge_signed_half_irreducible_splitsplitproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitproduct) * (ge_second_rp_irreducible_splitsplitproduct))) + (((ge_first_rn_irreducible_splitsplitproduct) * (ge_second_rn_irreducible_splitsplitproduct))))) + (((((ge_first_ip_irreducible_splitsplitproduct) * (ge_second_in_irreducible_splitsplitproduct))) + (((ge_first_in_irreducible_splitsplitproduct) * (ge_second_ip_irreducible_splitsplitproduct))))))) + ge_balance_negative_irreducible_splitsplitproductoutputreal = (((((((ge_first_rp_irreducible_splitsplitproduct) * (ge_second_rn_irreducible_splitsplitproduct))) + (((ge_first_rn_irreducible_splitsplitproduct) * (ge_second_rp_irreducible_splitsplitproduct))))) + (((((ge_first_ip_irreducible_splitsplitproduct) * (ge_second_ip_irreducible_splitsplitproduct))) + (((ge_first_in_irreducible_splitsplitproduct) * (ge_second_in_irreducible_splitsplitproduct))))))) + ge_balance_positive_irreducible_splitsplitproductoutputreal))) /\ (exists ge_balance_positive_irreducible_splitsplitproductoutputimaginary ge_balance_negative_irreducible_splitsplitproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitproductoutput) = 2 * (ge_balance_positive_irreducible_splitsplitproductoutputimaginary) /\ (ge_balance_negative_irreducible_splitsplitproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitproductoutput) = 2 * ge_signed_half_irreducible_splitsplitproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductoutputimaginary) = S ge_signed_half_irreducible_splitsplitproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitproduct) * (ge_second_ip_irreducible_splitsplitproduct))) + (((ge_first_rn_irreducible_splitsplitproduct) * (ge_second_in_irreducible_splitsplitproduct))))) + (((((ge_first_ip_irreducible_splitsplitproduct) * (ge_second_rp_irreducible_splitsplitproduct))) + (((ge_first_in_irreducible_splitsplitproduct) * (ge_second_rn_irreducible_splitsplitproduct))))))) + ge_balance_negative_irreducible_splitsplitproductoutputimaginary = (((((((ge_first_rp_irreducible_splitsplitproduct) * (ge_second_in_irreducible_splitsplitproduct))) + (((ge_first_rn_irreducible_splitsplitproduct) * (ge_second_ip_irreducible_splitsplitproduct))))) + (((((ge_first_ip_irreducible_splitsplitproduct) * (ge_second_rn_irreducible_splitsplitproduct))) + (((ge_first_in_irreducible_splitsplitproduct) * (ge_second_rp_irreducible_splitsplitproduct))))))) + ge_balance_positive_irreducible_splitsplitproductoutputimaginary))))))))) /\ ((exists ge_norm_rp_irreducible_splitsplitfirst_norm ge_norm_rn_irreducible_splitsplitfirst_norm ge_norm_ip_irreducible_splitsplitfirst_norm ge_norm_in_irreducible_splitsplitfirst_norm. ((exists ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation. (((gr_split_first_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation)) * S ((ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_splitsplitfirst_normrepresentationreal ge_balance_negative_irreducible_splitsplitfirst_normrepresentationreal. (((((ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_normrepresentationreal) /\ (ge_balance_negative_irreducible_splitsplitfirst_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation) = 2 * ge_signed_half_irreducible_splitsplitfirst_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_normrepresentationreal) = S ge_signed_half_irreducible_splitsplitfirst_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_splitsplitfirst_norm) + ge_balance_negative_irreducible_splitsplitfirst_normrepresentationreal = (ge_norm_rn_irreducible_splitsplitfirst_norm) + ge_balance_positive_irreducible_splitsplitfirst_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_splitsplitfirst_normrepresentationimaginary ge_balance_negative_irreducible_splitsplitfirst_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_splitsplitfirst_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation) = 2 * ge_signed_half_irreducible_splitsplitfirst_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_normrepresentationimaginary) = S ge_signed_half_irreducible_splitsplitfirst_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_splitsplitfirst_norm) + ge_balance_negative_irreducible_splitsplitfirst_normrepresentationimaginary = (ge_norm_in_irreducible_splitsplitfirst_norm) + ge_balance_positive_irreducible_splitsplitfirst_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_splitsplitfirst_normsquare ge_imaginary_square_irreducible_splitsplitfirst_normsquare. ((((((ge_norm_rp_irreducible_splitsplitfirst_norm) * (ge_norm_rp_irreducible_splitsplitfirst_norm))) + (((ge_norm_rn_irreducible_splitsplitfirst_norm) * (ge_norm_rn_irreducible_splitsplitfirst_norm)))) = ((ge_real_square_irreducible_splitsplitfirst_normsquare) + (((((ge_norm_rp_irreducible_splitsplitfirst_norm) * (ge_norm_rn_irreducible_splitsplitfirst_norm))) + (((ge_norm_rn_irreducible_splitsplitfirst_norm) * (ge_norm_rp_irreducible_splitsplitfirst_norm))))))) /\ ((((((ge_norm_ip_irreducible_splitsplitfirst_norm) * (ge_norm_ip_irreducible_splitsplitfirst_norm))) + (((ge_norm_in_irreducible_splitsplitfirst_norm) * (ge_norm_in_irreducible_splitsplitfirst_norm)))) = ((ge_imaginary_square_irreducible_splitsplitfirst_normsquare) + (((((ge_norm_ip_irreducible_splitsplitfirst_norm) * (ge_norm_in_irreducible_splitsplitfirst_norm))) + (((ge_norm_in_irreducible_splitsplitfirst_norm) * (ge_norm_ip_irreducible_splitsplitfirst_norm))))))) /\ ((gr_split_first_norm_irreducible_split) = ge_real_square_irreducible_splitsplitfirst_normsquare + ge_imaginary_square_irreducible_splitsplitfirst_normsquare)))))) /\ ((exists ge_norm_rp_irreducible_splitsplitsecond_norm ge_norm_rn_irreducible_splitsplitsecond_norm ge_norm_ip_irreducible_splitsplitsecond_norm ge_norm_in_irreducible_splitsplitsecond_norm. ((exists ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation. (((gr_split_second_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation)) * S ((ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_splitsplitsecond_normrepresentationreal ge_balance_negative_irreducible_splitsplitsecond_normrepresentationreal. (((((ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_normrepresentationreal) /\ (ge_balance_negative_irreducible_splitsplitsecond_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation) = 2 * ge_signed_half_irreducible_splitsplitsecond_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_normrepresentationreal) = S ge_signed_half_irreducible_splitsplitsecond_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_splitsplitsecond_norm) + ge_balance_negative_irreducible_splitsplitsecond_normrepresentationreal = (ge_norm_rn_irreducible_splitsplitsecond_norm) + ge_balance_positive_irreducible_splitsplitsecond_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_splitsplitsecond_normrepresentationimaginary ge_balance_negative_irreducible_splitsplitsecond_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_splitsplitsecond_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation) = 2 * ge_signed_half_irreducible_splitsplitsecond_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_normrepresentationimaginary) = S ge_signed_half_irreducible_splitsplitsecond_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_splitsplitsecond_norm) + ge_balance_negative_irreducible_splitsplitsecond_normrepresentationimaginary = (ge_norm_in_irreducible_splitsplitsecond_norm) + ge_balance_positive_irreducible_splitsplitsecond_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_splitsplitsecond_normsquare ge_imaginary_square_irreducible_splitsplitsecond_normsquare. ((((((ge_norm_rp_irreducible_splitsplitsecond_norm) * (ge_norm_rp_irreducible_splitsplitsecond_norm))) + (((ge_norm_rn_irreducible_splitsplitsecond_norm) * (ge_norm_rn_irreducible_splitsplitsecond_norm)))) = ((ge_real_square_irreducible_splitsplitsecond_normsquare) + (((((ge_norm_rp_irreducible_splitsplitsecond_norm) * (ge_norm_rn_irreducible_splitsplitsecond_norm))) + (((ge_norm_rn_irreducible_splitsplitsecond_norm) * (ge_norm_rp_irreducible_splitsplitsecond_norm))))))) /\ ((((((ge_norm_ip_irreducible_splitsplitsecond_norm) * (ge_norm_ip_irreducible_splitsplitsecond_norm))) + (((ge_norm_in_irreducible_splitsplitsecond_norm) * (ge_norm_in_irreducible_splitsplitsecond_norm)))) = ((ge_imaginary_square_irreducible_splitsplitsecond_normsquare) + (((((ge_norm_ip_irreducible_splitsplitsecond_norm) * (ge_norm_in_irreducible_splitsplitsecond_norm))) + (((ge_norm_in_irreducible_splitsplitsecond_norm) * (ge_norm_ip_irreducible_splitsplitsecond_norm))))))) /\ ((gr_split_second_norm_irreducible_split) = ge_real_square_irreducible_splitsplitsecond_normsquare + ge_imaginary_square_irreducible_splitsplitsecond_normsquare)))))) /\ ((~(exists gr_inverse_irreducible_splitsplitfirst_nonunit. (exists ge_first_rp_irreducible_splitsplitfirst_nonunitidentity ge_first_rn_irreducible_splitsplitfirst_nonunitidentity ge_first_ip_irreducible_splitsplitfirst_nonunitidentity ge_first_in_irreducible_splitsplitfirst_nonunitidentity ge_second_rp_irreducible_splitsplitfirst_nonunitidentity ge_second_rn_irreducible_splitsplitfirst_nonunitidentity ge_second_ip_irreducible_splitsplitfirst_nonunitidentity ge_second_in_irreducible_splitsplitfirst_nonunitidentity. ((exists ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst. (((gr_split_first_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstreal ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstreal) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstreal = (ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstimaginary ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstimaginary = (ge_first_in_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond. (((gr_inverse_irreducible_splitsplitfirst_nonunit) = ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondreal ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondreal) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondreal = (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondimaginary ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondimaginary = (ge_second_in_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputreal ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputreal) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_splitsplitfirst_nonunitidentity))))))) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_splitsplitfirst_nonunitidentity))))))) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputimaginary ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity))))))) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_splitsplitfirst_nonunitidentity))))))) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputimaginary))))))))))) /\ ((~(exists gr_inverse_irreducible_splitsplitsecond_nonunit. (exists ge_first_rp_irreducible_splitsplitsecond_nonunitidentity ge_first_rn_irreducible_splitsplitsecond_nonunitidentity ge_first_ip_irreducible_splitsplitsecond_nonunitidentity ge_first_in_irreducible_splitsplitsecond_nonunitidentity ge_second_rp_irreducible_splitsplitsecond_nonunitidentity ge_second_rn_irreducible_splitsplitsecond_nonunitidentity ge_second_ip_irreducible_splitsplitsecond_nonunitidentity ge_second_in_irreducible_splitsplitsecond_nonunitidentity. ((exists ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst. (((gr_split_second_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstreal ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstreal) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstreal = (ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstimaginary ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstimaginary = (ge_first_in_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond. (((gr_inverse_irreducible_splitsplitsecond_nonunit) = ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondreal ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondreal) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondreal = (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondimaginary ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondimaginary = (ge_second_in_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputreal ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputreal) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_splitsplitsecond_nonunitidentity))))))) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_splitsplitsecond_nonunitidentity))))))) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputimaginary ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity))))))) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_splitsplitsecond_nonunitidentity))))))) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputimaginary))))))))))) /\ ((exists ge_gap_irreducible_splitsplitfirst_strict. ge_gap_irreducible_splitsplitfirst_strict + S (gr_split_first_norm_irreducible_split) = (N)) /\ (exists ge_gap_irreducible_splitsplitsecond_strict. ge_gap_irreducible_splitsplitsecond_strict + S (gr_split_second_norm_irreducible_split) = (N)))))))))))