gaussian_irreducible_divisor_product_member

Exact expanded first-order arithmetic statement

forall l b c P p. (forall gr_factor_index_member_factors gr_factor_value_member_factors. (exists ge_gap_member_factorsindex. ge_gap_member_factorsindex + S (gr_factor_index_member_factors) = (l)) -> (((exists ff_h_gprod_member_factorsentry. ff_h_gprod_member_factorsentry + S (gr_factor_value_member_factors) = S ((S (gr_factor_index_member_factors)) * c)) /\ exists ff_q_gprod_member_factorsentry. b = ff_q_gprod_member_factorsentry * S ((S (gr_factor_index_member_factors)) * c) + (gr_factor_value_member_factors))) -> (((exists ge_real_positive_member_factorsirreduciblecarrier ge_real_negative_member_factorsirreduciblecarrier ge_imaginary_positive_member_factorsirreduciblecarrier ge_imaginary_negative_member_factorsirreduciblecarrier. (exists ge_real_code_member_factorsirreduciblecarrierdecode ge_imaginary_code_member_factorsirreduciblecarrierdecode. (((gr_factor_value_member_factors) = ((ge_real_code_member_factorsirreduciblecarrierdecode) + (ge_imaginary_code_member_factorsirreduciblecarrierdecode)) * S ((ge_real_code_member_factorsirreduciblecarrierdecode) + (ge_imaginary_code_member_factorsirreduciblecarrierdecode)) + ((ge_imaginary_code_member_factorsirreduciblecarrierdecode) + (ge_imaginary_code_member_factorsirreduciblecarrierdecode))) /\ (((((ge_real_code_member_factorsirreduciblecarrierdecode) = 2 * (ge_real_positive_member_factorsirreduciblecarrier) /\ (ge_real_negative_member_factorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_member_factorsirreduciblecarrierdecode_real. (((ge_real_code_member_factorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_member_factorsirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_member_factorsirreduciblecarrier) = 0) /\ (ge_real_negative_member_factorsirreduciblecarrier) = S ge_signed_half_ge_member_factorsirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_member_factorsirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_member_factorsirreduciblecarrier) /\ (ge_imaginary_negative_member_factorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_member_factorsirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_member_factorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_member_factorsirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_member_factorsirreduciblecarrier) = 0) /\ (ge_imaginary_negative_member_factorsirreduciblecarrier) = S ge_signed_half_ge_member_factorsirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_member_factors)=0)) /\ ((~(exists gr_inverse_member_factorsirreduciblenonunit. (exists ge_first_rp_member_factorsirreduciblenonunitidentity ge_first_rn_member_factorsirreduciblenonunitidentity ge_first_ip_member_factorsirreduciblenonunitidentity ge_first_in_member_factorsirreduciblenonunitidentity ge_second_rp_member_factorsirreduciblenonunitidentity ge_second_rn_member_factorsirreduciblenonunitidentity ge_second_ip_member_factorsirreduciblenonunitidentity ge_second_in_member_factorsirreduciblenonunitidentity. ((exists ge_representation_real_code_member_factorsirreduciblenonunitidentityfirst ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityfirst. (((gr_factor_value_member_factors) = ((ge_representation_real_code_member_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_member_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_member_factorsirreduciblenonunitidentityfirstreal ge_balance_negative_member_factorsirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_member_factorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_member_factorsirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_member_factorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_member_factorsirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentityfirstreal) = S ge_signed_half_member_factorsirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_member_factorsirreduciblenonunitidentity) + ge_balance_negative_member_factorsirreduciblenonunitidentityfirstreal = (ge_first_rn_member_factorsirreduciblenonunitidentity) + ge_balance_positive_member_factorsirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_member_factorsirreduciblenonunitidentityfirstimaginary ge_balance_negative_member_factorsirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_member_factorsirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_member_factorsirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_member_factorsirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_member_factorsirreduciblenonunitidentity) + ge_balance_negative_member_factorsirreduciblenonunitidentityfirstimaginary = (ge_first_in_member_factorsirreduciblenonunitidentity) + ge_balance_positive_member_factorsirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_factorsirreduciblenonunitidentitysecond ge_representation_imaginary_code_member_factorsirreduciblenonunitidentitysecond. (((gr_inverse_member_factorsirreduciblenonunit) = ((ge_representation_real_code_member_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_member_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_member_factorsirreduciblenonunitidentitysecondreal ge_balance_negative_member_factorsirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_member_factorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_member_factorsirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_member_factorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_member_factorsirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentitysecondreal) = S ge_signed_half_member_factorsirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_member_factorsirreduciblenonunitidentity) + ge_balance_negative_member_factorsirreduciblenonunitidentitysecondreal = (ge_second_rn_member_factorsirreduciblenonunitidentity) + ge_balance_positive_member_factorsirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_member_factorsirreduciblenonunitidentitysecondimaginary ge_balance_negative_member_factorsirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_member_factorsirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_member_factorsirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_member_factorsirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_member_factorsirreduciblenonunitidentity) + ge_balance_negative_member_factorsirreduciblenonunitidentitysecondimaginary = (ge_second_in_member_factorsirreduciblenonunitidentity) + ge_balance_positive_member_factorsirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_member_factorsirreduciblenonunitidentityoutput ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_member_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_member_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_member_factorsirreduciblenonunitidentityoutputreal ge_balance_negative_member_factorsirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_member_factorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_member_factorsirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_member_factorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_member_factorsirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentityoutputreal) = S ge_signed_half_member_factorsirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_member_factorsirreduciblenonunitidentity) * (ge_second_rp_member_factorsirreduciblenonunitidentity))) + (((ge_first_rn_member_factorsirreduciblenonunitidentity) * (ge_second_rn_member_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_member_factorsirreduciblenonunitidentity) * (ge_second_in_member_factorsirreduciblenonunitidentity))) + (((ge_first_in_member_factorsirreduciblenonunitidentity) * (ge_second_ip_member_factorsirreduciblenonunitidentity))))))) + ge_balance_negative_member_factorsirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_member_factorsirreduciblenonunitidentity) * (ge_second_rn_member_factorsirreduciblenonunitidentity))) + (((ge_first_rn_member_factorsirreduciblenonunitidentity) * (ge_second_rp_member_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_member_factorsirreduciblenonunitidentity) * (ge_second_ip_member_factorsirreduciblenonunitidentity))) + (((ge_first_in_member_factorsirreduciblenonunitidentity) * (ge_second_in_member_factorsirreduciblenonunitidentity))))))) + ge_balance_positive_member_factorsirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_member_factorsirreduciblenonunitidentityoutputimaginary ge_balance_negative_member_factorsirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_member_factorsirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_member_factorsirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_member_factorsirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_factorsirreduciblenonunitidentity) * (ge_second_ip_member_factorsirreduciblenonunitidentity))) + (((ge_first_rn_member_factorsirreduciblenonunitidentity) * (ge_second_in_member_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_member_factorsirreduciblenonunitidentity) * (ge_second_rp_member_factorsirreduciblenonunitidentity))) + (((ge_first_in_member_factorsirreduciblenonunitidentity) * (ge_second_rn_member_factorsirreduciblenonunitidentity))))))) + ge_balance_negative_member_factorsirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_member_factorsirreduciblenonunitidentity) * (ge_second_in_member_factorsirreduciblenonunitidentity))) + (((ge_first_rn_member_factorsirreduciblenonunitidentity) * (ge_second_ip_member_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_member_factorsirreduciblenonunitidentity) * (ge_second_rn_member_factorsirreduciblenonunitidentity))) + (((ge_first_in_member_factorsirreduciblenonunitidentity) * (ge_second_rp_member_factorsirreduciblenonunitidentity))))))) + ge_balance_positive_member_factorsirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_member_factorsirreducible gr_second_factor_member_factorsirreducible. (exists ge_first_rp_member_factorsirreduciblefactorization ge_first_rn_member_factorsirreduciblefactorization ge_first_ip_member_factorsirreduciblefactorization ge_first_in_member_factorsirreduciblefactorization ge_second_rp_member_factorsirreduciblefactorization ge_second_rn_member_factorsirreduciblefactorization ge_second_ip_member_factorsirreduciblefactorization ge_second_in_member_factorsirreduciblefactorization. ((exists ge_representation_real_code_member_factorsirreduciblefactorizationfirst ge_representation_imaginary_code_member_factorsirreduciblefactorizationfirst. (((gr_first_factor_member_factorsirreducible) = ((ge_representation_real_code_member_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationfirst)) * S ((ge_representation_real_code_member_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_member_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_member_factorsirreduciblefactorizationfirstreal ge_balance_negative_member_factorsirreduciblefactorizationfirstreal. (((((ge_representation_real_code_member_factorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_member_factorsirreduciblefactorizationfirstreal) /\ (ge_balance_negative_member_factorsirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_member_factorsirreduciblefactorizationfirst) = 2 * ge_signed_half_member_factorsirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblefactorizationfirstreal) = S ge_signed_half_member_factorsirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_member_factorsirreduciblefactorization) + ge_balance_negative_member_factorsirreduciblefactorizationfirstreal = (ge_first_rn_member_factorsirreduciblefactorization) + ge_balance_positive_member_factorsirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_member_factorsirreduciblefactorizationfirstimaginary ge_balance_negative_member_factorsirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_member_factorsirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_member_factorsirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblefactorizationfirst) = 2 * ge_signed_half_member_factorsirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblefactorizationfirstimaginary) = S ge_signed_half_member_factorsirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_member_factorsirreduciblefactorization) + ge_balance_negative_member_factorsirreduciblefactorizationfirstimaginary = (ge_first_in_member_factorsirreduciblefactorization) + ge_balance_positive_member_factorsirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_factorsirreduciblefactorizationsecond ge_representation_imaginary_code_member_factorsirreduciblefactorizationsecond. (((gr_second_factor_member_factorsirreducible) = ((ge_representation_real_code_member_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationsecond)) * S ((ge_representation_real_code_member_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_member_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_member_factorsirreduciblefactorizationsecondreal ge_balance_negative_member_factorsirreduciblefactorizationsecondreal. (((((ge_representation_real_code_member_factorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_member_factorsirreduciblefactorizationsecondreal) /\ (ge_balance_negative_member_factorsirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_member_factorsirreduciblefactorizationsecond) = 2 * ge_signed_half_member_factorsirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblefactorizationsecondreal) = S ge_signed_half_member_factorsirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_member_factorsirreduciblefactorization) + ge_balance_negative_member_factorsirreduciblefactorizationsecondreal = (ge_second_rn_member_factorsirreduciblefactorization) + ge_balance_positive_member_factorsirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_member_factorsirreduciblefactorizationsecondimaginary ge_balance_negative_member_factorsirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_member_factorsirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_member_factorsirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblefactorizationsecond) = 2 * ge_signed_half_member_factorsirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblefactorizationsecondimaginary) = S ge_signed_half_member_factorsirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_member_factorsirreduciblefactorization) + ge_balance_negative_member_factorsirreduciblefactorizationsecondimaginary = (ge_second_in_member_factorsirreduciblefactorization) + ge_balance_positive_member_factorsirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_member_factorsirreduciblefactorizationoutput ge_representation_imaginary_code_member_factorsirreduciblefactorizationoutput. (((gr_factor_value_member_factors) = ((ge_representation_real_code_member_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationoutput)) * S ((ge_representation_real_code_member_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_member_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_member_factorsirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_member_factorsirreduciblefactorizationoutputreal ge_balance_negative_member_factorsirreduciblefactorizationoutputreal. (((((ge_representation_real_code_member_factorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_member_factorsirreduciblefactorizationoutputreal) /\ (ge_balance_negative_member_factorsirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_member_factorsirreduciblefactorizationoutput) = 2 * ge_signed_half_member_factorsirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblefactorizationoutputreal) = S ge_signed_half_member_factorsirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_member_factorsirreduciblefactorization) * (ge_second_rp_member_factorsirreduciblefactorization))) + (((ge_first_rn_member_factorsirreduciblefactorization) * (ge_second_rn_member_factorsirreduciblefactorization))))) + (((((ge_first_ip_member_factorsirreduciblefactorization) * (ge_second_in_member_factorsirreduciblefactorization))) + (((ge_first_in_member_factorsirreduciblefactorization) * (ge_second_ip_member_factorsirreduciblefactorization))))))) + ge_balance_negative_member_factorsirreduciblefactorizationoutputreal = (((((((ge_first_rp_member_factorsirreduciblefactorization) * (ge_second_rn_member_factorsirreduciblefactorization))) + (((ge_first_rn_member_factorsirreduciblefactorization) * (ge_second_rp_member_factorsirreduciblefactorization))))) + (((((ge_first_ip_member_factorsirreduciblefactorization) * (ge_second_ip_member_factorsirreduciblefactorization))) + (((ge_first_in_member_factorsirreduciblefactorization) * (ge_second_in_member_factorsirreduciblefactorization))))))) + ge_balance_positive_member_factorsirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_member_factorsirreduciblefactorizationoutputimaginary ge_balance_negative_member_factorsirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_member_factorsirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_member_factorsirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblefactorizationoutput) = 2 * ge_signed_half_member_factorsirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblefactorizationoutputimaginary) = S ge_signed_half_member_factorsirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_factorsirreduciblefactorization) * (ge_second_ip_member_factorsirreduciblefactorization))) + (((ge_first_rn_member_factorsirreduciblefactorization) * (ge_second_in_member_factorsirreduciblefactorization))))) + (((((ge_first_ip_member_factorsirreduciblefactorization) * (ge_second_rp_member_factorsirreduciblefactorization))) + (((ge_first_in_member_factorsirreduciblefactorization) * (ge_second_rn_member_factorsirreduciblefactorization))))))) + ge_balance_negative_member_factorsirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_member_factorsirreduciblefactorization) * (ge_second_in_member_factorsirreduciblefactorization))) + (((ge_first_rn_member_factorsirreduciblefactorization) * (ge_second_ip_member_factorsirreduciblefactorization))))) + (((((ge_first_ip_member_factorsirreduciblefactorization) * (ge_second_rn_member_factorsirreduciblefactorization))) + (((ge_first_in_member_factorsirreduciblefactorization) * (ge_second_rp_member_factorsirreduciblefactorization))))))) + ge_balance_positive_member_factorsirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_member_factorsirreduciblefirst_unit. (exists ge_first_rp_member_factorsirreduciblefirst_unitidentity ge_first_rn_member_factorsirreduciblefirst_unitidentity ge_first_ip_member_factorsirreduciblefirst_unitidentity ge_first_in_member_factorsirreduciblefirst_unitidentity ge_second_rp_member_factorsirreduciblefirst_unitidentity ge_second_rn_member_factorsirreduciblefirst_unitidentity ge_second_ip_member_factorsirreduciblefirst_unitidentity ge_second_in_member_factorsirreduciblefirst_unitidentity. ((exists ge_representation_real_code_member_factorsirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityfirst. (((gr_first_factor_member_factorsirreducible) = ((ge_representation_real_code_member_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_member_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_member_factorsirreduciblefirst_unitidentityfirstreal ge_balance_negative_member_factorsirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_member_factorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_member_factorsirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_member_factorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_member_factorsirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_member_factorsirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_member_factorsirreduciblefirst_unitidentity) + ge_balance_negative_member_factorsirreduciblefirst_unitidentityfirstreal = (ge_first_rn_member_factorsirreduciblefirst_unitidentity) + ge_balance_positive_member_factorsirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_member_factorsirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_member_factorsirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_member_factorsirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_member_factorsirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_member_factorsirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_member_factorsirreduciblefirst_unitidentity) + ge_balance_negative_member_factorsirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_member_factorsirreduciblefirst_unitidentity) + ge_balance_positive_member_factorsirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_factorsirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentitysecond. (((gr_inverse_member_factorsirreduciblefirst_unit) = ((ge_representation_real_code_member_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_member_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_member_factorsirreduciblefirst_unitidentitysecondreal ge_balance_negative_member_factorsirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_member_factorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_member_factorsirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_member_factorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_member_factorsirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_member_factorsirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_member_factorsirreduciblefirst_unitidentity) + ge_balance_negative_member_factorsirreduciblefirst_unitidentitysecondreal = (ge_second_rn_member_factorsirreduciblefirst_unitidentity) + ge_balance_positive_member_factorsirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_member_factorsirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_member_factorsirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_member_factorsirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_member_factorsirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_member_factorsirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_member_factorsirreduciblefirst_unitidentity) + ge_balance_negative_member_factorsirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_member_factorsirreduciblefirst_unitidentity) + ge_balance_positive_member_factorsirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_member_factorsirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_member_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_member_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_member_factorsirreduciblefirst_unitidentityoutputreal ge_balance_negative_member_factorsirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_member_factorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_member_factorsirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_member_factorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_member_factorsirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_member_factorsirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_member_factorsirreduciblefirst_unitidentity) * (ge_second_rp_member_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_member_factorsirreduciblefirst_unitidentity) * (ge_second_rn_member_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_member_factorsirreduciblefirst_unitidentity) * (ge_second_in_member_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_member_factorsirreduciblefirst_unitidentity) * (ge_second_ip_member_factorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_member_factorsirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_member_factorsirreduciblefirst_unitidentity) * (ge_second_rn_member_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_member_factorsirreduciblefirst_unitidentity) * (ge_second_rp_member_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_member_factorsirreduciblefirst_unitidentity) * (ge_second_ip_member_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_member_factorsirreduciblefirst_unitidentity) * (ge_second_in_member_factorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_member_factorsirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_member_factorsirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_member_factorsirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_member_factorsirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_member_factorsirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_member_factorsirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_factorsirreduciblefirst_unitidentity) * (ge_second_ip_member_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_member_factorsirreduciblefirst_unitidentity) * (ge_second_in_member_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_member_factorsirreduciblefirst_unitidentity) * (ge_second_rp_member_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_member_factorsirreduciblefirst_unitidentity) * (ge_second_rn_member_factorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_member_factorsirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_member_factorsirreduciblefirst_unitidentity) * (ge_second_in_member_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_member_factorsirreduciblefirst_unitidentity) * (ge_second_ip_member_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_member_factorsirreduciblefirst_unitidentity) * (ge_second_rn_member_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_member_factorsirreduciblefirst_unitidentity) * (ge_second_rp_member_factorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_member_factorsirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_member_factorsirreduciblesecond_unit. (exists ge_first_rp_member_factorsirreduciblesecond_unitidentity ge_first_rn_member_factorsirreduciblesecond_unitidentity ge_first_ip_member_factorsirreduciblesecond_unitidentity ge_first_in_member_factorsirreduciblesecond_unitidentity ge_second_rp_member_factorsirreduciblesecond_unitidentity ge_second_rn_member_factorsirreduciblesecond_unitidentity ge_second_ip_member_factorsirreduciblesecond_unitidentity ge_second_in_member_factorsirreduciblesecond_unitidentity. ((exists ge_representation_real_code_member_factorsirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityfirst. (((gr_second_factor_member_factorsirreducible) = ((ge_representation_real_code_member_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_member_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_member_factorsirreduciblesecond_unitidentityfirstreal ge_balance_negative_member_factorsirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_member_factorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_member_factorsirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_member_factorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_member_factorsirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_member_factorsirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_member_factorsirreduciblesecond_unitidentity) + ge_balance_negative_member_factorsirreduciblesecond_unitidentityfirstreal = (ge_first_rn_member_factorsirreduciblesecond_unitidentity) + ge_balance_positive_member_factorsirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_member_factorsirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_member_factorsirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_member_factorsirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_member_factorsirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_member_factorsirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_member_factorsirreduciblesecond_unitidentity) + ge_balance_negative_member_factorsirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_member_factorsirreduciblesecond_unitidentity) + ge_balance_positive_member_factorsirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_factorsirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentitysecond. (((gr_inverse_member_factorsirreduciblesecond_unit) = ((ge_representation_real_code_member_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_member_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_member_factorsirreduciblesecond_unitidentitysecondreal ge_balance_negative_member_factorsirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_member_factorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_member_factorsirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_member_factorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_member_factorsirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_member_factorsirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_member_factorsirreduciblesecond_unitidentity) + ge_balance_negative_member_factorsirreduciblesecond_unitidentitysecondreal = (ge_second_rn_member_factorsirreduciblesecond_unitidentity) + ge_balance_positive_member_factorsirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_member_factorsirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_member_factorsirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_member_factorsirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_member_factorsirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_member_factorsirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_member_factorsirreduciblesecond_unitidentity) + ge_balance_negative_member_factorsirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_member_factorsirreduciblesecond_unitidentity) + ge_balance_positive_member_factorsirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_member_factorsirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_member_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_member_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_member_factorsirreduciblesecond_unitidentityoutputreal ge_balance_negative_member_factorsirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_member_factorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_member_factorsirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_member_factorsirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_member_factorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_member_factorsirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_member_factorsirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_member_factorsirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_member_factorsirreduciblesecond_unitidentity) * (ge_second_rp_member_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_member_factorsirreduciblesecond_unitidentity) * (ge_second_rn_member_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_member_factorsirreduciblesecond_unitidentity) * (ge_second_in_member_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_member_factorsirreduciblesecond_unitidentity) * (ge_second_ip_member_factorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_member_factorsirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_member_factorsirreduciblesecond_unitidentity) * (ge_second_rn_member_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_member_factorsirreduciblesecond_unitidentity) * (ge_second_rp_member_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_member_factorsirreduciblesecond_unitidentity) * (ge_second_ip_member_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_member_factorsirreduciblesecond_unitidentity) * (ge_second_in_member_factorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_member_factorsirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_member_factorsirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_member_factorsirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_member_factorsirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_member_factorsirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_member_factorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_member_factorsirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_member_factorsirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_member_factorsirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_member_factorsirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_factorsirreduciblesecond_unitidentity) * (ge_second_ip_member_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_member_factorsirreduciblesecond_unitidentity) * (ge_second_in_member_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_member_factorsirreduciblesecond_unitidentity) * (ge_second_rp_member_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_member_factorsirreduciblesecond_unitidentity) * (ge_second_rn_member_factorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_member_factorsirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_member_factorsirreduciblesecond_unitidentity) * (ge_second_in_member_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_member_factorsirreduciblesecond_unitidentity) * (ge_second_ip_member_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_member_factorsirreduciblesecond_unitidentity) * (ge_second_rn_member_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_member_factorsirreduciblesecond_unitidentity) * (ge_second_rp_member_factorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_member_factorsirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (exists gr_product_trace_member_trace gr_product_scale_member_trace. ((((exists ff_h_gprod_member_tracestart. ff_h_gprod_member_tracestart + S (6) = S ((S (0)) * gr_product_scale_member_trace)) /\ exists ff_q_gprod_member_tracestart. gr_product_trace_member_trace = ff_q_gprod_member_tracestart * S ((S (0)) * gr_product_scale_member_trace) + (6))) /\ ((((exists ff_h_gprod_member_traceend. ff_h_gprod_member_traceend + S (P) = S ((S (l)) * gr_product_scale_member_trace)) /\ exists ff_q_gprod_member_traceend. gr_product_trace_member_trace = ff_q_gprod_member_traceend * S ((S (l)) * gr_product_scale_member_trace) + (P))) /\ (forall gr_product_index_member_tracesteps. (exists ge_gap_member_tracestepsindex_bound. ge_gap_member_tracestepsindex_bound + S (gr_product_index_member_tracesteps) = (l)) -> exists gr_product_factor_member_tracesteps gr_product_before_member_tracesteps gr_product_after_member_tracesteps. ((((exists ff_h_gprod_member_tracestepsfactor. ff_h_gprod_member_tracestepsfactor + S (gr_product_factor_member_tracesteps) = S ((S (gr_product_index_member_tracesteps)) * c)) /\ exists ff_q_gprod_member_tracestepsfactor. b = ff_q_gprod_member_tracestepsfactor * S ((S (gr_product_index_member_tracesteps)) * c) + (gr_product_factor_member_tracesteps))) /\ ((((exists ff_h_gprod_member_tracestepsbefore. ff_h_gprod_member_tracestepsbefore + S (gr_product_before_member_tracesteps) = S ((S (gr_product_index_member_tracesteps)) * gr_product_scale_member_trace)) /\ exists ff_q_gprod_member_tracestepsbefore. gr_product_trace_member_trace = ff_q_gprod_member_tracestepsbefore * S ((S (gr_product_index_member_tracesteps)) * gr_product_scale_member_trace) + (gr_product_before_member_tracesteps))) /\ ((((exists ff_h_gprod_member_tracestepsafter. ff_h_gprod_member_tracestepsafter + S (gr_product_after_member_tracesteps) = S ((S (S (gr_product_index_member_tracesteps))) * gr_product_scale_member_trace)) /\ exists ff_q_gprod_member_tracestepsafter. gr_product_trace_member_trace = ff_q_gprod_member_tracestepsafter * S ((S (S (gr_product_index_member_tracesteps))) * gr_product_scale_member_trace) + (gr_product_after_member_tracesteps))) /\ (exists ge_first_rp_member_tracestepsmultiply ge_first_rn_member_tracestepsmultiply ge_first_ip_member_tracestepsmultiply ge_first_in_member_tracestepsmultiply ge_second_rp_member_tracestepsmultiply ge_second_rn_member_tracestepsmultiply ge_second_ip_member_tracestepsmultiply ge_second_in_member_tracestepsmultiply. ((exists ge_representation_real_code_member_tracestepsmultiplyfirst ge_representation_imaginary_code_member_tracestepsmultiplyfirst. (((gr_product_before_member_tracesteps) = ((ge_representation_real_code_member_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_member_tracestepsmultiplyfirst)) * S ((ge_representation_real_code_member_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_member_tracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_member_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_member_tracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_member_tracestepsmultiplyfirstreal ge_balance_negative_member_tracestepsmultiplyfirstreal. (((((ge_representation_real_code_member_tracestepsmultiplyfirst) = 2 * (ge_balance_positive_member_tracestepsmultiplyfirstreal) /\ (ge_balance_negative_member_tracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_member_tracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_member_tracestepsmultiplyfirst) = 2 * ge_signed_half_member_tracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_member_tracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_member_tracestepsmultiplyfirstreal) = S ge_signed_half_member_tracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_member_tracestepsmultiply) + ge_balance_negative_member_tracestepsmultiplyfirstreal = (ge_first_rn_member_tracestepsmultiply) + ge_balance_positive_member_tracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_member_tracestepsmultiplyfirstimaginary ge_balance_negative_member_tracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_member_tracestepsmultiplyfirst) = 2 * (ge_balance_positive_member_tracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_member_tracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_member_tracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_member_tracestepsmultiplyfirst) = 2 * ge_signed_half_member_tracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_member_tracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_member_tracestepsmultiplyfirstimaginary) = S ge_signed_half_member_tracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_member_tracestepsmultiply) + ge_balance_negative_member_tracestepsmultiplyfirstimaginary = (ge_first_in_member_tracestepsmultiply) + ge_balance_positive_member_tracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_tracestepsmultiplysecond ge_representation_imaginary_code_member_tracestepsmultiplysecond. (((gr_product_factor_member_tracesteps) = ((ge_representation_real_code_member_tracestepsmultiplysecond) + (ge_representation_imaginary_code_member_tracestepsmultiplysecond)) * S ((ge_representation_real_code_member_tracestepsmultiplysecond) + (ge_representation_imaginary_code_member_tracestepsmultiplysecond)) + ((ge_representation_imaginary_code_member_tracestepsmultiplysecond) + (ge_representation_imaginary_code_member_tracestepsmultiplysecond))) /\ ((exists ge_balance_positive_member_tracestepsmultiplysecondreal ge_balance_negative_member_tracestepsmultiplysecondreal. (((((ge_representation_real_code_member_tracestepsmultiplysecond) = 2 * (ge_balance_positive_member_tracestepsmultiplysecondreal) /\ (ge_balance_negative_member_tracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_member_tracestepsmultiplysecondrealdecode. (((ge_representation_real_code_member_tracestepsmultiplysecond) = 2 * ge_signed_half_member_tracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_member_tracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_member_tracestepsmultiplysecondreal) = S ge_signed_half_member_tracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_member_tracestepsmultiply) + ge_balance_negative_member_tracestepsmultiplysecondreal = (ge_second_rn_member_tracestepsmultiply) + ge_balance_positive_member_tracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_member_tracestepsmultiplysecondimaginary ge_balance_negative_member_tracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_member_tracestepsmultiplysecond) = 2 * (ge_balance_positive_member_tracestepsmultiplysecondimaginary) /\ (ge_balance_negative_member_tracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_member_tracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_member_tracestepsmultiplysecond) = 2 * ge_signed_half_member_tracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_member_tracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_member_tracestepsmultiplysecondimaginary) = S ge_signed_half_member_tracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_member_tracestepsmultiply) + ge_balance_negative_member_tracestepsmultiplysecondimaginary = (ge_second_in_member_tracestepsmultiply) + ge_balance_positive_member_tracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_member_tracestepsmultiplyoutput ge_representation_imaginary_code_member_tracestepsmultiplyoutput. (((gr_product_after_member_tracesteps) = ((ge_representation_real_code_member_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_member_tracestepsmultiplyoutput)) * S ((ge_representation_real_code_member_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_member_tracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_member_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_member_tracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_member_tracestepsmultiplyoutputreal ge_balance_negative_member_tracestepsmultiplyoutputreal. (((((ge_representation_real_code_member_tracestepsmultiplyoutput) = 2 * (ge_balance_positive_member_tracestepsmultiplyoutputreal) /\ (ge_balance_negative_member_tracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_member_tracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_member_tracestepsmultiplyoutput) = 2 * ge_signed_half_member_tracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_member_tracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_member_tracestepsmultiplyoutputreal) = S ge_signed_half_member_tracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_member_tracestepsmultiply) * (ge_second_rp_member_tracestepsmultiply))) + (((ge_first_rn_member_tracestepsmultiply) * (ge_second_rn_member_tracestepsmultiply))))) + (((((ge_first_ip_member_tracestepsmultiply) * (ge_second_in_member_tracestepsmultiply))) + (((ge_first_in_member_tracestepsmultiply) * (ge_second_ip_member_tracestepsmultiply))))))) + ge_balance_negative_member_tracestepsmultiplyoutputreal = (((((((ge_first_rp_member_tracestepsmultiply) * (ge_second_rn_member_tracestepsmultiply))) + (((ge_first_rn_member_tracestepsmultiply) * (ge_second_rp_member_tracestepsmultiply))))) + (((((ge_first_ip_member_tracestepsmultiply) * (ge_second_ip_member_tracestepsmultiply))) + (((ge_first_in_member_tracestepsmultiply) * (ge_second_in_member_tracestepsmultiply))))))) + ge_balance_positive_member_tracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_member_tracestepsmultiplyoutputimaginary ge_balance_negative_member_tracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_member_tracestepsmultiplyoutput) = 2 * (ge_balance_positive_member_tracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_member_tracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_member_tracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_member_tracestepsmultiplyoutput) = 2 * ge_signed_half_member_tracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_member_tracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_member_tracestepsmultiplyoutputimaginary) = S ge_signed_half_member_tracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_tracestepsmultiply) * (ge_second_ip_member_tracestepsmultiply))) + (((ge_first_rn_member_tracestepsmultiply) * (ge_second_in_member_tracestepsmultiply))))) + (((((ge_first_ip_member_tracestepsmultiply) * (ge_second_rp_member_tracestepsmultiply))) + (((ge_first_in_member_tracestepsmultiply) * (ge_second_rn_member_tracestepsmultiply))))))) + ge_balance_negative_member_tracestepsmultiplyoutputimaginary = (((((((ge_first_rp_member_tracestepsmultiply) * (ge_second_in_member_tracestepsmultiply))) + (((ge_first_rn_member_tracestepsmultiply) * (ge_second_ip_member_tracestepsmultiply))))) + (((((ge_first_ip_member_tracestepsmultiply) * (ge_second_rn_member_tracestepsmultiply))) + (((ge_first_in_member_tracestepsmultiply) * (ge_second_rp_member_tracestepsmultiply))))))) + ge_balance_positive_member_tracestepsmultiplyoutputimaginary)))))))))))))))) -> (((exists ge_real_positive_member_primecarrier ge_real_negative_member_primecarrier ge_imaginary_positive_member_primecarrier ge_imaginary_negative_member_primecarrier. (exists ge_real_code_member_primecarrierdecode ge_imaginary_code_member_primecarrierdecode. (((p) = ((ge_real_code_member_primecarrierdecode) + (ge_imaginary_code_member_primecarrierdecode)) * S ((ge_real_code_member_primecarrierdecode) + (ge_imaginary_code_member_primecarrierdecode)) + ((ge_imaginary_code_member_primecarrierdecode) + (ge_imaginary_code_member_primecarrierdecode))) /\ (((((ge_real_code_member_primecarrierdecode) = 2 * (ge_real_positive_member_primecarrier) /\ (ge_real_negative_member_primecarrier) = 0) \/ exists ge_signed_half_ge_member_primecarrierdecode_real. (((ge_real_code_member_primecarrierdecode) = 2 * ge_signed_half_ge_member_primecarrierdecode_real + 1 /\ (ge_real_positive_member_primecarrier) = 0) /\ (ge_real_negative_member_primecarrier) = S ge_signed_half_ge_member_primecarrierdecode_real))) /\ ((((ge_imaginary_code_member_primecarrierdecode) = 2 * (ge_imaginary_positive_member_primecarrier) /\ (ge_imaginary_negative_member_primecarrier) = 0) \/ exists ge_signed_half_ge_member_primecarrierdecode_imaginary. (((ge_imaginary_code_member_primecarrierdecode) = 2 * ge_signed_half_ge_member_primecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_member_primecarrier) = 0) /\ (ge_imaginary_negative_member_primecarrier) = S ge_signed_half_ge_member_primecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_member_primenonunit. (exists ge_first_rp_member_primenonunitidentity ge_first_rn_member_primenonunitidentity ge_first_ip_member_primenonunitidentity ge_first_in_member_primenonunitidentity ge_second_rp_member_primenonunitidentity ge_second_rn_member_primenonunitidentity ge_second_ip_member_primenonunitidentity ge_second_in_member_primenonunitidentity. ((exists ge_representation_real_code_member_primenonunitidentityfirst ge_representation_imaginary_code_member_primenonunitidentityfirst. (((p) = ((ge_representation_real_code_member_primenonunitidentityfirst) + (ge_representation_imaginary_code_member_primenonunitidentityfirst)) * S ((ge_representation_real_code_member_primenonunitidentityfirst) + (ge_representation_imaginary_code_member_primenonunitidentityfirst)) + ((ge_representation_imaginary_code_member_primenonunitidentityfirst) + (ge_representation_imaginary_code_member_primenonunitidentityfirst))) /\ ((exists ge_balance_positive_member_primenonunitidentityfirstreal ge_balance_negative_member_primenonunitidentityfirstreal. (((((ge_representation_real_code_member_primenonunitidentityfirst) = 2 * (ge_balance_positive_member_primenonunitidentityfirstreal) /\ (ge_balance_negative_member_primenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_member_primenonunitidentityfirstrealdecode. (((ge_representation_real_code_member_primenonunitidentityfirst) = 2 * ge_signed_half_member_primenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_member_primenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_member_primenonunitidentityfirstreal) = S ge_signed_half_member_primenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_member_primenonunitidentity) + ge_balance_negative_member_primenonunitidentityfirstreal = (ge_first_rn_member_primenonunitidentity) + ge_balance_positive_member_primenonunitidentityfirstreal))) /\ (exists ge_balance_positive_member_primenonunitidentityfirstimaginary ge_balance_negative_member_primenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_member_primenonunitidentityfirst) = 2 * (ge_balance_positive_member_primenonunitidentityfirstimaginary) /\ (ge_balance_negative_member_primenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_member_primenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_member_primenonunitidentityfirst) = 2 * ge_signed_half_member_primenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_member_primenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_member_primenonunitidentityfirstimaginary) = S ge_signed_half_member_primenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_member_primenonunitidentity) + ge_balance_negative_member_primenonunitidentityfirstimaginary = (ge_first_in_member_primenonunitidentity) + ge_balance_positive_member_primenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_primenonunitidentitysecond ge_representation_imaginary_code_member_primenonunitidentitysecond. (((gr_inverse_member_primenonunit) = ((ge_representation_real_code_member_primenonunitidentitysecond) + (ge_representation_imaginary_code_member_primenonunitidentitysecond)) * S ((ge_representation_real_code_member_primenonunitidentitysecond) + (ge_representation_imaginary_code_member_primenonunitidentitysecond)) + ((ge_representation_imaginary_code_member_primenonunitidentitysecond) + (ge_representation_imaginary_code_member_primenonunitidentitysecond))) /\ ((exists ge_balance_positive_member_primenonunitidentitysecondreal ge_balance_negative_member_primenonunitidentitysecondreal. (((((ge_representation_real_code_member_primenonunitidentitysecond) = 2 * (ge_balance_positive_member_primenonunitidentitysecondreal) /\ (ge_balance_negative_member_primenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_member_primenonunitidentitysecondrealdecode. (((ge_representation_real_code_member_primenonunitidentitysecond) = 2 * ge_signed_half_member_primenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_member_primenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_member_primenonunitidentitysecondreal) = S ge_signed_half_member_primenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_member_primenonunitidentity) + ge_balance_negative_member_primenonunitidentitysecondreal = (ge_second_rn_member_primenonunitidentity) + ge_balance_positive_member_primenonunitidentitysecondreal))) /\ (exists ge_balance_positive_member_primenonunitidentitysecondimaginary ge_balance_negative_member_primenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_member_primenonunitidentitysecond) = 2 * (ge_balance_positive_member_primenonunitidentitysecondimaginary) /\ (ge_balance_negative_member_primenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_member_primenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_member_primenonunitidentitysecond) = 2 * ge_signed_half_member_primenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_member_primenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_member_primenonunitidentitysecondimaginary) = S ge_signed_half_member_primenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_member_primenonunitidentity) + ge_balance_negative_member_primenonunitidentitysecondimaginary = (ge_second_in_member_primenonunitidentity) + ge_balance_positive_member_primenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_member_primenonunitidentityoutput ge_representation_imaginary_code_member_primenonunitidentityoutput. (((6) = ((ge_representation_real_code_member_primenonunitidentityoutput) + (ge_representation_imaginary_code_member_primenonunitidentityoutput)) * S ((ge_representation_real_code_member_primenonunitidentityoutput) + (ge_representation_imaginary_code_member_primenonunitidentityoutput)) + ((ge_representation_imaginary_code_member_primenonunitidentityoutput) + (ge_representation_imaginary_code_member_primenonunitidentityoutput))) /\ ((exists ge_balance_positive_member_primenonunitidentityoutputreal ge_balance_negative_member_primenonunitidentityoutputreal. (((((ge_representation_real_code_member_primenonunitidentityoutput) = 2 * (ge_balance_positive_member_primenonunitidentityoutputreal) /\ (ge_balance_negative_member_primenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_member_primenonunitidentityoutputrealdecode. (((ge_representation_real_code_member_primenonunitidentityoutput) = 2 * ge_signed_half_member_primenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_member_primenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_member_primenonunitidentityoutputreal) = S ge_signed_half_member_primenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_member_primenonunitidentity) * (ge_second_rp_member_primenonunitidentity))) + (((ge_first_rn_member_primenonunitidentity) * (ge_second_rn_member_primenonunitidentity))))) + (((((ge_first_ip_member_primenonunitidentity) * (ge_second_in_member_primenonunitidentity))) + (((ge_first_in_member_primenonunitidentity) * (ge_second_ip_member_primenonunitidentity))))))) + ge_balance_negative_member_primenonunitidentityoutputreal = (((((((ge_first_rp_member_primenonunitidentity) * (ge_second_rn_member_primenonunitidentity))) + (((ge_first_rn_member_primenonunitidentity) * (ge_second_rp_member_primenonunitidentity))))) + (((((ge_first_ip_member_primenonunitidentity) * (ge_second_ip_member_primenonunitidentity))) + (((ge_first_in_member_primenonunitidentity) * (ge_second_in_member_primenonunitidentity))))))) + ge_balance_positive_member_primenonunitidentityoutputreal))) /\ (exists ge_balance_positive_member_primenonunitidentityoutputimaginary ge_balance_negative_member_primenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_member_primenonunitidentityoutput) = 2 * (ge_balance_positive_member_primenonunitidentityoutputimaginary) /\ (ge_balance_negative_member_primenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_member_primenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_member_primenonunitidentityoutput) = 2 * ge_signed_half_member_primenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_member_primenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_member_primenonunitidentityoutputimaginary) = S ge_signed_half_member_primenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_primenonunitidentity) * (ge_second_ip_member_primenonunitidentity))) + (((ge_first_rn_member_primenonunitidentity) * (ge_second_in_member_primenonunitidentity))))) + (((((ge_first_ip_member_primenonunitidentity) * (ge_second_rp_member_primenonunitidentity))) + (((ge_first_in_member_primenonunitidentity) * (ge_second_rn_member_primenonunitidentity))))))) + ge_balance_negative_member_primenonunitidentityoutputimaginary = (((((((ge_first_rp_member_primenonunitidentity) * (ge_second_in_member_primenonunitidentity))) + (((ge_first_rn_member_primenonunitidentity) * (ge_second_ip_member_primenonunitidentity))))) + (((((ge_first_ip_member_primenonunitidentity) * (ge_second_rn_member_primenonunitidentity))) + (((ge_first_in_member_primenonunitidentity) * (ge_second_rp_member_primenonunitidentity))))))) + ge_balance_positive_member_primenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_member_prime gr_second_factor_member_prime. (exists ge_first_rp_member_primefactorization ge_first_rn_member_primefactorization ge_first_ip_member_primefactorization ge_first_in_member_primefactorization ge_second_rp_member_primefactorization ge_second_rn_member_primefactorization ge_second_ip_member_primefactorization ge_second_in_member_primefactorization. ((exists ge_representation_real_code_member_primefactorizationfirst ge_representation_imaginary_code_member_primefactorizationfirst. (((gr_first_factor_member_prime) = ((ge_representation_real_code_member_primefactorizationfirst) + (ge_representation_imaginary_code_member_primefactorizationfirst)) * S ((ge_representation_real_code_member_primefactorizationfirst) + (ge_representation_imaginary_code_member_primefactorizationfirst)) + ((ge_representation_imaginary_code_member_primefactorizationfirst) + (ge_representation_imaginary_code_member_primefactorizationfirst))) /\ ((exists ge_balance_positive_member_primefactorizationfirstreal ge_balance_negative_member_primefactorizationfirstreal. (((((ge_representation_real_code_member_primefactorizationfirst) = 2 * (ge_balance_positive_member_primefactorizationfirstreal) /\ (ge_balance_negative_member_primefactorizationfirstreal) = 0) \/ exists ge_signed_half_member_primefactorizationfirstrealdecode. (((ge_representation_real_code_member_primefactorizationfirst) = 2 * ge_signed_half_member_primefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_member_primefactorizationfirstreal) = 0) /\ (ge_balance_negative_member_primefactorizationfirstreal) = S ge_signed_half_member_primefactorizationfirstrealdecode))) /\ ((ge_first_rp_member_primefactorization) + ge_balance_negative_member_primefactorizationfirstreal = (ge_first_rn_member_primefactorization) + ge_balance_positive_member_primefactorizationfirstreal))) /\ (exists ge_balance_positive_member_primefactorizationfirstimaginary ge_balance_negative_member_primefactorizationfirstimaginary. (((((ge_representation_imaginary_code_member_primefactorizationfirst) = 2 * (ge_balance_positive_member_primefactorizationfirstimaginary) /\ (ge_balance_negative_member_primefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_member_primefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_member_primefactorizationfirst) = 2 * ge_signed_half_member_primefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_member_primefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_member_primefactorizationfirstimaginary) = S ge_signed_half_member_primefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_member_primefactorization) + ge_balance_negative_member_primefactorizationfirstimaginary = (ge_first_in_member_primefactorization) + ge_balance_positive_member_primefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_primefactorizationsecond ge_representation_imaginary_code_member_primefactorizationsecond. (((gr_second_factor_member_prime) = ((ge_representation_real_code_member_primefactorizationsecond) + (ge_representation_imaginary_code_member_primefactorizationsecond)) * S ((ge_representation_real_code_member_primefactorizationsecond) + (ge_representation_imaginary_code_member_primefactorizationsecond)) + ((ge_representation_imaginary_code_member_primefactorizationsecond) + (ge_representation_imaginary_code_member_primefactorizationsecond))) /\ ((exists ge_balance_positive_member_primefactorizationsecondreal ge_balance_negative_member_primefactorizationsecondreal. (((((ge_representation_real_code_member_primefactorizationsecond) = 2 * (ge_balance_positive_member_primefactorizationsecondreal) /\ (ge_balance_negative_member_primefactorizationsecondreal) = 0) \/ exists ge_signed_half_member_primefactorizationsecondrealdecode. (((ge_representation_real_code_member_primefactorizationsecond) = 2 * ge_signed_half_member_primefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_member_primefactorizationsecondreal) = 0) /\ (ge_balance_negative_member_primefactorizationsecondreal) = S ge_signed_half_member_primefactorizationsecondrealdecode))) /\ ((ge_second_rp_member_primefactorization) + ge_balance_negative_member_primefactorizationsecondreal = (ge_second_rn_member_primefactorization) + ge_balance_positive_member_primefactorizationsecondreal))) /\ (exists ge_balance_positive_member_primefactorizationsecondimaginary ge_balance_negative_member_primefactorizationsecondimaginary. (((((ge_representation_imaginary_code_member_primefactorizationsecond) = 2 * (ge_balance_positive_member_primefactorizationsecondimaginary) /\ (ge_balance_negative_member_primefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_member_primefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_member_primefactorizationsecond) = 2 * ge_signed_half_member_primefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_member_primefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_member_primefactorizationsecondimaginary) = S ge_signed_half_member_primefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_member_primefactorization) + ge_balance_negative_member_primefactorizationsecondimaginary = (ge_second_in_member_primefactorization) + ge_balance_positive_member_primefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_member_primefactorizationoutput ge_representation_imaginary_code_member_primefactorizationoutput. (((p) = ((ge_representation_real_code_member_primefactorizationoutput) + (ge_representation_imaginary_code_member_primefactorizationoutput)) * S ((ge_representation_real_code_member_primefactorizationoutput) + (ge_representation_imaginary_code_member_primefactorizationoutput)) + ((ge_representation_imaginary_code_member_primefactorizationoutput) + (ge_representation_imaginary_code_member_primefactorizationoutput))) /\ ((exists ge_balance_positive_member_primefactorizationoutputreal ge_balance_negative_member_primefactorizationoutputreal. (((((ge_representation_real_code_member_primefactorizationoutput) = 2 * (ge_balance_positive_member_primefactorizationoutputreal) /\ (ge_balance_negative_member_primefactorizationoutputreal) = 0) \/ exists ge_signed_half_member_primefactorizationoutputrealdecode. (((ge_representation_real_code_member_primefactorizationoutput) = 2 * ge_signed_half_member_primefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_member_primefactorizationoutputreal) = 0) /\ (ge_balance_negative_member_primefactorizationoutputreal) = S ge_signed_half_member_primefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_member_primefactorization) * (ge_second_rp_member_primefactorization))) + (((ge_first_rn_member_primefactorization) * (ge_second_rn_member_primefactorization))))) + (((((ge_first_ip_member_primefactorization) * (ge_second_in_member_primefactorization))) + (((ge_first_in_member_primefactorization) * (ge_second_ip_member_primefactorization))))))) + ge_balance_negative_member_primefactorizationoutputreal = (((((((ge_first_rp_member_primefactorization) * (ge_second_rn_member_primefactorization))) + (((ge_first_rn_member_primefactorization) * (ge_second_rp_member_primefactorization))))) + (((((ge_first_ip_member_primefactorization) * (ge_second_ip_member_primefactorization))) + (((ge_first_in_member_primefactorization) * (ge_second_in_member_primefactorization))))))) + ge_balance_positive_member_primefactorizationoutputreal))) /\ (exists ge_balance_positive_member_primefactorizationoutputimaginary ge_balance_negative_member_primefactorizationoutputimaginary. (((((ge_representation_imaginary_code_member_primefactorizationoutput) = 2 * (ge_balance_positive_member_primefactorizationoutputimaginary) /\ (ge_balance_negative_member_primefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_member_primefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_member_primefactorizationoutput) = 2 * ge_signed_half_member_primefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_member_primefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_member_primefactorizationoutputimaginary) = S ge_signed_half_member_primefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_primefactorization) * (ge_second_ip_member_primefactorization))) + (((ge_first_rn_member_primefactorization) * (ge_second_in_member_primefactorization))))) + (((((ge_first_ip_member_primefactorization) * (ge_second_rp_member_primefactorization))) + (((ge_first_in_member_primefactorization) * (ge_second_rn_member_primefactorization))))))) + ge_balance_negative_member_primefactorizationoutputimaginary = (((((((ge_first_rp_member_primefactorization) * (ge_second_in_member_primefactorization))) + (((ge_first_rn_member_primefactorization) * (ge_second_ip_member_primefactorization))))) + (((((ge_first_ip_member_primefactorization) * (ge_second_rn_member_primefactorization))) + (((ge_first_in_member_primefactorization) * (ge_second_rp_member_primefactorization))))))) + ge_balance_positive_member_primefactorizationoutputimaginary))))))))) -> (exists gr_inverse_member_primefirst_unit. (exists ge_first_rp_member_primefirst_unitidentity ge_first_rn_member_primefirst_unitidentity ge_first_ip_member_primefirst_unitidentity ge_first_in_member_primefirst_unitidentity ge_second_rp_member_primefirst_unitidentity ge_second_rn_member_primefirst_unitidentity ge_second_ip_member_primefirst_unitidentity ge_second_in_member_primefirst_unitidentity. ((exists ge_representation_real_code_member_primefirst_unitidentityfirst ge_representation_imaginary_code_member_primefirst_unitidentityfirst. (((gr_first_factor_member_prime) = ((ge_representation_real_code_member_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_member_primefirst_unitidentityfirst)) * S ((ge_representation_real_code_member_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_member_primefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_member_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_member_primefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_member_primefirst_unitidentityfirstreal ge_balance_negative_member_primefirst_unitidentityfirstreal. (((((ge_representation_real_code_member_primefirst_unitidentityfirst) = 2 * (ge_balance_positive_member_primefirst_unitidentityfirstreal) /\ (ge_balance_negative_member_primefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_member_primefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_member_primefirst_unitidentityfirst) = 2 * ge_signed_half_member_primefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_member_primefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_member_primefirst_unitidentityfirstreal) = S ge_signed_half_member_primefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_member_primefirst_unitidentity) + ge_balance_negative_member_primefirst_unitidentityfirstreal = (ge_first_rn_member_primefirst_unitidentity) + ge_balance_positive_member_primefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_member_primefirst_unitidentityfirstimaginary ge_balance_negative_member_primefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_member_primefirst_unitidentityfirst) = 2 * (ge_balance_positive_member_primefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_member_primefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_member_primefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_member_primefirst_unitidentityfirst) = 2 * ge_signed_half_member_primefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_member_primefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_member_primefirst_unitidentityfirstimaginary) = S ge_signed_half_member_primefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_member_primefirst_unitidentity) + ge_balance_negative_member_primefirst_unitidentityfirstimaginary = (ge_first_in_member_primefirst_unitidentity) + ge_balance_positive_member_primefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_primefirst_unitidentitysecond ge_representation_imaginary_code_member_primefirst_unitidentitysecond. (((gr_inverse_member_primefirst_unit) = ((ge_representation_real_code_member_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_member_primefirst_unitidentitysecond)) * S ((ge_representation_real_code_member_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_member_primefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_member_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_member_primefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_member_primefirst_unitidentitysecondreal ge_balance_negative_member_primefirst_unitidentitysecondreal. (((((ge_representation_real_code_member_primefirst_unitidentitysecond) = 2 * (ge_balance_positive_member_primefirst_unitidentitysecondreal) /\ (ge_balance_negative_member_primefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_member_primefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_member_primefirst_unitidentitysecond) = 2 * ge_signed_half_member_primefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_member_primefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_member_primefirst_unitidentitysecondreal) = S ge_signed_half_member_primefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_member_primefirst_unitidentity) + ge_balance_negative_member_primefirst_unitidentitysecondreal = (ge_second_rn_member_primefirst_unitidentity) + ge_balance_positive_member_primefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_member_primefirst_unitidentitysecondimaginary ge_balance_negative_member_primefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_member_primefirst_unitidentitysecond) = 2 * (ge_balance_positive_member_primefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_member_primefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_member_primefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_member_primefirst_unitidentitysecond) = 2 * ge_signed_half_member_primefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_member_primefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_member_primefirst_unitidentitysecondimaginary) = S ge_signed_half_member_primefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_member_primefirst_unitidentity) + ge_balance_negative_member_primefirst_unitidentitysecondimaginary = (ge_second_in_member_primefirst_unitidentity) + ge_balance_positive_member_primefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_member_primefirst_unitidentityoutput ge_representation_imaginary_code_member_primefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_member_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_member_primefirst_unitidentityoutput)) * S ((ge_representation_real_code_member_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_member_primefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_member_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_member_primefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_member_primefirst_unitidentityoutputreal ge_balance_negative_member_primefirst_unitidentityoutputreal. (((((ge_representation_real_code_member_primefirst_unitidentityoutput) = 2 * (ge_balance_positive_member_primefirst_unitidentityoutputreal) /\ (ge_balance_negative_member_primefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_member_primefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_member_primefirst_unitidentityoutput) = 2 * ge_signed_half_member_primefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_member_primefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_member_primefirst_unitidentityoutputreal) = S ge_signed_half_member_primefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_member_primefirst_unitidentity) * (ge_second_rp_member_primefirst_unitidentity))) + (((ge_first_rn_member_primefirst_unitidentity) * (ge_second_rn_member_primefirst_unitidentity))))) + (((((ge_first_ip_member_primefirst_unitidentity) * (ge_second_in_member_primefirst_unitidentity))) + (((ge_first_in_member_primefirst_unitidentity) * (ge_second_ip_member_primefirst_unitidentity))))))) + ge_balance_negative_member_primefirst_unitidentityoutputreal = (((((((ge_first_rp_member_primefirst_unitidentity) * (ge_second_rn_member_primefirst_unitidentity))) + (((ge_first_rn_member_primefirst_unitidentity) * (ge_second_rp_member_primefirst_unitidentity))))) + (((((ge_first_ip_member_primefirst_unitidentity) * (ge_second_ip_member_primefirst_unitidentity))) + (((ge_first_in_member_primefirst_unitidentity) * (ge_second_in_member_primefirst_unitidentity))))))) + ge_balance_positive_member_primefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_member_primefirst_unitidentityoutputimaginary ge_balance_negative_member_primefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_member_primefirst_unitidentityoutput) = 2 * (ge_balance_positive_member_primefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_member_primefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_member_primefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_member_primefirst_unitidentityoutput) = 2 * ge_signed_half_member_primefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_member_primefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_member_primefirst_unitidentityoutputimaginary) = S ge_signed_half_member_primefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_primefirst_unitidentity) * (ge_second_ip_member_primefirst_unitidentity))) + (((ge_first_rn_member_primefirst_unitidentity) * (ge_second_in_member_primefirst_unitidentity))))) + (((((ge_first_ip_member_primefirst_unitidentity) * (ge_second_rp_member_primefirst_unitidentity))) + (((ge_first_in_member_primefirst_unitidentity) * (ge_second_rn_member_primefirst_unitidentity))))))) + ge_balance_negative_member_primefirst_unitidentityoutputimaginary = (((((((ge_first_rp_member_primefirst_unitidentity) * (ge_second_in_member_primefirst_unitidentity))) + (((ge_first_rn_member_primefirst_unitidentity) * (ge_second_ip_member_primefirst_unitidentity))))) + (((((ge_first_ip_member_primefirst_unitidentity) * (ge_second_rn_member_primefirst_unitidentity))) + (((ge_first_in_member_primefirst_unitidentity) * (ge_second_rp_member_primefirst_unitidentity))))))) + ge_balance_positive_member_primefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_member_primesecond_unit. (exists ge_first_rp_member_primesecond_unitidentity ge_first_rn_member_primesecond_unitidentity ge_first_ip_member_primesecond_unitidentity ge_first_in_member_primesecond_unitidentity ge_second_rp_member_primesecond_unitidentity ge_second_rn_member_primesecond_unitidentity ge_second_ip_member_primesecond_unitidentity ge_second_in_member_primesecond_unitidentity. ((exists ge_representation_real_code_member_primesecond_unitidentityfirst ge_representation_imaginary_code_member_primesecond_unitidentityfirst. (((gr_second_factor_member_prime) = ((ge_representation_real_code_member_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_member_primesecond_unitidentityfirst)) * S ((ge_representation_real_code_member_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_member_primesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_member_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_member_primesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_member_primesecond_unitidentityfirstreal ge_balance_negative_member_primesecond_unitidentityfirstreal. (((((ge_representation_real_code_member_primesecond_unitidentityfirst) = 2 * (ge_balance_positive_member_primesecond_unitidentityfirstreal) /\ (ge_balance_negative_member_primesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_member_primesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_member_primesecond_unitidentityfirst) = 2 * ge_signed_half_member_primesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_member_primesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_member_primesecond_unitidentityfirstreal) = S ge_signed_half_member_primesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_member_primesecond_unitidentity) + ge_balance_negative_member_primesecond_unitidentityfirstreal = (ge_first_rn_member_primesecond_unitidentity) + ge_balance_positive_member_primesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_member_primesecond_unitidentityfirstimaginary ge_balance_negative_member_primesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_member_primesecond_unitidentityfirst) = 2 * (ge_balance_positive_member_primesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_member_primesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_member_primesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_member_primesecond_unitidentityfirst) = 2 * ge_signed_half_member_primesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_member_primesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_member_primesecond_unitidentityfirstimaginary) = S ge_signed_half_member_primesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_member_primesecond_unitidentity) + ge_balance_negative_member_primesecond_unitidentityfirstimaginary = (ge_first_in_member_primesecond_unitidentity) + ge_balance_positive_member_primesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_primesecond_unitidentitysecond ge_representation_imaginary_code_member_primesecond_unitidentitysecond. (((gr_inverse_member_primesecond_unit) = ((ge_representation_real_code_member_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_member_primesecond_unitidentitysecond)) * S ((ge_representation_real_code_member_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_member_primesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_member_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_member_primesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_member_primesecond_unitidentitysecondreal ge_balance_negative_member_primesecond_unitidentitysecondreal. (((((ge_representation_real_code_member_primesecond_unitidentitysecond) = 2 * (ge_balance_positive_member_primesecond_unitidentitysecondreal) /\ (ge_balance_negative_member_primesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_member_primesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_member_primesecond_unitidentitysecond) = 2 * ge_signed_half_member_primesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_member_primesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_member_primesecond_unitidentitysecondreal) = S ge_signed_half_member_primesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_member_primesecond_unitidentity) + ge_balance_negative_member_primesecond_unitidentitysecondreal = (ge_second_rn_member_primesecond_unitidentity) + ge_balance_positive_member_primesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_member_primesecond_unitidentitysecondimaginary ge_balance_negative_member_primesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_member_primesecond_unitidentitysecond) = 2 * (ge_balance_positive_member_primesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_member_primesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_member_primesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_member_primesecond_unitidentitysecond) = 2 * ge_signed_half_member_primesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_member_primesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_member_primesecond_unitidentitysecondimaginary) = S ge_signed_half_member_primesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_member_primesecond_unitidentity) + ge_balance_negative_member_primesecond_unitidentitysecondimaginary = (ge_second_in_member_primesecond_unitidentity) + ge_balance_positive_member_primesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_member_primesecond_unitidentityoutput ge_representation_imaginary_code_member_primesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_member_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_member_primesecond_unitidentityoutput)) * S ((ge_representation_real_code_member_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_member_primesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_member_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_member_primesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_member_primesecond_unitidentityoutputreal ge_balance_negative_member_primesecond_unitidentityoutputreal. (((((ge_representation_real_code_member_primesecond_unitidentityoutput) = 2 * (ge_balance_positive_member_primesecond_unitidentityoutputreal) /\ (ge_balance_negative_member_primesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_member_primesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_member_primesecond_unitidentityoutput) = 2 * ge_signed_half_member_primesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_member_primesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_member_primesecond_unitidentityoutputreal) = S ge_signed_half_member_primesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_member_primesecond_unitidentity) * (ge_second_rp_member_primesecond_unitidentity))) + (((ge_first_rn_member_primesecond_unitidentity) * (ge_second_rn_member_primesecond_unitidentity))))) + (((((ge_first_ip_member_primesecond_unitidentity) * (ge_second_in_member_primesecond_unitidentity))) + (((ge_first_in_member_primesecond_unitidentity) * (ge_second_ip_member_primesecond_unitidentity))))))) + ge_balance_negative_member_primesecond_unitidentityoutputreal = (((((((ge_first_rp_member_primesecond_unitidentity) * (ge_second_rn_member_primesecond_unitidentity))) + (((ge_first_rn_member_primesecond_unitidentity) * (ge_second_rp_member_primesecond_unitidentity))))) + (((((ge_first_ip_member_primesecond_unitidentity) * (ge_second_ip_member_primesecond_unitidentity))) + (((ge_first_in_member_primesecond_unitidentity) * (ge_second_in_member_primesecond_unitidentity))))))) + ge_balance_positive_member_primesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_member_primesecond_unitidentityoutputimaginary ge_balance_negative_member_primesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_member_primesecond_unitidentityoutput) = 2 * (ge_balance_positive_member_primesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_member_primesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_member_primesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_member_primesecond_unitidentityoutput) = 2 * ge_signed_half_member_primesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_member_primesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_member_primesecond_unitidentityoutputimaginary) = S ge_signed_half_member_primesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_primesecond_unitidentity) * (ge_second_ip_member_primesecond_unitidentity))) + (((ge_first_rn_member_primesecond_unitidentity) * (ge_second_in_member_primesecond_unitidentity))))) + (((((ge_first_ip_member_primesecond_unitidentity) * (ge_second_rp_member_primesecond_unitidentity))) + (((ge_first_in_member_primesecond_unitidentity) * (ge_second_rn_member_primesecond_unitidentity))))))) + ge_balance_negative_member_primesecond_unitidentityoutputimaginary = (((((((ge_first_rp_member_primesecond_unitidentity) * (ge_second_in_member_primesecond_unitidentity))) + (((ge_first_rn_member_primesecond_unitidentity) * (ge_second_ip_member_primesecond_unitidentity))))) + (((((ge_first_ip_member_primesecond_unitidentity) * (ge_second_rn_member_primesecond_unitidentity))) + (((ge_first_in_member_primesecond_unitidentity) * (ge_second_rp_member_primesecond_unitidentity))))))) + ge_balance_positive_member_primesecond_unitidentityoutputimaginary))))))))))))))) -> (exists gr_quotient_member_divisor. (exists ge_first_rp_member_divisorproduct ge_first_rn_member_divisorproduct ge_first_ip_member_divisorproduct ge_first_in_member_divisorproduct ge_second_rp_member_divisorproduct ge_second_rn_member_divisorproduct ge_second_ip_member_divisorproduct ge_second_in_member_divisorproduct. ((exists ge_representation_real_code_member_divisorproductfirst ge_representation_imaginary_code_member_divisorproductfirst. (((p) = ((ge_representation_real_code_member_divisorproductfirst) + (ge_representation_imaginary_code_member_divisorproductfirst)) * S ((ge_representation_real_code_member_divisorproductfirst) + (ge_representation_imaginary_code_member_divisorproductfirst)) + ((ge_representation_imaginary_code_member_divisorproductfirst) + (ge_representation_imaginary_code_member_divisorproductfirst))) /\ ((exists ge_balance_positive_member_divisorproductfirstreal ge_balance_negative_member_divisorproductfirstreal. (((((ge_representation_real_code_member_divisorproductfirst) = 2 * (ge_balance_positive_member_divisorproductfirstreal) /\ (ge_balance_negative_member_divisorproductfirstreal) = 0) \/ exists ge_signed_half_member_divisorproductfirstrealdecode. (((ge_representation_real_code_member_divisorproductfirst) = 2 * ge_signed_half_member_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_member_divisorproductfirstreal) = 0) /\ (ge_balance_negative_member_divisorproductfirstreal) = S ge_signed_half_member_divisorproductfirstrealdecode))) /\ ((ge_first_rp_member_divisorproduct) + ge_balance_negative_member_divisorproductfirstreal = (ge_first_rn_member_divisorproduct) + ge_balance_positive_member_divisorproductfirstreal))) /\ (exists ge_balance_positive_member_divisorproductfirstimaginary ge_balance_negative_member_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_member_divisorproductfirst) = 2 * (ge_balance_positive_member_divisorproductfirstimaginary) /\ (ge_balance_negative_member_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_member_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_member_divisorproductfirst) = 2 * ge_signed_half_member_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_member_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_member_divisorproductfirstimaginary) = S ge_signed_half_member_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_member_divisorproduct) + ge_balance_negative_member_divisorproductfirstimaginary = (ge_first_in_member_divisorproduct) + ge_balance_positive_member_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_divisorproductsecond ge_representation_imaginary_code_member_divisorproductsecond. (((gr_quotient_member_divisor) = ((ge_representation_real_code_member_divisorproductsecond) + (ge_representation_imaginary_code_member_divisorproductsecond)) * S ((ge_representation_real_code_member_divisorproductsecond) + (ge_representation_imaginary_code_member_divisorproductsecond)) + ((ge_representation_imaginary_code_member_divisorproductsecond) + (ge_representation_imaginary_code_member_divisorproductsecond))) /\ ((exists ge_balance_positive_member_divisorproductsecondreal ge_balance_negative_member_divisorproductsecondreal. (((((ge_representation_real_code_member_divisorproductsecond) = 2 * (ge_balance_positive_member_divisorproductsecondreal) /\ (ge_balance_negative_member_divisorproductsecondreal) = 0) \/ exists ge_signed_half_member_divisorproductsecondrealdecode. (((ge_representation_real_code_member_divisorproductsecond) = 2 * ge_signed_half_member_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_member_divisorproductsecondreal) = 0) /\ (ge_balance_negative_member_divisorproductsecondreal) = S ge_signed_half_member_divisorproductsecondrealdecode))) /\ ((ge_second_rp_member_divisorproduct) + ge_balance_negative_member_divisorproductsecondreal = (ge_second_rn_member_divisorproduct) + ge_balance_positive_member_divisorproductsecondreal))) /\ (exists ge_balance_positive_member_divisorproductsecondimaginary ge_balance_negative_member_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_member_divisorproductsecond) = 2 * (ge_balance_positive_member_divisorproductsecondimaginary) /\ (ge_balance_negative_member_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_member_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_member_divisorproductsecond) = 2 * ge_signed_half_member_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_member_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_member_divisorproductsecondimaginary) = S ge_signed_half_member_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_member_divisorproduct) + ge_balance_negative_member_divisorproductsecondimaginary = (ge_second_in_member_divisorproduct) + ge_balance_positive_member_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_member_divisorproductoutput ge_representation_imaginary_code_member_divisorproductoutput. (((P) = ((ge_representation_real_code_member_divisorproductoutput) + (ge_representation_imaginary_code_member_divisorproductoutput)) * S ((ge_representation_real_code_member_divisorproductoutput) + (ge_representation_imaginary_code_member_divisorproductoutput)) + ((ge_representation_imaginary_code_member_divisorproductoutput) + (ge_representation_imaginary_code_member_divisorproductoutput))) /\ ((exists ge_balance_positive_member_divisorproductoutputreal ge_balance_negative_member_divisorproductoutputreal. (((((ge_representation_real_code_member_divisorproductoutput) = 2 * (ge_balance_positive_member_divisorproductoutputreal) /\ (ge_balance_negative_member_divisorproductoutputreal) = 0) \/ exists ge_signed_half_member_divisorproductoutputrealdecode. (((ge_representation_real_code_member_divisorproductoutput) = 2 * ge_signed_half_member_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_member_divisorproductoutputreal) = 0) /\ (ge_balance_negative_member_divisorproductoutputreal) = S ge_signed_half_member_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_member_divisorproduct) * (ge_second_rp_member_divisorproduct))) + (((ge_first_rn_member_divisorproduct) * (ge_second_rn_member_divisorproduct))))) + (((((ge_first_ip_member_divisorproduct) * (ge_second_in_member_divisorproduct))) + (((ge_first_in_member_divisorproduct) * (ge_second_ip_member_divisorproduct))))))) + ge_balance_negative_member_divisorproductoutputreal = (((((((ge_first_rp_member_divisorproduct) * (ge_second_rn_member_divisorproduct))) + (((ge_first_rn_member_divisorproduct) * (ge_second_rp_member_divisorproduct))))) + (((((ge_first_ip_member_divisorproduct) * (ge_second_ip_member_divisorproduct))) + (((ge_first_in_member_divisorproduct) * (ge_second_in_member_divisorproduct))))))) + ge_balance_positive_member_divisorproductoutputreal))) /\ (exists ge_balance_positive_member_divisorproductoutputimaginary ge_balance_negative_member_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_member_divisorproductoutput) = 2 * (ge_balance_positive_member_divisorproductoutputimaginary) /\ (ge_balance_negative_member_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_member_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_member_divisorproductoutput) = 2 * ge_signed_half_member_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_member_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_member_divisorproductoutputimaginary) = S ge_signed_half_member_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_divisorproduct) * (ge_second_ip_member_divisorproduct))) + (((ge_first_rn_member_divisorproduct) * (ge_second_in_member_divisorproduct))))) + (((((ge_first_ip_member_divisorproduct) * (ge_second_rp_member_divisorproduct))) + (((ge_first_in_member_divisorproduct) * (ge_second_rn_member_divisorproduct))))))) + ge_balance_negative_member_divisorproductoutputimaginary = (((((((ge_first_rp_member_divisorproduct) * (ge_second_in_member_divisorproduct))) + (((ge_first_rn_member_divisorproduct) * (ge_second_ip_member_divisorproduct))))) + (((((ge_first_ip_member_divisorproduct) * (ge_second_rn_member_divisorproduct))) + (((ge_first_in_member_divisorproduct) * (ge_second_rp_member_divisorproduct))))))) + ge_balance_positive_member_divisorproductoutputimaginary)))))))))) -> exists i q. ((exists ge_gap_member_index. ge_gap_member_index + S (i) = (l)) /\ ((((exists ff_h_gprod_member_factor. ff_h_gprod_member_factor + S (q) = S ((S (i)) * c)) /\ exists ff_q_gprod_member_factor. b = ff_q_gprod_member_factor * S ((S (i)) * c) + (q))) /\ (exists gr_unit_member_association. ((exists gr_inverse_member_associationunit. (exists ge_first_rp_member_associationunitidentity ge_first_rn_member_associationunitidentity ge_first_ip_member_associationunitidentity ge_first_in_member_associationunitidentity ge_second_rp_member_associationunitidentity ge_second_rn_member_associationunitidentity ge_second_ip_member_associationunitidentity ge_second_in_member_associationunitidentity. ((exists ge_representation_real_code_member_associationunitidentityfirst ge_representation_imaginary_code_member_associationunitidentityfirst. (((gr_unit_member_association) = ((ge_representation_real_code_member_associationunitidentityfirst) + (ge_representation_imaginary_code_member_associationunitidentityfirst)) * S ((ge_representation_real_code_member_associationunitidentityfirst) + (ge_representation_imaginary_code_member_associationunitidentityfirst)) + ((ge_representation_imaginary_code_member_associationunitidentityfirst) + (ge_representation_imaginary_code_member_associationunitidentityfirst))) /\ ((exists ge_balance_positive_member_associationunitidentityfirstreal ge_balance_negative_member_associationunitidentityfirstreal. (((((ge_representation_real_code_member_associationunitidentityfirst) = 2 * (ge_balance_positive_member_associationunitidentityfirstreal) /\ (ge_balance_negative_member_associationunitidentityfirstreal) = 0) \/ exists ge_signed_half_member_associationunitidentityfirstrealdecode. (((ge_representation_real_code_member_associationunitidentityfirst) = 2 * ge_signed_half_member_associationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_member_associationunitidentityfirstreal) = 0) /\ (ge_balance_negative_member_associationunitidentityfirstreal) = S ge_signed_half_member_associationunitidentityfirstrealdecode))) /\ ((ge_first_rp_member_associationunitidentity) + ge_balance_negative_member_associationunitidentityfirstreal = (ge_first_rn_member_associationunitidentity) + ge_balance_positive_member_associationunitidentityfirstreal))) /\ (exists ge_balance_positive_member_associationunitidentityfirstimaginary ge_balance_negative_member_associationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_member_associationunitidentityfirst) = 2 * (ge_balance_positive_member_associationunitidentityfirstimaginary) /\ (ge_balance_negative_member_associationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_member_associationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_member_associationunitidentityfirst) = 2 * ge_signed_half_member_associationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_member_associationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_member_associationunitidentityfirstimaginary) = S ge_signed_half_member_associationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_member_associationunitidentity) + ge_balance_negative_member_associationunitidentityfirstimaginary = (ge_first_in_member_associationunitidentity) + ge_balance_positive_member_associationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_associationunitidentitysecond ge_representation_imaginary_code_member_associationunitidentitysecond. (((gr_inverse_member_associationunit) = ((ge_representation_real_code_member_associationunitidentitysecond) + (ge_representation_imaginary_code_member_associationunitidentitysecond)) * S ((ge_representation_real_code_member_associationunitidentitysecond) + (ge_representation_imaginary_code_member_associationunitidentitysecond)) + ((ge_representation_imaginary_code_member_associationunitidentitysecond) + (ge_representation_imaginary_code_member_associationunitidentitysecond))) /\ ((exists ge_balance_positive_member_associationunitidentitysecondreal ge_balance_negative_member_associationunitidentitysecondreal. (((((ge_representation_real_code_member_associationunitidentitysecond) = 2 * (ge_balance_positive_member_associationunitidentitysecondreal) /\ (ge_balance_negative_member_associationunitidentitysecondreal) = 0) \/ exists ge_signed_half_member_associationunitidentitysecondrealdecode. (((ge_representation_real_code_member_associationunitidentitysecond) = 2 * ge_signed_half_member_associationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_member_associationunitidentitysecondreal) = 0) /\ (ge_balance_negative_member_associationunitidentitysecondreal) = S ge_signed_half_member_associationunitidentitysecondrealdecode))) /\ ((ge_second_rp_member_associationunitidentity) + ge_balance_negative_member_associationunitidentitysecondreal = (ge_second_rn_member_associationunitidentity) + ge_balance_positive_member_associationunitidentitysecondreal))) /\ (exists ge_balance_positive_member_associationunitidentitysecondimaginary ge_balance_negative_member_associationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_member_associationunitidentitysecond) = 2 * (ge_balance_positive_member_associationunitidentitysecondimaginary) /\ (ge_balance_negative_member_associationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_member_associationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_member_associationunitidentitysecond) = 2 * ge_signed_half_member_associationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_member_associationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_member_associationunitidentitysecondimaginary) = S ge_signed_half_member_associationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_member_associationunitidentity) + ge_balance_negative_member_associationunitidentitysecondimaginary = (ge_second_in_member_associationunitidentity) + ge_balance_positive_member_associationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_member_associationunitidentityoutput ge_representation_imaginary_code_member_associationunitidentityoutput. (((6) = ((ge_representation_real_code_member_associationunitidentityoutput) + (ge_representation_imaginary_code_member_associationunitidentityoutput)) * S ((ge_representation_real_code_member_associationunitidentityoutput) + (ge_representation_imaginary_code_member_associationunitidentityoutput)) + ((ge_representation_imaginary_code_member_associationunitidentityoutput) + (ge_representation_imaginary_code_member_associationunitidentityoutput))) /\ ((exists ge_balance_positive_member_associationunitidentityoutputreal ge_balance_negative_member_associationunitidentityoutputreal. (((((ge_representation_real_code_member_associationunitidentityoutput) = 2 * (ge_balance_positive_member_associationunitidentityoutputreal) /\ (ge_balance_negative_member_associationunitidentityoutputreal) = 0) \/ exists ge_signed_half_member_associationunitidentityoutputrealdecode. (((ge_representation_real_code_member_associationunitidentityoutput) = 2 * ge_signed_half_member_associationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_member_associationunitidentityoutputreal) = 0) /\ (ge_balance_negative_member_associationunitidentityoutputreal) = S ge_signed_half_member_associationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_member_associationunitidentity) * (ge_second_rp_member_associationunitidentity))) + (((ge_first_rn_member_associationunitidentity) * (ge_second_rn_member_associationunitidentity))))) + (((((ge_first_ip_member_associationunitidentity) * (ge_second_in_member_associationunitidentity))) + (((ge_first_in_member_associationunitidentity) * (ge_second_ip_member_associationunitidentity))))))) + ge_balance_negative_member_associationunitidentityoutputreal = (((((((ge_first_rp_member_associationunitidentity) * (ge_second_rn_member_associationunitidentity))) + (((ge_first_rn_member_associationunitidentity) * (ge_second_rp_member_associationunitidentity))))) + (((((ge_first_ip_member_associationunitidentity) * (ge_second_ip_member_associationunitidentity))) + (((ge_first_in_member_associationunitidentity) * (ge_second_in_member_associationunitidentity))))))) + ge_balance_positive_member_associationunitidentityoutputreal))) /\ (exists ge_balance_positive_member_associationunitidentityoutputimaginary ge_balance_negative_member_associationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_member_associationunitidentityoutput) = 2 * (ge_balance_positive_member_associationunitidentityoutputimaginary) /\ (ge_balance_negative_member_associationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_member_associationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_member_associationunitidentityoutput) = 2 * ge_signed_half_member_associationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_member_associationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_member_associationunitidentityoutputimaginary) = S ge_signed_half_member_associationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_associationunitidentity) * (ge_second_ip_member_associationunitidentity))) + (((ge_first_rn_member_associationunitidentity) * (ge_second_in_member_associationunitidentity))))) + (((((ge_first_ip_member_associationunitidentity) * (ge_second_rp_member_associationunitidentity))) + (((ge_first_in_member_associationunitidentity) * (ge_second_rn_member_associationunitidentity))))))) + ge_balance_negative_member_associationunitidentityoutputimaginary = (((((((ge_first_rp_member_associationunitidentity) * (ge_second_in_member_associationunitidentity))) + (((ge_first_rn_member_associationunitidentity) * (ge_second_ip_member_associationunitidentity))))) + (((((ge_first_ip_member_associationunitidentity) * (ge_second_rn_member_associationunitidentity))) + (((ge_first_in_member_associationunitidentity) * (ge_second_rp_member_associationunitidentity))))))) + ge_balance_positive_member_associationunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_member_associationtransport ge_first_rn_member_associationtransport ge_first_ip_member_associationtransport ge_first_in_member_associationtransport ge_second_rp_member_associationtransport ge_second_rn_member_associationtransport ge_second_ip_member_associationtransport ge_second_in_member_associationtransport. ((exists ge_representation_real_code_member_associationtransportfirst ge_representation_imaginary_code_member_associationtransportfirst. (((gr_unit_member_association) = ((ge_representation_real_code_member_associationtransportfirst) + (ge_representation_imaginary_code_member_associationtransportfirst)) * S ((ge_representation_real_code_member_associationtransportfirst) + (ge_representation_imaginary_code_member_associationtransportfirst)) + ((ge_representation_imaginary_code_member_associationtransportfirst) + (ge_representation_imaginary_code_member_associationtransportfirst))) /\ ((exists ge_balance_positive_member_associationtransportfirstreal ge_balance_negative_member_associationtransportfirstreal. (((((ge_representation_real_code_member_associationtransportfirst) = 2 * (ge_balance_positive_member_associationtransportfirstreal) /\ (ge_balance_negative_member_associationtransportfirstreal) = 0) \/ exists ge_signed_half_member_associationtransportfirstrealdecode. (((ge_representation_real_code_member_associationtransportfirst) = 2 * ge_signed_half_member_associationtransportfirstrealdecode + 1 /\ (ge_balance_positive_member_associationtransportfirstreal) = 0) /\ (ge_balance_negative_member_associationtransportfirstreal) = S ge_signed_half_member_associationtransportfirstrealdecode))) /\ ((ge_first_rp_member_associationtransport) + ge_balance_negative_member_associationtransportfirstreal = (ge_first_rn_member_associationtransport) + ge_balance_positive_member_associationtransportfirstreal))) /\ (exists ge_balance_positive_member_associationtransportfirstimaginary ge_balance_negative_member_associationtransportfirstimaginary. (((((ge_representation_imaginary_code_member_associationtransportfirst) = 2 * (ge_balance_positive_member_associationtransportfirstimaginary) /\ (ge_balance_negative_member_associationtransportfirstimaginary) = 0) \/ exists ge_signed_half_member_associationtransportfirstimaginarydecode. (((ge_representation_imaginary_code_member_associationtransportfirst) = 2 * ge_signed_half_member_associationtransportfirstimaginarydecode + 1 /\ (ge_balance_positive_member_associationtransportfirstimaginary) = 0) /\ (ge_balance_negative_member_associationtransportfirstimaginary) = S ge_signed_half_member_associationtransportfirstimaginarydecode))) /\ ((ge_first_ip_member_associationtransport) + ge_balance_negative_member_associationtransportfirstimaginary = (ge_first_in_member_associationtransport) + ge_balance_positive_member_associationtransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_member_associationtransportsecond ge_representation_imaginary_code_member_associationtransportsecond. (((p) = ((ge_representation_real_code_member_associationtransportsecond) + (ge_representation_imaginary_code_member_associationtransportsecond)) * S ((ge_representation_real_code_member_associationtransportsecond) + (ge_representation_imaginary_code_member_associationtransportsecond)) + ((ge_representation_imaginary_code_member_associationtransportsecond) + (ge_representation_imaginary_code_member_associationtransportsecond))) /\ ((exists ge_balance_positive_member_associationtransportsecondreal ge_balance_negative_member_associationtransportsecondreal. (((((ge_representation_real_code_member_associationtransportsecond) = 2 * (ge_balance_positive_member_associationtransportsecondreal) /\ (ge_balance_negative_member_associationtransportsecondreal) = 0) \/ exists ge_signed_half_member_associationtransportsecondrealdecode. (((ge_representation_real_code_member_associationtransportsecond) = 2 * ge_signed_half_member_associationtransportsecondrealdecode + 1 /\ (ge_balance_positive_member_associationtransportsecondreal) = 0) /\ (ge_balance_negative_member_associationtransportsecondreal) = S ge_signed_half_member_associationtransportsecondrealdecode))) /\ ((ge_second_rp_member_associationtransport) + ge_balance_negative_member_associationtransportsecondreal = (ge_second_rn_member_associationtransport) + ge_balance_positive_member_associationtransportsecondreal))) /\ (exists ge_balance_positive_member_associationtransportsecondimaginary ge_balance_negative_member_associationtransportsecondimaginary. (((((ge_representation_imaginary_code_member_associationtransportsecond) = 2 * (ge_balance_positive_member_associationtransportsecondimaginary) /\ (ge_balance_negative_member_associationtransportsecondimaginary) = 0) \/ exists ge_signed_half_member_associationtransportsecondimaginarydecode. (((ge_representation_imaginary_code_member_associationtransportsecond) = 2 * ge_signed_half_member_associationtransportsecondimaginarydecode + 1 /\ (ge_balance_positive_member_associationtransportsecondimaginary) = 0) /\ (ge_balance_negative_member_associationtransportsecondimaginary) = S ge_signed_half_member_associationtransportsecondimaginarydecode))) /\ ((ge_second_ip_member_associationtransport) + ge_balance_negative_member_associationtransportsecondimaginary = (ge_second_in_member_associationtransport) + ge_balance_positive_member_associationtransportsecondimaginary)))))) /\ (exists ge_representation_real_code_member_associationtransportoutput ge_representation_imaginary_code_member_associationtransportoutput. (((q) = ((ge_representation_real_code_member_associationtransportoutput) + (ge_representation_imaginary_code_member_associationtransportoutput)) * S ((ge_representation_real_code_member_associationtransportoutput) + (ge_representation_imaginary_code_member_associationtransportoutput)) + ((ge_representation_imaginary_code_member_associationtransportoutput) + (ge_representation_imaginary_code_member_associationtransportoutput))) /\ ((exists ge_balance_positive_member_associationtransportoutputreal ge_balance_negative_member_associationtransportoutputreal. (((((ge_representation_real_code_member_associationtransportoutput) = 2 * (ge_balance_positive_member_associationtransportoutputreal) /\ (ge_balance_negative_member_associationtransportoutputreal) = 0) \/ exists ge_signed_half_member_associationtransportoutputrealdecode. (((ge_representation_real_code_member_associationtransportoutput) = 2 * ge_signed_half_member_associationtransportoutputrealdecode + 1 /\ (ge_balance_positive_member_associationtransportoutputreal) = 0) /\ (ge_balance_negative_member_associationtransportoutputreal) = S ge_signed_half_member_associationtransportoutputrealdecode))) /\ ((((((((ge_first_rp_member_associationtransport) * (ge_second_rp_member_associationtransport))) + (((ge_first_rn_member_associationtransport) * (ge_second_rn_member_associationtransport))))) + (((((ge_first_ip_member_associationtransport) * (ge_second_in_member_associationtransport))) + (((ge_first_in_member_associationtransport) * (ge_second_ip_member_associationtransport))))))) + ge_balance_negative_member_associationtransportoutputreal = (((((((ge_first_rp_member_associationtransport) * (ge_second_rn_member_associationtransport))) + (((ge_first_rn_member_associationtransport) * (ge_second_rp_member_associationtransport))))) + (((((ge_first_ip_member_associationtransport) * (ge_second_ip_member_associationtransport))) + (((ge_first_in_member_associationtransport) * (ge_second_in_member_associationtransport))))))) + ge_balance_positive_member_associationtransportoutputreal))) /\ (exists ge_balance_positive_member_associationtransportoutputimaginary ge_balance_negative_member_associationtransportoutputimaginary. (((((ge_representation_imaginary_code_member_associationtransportoutput) = 2 * (ge_balance_positive_member_associationtransportoutputimaginary) /\ (ge_balance_negative_member_associationtransportoutputimaginary) = 0) \/ exists ge_signed_half_member_associationtransportoutputimaginarydecode. (((ge_representation_imaginary_code_member_associationtransportoutput) = 2 * ge_signed_half_member_associationtransportoutputimaginarydecode + 1 /\ (ge_balance_positive_member_associationtransportoutputimaginary) = 0) /\ (ge_balance_negative_member_associationtransportoutputimaginary) = S ge_signed_half_member_associationtransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_member_associationtransport) * (ge_second_ip_member_associationtransport))) + (((ge_first_rn_member_associationtransport) * (ge_second_in_member_associationtransport))))) + (((((ge_first_ip_member_associationtransport) * (ge_second_rp_member_associationtransport))) + (((ge_first_in_member_associationtransport) * (ge_second_rn_member_associationtransport))))))) + ge_balance_negative_member_associationtransportoutputimaginary = (((((((ge_first_rp_member_associationtransport) * (ge_second_in_member_associationtransport))) + (((ge_first_rn_member_associationtransport) * (ge_second_ip_member_associationtransport))))) + (((((ge_first_ip_member_associationtransport) * (ge_second_rn_member_associationtransport))) + (((ge_first_in_member_associationtransport) * (ge_second_rp_member_associationtransport))))))) + ge_balance_positive_member_associationtransportoutputimaginary)))))))))))))