gaussian_factor_swap_all_irreducible

Exact expanded first-order arithmetic statement

forall b c d e l i p q. (exists ge_gap_swap_irreducible_index. ge_gap_swap_irreducible_index + S (i) = (l)) -> (forall gr_factor_index_swap_irreducible_old gr_factor_value_swap_irreducible_old. (exists ge_gap_swap_irreducible_oldindex. ge_gap_swap_irreducible_oldindex + S (gr_factor_index_swap_irreducible_old) = (S l)) -> (((exists ff_h_gprod_swap_irreducible_oldentry. ff_h_gprod_swap_irreducible_oldentry + S (gr_factor_value_swap_irreducible_old) = S ((S (gr_factor_index_swap_irreducible_old)) * c)) /\ exists ff_q_gprod_swap_irreducible_oldentry. b = ff_q_gprod_swap_irreducible_oldentry * S ((S (gr_factor_index_swap_irreducible_old)) * c) + (gr_factor_value_swap_irreducible_old))) -> (((exists ge_real_positive_swap_irreducible_oldirreduciblecarrier ge_real_negative_swap_irreducible_oldirreduciblecarrier ge_imaginary_positive_swap_irreducible_oldirreduciblecarrier ge_imaginary_negative_swap_irreducible_oldirreduciblecarrier. (exists ge_real_code_swap_irreducible_oldirreduciblecarrierdecode ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode. (((gr_factor_value_swap_irreducible_old) = ((ge_real_code_swap_irreducible_oldirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode)) * S ((ge_real_code_swap_irreducible_oldirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode)) + ((ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode))) /\ (((((ge_real_code_swap_irreducible_oldirreduciblecarrierdecode) = 2 * (ge_real_positive_swap_irreducible_oldirreduciblecarrier) /\ (ge_real_negative_swap_irreducible_oldirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_real. (((ge_real_code_swap_irreducible_oldirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_swap_irreducible_oldirreduciblecarrier) = 0) /\ (ge_real_negative_swap_irreducible_oldirreduciblecarrier) = S ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_swap_irreducible_oldirreduciblecarrier) /\ (ge_imaginary_negative_swap_irreducible_oldirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_swap_irreducible_oldirreduciblecarrier) = 0) /\ (ge_imaginary_negative_swap_irreducible_oldirreduciblecarrier) = S ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_swap_irreducible_old)=0)) /\ ((~(exists gr_inverse_swap_irreducible_oldirreduciblenonunit. (exists ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity ge_first_in_swap_irreducible_oldirreduciblenonunitidentity ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity ge_second_in_swap_irreducible_oldirreduciblenonunitidentity. ((exists ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst. (((gr_factor_value_swap_irreducible_old) = ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstreal ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstreal) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstreal = (ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary = (ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond. (((gr_inverse_swap_irreducible_oldirreduciblenonunit) = ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondreal ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondreal) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondreal = (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary = (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputreal ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputreal) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_swap_irreducible_oldirreducible gr_second_factor_swap_irreducible_oldirreducible. (exists ge_first_rp_swap_irreducible_oldirreduciblefactorization ge_first_rn_swap_irreducible_oldirreduciblefactorization ge_first_ip_swap_irreducible_oldirreduciblefactorization ge_first_in_swap_irreducible_oldirreduciblefactorization ge_second_rp_swap_irreducible_oldirreduciblefactorization ge_second_rn_swap_irreducible_oldirreduciblefactorization ge_second_ip_swap_irreducible_oldirreduciblefactorization ge_second_in_swap_irreducible_oldirreduciblefactorization. ((exists ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst. (((gr_first_factor_swap_irreducible_oldirreducible) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstreal ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstreal) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_oldirreduciblefactorization) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstreal = (ge_first_rn_swap_irreducible_oldirreduciblefactorization) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstimaginary ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_oldirreduciblefactorization) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstimaginary = (ge_first_in_swap_irreducible_oldirreduciblefactorization) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond. (((gr_second_factor_swap_irreducible_oldirreducible) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondreal ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondreal) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_oldirreduciblefactorization) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondreal = (ge_second_rn_swap_irreducible_oldirreduciblefactorization) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondimaginary ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_oldirreduciblefactorization) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondimaginary = (ge_second_in_swap_irreducible_oldirreduciblefactorization) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput. (((gr_factor_value_swap_irreducible_old) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputreal ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputreal) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblefactorization) * (ge_second_rp_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_oldirreduciblefactorization) * (ge_second_rn_swap_irreducible_oldirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefactorization) * (ge_second_in_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_in_swap_irreducible_oldirreduciblefactorization) * (ge_second_ip_swap_irreducible_oldirreduciblefactorization))))))) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputreal = (((((((ge_first_rp_swap_irreducible_oldirreduciblefactorization) * (ge_second_rn_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_oldirreduciblefactorization) * (ge_second_rp_swap_irreducible_oldirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefactorization) * (ge_second_ip_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_in_swap_irreducible_oldirreduciblefactorization) * (ge_second_in_swap_irreducible_oldirreduciblefactorization))))))) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputimaginary ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblefactorization) * (ge_second_ip_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_oldirreduciblefactorization) * (ge_second_in_swap_irreducible_oldirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefactorization) * (ge_second_rp_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_in_swap_irreducible_oldirreduciblefactorization) * (ge_second_rn_swap_irreducible_oldirreduciblefactorization))))))) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_swap_irreducible_oldirreduciblefactorization) * (ge_second_in_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_oldirreduciblefactorization) * (ge_second_ip_swap_irreducible_oldirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefactorization) * (ge_second_rn_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_in_swap_irreducible_oldirreduciblefactorization) * (ge_second_rp_swap_irreducible_oldirreduciblefactorization))))))) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_swap_irreducible_oldirreduciblefirst_unit. (exists ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity. ((exists ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst. (((gr_first_factor_swap_irreducible_oldirreducible) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal = (ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond. (((gr_inverse_swap_irreducible_oldirreduciblefirst_unit) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal = (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_swap_irreducible_oldirreduciblesecond_unit. (exists ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity. ((exists ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst. (((gr_second_factor_swap_irreducible_oldirreducible) = ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal = (ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond. (((gr_inverse_swap_irreducible_oldirreduciblesecond_unit) = ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal = (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (((((exists ff_h_pfp_swap_irreducible_dataoldi. ff_h_pfp_swap_irreducible_dataoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_irreducible_dataoldi. b = ff_q_pfp_swap_irreducible_dataoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_irreducible_dataoldlast. ff_h_pfp_swap_irreducible_dataoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_irreducible_dataoldlast. b = ff_q_pfp_swap_irreducible_dataoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swap_irreducible_datanewi. ff_h_pfp_swap_irreducible_datanewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_irreducible_datanewi. d = ff_q_pfp_swap_irreducible_datanewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swap_irreducible_datanewlast. ff_h_pfp_swap_irreducible_datanewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_irreducible_datanewlast. d = ff_q_pfp_swap_irreducible_datanewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap_irreducible_data pfp_a_swap_irreducible_data. (exists pfp_gap_swap_irreducible_databound. pfp_gap_swap_irreducible_databound + S (pfp_j_swap_irreducible_data) = (S (l))) -> ~(pfp_j_swap_irreducible_data = i) -> ~(pfp_j_swap_irreducible_data = l) -> (((exists ff_h_pfp_swap_irreducible_dataold. ff_h_pfp_swap_irreducible_dataold + S (pfp_a_swap_irreducible_data) = S ((S (pfp_j_swap_irreducible_data)) * c)) /\ exists ff_q_pfp_swap_irreducible_dataold. b = ff_q_pfp_swap_irreducible_dataold * S ((S (pfp_j_swap_irreducible_data)) * c) + (pfp_a_swap_irreducible_data))) -> (((exists ff_h_pfp_swap_irreducible_datanew. ff_h_pfp_swap_irreducible_datanew + S (pfp_a_swap_irreducible_data) = S ((S (pfp_j_swap_irreducible_data)) * e)) /\ exists ff_q_pfp_swap_irreducible_datanew. d = ff_q_pfp_swap_irreducible_datanew * S ((S (pfp_j_swap_irreducible_data)) * e) + (pfp_a_swap_irreducible_data)))))))))))) -> (forall gr_factor_index_swap_irreducible_new gr_factor_value_swap_irreducible_new. (exists ge_gap_swap_irreducible_newindex. ge_gap_swap_irreducible_newindex + S (gr_factor_index_swap_irreducible_new) = (S l)) -> (((exists ff_h_gprod_swap_irreducible_newentry. ff_h_gprod_swap_irreducible_newentry + S (gr_factor_value_swap_irreducible_new) = S ((S (gr_factor_index_swap_irreducible_new)) * e)) /\ exists ff_q_gprod_swap_irreducible_newentry. d = ff_q_gprod_swap_irreducible_newentry * S ((S (gr_factor_index_swap_irreducible_new)) * e) + (gr_factor_value_swap_irreducible_new))) -> (((exists ge_real_positive_swap_irreducible_newirreduciblecarrier ge_real_negative_swap_irreducible_newirreduciblecarrier ge_imaginary_positive_swap_irreducible_newirreduciblecarrier ge_imaginary_negative_swap_irreducible_newirreduciblecarrier. (exists ge_real_code_swap_irreducible_newirreduciblecarrierdecode ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode. (((gr_factor_value_swap_irreducible_new) = ((ge_real_code_swap_irreducible_newirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode)) * S ((ge_real_code_swap_irreducible_newirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode)) + ((ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode))) /\ (((((ge_real_code_swap_irreducible_newirreduciblecarrierdecode) = 2 * (ge_real_positive_swap_irreducible_newirreduciblecarrier) /\ (ge_real_negative_swap_irreducible_newirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_real. (((ge_real_code_swap_irreducible_newirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_swap_irreducible_newirreduciblecarrier) = 0) /\ (ge_real_negative_swap_irreducible_newirreduciblecarrier) = S ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_swap_irreducible_newirreduciblecarrier) /\ (ge_imaginary_negative_swap_irreducible_newirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_swap_irreducible_newirreduciblecarrier) = 0) /\ (ge_imaginary_negative_swap_irreducible_newirreduciblecarrier) = S ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_swap_irreducible_new)=0)) /\ ((~(exists gr_inverse_swap_irreducible_newirreduciblenonunit. (exists ge_first_rp_swap_irreducible_newirreduciblenonunitidentity ge_first_rn_swap_irreducible_newirreduciblenonunitidentity ge_first_ip_swap_irreducible_newirreduciblenonunitidentity ge_first_in_swap_irreducible_newirreduciblenonunitidentity ge_second_rp_swap_irreducible_newirreduciblenonunitidentity ge_second_rn_swap_irreducible_newirreduciblenonunitidentity ge_second_ip_swap_irreducible_newirreduciblenonunitidentity ge_second_in_swap_irreducible_newirreduciblenonunitidentity. ((exists ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst. (((gr_factor_value_swap_irreducible_new) = ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstreal ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstreal) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstreal = (ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstimaginary ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstimaginary = (ge_first_in_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond. (((gr_inverse_swap_irreducible_newirreduciblenonunit) = ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondreal ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondreal) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondreal = (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondimaginary ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondimaginary = (ge_second_in_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputreal ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputreal) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_newirreduciblenonunitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_newirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_newirreduciblenonunitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputimaginary ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_newirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_newirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_newirreduciblenonunitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_swap_irreducible_newirreducible gr_second_factor_swap_irreducible_newirreducible. (exists ge_first_rp_swap_irreducible_newirreduciblefactorization ge_first_rn_swap_irreducible_newirreduciblefactorization ge_first_ip_swap_irreducible_newirreduciblefactorization ge_first_in_swap_irreducible_newirreduciblefactorization ge_second_rp_swap_irreducible_newirreduciblefactorization ge_second_rn_swap_irreducible_newirreduciblefactorization ge_second_ip_swap_irreducible_newirreduciblefactorization ge_second_in_swap_irreducible_newirreduciblefactorization. ((exists ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst. (((gr_first_factor_swap_irreducible_newirreducible) = ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstreal ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstreal) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_newirreduciblefactorization) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstreal = (ge_first_rn_swap_irreducible_newirreduciblefactorization) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstimaginary ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_newirreduciblefactorization) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstimaginary = (ge_first_in_swap_irreducible_newirreduciblefactorization) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond. (((gr_second_factor_swap_irreducible_newirreducible) = ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondreal ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondreal) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_newirreduciblefactorization) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondreal = (ge_second_rn_swap_irreducible_newirreduciblefactorization) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondimaginary ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_newirreduciblefactorization) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondimaginary = (ge_second_in_swap_irreducible_newirreduciblefactorization) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput. (((gr_factor_value_swap_irreducible_new) = ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputreal ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputreal) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblefactorization) * (ge_second_rp_swap_irreducible_newirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_newirreduciblefactorization) * (ge_second_rn_swap_irreducible_newirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefactorization) * (ge_second_in_swap_irreducible_newirreduciblefactorization))) + (((ge_first_in_swap_irreducible_newirreduciblefactorization) * (ge_second_ip_swap_irreducible_newirreduciblefactorization))))))) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputreal = (((((((ge_first_rp_swap_irreducible_newirreduciblefactorization) * (ge_second_rn_swap_irreducible_newirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_newirreduciblefactorization) * (ge_second_rp_swap_irreducible_newirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefactorization) * (ge_second_ip_swap_irreducible_newirreduciblefactorization))) + (((ge_first_in_swap_irreducible_newirreduciblefactorization) * (ge_second_in_swap_irreducible_newirreduciblefactorization))))))) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputimaginary ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblefactorization) * (ge_second_ip_swap_irreducible_newirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_newirreduciblefactorization) * (ge_second_in_swap_irreducible_newirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefactorization) * (ge_second_rp_swap_irreducible_newirreduciblefactorization))) + (((ge_first_in_swap_irreducible_newirreduciblefactorization) * (ge_second_rn_swap_irreducible_newirreduciblefactorization))))))) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_swap_irreducible_newirreduciblefactorization) * (ge_second_in_swap_irreducible_newirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_newirreduciblefactorization) * (ge_second_ip_swap_irreducible_newirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefactorization) * (ge_second_rn_swap_irreducible_newirreduciblefactorization))) + (((ge_first_in_swap_irreducible_newirreduciblefactorization) * (ge_second_rp_swap_irreducible_newirreduciblefactorization))))))) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_swap_irreducible_newirreduciblefirst_unit. (exists ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity. ((exists ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst. (((gr_first_factor_swap_irreducible_newirreducible) = ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstreal ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstreal = (ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond. (((gr_inverse_swap_irreducible_newirreduciblefirst_unit) = ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondreal ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondreal = (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputreal ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_swap_irreducible_newirreduciblesecond_unit. (exists ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity. ((exists ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst. (((gr_second_factor_swap_irreducible_newirreducible) = ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstreal ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstreal = (ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond. (((gr_inverse_swap_irreducible_newirreduciblesecond_unit) = ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondreal ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondreal = (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputreal ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary))))))))))))))))