gaussian_factor_swapped_product_exists

Exact expanded first-order arithmetic statement

forall b c l i p P. (forall gr_factor_index_swap_product_original_factors gr_factor_value_swap_product_original_factors. (exists ge_gap_swap_product_original_factorsindex. ge_gap_swap_product_original_factorsindex + S (gr_factor_index_swap_product_original_factors) = (S l)) -> (((exists ff_h_gprod_swap_product_original_factorsentry. ff_h_gprod_swap_product_original_factorsentry + S (gr_factor_value_swap_product_original_factors) = S ((S (gr_factor_index_swap_product_original_factors)) * c)) /\ exists ff_q_gprod_swap_product_original_factorsentry. b = ff_q_gprod_swap_product_original_factorsentry * S ((S (gr_factor_index_swap_product_original_factors)) * c) + (gr_factor_value_swap_product_original_factors))) -> (((exists ge_real_positive_swap_product_original_factorsirreduciblecarrier ge_real_negative_swap_product_original_factorsirreduciblecarrier ge_imaginary_positive_swap_product_original_factorsirreduciblecarrier ge_imaginary_negative_swap_product_original_factorsirreduciblecarrier. (exists ge_real_code_swap_product_original_factorsirreduciblecarrierdecode ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode. (((gr_factor_value_swap_product_original_factors) = ((ge_real_code_swap_product_original_factorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode)) * S ((ge_real_code_swap_product_original_factorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode)) + ((ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode))) /\ (((((ge_real_code_swap_product_original_factorsirreduciblecarrierdecode) = 2 * (ge_real_positive_swap_product_original_factorsirreduciblecarrier) /\ (ge_real_negative_swap_product_original_factorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_real. (((ge_real_code_swap_product_original_factorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_swap_product_original_factorsirreduciblecarrier) = 0) /\ (ge_real_negative_swap_product_original_factorsirreduciblecarrier) = S ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_swap_product_original_factorsirreduciblecarrier) /\ (ge_imaginary_negative_swap_product_original_factorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_swap_product_original_factorsirreduciblecarrier) = 0) /\ (ge_imaginary_negative_swap_product_original_factorsirreduciblecarrier) = S ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_swap_product_original_factors)=0)) /\ ((~(exists gr_inverse_swap_product_original_factorsirreduciblenonunit. (exists ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity ge_first_in_swap_product_original_factorsirreduciblenonunitidentity ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity ge_second_in_swap_product_original_factorsirreduciblenonunitidentity. ((exists ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst. (((gr_factor_value_swap_product_original_factors) = ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstreal ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstreal) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstreal = (ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary = (ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond. (((gr_inverse_swap_product_original_factorsirreduciblenonunit) = ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondreal ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondreal) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondreal = (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary = (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputreal ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputreal) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_swap_product_original_factorsirreducible gr_second_factor_swap_product_original_factorsirreducible. (exists ge_first_rp_swap_product_original_factorsirreduciblefactorization ge_first_rn_swap_product_original_factorsirreduciblefactorization ge_first_ip_swap_product_original_factorsirreduciblefactorization ge_first_in_swap_product_original_factorsirreduciblefactorization ge_second_rp_swap_product_original_factorsirreduciblefactorization ge_second_rn_swap_product_original_factorsirreduciblefactorization ge_second_ip_swap_product_original_factorsirreduciblefactorization ge_second_in_swap_product_original_factorsirreduciblefactorization. ((exists ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst. (((gr_first_factor_swap_product_original_factorsirreducible) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstreal ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstreal) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_factorsirreduciblefactorization) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstreal = (ge_first_rn_swap_product_original_factorsirreduciblefactorization) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstimaginary ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_factorsirreduciblefactorization) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstimaginary = (ge_first_in_swap_product_original_factorsirreduciblefactorization) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond. (((gr_second_factor_swap_product_original_factorsirreducible) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondreal ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondreal) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_swap_product_original_factorsirreduciblefactorization) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondreal = (ge_second_rn_swap_product_original_factorsirreduciblefactorization) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondimaginary ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_factorsirreduciblefactorization) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondimaginary = (ge_second_in_swap_product_original_factorsirreduciblefactorization) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput. (((gr_factor_value_swap_product_original_factors) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputreal ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputreal) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblefactorization) * (ge_second_rp_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_rn_swap_product_original_factorsirreduciblefactorization) * (ge_second_rn_swap_product_original_factorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefactorization) * (ge_second_in_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_in_swap_product_original_factorsirreduciblefactorization) * (ge_second_ip_swap_product_original_factorsirreduciblefactorization))))))) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputreal = (((((((ge_first_rp_swap_product_original_factorsirreduciblefactorization) * (ge_second_rn_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_rn_swap_product_original_factorsirreduciblefactorization) * (ge_second_rp_swap_product_original_factorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefactorization) * (ge_second_ip_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_in_swap_product_original_factorsirreduciblefactorization) * (ge_second_in_swap_product_original_factorsirreduciblefactorization))))))) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputimaginary ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblefactorization) * (ge_second_ip_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_rn_swap_product_original_factorsirreduciblefactorization) * (ge_second_in_swap_product_original_factorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefactorization) * (ge_second_rp_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_in_swap_product_original_factorsirreduciblefactorization) * (ge_second_rn_swap_product_original_factorsirreduciblefactorization))))))) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_swap_product_original_factorsirreduciblefactorization) * (ge_second_in_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_rn_swap_product_original_factorsirreduciblefactorization) * (ge_second_ip_swap_product_original_factorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefactorization) * (ge_second_rn_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_in_swap_product_original_factorsirreduciblefactorization) * (ge_second_rp_swap_product_original_factorsirreduciblefactorization))))))) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_swap_product_original_factorsirreduciblefirst_unit. (exists ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity. ((exists ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst. (((gr_first_factor_swap_product_original_factorsirreducible) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal = (ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond. (((gr_inverse_swap_product_original_factorsirreduciblefirst_unit) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal = (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_swap_product_original_factorsirreduciblesecond_unit. (exists ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity. ((exists ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst. (((gr_second_factor_swap_product_original_factorsirreducible) = ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal = (ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond. (((gr_inverse_swap_product_original_factorsirreduciblesecond_unit) = ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal = (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (exists gr_product_trace_swap_product_original_trace gr_product_scale_swap_product_original_trace. ((((exists ff_h_gprod_swap_product_original_tracestart. ff_h_gprod_swap_product_original_tracestart + S (6) = S ((S (0)) * gr_product_scale_swap_product_original_trace)) /\ exists ff_q_gprod_swap_product_original_tracestart. gr_product_trace_swap_product_original_trace = ff_q_gprod_swap_product_original_tracestart * S ((S (0)) * gr_product_scale_swap_product_original_trace) + (6))) /\ ((((exists ff_h_gprod_swap_product_original_traceend. ff_h_gprod_swap_product_original_traceend + S (P) = S ((S (S l)) * gr_product_scale_swap_product_original_trace)) /\ exists ff_q_gprod_swap_product_original_traceend. gr_product_trace_swap_product_original_trace = ff_q_gprod_swap_product_original_traceend * S ((S (S l)) * gr_product_scale_swap_product_original_trace) + (P))) /\ (forall gr_product_index_swap_product_original_tracesteps. (exists ge_gap_swap_product_original_tracestepsindex_bound. ge_gap_swap_product_original_tracestepsindex_bound + S (gr_product_index_swap_product_original_tracesteps) = (S l)) -> exists gr_product_factor_swap_product_original_tracesteps gr_product_before_swap_product_original_tracesteps gr_product_after_swap_product_original_tracesteps. ((((exists ff_h_gprod_swap_product_original_tracestepsfactor. ff_h_gprod_swap_product_original_tracestepsfactor + S (gr_product_factor_swap_product_original_tracesteps) = S ((S (gr_product_index_swap_product_original_tracesteps)) * c)) /\ exists ff_q_gprod_swap_product_original_tracestepsfactor. b = ff_q_gprod_swap_product_original_tracestepsfactor * S ((S (gr_product_index_swap_product_original_tracesteps)) * c) + (gr_product_factor_swap_product_original_tracesteps))) /\ ((((exists ff_h_gprod_swap_product_original_tracestepsbefore. ff_h_gprod_swap_product_original_tracestepsbefore + S (gr_product_before_swap_product_original_tracesteps) = S ((S (gr_product_index_swap_product_original_tracesteps)) * gr_product_scale_swap_product_original_trace)) /\ exists ff_q_gprod_swap_product_original_tracestepsbefore. gr_product_trace_swap_product_original_trace = ff_q_gprod_swap_product_original_tracestepsbefore * S ((S (gr_product_index_swap_product_original_tracesteps)) * gr_product_scale_swap_product_original_trace) + (gr_product_before_swap_product_original_tracesteps))) /\ ((((exists ff_h_gprod_swap_product_original_tracestepsafter. ff_h_gprod_swap_product_original_tracestepsafter + S (gr_product_after_swap_product_original_tracesteps) = S ((S (S (gr_product_index_swap_product_original_tracesteps))) * gr_product_scale_swap_product_original_trace)) /\ exists ff_q_gprod_swap_product_original_tracestepsafter. gr_product_trace_swap_product_original_trace = ff_q_gprod_swap_product_original_tracestepsafter * S ((S (S (gr_product_index_swap_product_original_tracesteps))) * gr_product_scale_swap_product_original_trace) + (gr_product_after_swap_product_original_tracesteps))) /\ (exists ge_first_rp_swap_product_original_tracestepsmultiply ge_first_rn_swap_product_original_tracestepsmultiply ge_first_ip_swap_product_original_tracestepsmultiply ge_first_in_swap_product_original_tracestepsmultiply ge_second_rp_swap_product_original_tracestepsmultiply ge_second_rn_swap_product_original_tracestepsmultiply ge_second_ip_swap_product_original_tracestepsmultiply ge_second_in_swap_product_original_tracestepsmultiply. ((exists ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst. (((gr_product_before_swap_product_original_tracesteps) = ((ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst)) * S ((ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_product_original_tracestepsmultiplyfirstreal ge_balance_negative_swap_product_original_tracestepsmultiplyfirstreal. (((((ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplyfirstreal) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyfirstreal) = S ge_signed_half_swap_product_original_tracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_tracestepsmultiply) + ge_balance_negative_swap_product_original_tracestepsmultiplyfirstreal = (ge_first_rn_swap_product_original_tracestepsmultiply) + ge_balance_positive_swap_product_original_tracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_product_original_tracestepsmultiplyfirstimaginary ge_balance_negative_swap_product_original_tracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyfirstimaginary) = S ge_signed_half_swap_product_original_tracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_tracestepsmultiply) + ge_balance_negative_swap_product_original_tracestepsmultiplyfirstimaginary = (ge_first_in_swap_product_original_tracestepsmultiply) + ge_balance_positive_swap_product_original_tracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_tracestepsmultiplysecond ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond. (((gr_product_factor_swap_product_original_tracesteps) = ((ge_representation_real_code_swap_product_original_tracestepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond)) * S ((ge_representation_real_code_swap_product_original_tracestepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_product_original_tracestepsmultiplysecondreal ge_balance_negative_swap_product_original_tracestepsmultiplysecondreal. (((((ge_representation_real_code_swap_product_original_tracestepsmultiplysecond) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplysecondreal) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_product_original_tracestepsmultiplysecond) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplysecondreal) = S ge_signed_half_swap_product_original_tracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_product_original_tracestepsmultiply) + ge_balance_negative_swap_product_original_tracestepsmultiplysecondreal = (ge_second_rn_swap_product_original_tracestepsmultiply) + ge_balance_positive_swap_product_original_tracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_product_original_tracestepsmultiplysecondimaginary ge_balance_negative_swap_product_original_tracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplysecondimaginary) = S ge_signed_half_swap_product_original_tracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_tracestepsmultiply) + ge_balance_negative_swap_product_original_tracestepsmultiplysecondimaginary = (ge_second_in_swap_product_original_tracestepsmultiply) + ge_balance_positive_swap_product_original_tracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput. (((gr_product_after_swap_product_original_tracesteps) = ((ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput)) * S ((ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_product_original_tracestepsmultiplyoutputreal ge_balance_negative_swap_product_original_tracestepsmultiplyoutputreal. (((((ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplyoutputreal) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyoutputreal) = S ge_signed_half_swap_product_original_tracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_tracestepsmultiply) * (ge_second_rp_swap_product_original_tracestepsmultiply))) + (((ge_first_rn_swap_product_original_tracestepsmultiply) * (ge_second_rn_swap_product_original_tracestepsmultiply))))) + (((((ge_first_ip_swap_product_original_tracestepsmultiply) * (ge_second_in_swap_product_original_tracestepsmultiply))) + (((ge_first_in_swap_product_original_tracestepsmultiply) * (ge_second_ip_swap_product_original_tracestepsmultiply))))))) + ge_balance_negative_swap_product_original_tracestepsmultiplyoutputreal = (((((((ge_first_rp_swap_product_original_tracestepsmultiply) * (ge_second_rn_swap_product_original_tracestepsmultiply))) + (((ge_first_rn_swap_product_original_tracestepsmultiply) * (ge_second_rp_swap_product_original_tracestepsmultiply))))) + (((((ge_first_ip_swap_product_original_tracestepsmultiply) * (ge_second_ip_swap_product_original_tracestepsmultiply))) + (((ge_first_in_swap_product_original_tracestepsmultiply) * (ge_second_in_swap_product_original_tracestepsmultiply))))))) + ge_balance_positive_swap_product_original_tracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_product_original_tracestepsmultiplyoutputimaginary ge_balance_negative_swap_product_original_tracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyoutputimaginary) = S ge_signed_half_swap_product_original_tracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_tracestepsmultiply) * (ge_second_ip_swap_product_original_tracestepsmultiply))) + (((ge_first_rn_swap_product_original_tracestepsmultiply) * (ge_second_in_swap_product_original_tracestepsmultiply))))) + (((((ge_first_ip_swap_product_original_tracestepsmultiply) * (ge_second_rp_swap_product_original_tracestepsmultiply))) + (((ge_first_in_swap_product_original_tracestepsmultiply) * (ge_second_rn_swap_product_original_tracestepsmultiply))))))) + ge_balance_negative_swap_product_original_tracestepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_product_original_tracestepsmultiply) * (ge_second_in_swap_product_original_tracestepsmultiply))) + (((ge_first_rn_swap_product_original_tracestepsmultiply) * (ge_second_ip_swap_product_original_tracestepsmultiply))))) + (((((ge_first_ip_swap_product_original_tracestepsmultiply) * (ge_second_rn_swap_product_original_tracestepsmultiply))) + (((ge_first_in_swap_product_original_tracestepsmultiply) * (ge_second_rp_swap_product_original_tracestepsmultiply))))))) + ge_balance_positive_swap_product_original_tracestepsmultiplyoutputimaginary)))))))))))))))) -> (exists ge_gap_swap_product_selected_index. ge_gap_swap_product_selected_index + S (i) = (l)) -> (((exists ff_h_gprod_swap_product_selected_factor. ff_h_gprod_swap_product_selected_factor + S (p) = S ((S (i)) * c)) /\ exists ff_q_gprod_swap_product_selected_factor. b = ff_q_gprod_swap_product_selected_factor * S ((S (i)) * c) + (p))) -> exists d e q. (((forall gr_factor_index_swap_product_resultfactors gr_factor_value_swap_product_resultfactors. (exists ge_gap_swap_product_resultfactorsindex. ge_gap_swap_product_resultfactorsindex + S (gr_factor_index_swap_product_resultfactors) = (S (l))) -> (((exists ff_h_gprod_swap_product_resultfactorsentry. ff_h_gprod_swap_product_resultfactorsentry + S (gr_factor_value_swap_product_resultfactors) = S ((S (gr_factor_index_swap_product_resultfactors)) * e)) /\ exists ff_q_gprod_swap_product_resultfactorsentry. d = ff_q_gprod_swap_product_resultfactorsentry * S ((S (gr_factor_index_swap_product_resultfactors)) * e) + (gr_factor_value_swap_product_resultfactors))) -> (((exists ge_real_positive_swap_product_resultfactorsirreduciblecarrier ge_real_negative_swap_product_resultfactorsirreduciblecarrier ge_imaginary_positive_swap_product_resultfactorsirreduciblecarrier ge_imaginary_negative_swap_product_resultfactorsirreduciblecarrier. (exists ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode. (((gr_factor_value_swap_product_resultfactors) = ((ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode)) * S ((ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode)) + ((ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode))) /\ (((((ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode) = 2 * (ge_real_positive_swap_product_resultfactorsirreduciblecarrier) /\ (ge_real_negative_swap_product_resultfactorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_real. (((ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_swap_product_resultfactorsirreduciblecarrier) = 0) /\ (ge_real_negative_swap_product_resultfactorsirreduciblecarrier) = S ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_swap_product_resultfactorsirreduciblecarrier) /\ (ge_imaginary_negative_swap_product_resultfactorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_swap_product_resultfactorsirreduciblecarrier) = 0) /\ (ge_imaginary_negative_swap_product_resultfactorsirreduciblecarrier) = S ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_swap_product_resultfactors)=0)) /\ ((~(exists gr_inverse_swap_product_resultfactorsirreduciblenonunit. (exists ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity. ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst. (((gr_factor_value_swap_product_resultfactors) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstreal ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstreal) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstreal = (ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary = (ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond. (((gr_inverse_swap_product_resultfactorsirreduciblenonunit) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondreal ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondreal) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondreal = (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary = (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputreal ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputreal) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_swap_product_resultfactorsirreducible gr_second_factor_swap_product_resultfactorsirreducible. (exists ge_first_rp_swap_product_resultfactorsirreduciblefactorization ge_first_rn_swap_product_resultfactorsirreduciblefactorization ge_first_ip_swap_product_resultfactorsirreduciblefactorization ge_first_in_swap_product_resultfactorsirreduciblefactorization ge_second_rp_swap_product_resultfactorsirreduciblefactorization ge_second_rn_swap_product_resultfactorsirreduciblefactorization ge_second_ip_swap_product_resultfactorsirreduciblefactorization ge_second_in_swap_product_resultfactorsirreduciblefactorization. ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst. (((gr_first_factor_swap_product_resultfactorsirreducible) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstreal ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstreal = (ge_first_rn_swap_product_resultfactorsirreduciblefactorization) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstimaginary = (ge_first_in_swap_product_resultfactorsirreduciblefactorization) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond. (((gr_second_factor_swap_product_resultfactorsirreducible) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondreal ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_swap_product_resultfactorsirreduciblefactorization) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondreal = (ge_second_rn_swap_product_resultfactorsirreduciblefactorization) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultfactorsirreduciblefactorization) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondimaginary = (ge_second_in_swap_product_resultfactorsirreduciblefactorization) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput. (((gr_factor_value_swap_product_resultfactors) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputreal ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rp_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rn_swap_product_resultfactorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) * (ge_second_in_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_in_swap_product_resultfactorsirreduciblefactorization) * (ge_second_ip_swap_product_resultfactorsirreduciblefactorization))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputreal = (((((((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rn_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rp_swap_product_resultfactorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) * (ge_second_ip_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_in_swap_product_resultfactorsirreduciblefactorization) * (ge_second_in_swap_product_resultfactorsirreduciblefactorization))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) * (ge_second_ip_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefactorization) * (ge_second_in_swap_product_resultfactorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rp_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_in_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rn_swap_product_resultfactorsirreduciblefactorization))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) * (ge_second_in_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefactorization) * (ge_second_ip_swap_product_resultfactorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rn_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_in_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rp_swap_product_resultfactorsirreduciblefactorization))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_swap_product_resultfactorsirreduciblefirst_unit. (exists ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity. ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst. (((gr_first_factor_swap_product_resultfactorsirreducible) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal = (ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond. (((gr_inverse_swap_product_resultfactorsirreduciblefirst_unit) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal = (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_swap_product_resultfactorsirreduciblesecond_unit. (exists ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity. ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst. (((gr_second_factor_swap_product_resultfactorsirreducible) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal = (ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond. (((gr_inverse_swap_product_resultfactorsirreduciblesecond_unit) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal = (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ ((exists gr_product_trace_swap_product_resultproduct gr_product_scale_swap_product_resultproduct. ((((exists ff_h_gprod_swap_product_resultproductstart. ff_h_gprod_swap_product_resultproductstart + S (6) = S ((S (0)) * gr_product_scale_swap_product_resultproduct)) /\ exists ff_q_gprod_swap_product_resultproductstart. gr_product_trace_swap_product_resultproduct = ff_q_gprod_swap_product_resultproductstart * S ((S (0)) * gr_product_scale_swap_product_resultproduct) + (6))) /\ ((((exists ff_h_gprod_swap_product_resultproductend. ff_h_gprod_swap_product_resultproductend + S (P) = S ((S (S (l))) * gr_product_scale_swap_product_resultproduct)) /\ exists ff_q_gprod_swap_product_resultproductend. gr_product_trace_swap_product_resultproduct = ff_q_gprod_swap_product_resultproductend * S ((S (S (l))) * gr_product_scale_swap_product_resultproduct) + (P))) /\ (forall gr_product_index_swap_product_resultproductsteps. (exists ge_gap_swap_product_resultproductstepsindex_bound. ge_gap_swap_product_resultproductstepsindex_bound + S (gr_product_index_swap_product_resultproductsteps) = (S (l))) -> exists gr_product_factor_swap_product_resultproductsteps gr_product_before_swap_product_resultproductsteps gr_product_after_swap_product_resultproductsteps. ((((exists ff_h_gprod_swap_product_resultproductstepsfactor. ff_h_gprod_swap_product_resultproductstepsfactor + S (gr_product_factor_swap_product_resultproductsteps) = S ((S (gr_product_index_swap_product_resultproductsteps)) * e)) /\ exists ff_q_gprod_swap_product_resultproductstepsfactor. d = ff_q_gprod_swap_product_resultproductstepsfactor * S ((S (gr_product_index_swap_product_resultproductsteps)) * e) + (gr_product_factor_swap_product_resultproductsteps))) /\ ((((exists ff_h_gprod_swap_product_resultproductstepsbefore. ff_h_gprod_swap_product_resultproductstepsbefore + S (gr_product_before_swap_product_resultproductsteps) = S ((S (gr_product_index_swap_product_resultproductsteps)) * gr_product_scale_swap_product_resultproduct)) /\ exists ff_q_gprod_swap_product_resultproductstepsbefore. gr_product_trace_swap_product_resultproduct = ff_q_gprod_swap_product_resultproductstepsbefore * S ((S (gr_product_index_swap_product_resultproductsteps)) * gr_product_scale_swap_product_resultproduct) + (gr_product_before_swap_product_resultproductsteps))) /\ ((((exists ff_h_gprod_swap_product_resultproductstepsafter. ff_h_gprod_swap_product_resultproductstepsafter + S (gr_product_after_swap_product_resultproductsteps) = S ((S (S (gr_product_index_swap_product_resultproductsteps))) * gr_product_scale_swap_product_resultproduct)) /\ exists ff_q_gprod_swap_product_resultproductstepsafter. gr_product_trace_swap_product_resultproduct = ff_q_gprod_swap_product_resultproductstepsafter * S ((S (S (gr_product_index_swap_product_resultproductsteps))) * gr_product_scale_swap_product_resultproduct) + (gr_product_after_swap_product_resultproductsteps))) /\ (exists ge_first_rp_swap_product_resultproductstepsmultiply ge_first_rn_swap_product_resultproductstepsmultiply ge_first_ip_swap_product_resultproductstepsmultiply ge_first_in_swap_product_resultproductstepsmultiply ge_second_rp_swap_product_resultproductstepsmultiply ge_second_rn_swap_product_resultproductstepsmultiply ge_second_ip_swap_product_resultproductstepsmultiply ge_second_in_swap_product_resultproductstepsmultiply. ((exists ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst. (((gr_product_before_swap_product_resultproductsteps) = ((ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst)) * S ((ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_product_resultproductstepsmultiplyfirstreal ge_balance_negative_swap_product_resultproductstepsmultiplyfirstreal. (((((ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplyfirstreal) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyfirstreal) = S ge_signed_half_swap_product_resultproductstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultproductstepsmultiply) + ge_balance_negative_swap_product_resultproductstepsmultiplyfirstreal = (ge_first_rn_swap_product_resultproductstepsmultiply) + ge_balance_positive_swap_product_resultproductstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_product_resultproductstepsmultiplyfirstimaginary ge_balance_negative_swap_product_resultproductstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyfirstimaginary) = S ge_signed_half_swap_product_resultproductstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultproductstepsmultiply) + ge_balance_negative_swap_product_resultproductstepsmultiplyfirstimaginary = (ge_first_in_swap_product_resultproductstepsmultiply) + ge_balance_positive_swap_product_resultproductstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultproductstepsmultiplysecond ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond. (((gr_product_factor_swap_product_resultproductsteps) = ((ge_representation_real_code_swap_product_resultproductstepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond)) * S ((ge_representation_real_code_swap_product_resultproductstepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_product_resultproductstepsmultiplysecondreal ge_balance_negative_swap_product_resultproductstepsmultiplysecondreal. (((((ge_representation_real_code_swap_product_resultproductstepsmultiplysecond) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplysecondreal) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_product_resultproductstepsmultiplysecond) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplysecondreal) = S ge_signed_half_swap_product_resultproductstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_product_resultproductstepsmultiply) + ge_balance_negative_swap_product_resultproductstepsmultiplysecondreal = (ge_second_rn_swap_product_resultproductstepsmultiply) + ge_balance_positive_swap_product_resultproductstepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_product_resultproductstepsmultiplysecondimaginary ge_balance_negative_swap_product_resultproductstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplysecondimaginary) = S ge_signed_half_swap_product_resultproductstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultproductstepsmultiply) + ge_balance_negative_swap_product_resultproductstepsmultiplysecondimaginary = (ge_second_in_swap_product_resultproductstepsmultiply) + ge_balance_positive_swap_product_resultproductstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput. (((gr_product_after_swap_product_resultproductsteps) = ((ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput)) * S ((ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_product_resultproductstepsmultiplyoutputreal ge_balance_negative_swap_product_resultproductstepsmultiplyoutputreal. (((((ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplyoutputreal) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyoutputreal) = S ge_signed_half_swap_product_resultproductstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultproductstepsmultiply) * (ge_second_rp_swap_product_resultproductstepsmultiply))) + (((ge_first_rn_swap_product_resultproductstepsmultiply) * (ge_second_rn_swap_product_resultproductstepsmultiply))))) + (((((ge_first_ip_swap_product_resultproductstepsmultiply) * (ge_second_in_swap_product_resultproductstepsmultiply))) + (((ge_first_in_swap_product_resultproductstepsmultiply) * (ge_second_ip_swap_product_resultproductstepsmultiply))))))) + ge_balance_negative_swap_product_resultproductstepsmultiplyoutputreal = (((((((ge_first_rp_swap_product_resultproductstepsmultiply) * (ge_second_rn_swap_product_resultproductstepsmultiply))) + (((ge_first_rn_swap_product_resultproductstepsmultiply) * (ge_second_rp_swap_product_resultproductstepsmultiply))))) + (((((ge_first_ip_swap_product_resultproductstepsmultiply) * (ge_second_ip_swap_product_resultproductstepsmultiply))) + (((ge_first_in_swap_product_resultproductstepsmultiply) * (ge_second_in_swap_product_resultproductstepsmultiply))))))) + ge_balance_positive_swap_product_resultproductstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_product_resultproductstepsmultiplyoutputimaginary ge_balance_negative_swap_product_resultproductstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyoutputimaginary) = S ge_signed_half_swap_product_resultproductstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultproductstepsmultiply) * (ge_second_ip_swap_product_resultproductstepsmultiply))) + (((ge_first_rn_swap_product_resultproductstepsmultiply) * (ge_second_in_swap_product_resultproductstepsmultiply))))) + (((((ge_first_ip_swap_product_resultproductstepsmultiply) * (ge_second_rp_swap_product_resultproductstepsmultiply))) + (((ge_first_in_swap_product_resultproductstepsmultiply) * (ge_second_rn_swap_product_resultproductstepsmultiply))))))) + ge_balance_negative_swap_product_resultproductstepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_product_resultproductstepsmultiply) * (ge_second_in_swap_product_resultproductstepsmultiply))) + (((ge_first_rn_swap_product_resultproductstepsmultiply) * (ge_second_ip_swap_product_resultproductstepsmultiply))))) + (((((ge_first_ip_swap_product_resultproductstepsmultiply) * (ge_second_rn_swap_product_resultproductstepsmultiply))) + (((ge_first_in_swap_product_resultproductstepsmultiply) * (ge_second_rp_swap_product_resultproductstepsmultiply))))))) + ge_balance_positive_swap_product_resultproductstepsmultiplyoutputimaginary)))))))))))))))) /\ (((((exists ff_h_pfp_swap_product_resultswapoldi. ff_h_pfp_swap_product_resultswapoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_product_resultswapoldi. b = ff_q_pfp_swap_product_resultswapoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_product_resultswapoldlast. ff_h_pfp_swap_product_resultswapoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_product_resultswapoldlast. b = ff_q_pfp_swap_product_resultswapoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swap_product_resultswapnewi. ff_h_pfp_swap_product_resultswapnewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_product_resultswapnewi. d = ff_q_pfp_swap_product_resultswapnewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swap_product_resultswapnewlast. ff_h_pfp_swap_product_resultswapnewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_product_resultswapnewlast. d = ff_q_pfp_swap_product_resultswapnewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap_product_resultswap pfp_a_swap_product_resultswap. (exists pfp_gap_swap_product_resultswapbound. pfp_gap_swap_product_resultswapbound + S (pfp_j_swap_product_resultswap) = (S (l))) -> ~(pfp_j_swap_product_resultswap = i) -> ~(pfp_j_swap_product_resultswap = l) -> (((exists ff_h_pfp_swap_product_resultswapold. ff_h_pfp_swap_product_resultswapold + S (pfp_a_swap_product_resultswap) = S ((S (pfp_j_swap_product_resultswap)) * c)) /\ exists ff_q_pfp_swap_product_resultswapold. b = ff_q_pfp_swap_product_resultswapold * S ((S (pfp_j_swap_product_resultswap)) * c) + (pfp_a_swap_product_resultswap))) -> (((exists ff_h_pfp_swap_product_resultswapnew. ff_h_pfp_swap_product_resultswapnew + S (pfp_a_swap_product_resultswap) = S ((S (pfp_j_swap_product_resultswap)) * e)) /\ exists ff_q_pfp_swap_product_resultswapnew. d = ff_q_pfp_swap_product_resultswapnew * S ((S (pfp_j_swap_product_resultswap)) * e) + (pfp_a_swap_product_resultswap)))))))))))))))