gaussian_irreducible_factorization_bounded_norm

Exact expanded first-order arithmetic statement

forall k z N. (exists ge_gap_factorization_bound. ge_gap_factorization_bound + (N) = (k)) -> (exists ge_norm_rp_factorization_norm ge_norm_rn_factorization_norm ge_norm_ip_factorization_norm ge_norm_in_factorization_norm. ((exists ge_representation_real_code_factorization_normrepresentation ge_representation_imaginary_code_factorization_normrepresentation. (((z) = ((ge_representation_real_code_factorization_normrepresentation) + (ge_representation_imaginary_code_factorization_normrepresentation)) * S ((ge_representation_real_code_factorization_normrepresentation) + (ge_representation_imaginary_code_factorization_normrepresentation)) + ((ge_representation_imaginary_code_factorization_normrepresentation) + (ge_representation_imaginary_code_factorization_normrepresentation))) /\ ((exists ge_balance_positive_factorization_normrepresentationreal ge_balance_negative_factorization_normrepresentationreal. (((((ge_representation_real_code_factorization_normrepresentation) = 2 * (ge_balance_positive_factorization_normrepresentationreal) /\ (ge_balance_negative_factorization_normrepresentationreal) = 0) \/ exists ge_signed_half_factorization_normrepresentationrealdecode. (((ge_representation_real_code_factorization_normrepresentation) = 2 * ge_signed_half_factorization_normrepresentationrealdecode + 1 /\ (ge_balance_positive_factorization_normrepresentationreal) = 0) /\ (ge_balance_negative_factorization_normrepresentationreal) = S ge_signed_half_factorization_normrepresentationrealdecode))) /\ ((ge_norm_rp_factorization_norm) + ge_balance_negative_factorization_normrepresentationreal = (ge_norm_rn_factorization_norm) + ge_balance_positive_factorization_normrepresentationreal))) /\ (exists ge_balance_positive_factorization_normrepresentationimaginary ge_balance_negative_factorization_normrepresentationimaginary. (((((ge_representation_imaginary_code_factorization_normrepresentation) = 2 * (ge_balance_positive_factorization_normrepresentationimaginary) /\ (ge_balance_negative_factorization_normrepresentationimaginary) = 0) \/ exists ge_signed_half_factorization_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_factorization_normrepresentation) = 2 * ge_signed_half_factorization_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_factorization_normrepresentationimaginary) = 0) /\ (ge_balance_negative_factorization_normrepresentationimaginary) = S ge_signed_half_factorization_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_factorization_norm) + ge_balance_negative_factorization_normrepresentationimaginary = (ge_norm_in_factorization_norm) + ge_balance_positive_factorization_normrepresentationimaginary)))))) /\ (exists ge_real_square_factorization_normsquare ge_imaginary_square_factorization_normsquare. ((((((ge_norm_rp_factorization_norm) * (ge_norm_rp_factorization_norm))) + (((ge_norm_rn_factorization_norm) * (ge_norm_rn_factorization_norm)))) = ((ge_real_square_factorization_normsquare) + (((((ge_norm_rp_factorization_norm) * (ge_norm_rn_factorization_norm))) + (((ge_norm_rn_factorization_norm) * (ge_norm_rp_factorization_norm))))))) /\ ((((((ge_norm_ip_factorization_norm) * (ge_norm_ip_factorization_norm))) + (((ge_norm_in_factorization_norm) * (ge_norm_in_factorization_norm)))) = ((ge_imaginary_square_factorization_normsquare) + (((((ge_norm_ip_factorization_norm) * (ge_norm_in_factorization_norm))) + (((ge_norm_in_factorization_norm) * (ge_norm_ip_factorization_norm))))))) /\ ((N) = ge_real_square_factorization_normsquare + ge_imaginary_square_factorization_normsquare)))))) -> ~(z=0) -> (exists u b c l. ((exists gr_inverse_factorization_existsunit. (exists ge_first_rp_factorization_existsunitidentity ge_first_rn_factorization_existsunitidentity ge_first_ip_factorization_existsunitidentity ge_first_in_factorization_existsunitidentity ge_second_rp_factorization_existsunitidentity ge_second_rn_factorization_existsunitidentity ge_second_ip_factorization_existsunitidentity ge_second_in_factorization_existsunitidentity. ((exists ge_representation_real_code_factorization_existsunitidentityfirst ge_representation_imaginary_code_factorization_existsunitidentityfirst. (((u) = ((ge_representation_real_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst)) * S ((ge_representation_real_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsunitidentityfirstreal ge_balance_negative_factorization_existsunitidentityfirstreal. (((((ge_representation_real_code_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsunitidentityfirstreal) /\ (ge_balance_negative_factorization_existsunitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsunitidentityfirst) = 2 * ge_signed_half_factorization_existsunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentityfirstreal) = S ge_signed_half_factorization_existsunitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentityfirstreal = (ge_first_rn_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsunitidentityfirstimaginary ge_balance_negative_factorization_existsunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsunitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentityfirst) = 2 * ge_signed_half_factorization_existsunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentityfirstimaginary) = S ge_signed_half_factorization_existsunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentityfirstimaginary = (ge_first_in_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsunitidentitysecond ge_representation_imaginary_code_factorization_existsunitidentitysecond. (((gr_inverse_factorization_existsunit) = ((ge_representation_real_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond)) * S ((ge_representation_real_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsunitidentitysecondreal ge_balance_negative_factorization_existsunitidentitysecondreal. (((((ge_representation_real_code_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsunitidentitysecondreal) /\ (ge_balance_negative_factorization_existsunitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsunitidentitysecond) = 2 * ge_signed_half_factorization_existsunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentitysecondreal) = S ge_signed_half_factorization_existsunitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentitysecondreal = (ge_second_rn_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsunitidentitysecondimaginary ge_balance_negative_factorization_existsunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsunitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentitysecond) = 2 * ge_signed_half_factorization_existsunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentitysecondimaginary) = S ge_signed_half_factorization_existsunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentitysecondimaginary = (ge_second_in_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsunitidentityoutput ge_representation_imaginary_code_factorization_existsunitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput)) * S ((ge_representation_real_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsunitidentityoutputreal ge_balance_negative_factorization_existsunitidentityoutputreal. (((((ge_representation_real_code_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsunitidentityoutputreal) /\ (ge_balance_negative_factorization_existsunitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsunitidentityoutput) = 2 * ge_signed_half_factorization_existsunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentityoutputreal) = S ge_signed_half_factorization_existsunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))))))) + ge_balance_negative_factorization_existsunitidentityoutputreal = (((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))))))) + ge_balance_positive_factorization_existsunitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsunitidentityoutputimaginary ge_balance_negative_factorization_existsunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsunitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentityoutput) = 2 * ge_signed_half_factorization_existsunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentityoutputimaginary) = S ge_signed_half_factorization_existsunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))))))) + ge_balance_negative_factorization_existsunitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))))))) + ge_balance_positive_factorization_existsunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factorization_existsirreducible gr_factor_value_factorization_existsirreducible. (exists ge_gap_factorization_existsirreducibleindex. ge_gap_factorization_existsirreducibleindex + S (gr_factor_index_factorization_existsirreducible) = (l)) -> (((exists ff_h_gprod_factorization_existsirreducibleentry. ff_h_gprod_factorization_existsirreducibleentry + S (gr_factor_value_factorization_existsirreducible) = S ((S (gr_factor_index_factorization_existsirreducible)) * c)) /\ exists ff_q_gprod_factorization_existsirreducibleentry. b = ff_q_gprod_factorization_existsirreducibleentry * S ((S (gr_factor_index_factorization_existsirreducible)) * c) + (gr_factor_value_factorization_existsirreducible))) -> (((exists ge_real_positive_factorization_existsirreducibleirreduciblecarrier ge_real_negative_factorization_existsirreducibleirreduciblecarrier ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier. (exists ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode. (((gr_factor_value_factorization_existsirreducible) = ((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factorization_existsirreducibleirreduciblecarrier) /\ (ge_real_negative_factorization_existsirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factorization_existsirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factorization_existsirreducibleirreduciblecarrier) = S ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier) = S ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factorization_existsirreducible)=0)) /\ ((~(exists gr_inverse_factorization_existsirreducibleirreduciblenonunit. (exists ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factorization_existsirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblenonunit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factorization_existsirreducibleirreducible gr_second_factor_factorization_existsirreducibleirreducible. (exists ge_first_rp_factorization_existsirreducibleirreduciblefactorization ge_first_rn_factorization_existsirreducibleirreduciblefactorization ge_first_ip_factorization_existsirreducibleirreduciblefactorization ge_first_in_factorization_existsirreducibleirreduciblefactorization ge_second_rp_factorization_existsirreducibleirreduciblefactorization ge_second_rn_factorization_existsirreducibleirreduciblefactorization ge_second_ip_factorization_existsirreducibleirreduciblefactorization ge_second_in_factorization_existsirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factorization_existsirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factorization_existsirreducibleirreduciblefirst_unit. (exists ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factorization_existsirreducibleirreduciblesecond_unit. (exists ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factorization_exists. ((exists gr_product_trace_factorization_existstrace gr_product_scale_factorization_existstrace. ((((exists ff_h_gprod_factorization_existstracestart. ff_h_gprod_factorization_existstracestart + S (6) = S ((S (0)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestart. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestart * S ((S (0)) * gr_product_scale_factorization_existstrace) + (6))) /\ ((((exists ff_h_gprod_factorization_existstraceend. ff_h_gprod_factorization_existstraceend + S (gr_factor_product_factorization_exists) = S ((S (l)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstraceend. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstraceend * S ((S (l)) * gr_product_scale_factorization_existstrace) + (gr_factor_product_factorization_exists))) /\ (forall gr_product_index_factorization_existstracesteps. (exists ge_gap_factorization_existstracestepsindex_bound. ge_gap_factorization_existstracestepsindex_bound + S (gr_product_index_factorization_existstracesteps) = (l)) -> exists gr_product_factor_factorization_existstracesteps gr_product_before_factorization_existstracesteps gr_product_after_factorization_existstracesteps. ((((exists ff_h_gprod_factorization_existstracestepsfactor. ff_h_gprod_factorization_existstracestepsfactor + S (gr_product_factor_factorization_existstracesteps) = S ((S (gr_product_index_factorization_existstracesteps)) * c)) /\ exists ff_q_gprod_factorization_existstracestepsfactor. b = ff_q_gprod_factorization_existstracestepsfactor * S ((S (gr_product_index_factorization_existstracesteps)) * c) + (gr_product_factor_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_factorization_existstracestepsbefore. ff_h_gprod_factorization_existstracestepsbefore + S (gr_product_before_factorization_existstracesteps) = S ((S (gr_product_index_factorization_existstracesteps)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestepsbefore. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestepsbefore * S ((S (gr_product_index_factorization_existstracesteps)) * gr_product_scale_factorization_existstrace) + (gr_product_before_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_factorization_existstracestepsafter. ff_h_gprod_factorization_existstracestepsafter + S (gr_product_after_factorization_existstracesteps) = S ((S (S (gr_product_index_factorization_existstracesteps))) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestepsafter. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestepsafter * S ((S (S (gr_product_index_factorization_existstracesteps))) * gr_product_scale_factorization_existstrace) + (gr_product_after_factorization_existstracesteps))) /\ (exists ge_first_rp_factorization_existstracestepsmultiply ge_first_rn_factorization_existstracestepsmultiply ge_first_ip_factorization_existstracestepsmultiply ge_first_in_factorization_existstracestepsmultiply ge_second_rp_factorization_existstracestepsmultiply ge_second_rn_factorization_existstracestepsmultiply ge_second_ip_factorization_existstracestepsmultiply ge_second_in_factorization_existstracestepsmultiply. ((exists ge_representation_real_code_factorization_existstracestepsmultiplyfirst ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst. (((gr_product_before_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplyfirstreal ge_balance_negative_factorization_existstracestepsmultiplyfirstreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyfirstreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstreal) = S ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplyfirstreal = (ge_first_rn_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary) = S ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary = (ge_first_in_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existstracestepsmultiplysecond ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond. (((gr_product_factor_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplysecondreal ge_balance_negative_factorization_existstracestepsmultiplysecondreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplysecondreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondreal) = S ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplysecondreal = (ge_second_rn_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary) = S ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary = (ge_second_in_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existstracestepsmultiplyoutput ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput. (((gr_product_after_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplyoutputreal ge_balance_negative_factorization_existstracestepsmultiplyoutputreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyoutputreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputreal) = S ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))))))) + ge_balance_negative_factorization_existstracestepsmultiplyoutputreal = (((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))))))) + ge_balance_positive_factorization_existstracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary) = S ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))))))) + ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))))))) + ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factorization_existsreconstruct ge_first_rn_factorization_existsreconstruct ge_first_ip_factorization_existsreconstruct ge_first_in_factorization_existsreconstruct ge_second_rp_factorization_existsreconstruct ge_second_rn_factorization_existsreconstruct ge_second_ip_factorization_existsreconstruct ge_second_in_factorization_existsreconstruct. ((exists ge_representation_real_code_factorization_existsreconstructfirst ge_representation_imaginary_code_factorization_existsreconstructfirst. (((u) = ((ge_representation_real_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst)) * S ((ge_representation_real_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst)) + ((ge_representation_imaginary_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst))) /\ ((exists ge_balance_positive_factorization_existsreconstructfirstreal ge_balance_negative_factorization_existsreconstructfirstreal. (((((ge_representation_real_code_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_factorization_existsreconstructfirstreal) /\ (ge_balance_negative_factorization_existsreconstructfirstreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructfirstrealdecode. (((ge_representation_real_code_factorization_existsreconstructfirst) = 2 * ge_signed_half_factorization_existsreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructfirstreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructfirstreal) = S ge_signed_half_factorization_existsreconstructfirstrealdecode))) /\ ((ge_first_rp_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructfirstreal = (ge_first_rn_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructfirstreal))) /\ (exists ge_balance_positive_factorization_existsreconstructfirstimaginary ge_balance_negative_factorization_existsreconstructfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_factorization_existsreconstructfirstimaginary) /\ (ge_balance_negative_factorization_existsreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructfirst) = 2 * ge_signed_half_factorization_existsreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructfirstimaginary) = S ge_signed_half_factorization_existsreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructfirstimaginary = (ge_first_in_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsreconstructsecond ge_representation_imaginary_code_factorization_existsreconstructsecond. (((gr_factor_product_factorization_exists) = ((ge_representation_real_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond)) * S ((ge_representation_real_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond)) + ((ge_representation_imaginary_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond))) /\ ((exists ge_balance_positive_factorization_existsreconstructsecondreal ge_balance_negative_factorization_existsreconstructsecondreal. (((((ge_representation_real_code_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_factorization_existsreconstructsecondreal) /\ (ge_balance_negative_factorization_existsreconstructsecondreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructsecondrealdecode. (((ge_representation_real_code_factorization_existsreconstructsecond) = 2 * ge_signed_half_factorization_existsreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructsecondreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructsecondreal) = S ge_signed_half_factorization_existsreconstructsecondrealdecode))) /\ ((ge_second_rp_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructsecondreal = (ge_second_rn_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructsecondreal))) /\ (exists ge_balance_positive_factorization_existsreconstructsecondimaginary ge_balance_negative_factorization_existsreconstructsecondimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_factorization_existsreconstructsecondimaginary) /\ (ge_balance_negative_factorization_existsreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructsecond) = 2 * ge_signed_half_factorization_existsreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructsecondimaginary) = S ge_signed_half_factorization_existsreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructsecondimaginary = (ge_second_in_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsreconstructoutput ge_representation_imaginary_code_factorization_existsreconstructoutput. (((z) = ((ge_representation_real_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput)) * S ((ge_representation_real_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput)) + ((ge_representation_imaginary_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput))) /\ ((exists ge_balance_positive_factorization_existsreconstructoutputreal ge_balance_negative_factorization_existsreconstructoutputreal. (((((ge_representation_real_code_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_factorization_existsreconstructoutputreal) /\ (ge_balance_negative_factorization_existsreconstructoutputreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructoutputrealdecode. (((ge_representation_real_code_factorization_existsreconstructoutput) = 2 * ge_signed_half_factorization_existsreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructoutputreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructoutputreal) = S ge_signed_half_factorization_existsreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))))))) + ge_balance_negative_factorization_existsreconstructoutputreal = (((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))))))) + ge_balance_positive_factorization_existsreconstructoutputreal))) /\ (exists ge_balance_positive_factorization_existsreconstructoutputimaginary ge_balance_negative_factorization_existsreconstructoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_factorization_existsreconstructoutputimaginary) /\ (ge_balance_negative_factorization_existsreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructoutput) = 2 * ge_signed_half_factorization_existsreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructoutputimaginary) = S ge_signed_half_factorization_existsreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))))))) + ge_balance_negative_factorization_existsreconstructoutputimaginary = (((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))))))) + ge_balance_positive_factorization_existsreconstructoutputimaginary))))))))))))))