gaussian_irreducible_products_associate_unique

Exact expanded first-order arithmetic statement

forall l b c P m d e Q. (forall gr_factor_index_unique_source_irreducible gr_factor_value_unique_source_irreducible. (exists ge_gap_unique_source_irreducibleindex. ge_gap_unique_source_irreducibleindex + S (gr_factor_index_unique_source_irreducible) = (l)) -> (((exists ff_h_gprod_unique_source_irreducibleentry. ff_h_gprod_unique_source_irreducibleentry + S (gr_factor_value_unique_source_irreducible) = S ((S (gr_factor_index_unique_source_irreducible)) * c)) /\ exists ff_q_gprod_unique_source_irreducibleentry. b = ff_q_gprod_unique_source_irreducibleentry * S ((S (gr_factor_index_unique_source_irreducible)) * c) + (gr_factor_value_unique_source_irreducible))) -> (((exists ge_real_positive_unique_source_irreducibleirreduciblecarrier ge_real_negative_unique_source_irreducibleirreduciblecarrier ge_imaginary_positive_unique_source_irreducibleirreduciblecarrier ge_imaginary_negative_unique_source_irreducibleirreduciblecarrier. (exists ge_real_code_unique_source_irreducibleirreduciblecarrierdecode ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode. (((gr_factor_value_unique_source_irreducible) = ((ge_real_code_unique_source_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode)) * S ((ge_real_code_unique_source_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_unique_source_irreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_unique_source_irreducibleirreduciblecarrier) /\ (ge_real_negative_unique_source_irreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_real. (((ge_real_code_unique_source_irreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_unique_source_irreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_unique_source_irreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_unique_source_irreducibleirreduciblecarrier) /\ (ge_imaginary_negative_unique_source_irreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unique_source_irreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_unique_source_irreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_unique_source_irreducible)=0)) /\ ((~(exists gr_inverse_unique_source_irreducibleirreduciblenonunit. (exists ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity ge_first_in_unique_source_irreducibleirreduciblenonunitidentity ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity ge_second_in_unique_source_irreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_unique_source_irreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond. (((gr_inverse_unique_source_irreducibleirreduciblenonunit) = ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unique_source_irreducibleirreducible gr_second_factor_unique_source_irreducibleirreducible. (exists ge_first_rp_unique_source_irreducibleirreduciblefactorization ge_first_rn_unique_source_irreducibleirreduciblefactorization ge_first_ip_unique_source_irreducibleirreduciblefactorization ge_first_in_unique_source_irreducibleirreduciblefactorization ge_second_rp_unique_source_irreducibleirreduciblefactorization ge_second_rn_unique_source_irreducibleirreduciblefactorization ge_second_ip_unique_source_irreducibleirreduciblefactorization ge_second_in_unique_source_irreducibleirreduciblefactorization. ((exists ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst. (((gr_first_factor_unique_source_irreducibleirreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstreal ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_unique_source_irreducibleirreduciblefactorization) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstreal = (ge_first_rn_unique_source_irreducibleirreduciblefactorization) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_irreducibleirreduciblefactorization) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_unique_source_irreducibleirreduciblefactorization) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond. (((gr_second_factor_unique_source_irreducibleirreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondreal ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_unique_source_irreducibleirreduciblefactorization) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondreal = (ge_second_rn_unique_source_irreducibleirreduciblefactorization) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_unique_source_irreducibleirreduciblefactorization) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_unique_source_irreducibleirreduciblefactorization) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput. (((gr_factor_value_unique_source_irreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputreal ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblefactorization) * (ge_second_rp_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_source_irreducibleirreduciblefactorization) * (ge_second_rn_unique_source_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefactorization) * (ge_second_in_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_source_irreducibleirreduciblefactorization) * (ge_second_ip_unique_source_irreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_unique_source_irreducibleirreduciblefactorization) * (ge_second_rn_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_source_irreducibleirreduciblefactorization) * (ge_second_rp_unique_source_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefactorization) * (ge_second_ip_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_source_irreducibleirreduciblefactorization) * (ge_second_in_unique_source_irreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblefactorization) * (ge_second_ip_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_source_irreducibleirreduciblefactorization) * (ge_second_in_unique_source_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefactorization) * (ge_second_rp_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_source_irreducibleirreduciblefactorization) * (ge_second_rn_unique_source_irreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_unique_source_irreducibleirreduciblefactorization) * (ge_second_in_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_source_irreducibleirreduciblefactorization) * (ge_second_ip_unique_source_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefactorization) * (ge_second_rn_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_source_irreducibleirreduciblefactorization) * (ge_second_rp_unique_source_irreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_unique_source_irreducibleirreduciblefirst_unit. (exists ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_unique_source_irreducibleirreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_unique_source_irreducibleirreduciblefirst_unit) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_unique_source_irreducibleirreduciblesecond_unit. (exists ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_unique_source_irreducibleirreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_unique_source_irreducibleirreduciblesecond_unit) = ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (exists gr_product_trace_unique_source_product gr_product_scale_unique_source_product. ((((exists ff_h_gprod_unique_source_productstart. ff_h_gprod_unique_source_productstart + S (6) = S ((S (0)) * gr_product_scale_unique_source_product)) /\ exists ff_q_gprod_unique_source_productstart. gr_product_trace_unique_source_product = ff_q_gprod_unique_source_productstart * S ((S (0)) * gr_product_scale_unique_source_product) + (6))) /\ ((((exists ff_h_gprod_unique_source_productend. ff_h_gprod_unique_source_productend + S (P) = S ((S (l)) * gr_product_scale_unique_source_product)) /\ exists ff_q_gprod_unique_source_productend. gr_product_trace_unique_source_product = ff_q_gprod_unique_source_productend * S ((S (l)) * gr_product_scale_unique_source_product) + (P))) /\ (forall gr_product_index_unique_source_productsteps. (exists ge_gap_unique_source_productstepsindex_bound. ge_gap_unique_source_productstepsindex_bound + S (gr_product_index_unique_source_productsteps) = (l)) -> exists gr_product_factor_unique_source_productsteps gr_product_before_unique_source_productsteps gr_product_after_unique_source_productsteps. ((((exists ff_h_gprod_unique_source_productstepsfactor. ff_h_gprod_unique_source_productstepsfactor + S (gr_product_factor_unique_source_productsteps) = S ((S (gr_product_index_unique_source_productsteps)) * c)) /\ exists ff_q_gprod_unique_source_productstepsfactor. b = ff_q_gprod_unique_source_productstepsfactor * S ((S (gr_product_index_unique_source_productsteps)) * c) + (gr_product_factor_unique_source_productsteps))) /\ ((((exists ff_h_gprod_unique_source_productstepsbefore. ff_h_gprod_unique_source_productstepsbefore + S (gr_product_before_unique_source_productsteps) = S ((S (gr_product_index_unique_source_productsteps)) * gr_product_scale_unique_source_product)) /\ exists ff_q_gprod_unique_source_productstepsbefore. gr_product_trace_unique_source_product = ff_q_gprod_unique_source_productstepsbefore * S ((S (gr_product_index_unique_source_productsteps)) * gr_product_scale_unique_source_product) + (gr_product_before_unique_source_productsteps))) /\ ((((exists ff_h_gprod_unique_source_productstepsafter. ff_h_gprod_unique_source_productstepsafter + S (gr_product_after_unique_source_productsteps) = S ((S (S (gr_product_index_unique_source_productsteps))) * gr_product_scale_unique_source_product)) /\ exists ff_q_gprod_unique_source_productstepsafter. gr_product_trace_unique_source_product = ff_q_gprod_unique_source_productstepsafter * S ((S (S (gr_product_index_unique_source_productsteps))) * gr_product_scale_unique_source_product) + (gr_product_after_unique_source_productsteps))) /\ (exists ge_first_rp_unique_source_productstepsmultiply ge_first_rn_unique_source_productstepsmultiply ge_first_ip_unique_source_productstepsmultiply ge_first_in_unique_source_productstepsmultiply ge_second_rp_unique_source_productstepsmultiply ge_second_rn_unique_source_productstepsmultiply ge_second_ip_unique_source_productstepsmultiply ge_second_in_unique_source_productstepsmultiply. ((exists ge_representation_real_code_unique_source_productstepsmultiplyfirst ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst. (((gr_product_before_unique_source_productsteps) = ((ge_representation_real_code_unique_source_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst)) * S ((ge_representation_real_code_unique_source_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_unique_source_productstepsmultiplyfirstreal ge_balance_negative_unique_source_productstepsmultiplyfirstreal. (((((ge_representation_real_code_unique_source_productstepsmultiplyfirst) = 2 * (ge_balance_positive_unique_source_productstepsmultiplyfirstreal) /\ (ge_balance_negative_unique_source_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_unique_source_productstepsmultiplyfirst) = 2 * ge_signed_half_unique_source_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplyfirstreal) = S ge_signed_half_unique_source_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unique_source_productstepsmultiply) + ge_balance_negative_unique_source_productstepsmultiplyfirstreal = (ge_first_rn_unique_source_productstepsmultiply) + ge_balance_positive_unique_source_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unique_source_productstepsmultiplyfirstimaginary ge_balance_negative_unique_source_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst) = 2 * (ge_balance_positive_unique_source_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_unique_source_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst) = 2 * ge_signed_half_unique_source_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplyfirstimaginary) = S ge_signed_half_unique_source_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_productstepsmultiply) + ge_balance_negative_unique_source_productstepsmultiplyfirstimaginary = (ge_first_in_unique_source_productstepsmultiply) + ge_balance_positive_unique_source_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_productstepsmultiplysecond ge_representation_imaginary_code_unique_source_productstepsmultiplysecond. (((gr_product_factor_unique_source_productsteps) = ((ge_representation_real_code_unique_source_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_source_productstepsmultiplysecond)) * S ((ge_representation_real_code_unique_source_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_source_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_unique_source_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_source_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_unique_source_productstepsmultiplysecondreal ge_balance_negative_unique_source_productstepsmultiplysecondreal. (((((ge_representation_real_code_unique_source_productstepsmultiplysecond) = 2 * (ge_balance_positive_unique_source_productstepsmultiplysecondreal) /\ (ge_balance_negative_unique_source_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_unique_source_productstepsmultiplysecond) = 2 * ge_signed_half_unique_source_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplysecondreal) = S ge_signed_half_unique_source_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unique_source_productstepsmultiply) + ge_balance_negative_unique_source_productstepsmultiplysecondreal = (ge_second_rn_unique_source_productstepsmultiply) + ge_balance_positive_unique_source_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_unique_source_productstepsmultiplysecondimaginary ge_balance_negative_unique_source_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unique_source_productstepsmultiplysecond) = 2 * (ge_balance_positive_unique_source_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_unique_source_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_productstepsmultiplysecond) = 2 * ge_signed_half_unique_source_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplysecondimaginary) = S ge_signed_half_unique_source_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unique_source_productstepsmultiply) + ge_balance_negative_unique_source_productstepsmultiplysecondimaginary = (ge_second_in_unique_source_productstepsmultiply) + ge_balance_positive_unique_source_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_productstepsmultiplyoutput ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput. (((gr_product_after_unique_source_productsteps) = ((ge_representation_real_code_unique_source_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput)) * S ((ge_representation_real_code_unique_source_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_unique_source_productstepsmultiplyoutputreal ge_balance_negative_unique_source_productstepsmultiplyoutputreal. (((((ge_representation_real_code_unique_source_productstepsmultiplyoutput) = 2 * (ge_balance_positive_unique_source_productstepsmultiplyoutputreal) /\ (ge_balance_negative_unique_source_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_unique_source_productstepsmultiplyoutput) = 2 * ge_signed_half_unique_source_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplyoutputreal) = S ge_signed_half_unique_source_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_productstepsmultiply) * (ge_second_rp_unique_source_productstepsmultiply))) + (((ge_first_rn_unique_source_productstepsmultiply) * (ge_second_rn_unique_source_productstepsmultiply))))) + (((((ge_first_ip_unique_source_productstepsmultiply) * (ge_second_in_unique_source_productstepsmultiply))) + (((ge_first_in_unique_source_productstepsmultiply) * (ge_second_ip_unique_source_productstepsmultiply))))))) + ge_balance_negative_unique_source_productstepsmultiplyoutputreal = (((((((ge_first_rp_unique_source_productstepsmultiply) * (ge_second_rn_unique_source_productstepsmultiply))) + (((ge_first_rn_unique_source_productstepsmultiply) * (ge_second_rp_unique_source_productstepsmultiply))))) + (((((ge_first_ip_unique_source_productstepsmultiply) * (ge_second_ip_unique_source_productstepsmultiply))) + (((ge_first_in_unique_source_productstepsmultiply) * (ge_second_in_unique_source_productstepsmultiply))))))) + ge_balance_positive_unique_source_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unique_source_productstepsmultiplyoutputimaginary ge_balance_negative_unique_source_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput) = 2 * (ge_balance_positive_unique_source_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_unique_source_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput) = 2 * ge_signed_half_unique_source_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplyoutputimaginary) = S ge_signed_half_unique_source_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_productstepsmultiply) * (ge_second_ip_unique_source_productstepsmultiply))) + (((ge_first_rn_unique_source_productstepsmultiply) * (ge_second_in_unique_source_productstepsmultiply))))) + (((((ge_first_ip_unique_source_productstepsmultiply) * (ge_second_rp_unique_source_productstepsmultiply))) + (((ge_first_in_unique_source_productstepsmultiply) * (ge_second_rn_unique_source_productstepsmultiply))))))) + ge_balance_negative_unique_source_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_unique_source_productstepsmultiply) * (ge_second_in_unique_source_productstepsmultiply))) + (((ge_first_rn_unique_source_productstepsmultiply) * (ge_second_ip_unique_source_productstepsmultiply))))) + (((((ge_first_ip_unique_source_productstepsmultiply) * (ge_second_rn_unique_source_productstepsmultiply))) + (((ge_first_in_unique_source_productstepsmultiply) * (ge_second_rp_unique_source_productstepsmultiply))))))) + ge_balance_positive_unique_source_productstepsmultiplyoutputimaginary)))))))))))))))) -> (forall gr_factor_index_unique_target_irreducible gr_factor_value_unique_target_irreducible. (exists ge_gap_unique_target_irreducibleindex. ge_gap_unique_target_irreducibleindex + S (gr_factor_index_unique_target_irreducible) = (m)) -> (((exists ff_h_gprod_unique_target_irreducibleentry. ff_h_gprod_unique_target_irreducibleentry + S (gr_factor_value_unique_target_irreducible) = S ((S (gr_factor_index_unique_target_irreducible)) * e)) /\ exists ff_q_gprod_unique_target_irreducibleentry. d = ff_q_gprod_unique_target_irreducibleentry * S ((S (gr_factor_index_unique_target_irreducible)) * e) + (gr_factor_value_unique_target_irreducible))) -> (((exists ge_real_positive_unique_target_irreducibleirreduciblecarrier ge_real_negative_unique_target_irreducibleirreduciblecarrier ge_imaginary_positive_unique_target_irreducibleirreduciblecarrier ge_imaginary_negative_unique_target_irreducibleirreduciblecarrier. (exists ge_real_code_unique_target_irreducibleirreduciblecarrierdecode ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode. (((gr_factor_value_unique_target_irreducible) = ((ge_real_code_unique_target_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode)) * S ((ge_real_code_unique_target_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_unique_target_irreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_unique_target_irreducibleirreduciblecarrier) /\ (ge_real_negative_unique_target_irreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_real. (((ge_real_code_unique_target_irreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_unique_target_irreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_unique_target_irreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_unique_target_irreducibleirreduciblecarrier) /\ (ge_imaginary_negative_unique_target_irreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unique_target_irreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_unique_target_irreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_unique_target_irreducible)=0)) /\ ((~(exists gr_inverse_unique_target_irreducibleirreduciblenonunit. (exists ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity ge_first_in_unique_target_irreducibleirreduciblenonunitidentity ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity ge_second_in_unique_target_irreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_unique_target_irreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond. (((gr_inverse_unique_target_irreducibleirreduciblenonunit) = ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unique_target_irreducibleirreducible gr_second_factor_unique_target_irreducibleirreducible. (exists ge_first_rp_unique_target_irreducibleirreduciblefactorization ge_first_rn_unique_target_irreducibleirreduciblefactorization ge_first_ip_unique_target_irreducibleirreduciblefactorization ge_first_in_unique_target_irreducibleirreduciblefactorization ge_second_rp_unique_target_irreducibleirreduciblefactorization ge_second_rn_unique_target_irreducibleirreduciblefactorization ge_second_ip_unique_target_irreducibleirreduciblefactorization ge_second_in_unique_target_irreducibleirreduciblefactorization. ((exists ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst. (((gr_first_factor_unique_target_irreducibleirreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstreal ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_unique_target_irreducibleirreduciblefactorization) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstreal = (ge_first_rn_unique_target_irreducibleirreduciblefactorization) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_irreducibleirreduciblefactorization) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_unique_target_irreducibleirreduciblefactorization) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond. (((gr_second_factor_unique_target_irreducibleirreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondreal ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_unique_target_irreducibleirreduciblefactorization) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondreal = (ge_second_rn_unique_target_irreducibleirreduciblefactorization) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_unique_target_irreducibleirreduciblefactorization) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_unique_target_irreducibleirreduciblefactorization) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput. (((gr_factor_value_unique_target_irreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputreal ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblefactorization) * (ge_second_rp_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_target_irreducibleirreduciblefactorization) * (ge_second_rn_unique_target_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefactorization) * (ge_second_in_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_target_irreducibleirreduciblefactorization) * (ge_second_ip_unique_target_irreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_unique_target_irreducibleirreduciblefactorization) * (ge_second_rn_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_target_irreducibleirreduciblefactorization) * (ge_second_rp_unique_target_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefactorization) * (ge_second_ip_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_target_irreducibleirreduciblefactorization) * (ge_second_in_unique_target_irreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblefactorization) * (ge_second_ip_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_target_irreducibleirreduciblefactorization) * (ge_second_in_unique_target_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefactorization) * (ge_second_rp_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_target_irreducibleirreduciblefactorization) * (ge_second_rn_unique_target_irreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_unique_target_irreducibleirreduciblefactorization) * (ge_second_in_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_target_irreducibleirreduciblefactorization) * (ge_second_ip_unique_target_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefactorization) * (ge_second_rn_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_target_irreducibleirreduciblefactorization) * (ge_second_rp_unique_target_irreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_unique_target_irreducibleirreduciblefirst_unit. (exists ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_unique_target_irreducibleirreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_unique_target_irreducibleirreduciblefirst_unit) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_unique_target_irreducibleirreduciblesecond_unit. (exists ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_unique_target_irreducibleirreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_unique_target_irreducibleirreduciblesecond_unit) = ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (exists gr_product_trace_unique_target_product gr_product_scale_unique_target_product. ((((exists ff_h_gprod_unique_target_productstart. ff_h_gprod_unique_target_productstart + S (6) = S ((S (0)) * gr_product_scale_unique_target_product)) /\ exists ff_q_gprod_unique_target_productstart. gr_product_trace_unique_target_product = ff_q_gprod_unique_target_productstart * S ((S (0)) * gr_product_scale_unique_target_product) + (6))) /\ ((((exists ff_h_gprod_unique_target_productend. ff_h_gprod_unique_target_productend + S (Q) = S ((S (m)) * gr_product_scale_unique_target_product)) /\ exists ff_q_gprod_unique_target_productend. gr_product_trace_unique_target_product = ff_q_gprod_unique_target_productend * S ((S (m)) * gr_product_scale_unique_target_product) + (Q))) /\ (forall gr_product_index_unique_target_productsteps. (exists ge_gap_unique_target_productstepsindex_bound. ge_gap_unique_target_productstepsindex_bound + S (gr_product_index_unique_target_productsteps) = (m)) -> exists gr_product_factor_unique_target_productsteps gr_product_before_unique_target_productsteps gr_product_after_unique_target_productsteps. ((((exists ff_h_gprod_unique_target_productstepsfactor. ff_h_gprod_unique_target_productstepsfactor + S (gr_product_factor_unique_target_productsteps) = S ((S (gr_product_index_unique_target_productsteps)) * e)) /\ exists ff_q_gprod_unique_target_productstepsfactor. d = ff_q_gprod_unique_target_productstepsfactor * S ((S (gr_product_index_unique_target_productsteps)) * e) + (gr_product_factor_unique_target_productsteps))) /\ ((((exists ff_h_gprod_unique_target_productstepsbefore. ff_h_gprod_unique_target_productstepsbefore + S (gr_product_before_unique_target_productsteps) = S ((S (gr_product_index_unique_target_productsteps)) * gr_product_scale_unique_target_product)) /\ exists ff_q_gprod_unique_target_productstepsbefore. gr_product_trace_unique_target_product = ff_q_gprod_unique_target_productstepsbefore * S ((S (gr_product_index_unique_target_productsteps)) * gr_product_scale_unique_target_product) + (gr_product_before_unique_target_productsteps))) /\ ((((exists ff_h_gprod_unique_target_productstepsafter. ff_h_gprod_unique_target_productstepsafter + S (gr_product_after_unique_target_productsteps) = S ((S (S (gr_product_index_unique_target_productsteps))) * gr_product_scale_unique_target_product)) /\ exists ff_q_gprod_unique_target_productstepsafter. gr_product_trace_unique_target_product = ff_q_gprod_unique_target_productstepsafter * S ((S (S (gr_product_index_unique_target_productsteps))) * gr_product_scale_unique_target_product) + (gr_product_after_unique_target_productsteps))) /\ (exists ge_first_rp_unique_target_productstepsmultiply ge_first_rn_unique_target_productstepsmultiply ge_first_ip_unique_target_productstepsmultiply ge_first_in_unique_target_productstepsmultiply ge_second_rp_unique_target_productstepsmultiply ge_second_rn_unique_target_productstepsmultiply ge_second_ip_unique_target_productstepsmultiply ge_second_in_unique_target_productstepsmultiply. ((exists ge_representation_real_code_unique_target_productstepsmultiplyfirst ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst. (((gr_product_before_unique_target_productsteps) = ((ge_representation_real_code_unique_target_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst)) * S ((ge_representation_real_code_unique_target_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_unique_target_productstepsmultiplyfirstreal ge_balance_negative_unique_target_productstepsmultiplyfirstreal. (((((ge_representation_real_code_unique_target_productstepsmultiplyfirst) = 2 * (ge_balance_positive_unique_target_productstepsmultiplyfirstreal) /\ (ge_balance_negative_unique_target_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_unique_target_productstepsmultiplyfirst) = 2 * ge_signed_half_unique_target_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplyfirstreal) = S ge_signed_half_unique_target_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unique_target_productstepsmultiply) + ge_balance_negative_unique_target_productstepsmultiplyfirstreal = (ge_first_rn_unique_target_productstepsmultiply) + ge_balance_positive_unique_target_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unique_target_productstepsmultiplyfirstimaginary ge_balance_negative_unique_target_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst) = 2 * (ge_balance_positive_unique_target_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_unique_target_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst) = 2 * ge_signed_half_unique_target_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplyfirstimaginary) = S ge_signed_half_unique_target_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_productstepsmultiply) + ge_balance_negative_unique_target_productstepsmultiplyfirstimaginary = (ge_first_in_unique_target_productstepsmultiply) + ge_balance_positive_unique_target_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_productstepsmultiplysecond ge_representation_imaginary_code_unique_target_productstepsmultiplysecond. (((gr_product_factor_unique_target_productsteps) = ((ge_representation_real_code_unique_target_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_target_productstepsmultiplysecond)) * S ((ge_representation_real_code_unique_target_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_target_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_unique_target_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_target_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_unique_target_productstepsmultiplysecondreal ge_balance_negative_unique_target_productstepsmultiplysecondreal. (((((ge_representation_real_code_unique_target_productstepsmultiplysecond) = 2 * (ge_balance_positive_unique_target_productstepsmultiplysecondreal) /\ (ge_balance_negative_unique_target_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_unique_target_productstepsmultiplysecond) = 2 * ge_signed_half_unique_target_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplysecondreal) = S ge_signed_half_unique_target_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unique_target_productstepsmultiply) + ge_balance_negative_unique_target_productstepsmultiplysecondreal = (ge_second_rn_unique_target_productstepsmultiply) + ge_balance_positive_unique_target_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_unique_target_productstepsmultiplysecondimaginary ge_balance_negative_unique_target_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unique_target_productstepsmultiplysecond) = 2 * (ge_balance_positive_unique_target_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_unique_target_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_productstepsmultiplysecond) = 2 * ge_signed_half_unique_target_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplysecondimaginary) = S ge_signed_half_unique_target_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unique_target_productstepsmultiply) + ge_balance_negative_unique_target_productstepsmultiplysecondimaginary = (ge_second_in_unique_target_productstepsmultiply) + ge_balance_positive_unique_target_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_productstepsmultiplyoutput ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput. (((gr_product_after_unique_target_productsteps) = ((ge_representation_real_code_unique_target_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput)) * S ((ge_representation_real_code_unique_target_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_unique_target_productstepsmultiplyoutputreal ge_balance_negative_unique_target_productstepsmultiplyoutputreal. (((((ge_representation_real_code_unique_target_productstepsmultiplyoutput) = 2 * (ge_balance_positive_unique_target_productstepsmultiplyoutputreal) /\ (ge_balance_negative_unique_target_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_unique_target_productstepsmultiplyoutput) = 2 * ge_signed_half_unique_target_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplyoutputreal) = S ge_signed_half_unique_target_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_productstepsmultiply) * (ge_second_rp_unique_target_productstepsmultiply))) + (((ge_first_rn_unique_target_productstepsmultiply) * (ge_second_rn_unique_target_productstepsmultiply))))) + (((((ge_first_ip_unique_target_productstepsmultiply) * (ge_second_in_unique_target_productstepsmultiply))) + (((ge_first_in_unique_target_productstepsmultiply) * (ge_second_ip_unique_target_productstepsmultiply))))))) + ge_balance_negative_unique_target_productstepsmultiplyoutputreal = (((((((ge_first_rp_unique_target_productstepsmultiply) * (ge_second_rn_unique_target_productstepsmultiply))) + (((ge_first_rn_unique_target_productstepsmultiply) * (ge_second_rp_unique_target_productstepsmultiply))))) + (((((ge_first_ip_unique_target_productstepsmultiply) * (ge_second_ip_unique_target_productstepsmultiply))) + (((ge_first_in_unique_target_productstepsmultiply) * (ge_second_in_unique_target_productstepsmultiply))))))) + ge_balance_positive_unique_target_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unique_target_productstepsmultiplyoutputimaginary ge_balance_negative_unique_target_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput) = 2 * (ge_balance_positive_unique_target_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_unique_target_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput) = 2 * ge_signed_half_unique_target_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplyoutputimaginary) = S ge_signed_half_unique_target_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_productstepsmultiply) * (ge_second_ip_unique_target_productstepsmultiply))) + (((ge_first_rn_unique_target_productstepsmultiply) * (ge_second_in_unique_target_productstepsmultiply))))) + (((((ge_first_ip_unique_target_productstepsmultiply) * (ge_second_rp_unique_target_productstepsmultiply))) + (((ge_first_in_unique_target_productstepsmultiply) * (ge_second_rn_unique_target_productstepsmultiply))))))) + ge_balance_negative_unique_target_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_unique_target_productstepsmultiply) * (ge_second_in_unique_target_productstepsmultiply))) + (((ge_first_rn_unique_target_productstepsmultiply) * (ge_second_ip_unique_target_productstepsmultiply))))) + (((((ge_first_ip_unique_target_productstepsmultiply) * (ge_second_rn_unique_target_productstepsmultiply))) + (((ge_first_in_unique_target_productstepsmultiply) * (ge_second_rp_unique_target_productstepsmultiply))))))) + ge_balance_positive_unique_target_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_unit_unique_products_associate. ((exists gr_inverse_unique_products_associateunit. (exists ge_first_rp_unique_products_associateunitidentity ge_first_rn_unique_products_associateunitidentity ge_first_ip_unique_products_associateunitidentity ge_first_in_unique_products_associateunitidentity ge_second_rp_unique_products_associateunitidentity ge_second_rn_unique_products_associateunitidentity ge_second_ip_unique_products_associateunitidentity ge_second_in_unique_products_associateunitidentity. ((exists ge_representation_real_code_unique_products_associateunitidentityfirst ge_representation_imaginary_code_unique_products_associateunitidentityfirst. (((gr_unit_unique_products_associate) = ((ge_representation_real_code_unique_products_associateunitidentityfirst) + (ge_representation_imaginary_code_unique_products_associateunitidentityfirst)) * S ((ge_representation_real_code_unique_products_associateunitidentityfirst) + (ge_representation_imaginary_code_unique_products_associateunitidentityfirst)) + ((ge_representation_imaginary_code_unique_products_associateunitidentityfirst) + (ge_representation_imaginary_code_unique_products_associateunitidentityfirst))) /\ ((exists ge_balance_positive_unique_products_associateunitidentityfirstreal ge_balance_negative_unique_products_associateunitidentityfirstreal. (((((ge_representation_real_code_unique_products_associateunitidentityfirst) = 2 * (ge_balance_positive_unique_products_associateunitidentityfirstreal) /\ (ge_balance_negative_unique_products_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_products_associateunitidentityfirstrealdecode. (((ge_representation_real_code_unique_products_associateunitidentityfirst) = 2 * ge_signed_half_unique_products_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_products_associateunitidentityfirstreal) = S ge_signed_half_unique_products_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_products_associateunitidentity) + ge_balance_negative_unique_products_associateunitidentityfirstreal = (ge_first_rn_unique_products_associateunitidentity) + ge_balance_positive_unique_products_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_products_associateunitidentityfirstimaginary ge_balance_negative_unique_products_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_products_associateunitidentityfirst) = 2 * (ge_balance_positive_unique_products_associateunitidentityfirstimaginary) /\ (ge_balance_negative_unique_products_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_products_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_products_associateunitidentityfirst) = 2 * ge_signed_half_unique_products_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_products_associateunitidentityfirstimaginary) = S ge_signed_half_unique_products_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_products_associateunitidentity) + ge_balance_negative_unique_products_associateunitidentityfirstimaginary = (ge_first_in_unique_products_associateunitidentity) + ge_balance_positive_unique_products_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_products_associateunitidentitysecond ge_representation_imaginary_code_unique_products_associateunitidentitysecond. (((gr_inverse_unique_products_associateunit) = ((ge_representation_real_code_unique_products_associateunitidentitysecond) + (ge_representation_imaginary_code_unique_products_associateunitidentitysecond)) * S ((ge_representation_real_code_unique_products_associateunitidentitysecond) + (ge_representation_imaginary_code_unique_products_associateunitidentitysecond)) + ((ge_representation_imaginary_code_unique_products_associateunitidentitysecond) + (ge_representation_imaginary_code_unique_products_associateunitidentitysecond))) /\ ((exists ge_balance_positive_unique_products_associateunitidentitysecondreal ge_balance_negative_unique_products_associateunitidentitysecondreal. (((((ge_representation_real_code_unique_products_associateunitidentitysecond) = 2 * (ge_balance_positive_unique_products_associateunitidentitysecondreal) /\ (ge_balance_negative_unique_products_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_products_associateunitidentitysecondrealdecode. (((ge_representation_real_code_unique_products_associateunitidentitysecond) = 2 * ge_signed_half_unique_products_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_products_associateunitidentitysecondreal) = S ge_signed_half_unique_products_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_products_associateunitidentity) + ge_balance_negative_unique_products_associateunitidentitysecondreal = (ge_second_rn_unique_products_associateunitidentity) + ge_balance_positive_unique_products_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_products_associateunitidentitysecondimaginary ge_balance_negative_unique_products_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_products_associateunitidentitysecond) = 2 * (ge_balance_positive_unique_products_associateunitidentitysecondimaginary) /\ (ge_balance_negative_unique_products_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_products_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_products_associateunitidentitysecond) = 2 * ge_signed_half_unique_products_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_products_associateunitidentitysecondimaginary) = S ge_signed_half_unique_products_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_products_associateunitidentity) + ge_balance_negative_unique_products_associateunitidentitysecondimaginary = (ge_second_in_unique_products_associateunitidentity) + ge_balance_positive_unique_products_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_products_associateunitidentityoutput ge_representation_imaginary_code_unique_products_associateunitidentityoutput. (((6) = ((ge_representation_real_code_unique_products_associateunitidentityoutput) + (ge_representation_imaginary_code_unique_products_associateunitidentityoutput)) * S ((ge_representation_real_code_unique_products_associateunitidentityoutput) + (ge_representation_imaginary_code_unique_products_associateunitidentityoutput)) + ((ge_representation_imaginary_code_unique_products_associateunitidentityoutput) + (ge_representation_imaginary_code_unique_products_associateunitidentityoutput))) /\ ((exists ge_balance_positive_unique_products_associateunitidentityoutputreal ge_balance_negative_unique_products_associateunitidentityoutputreal. (((((ge_representation_real_code_unique_products_associateunitidentityoutput) = 2 * (ge_balance_positive_unique_products_associateunitidentityoutputreal) /\ (ge_balance_negative_unique_products_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_products_associateunitidentityoutputrealdecode. (((ge_representation_real_code_unique_products_associateunitidentityoutput) = 2 * ge_signed_half_unique_products_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_products_associateunitidentityoutputreal) = S ge_signed_half_unique_products_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_products_associateunitidentity) * (ge_second_rp_unique_products_associateunitidentity))) + (((ge_first_rn_unique_products_associateunitidentity) * (ge_second_rn_unique_products_associateunitidentity))))) + (((((ge_first_ip_unique_products_associateunitidentity) * (ge_second_in_unique_products_associateunitidentity))) + (((ge_first_in_unique_products_associateunitidentity) * (ge_second_ip_unique_products_associateunitidentity))))))) + ge_balance_negative_unique_products_associateunitidentityoutputreal = (((((((ge_first_rp_unique_products_associateunitidentity) * (ge_second_rn_unique_products_associateunitidentity))) + (((ge_first_rn_unique_products_associateunitidentity) * (ge_second_rp_unique_products_associateunitidentity))))) + (((((ge_first_ip_unique_products_associateunitidentity) * (ge_second_ip_unique_products_associateunitidentity))) + (((ge_first_in_unique_products_associateunitidentity) * (ge_second_in_unique_products_associateunitidentity))))))) + ge_balance_positive_unique_products_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_products_associateunitidentityoutputimaginary ge_balance_negative_unique_products_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_products_associateunitidentityoutput) = 2 * (ge_balance_positive_unique_products_associateunitidentityoutputimaginary) /\ (ge_balance_negative_unique_products_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_products_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_products_associateunitidentityoutput) = 2 * ge_signed_half_unique_products_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_products_associateunitidentityoutputimaginary) = S ge_signed_half_unique_products_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_products_associateunitidentity) * (ge_second_ip_unique_products_associateunitidentity))) + (((ge_first_rn_unique_products_associateunitidentity) * (ge_second_in_unique_products_associateunitidentity))))) + (((((ge_first_ip_unique_products_associateunitidentity) * (ge_second_rp_unique_products_associateunitidentity))) + (((ge_first_in_unique_products_associateunitidentity) * (ge_second_rn_unique_products_associateunitidentity))))))) + ge_balance_negative_unique_products_associateunitidentityoutputimaginary = (((((((ge_first_rp_unique_products_associateunitidentity) * (ge_second_in_unique_products_associateunitidentity))) + (((ge_first_rn_unique_products_associateunitidentity) * (ge_second_ip_unique_products_associateunitidentity))))) + (((((ge_first_ip_unique_products_associateunitidentity) * (ge_second_rn_unique_products_associateunitidentity))) + (((ge_first_in_unique_products_associateunitidentity) * (ge_second_rp_unique_products_associateunitidentity))))))) + ge_balance_positive_unique_products_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unique_products_associatetransport ge_first_rn_unique_products_associatetransport ge_first_ip_unique_products_associatetransport ge_first_in_unique_products_associatetransport ge_second_rp_unique_products_associatetransport ge_second_rn_unique_products_associatetransport ge_second_ip_unique_products_associatetransport ge_second_in_unique_products_associatetransport. ((exists ge_representation_real_code_unique_products_associatetransportfirst ge_representation_imaginary_code_unique_products_associatetransportfirst. (((gr_unit_unique_products_associate) = ((ge_representation_real_code_unique_products_associatetransportfirst) + (ge_representation_imaginary_code_unique_products_associatetransportfirst)) * S ((ge_representation_real_code_unique_products_associatetransportfirst) + (ge_representation_imaginary_code_unique_products_associatetransportfirst)) + ((ge_representation_imaginary_code_unique_products_associatetransportfirst) + (ge_representation_imaginary_code_unique_products_associatetransportfirst))) /\ ((exists ge_balance_positive_unique_products_associatetransportfirstreal ge_balance_negative_unique_products_associatetransportfirstreal. (((((ge_representation_real_code_unique_products_associatetransportfirst) = 2 * (ge_balance_positive_unique_products_associatetransportfirstreal) /\ (ge_balance_negative_unique_products_associatetransportfirstreal) = 0) \/ exists ge_signed_half_unique_products_associatetransportfirstrealdecode. (((ge_representation_real_code_unique_products_associatetransportfirst) = 2 * ge_signed_half_unique_products_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_unique_products_associatetransportfirstreal) = 0) /\ (ge_balance_negative_unique_products_associatetransportfirstreal) = S ge_signed_half_unique_products_associatetransportfirstrealdecode))) /\ ((ge_first_rp_unique_products_associatetransport) + ge_balance_negative_unique_products_associatetransportfirstreal = (ge_first_rn_unique_products_associatetransport) + ge_balance_positive_unique_products_associatetransportfirstreal))) /\ (exists ge_balance_positive_unique_products_associatetransportfirstimaginary ge_balance_negative_unique_products_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_unique_products_associatetransportfirst) = 2 * (ge_balance_positive_unique_products_associatetransportfirstimaginary) /\ (ge_balance_negative_unique_products_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_unique_products_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_unique_products_associatetransportfirst) = 2 * ge_signed_half_unique_products_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_unique_products_associatetransportfirstimaginary) = S ge_signed_half_unique_products_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_unique_products_associatetransport) + ge_balance_negative_unique_products_associatetransportfirstimaginary = (ge_first_in_unique_products_associatetransport) + ge_balance_positive_unique_products_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_products_associatetransportsecond ge_representation_imaginary_code_unique_products_associatetransportsecond. (((P) = ((ge_representation_real_code_unique_products_associatetransportsecond) + (ge_representation_imaginary_code_unique_products_associatetransportsecond)) * S ((ge_representation_real_code_unique_products_associatetransportsecond) + (ge_representation_imaginary_code_unique_products_associatetransportsecond)) + ((ge_representation_imaginary_code_unique_products_associatetransportsecond) + (ge_representation_imaginary_code_unique_products_associatetransportsecond))) /\ ((exists ge_balance_positive_unique_products_associatetransportsecondreal ge_balance_negative_unique_products_associatetransportsecondreal. (((((ge_representation_real_code_unique_products_associatetransportsecond) = 2 * (ge_balance_positive_unique_products_associatetransportsecondreal) /\ (ge_balance_negative_unique_products_associatetransportsecondreal) = 0) \/ exists ge_signed_half_unique_products_associatetransportsecondrealdecode. (((ge_representation_real_code_unique_products_associatetransportsecond) = 2 * ge_signed_half_unique_products_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_unique_products_associatetransportsecondreal) = 0) /\ (ge_balance_negative_unique_products_associatetransportsecondreal) = S ge_signed_half_unique_products_associatetransportsecondrealdecode))) /\ ((ge_second_rp_unique_products_associatetransport) + ge_balance_negative_unique_products_associatetransportsecondreal = (ge_second_rn_unique_products_associatetransport) + ge_balance_positive_unique_products_associatetransportsecondreal))) /\ (exists ge_balance_positive_unique_products_associatetransportsecondimaginary ge_balance_negative_unique_products_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_unique_products_associatetransportsecond) = 2 * (ge_balance_positive_unique_products_associatetransportsecondimaginary) /\ (ge_balance_negative_unique_products_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_unique_products_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_unique_products_associatetransportsecond) = 2 * ge_signed_half_unique_products_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_unique_products_associatetransportsecondimaginary) = S ge_signed_half_unique_products_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_unique_products_associatetransport) + ge_balance_negative_unique_products_associatetransportsecondimaginary = (ge_second_in_unique_products_associatetransport) + ge_balance_positive_unique_products_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_products_associatetransportoutput ge_representation_imaginary_code_unique_products_associatetransportoutput. (((Q) = ((ge_representation_real_code_unique_products_associatetransportoutput) + (ge_representation_imaginary_code_unique_products_associatetransportoutput)) * S ((ge_representation_real_code_unique_products_associatetransportoutput) + (ge_representation_imaginary_code_unique_products_associatetransportoutput)) + ((ge_representation_imaginary_code_unique_products_associatetransportoutput) + (ge_representation_imaginary_code_unique_products_associatetransportoutput))) /\ ((exists ge_balance_positive_unique_products_associatetransportoutputreal ge_balance_negative_unique_products_associatetransportoutputreal. (((((ge_representation_real_code_unique_products_associatetransportoutput) = 2 * (ge_balance_positive_unique_products_associatetransportoutputreal) /\ (ge_balance_negative_unique_products_associatetransportoutputreal) = 0) \/ exists ge_signed_half_unique_products_associatetransportoutputrealdecode. (((ge_representation_real_code_unique_products_associatetransportoutput) = 2 * ge_signed_half_unique_products_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_unique_products_associatetransportoutputreal) = 0) /\ (ge_balance_negative_unique_products_associatetransportoutputreal) = S ge_signed_half_unique_products_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_unique_products_associatetransport) * (ge_second_rp_unique_products_associatetransport))) + (((ge_first_rn_unique_products_associatetransport) * (ge_second_rn_unique_products_associatetransport))))) + (((((ge_first_ip_unique_products_associatetransport) * (ge_second_in_unique_products_associatetransport))) + (((ge_first_in_unique_products_associatetransport) * (ge_second_ip_unique_products_associatetransport))))))) + ge_balance_negative_unique_products_associatetransportoutputreal = (((((((ge_first_rp_unique_products_associatetransport) * (ge_second_rn_unique_products_associatetransport))) + (((ge_first_rn_unique_products_associatetransport) * (ge_second_rp_unique_products_associatetransport))))) + (((((ge_first_ip_unique_products_associatetransport) * (ge_second_ip_unique_products_associatetransport))) + (((ge_first_in_unique_products_associatetransport) * (ge_second_in_unique_products_associatetransport))))))) + ge_balance_positive_unique_products_associatetransportoutputreal))) /\ (exists ge_balance_positive_unique_products_associatetransportoutputimaginary ge_balance_negative_unique_products_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_unique_products_associatetransportoutput) = 2 * (ge_balance_positive_unique_products_associatetransportoutputimaginary) /\ (ge_balance_negative_unique_products_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_unique_products_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_unique_products_associatetransportoutput) = 2 * ge_signed_half_unique_products_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_unique_products_associatetransportoutputimaginary) = S ge_signed_half_unique_products_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_products_associatetransport) * (ge_second_ip_unique_products_associatetransport))) + (((ge_first_rn_unique_products_associatetransport) * (ge_second_in_unique_products_associatetransport))))) + (((((ge_first_ip_unique_products_associatetransport) * (ge_second_rp_unique_products_associatetransport))) + (((ge_first_in_unique_products_associatetransport) * (ge_second_rn_unique_products_associatetransport))))))) + ge_balance_negative_unique_products_associatetransportoutputimaginary = (((((((ge_first_rp_unique_products_associatetransport) * (ge_second_in_unique_products_associatetransport))) + (((ge_first_rn_unique_products_associatetransport) * (ge_second_ip_unique_products_associatetransport))))) + (((((ge_first_ip_unique_products_associatetransport) * (ge_second_rn_unique_products_associatetransport))) + (((ge_first_in_unique_products_associatetransport) * (ge_second_rp_unique_products_associatetransport))))))) + ge_balance_positive_unique_products_associatetransportoutputimaginary))))))))))) -> ((((l)=(m)) /\ (exists gr_unique_map_product_unique gr_unique_scale_product_unique. (((((forall pfp_i_product_uniquematchingbijectionbounded. (exists pfp_gap_product_uniquematchingbijectionboundedindex. pfp_gap_product_uniquematchingbijectionboundedindex + S (pfp_i_product_uniquematchingbijectionbounded) = (l)) -> exists pfp_a_product_uniquematchingbijectionbounded. (((exists ff_h_pfp_product_uniquematchingbijectionboundedentry. ff_h_pfp_product_uniquematchingbijectionboundedentry + S (pfp_a_product_uniquematchingbijectionbounded) = S ((S (pfp_i_product_uniquematchingbijectionbounded)) * gr_unique_scale_product_unique)) /\ exists ff_q_pfp_product_uniquematchingbijectionboundedentry. gr_unique_map_product_unique = ff_q_pfp_product_uniquematchingbijectionboundedentry * S ((S (pfp_i_product_uniquematchingbijectionbounded)) * gr_unique_scale_product_unique) + (pfp_a_product_uniquematchingbijectionbounded))) /\ (exists pfp_gap_product_uniquematchingbijectionboundedvalue. pfp_gap_product_uniquematchingbijectionboundedvalue + S (pfp_a_product_uniquematchingbijectionbounded) = (l))) /\ (((forall pfp_i_product_uniquematchingbijectioninjective pfp_j_product_uniquematchingbijectioninjective pfp_a_product_uniquematchingbijectioninjective. (exists pfp_gap_product_uniquematchingbijectioninjectivefirst. pfp_gap_product_uniquematchingbijectioninjectivefirst + S (pfp_i_product_uniquematchingbijectioninjective) = (l)) -> (exists pfp_gap_product_uniquematchingbijectioninjectivesecond. pfp_gap_product_uniquematchingbijectioninjectivesecond + S (pfp_j_product_uniquematchingbijectioninjective) = (l)) -> (((exists ff_h_pfp_product_uniquematchingbijectioninjectiveleft. ff_h_pfp_product_uniquematchingbijectioninjectiveleft + S (pfp_a_product_uniquematchingbijectioninjective) = S ((S (pfp_i_product_uniquematchingbijectioninjective)) * gr_unique_scale_product_unique)) /\ exists ff_q_pfp_product_uniquematchingbijectioninjectiveleft. gr_unique_map_product_unique = ff_q_pfp_product_uniquematchingbijectioninjectiveleft * S ((S (pfp_i_product_uniquematchingbijectioninjective)) * gr_unique_scale_product_unique) + (pfp_a_product_uniquematchingbijectioninjective))) -> (((exists ff_h_pfp_product_uniquematchingbijectioninjectiveright. ff_h_pfp_product_uniquematchingbijectioninjectiveright + S (pfp_a_product_uniquematchingbijectioninjective) = S ((S (pfp_j_product_uniquematchingbijectioninjective)) * gr_unique_scale_product_unique)) /\ exists ff_q_pfp_product_uniquematchingbijectioninjectiveright. gr_unique_map_product_unique = ff_q_pfp_product_uniquematchingbijectioninjectiveright * S ((S (pfp_j_product_uniquematchingbijectioninjective)) * gr_unique_scale_product_unique) + (pfp_a_product_uniquematchingbijectioninjective))) -> pfp_i_product_uniquematchingbijectioninjective = pfp_j_product_uniquematchingbijectioninjective) /\ (forall pfp_a_product_uniquematchingbijectionsurjective. (exists pfp_gap_product_uniquematchingbijectionsurjectivevalue. pfp_gap_product_uniquematchingbijectionsurjectivevalue + S (pfp_a_product_uniquematchingbijectionsurjective) = (l)) -> exists pfp_i_product_uniquematchingbijectionsurjective. (exists pfp_gap_product_uniquematchingbijectionsurjectiveindex. pfp_gap_product_uniquematchingbijectionsurjectiveindex + S (pfp_i_product_uniquematchingbijectionsurjective) = (l)) /\ (((exists ff_h_pfp_product_uniquematchingbijectionsurjectiveentry. ff_h_pfp_product_uniquematchingbijectionsurjectiveentry + S (pfp_a_product_uniquematchingbijectionsurjective) = S ((S (pfp_i_product_uniquematchingbijectionsurjective)) * gr_unique_scale_product_unique)) /\ exists ff_q_pfp_product_uniquematchingbijectionsurjectiveentry. gr_unique_map_product_unique = ff_q_pfp_product_uniquematchingbijectionsurjectiveentry * S ((S (pfp_i_product_uniquematchingbijectionsurjective)) * gr_unique_scale_product_unique) + (pfp_a_product_uniquematchingbijectionsurjective)))))))) /\ (forall gr_match_index_product_uniquematchingmatching gr_match_image_product_uniquematchingmatching gr_match_source_product_uniquematchingmatching gr_match_target_product_uniquematchingmatching. (exists ge_gap_product_uniquematchingmatchingindex. ge_gap_product_uniquematchingmatchingindex + S (gr_match_index_product_uniquematchingmatching) = (l)) -> (((exists ff_h_gprod_product_uniquematchingmatchingmap. ff_h_gprod_product_uniquematchingmatchingmap + S (gr_match_image_product_uniquematchingmatching) = S ((S (gr_match_index_product_uniquematchingmatching)) * gr_unique_scale_product_unique)) /\ exists ff_q_gprod_product_uniquematchingmatchingmap. gr_unique_map_product_unique = ff_q_gprod_product_uniquematchingmatchingmap * S ((S (gr_match_index_product_uniquematchingmatching)) * gr_unique_scale_product_unique) + (gr_match_image_product_uniquematchingmatching))) -> (((exists ff_h_gprod_product_uniquematchingmatchingsource. ff_h_gprod_product_uniquematchingmatchingsource + S (gr_match_source_product_uniquematchingmatching) = S ((S (gr_match_index_product_uniquematchingmatching)) * c)) /\ exists ff_q_gprod_product_uniquematchingmatchingsource. b = ff_q_gprod_product_uniquematchingmatchingsource * S ((S (gr_match_index_product_uniquematchingmatching)) * c) + (gr_match_source_product_uniquematchingmatching))) -> (((exists ff_h_gprod_product_uniquematchingmatchingtarget. ff_h_gprod_product_uniquematchingmatchingtarget + S (gr_match_target_product_uniquematchingmatching) = S ((S (gr_match_image_product_uniquematchingmatching)) * e)) /\ exists ff_q_gprod_product_uniquematchingmatchingtarget. d = ff_q_gprod_product_uniquematchingmatchingtarget * S ((S (gr_match_image_product_uniquematchingmatching)) * e) + (gr_match_target_product_uniquematchingmatching))) -> (exists gr_unit_product_uniquematchingmatchingunit_witness. ((exists gr_inverse_product_uniquematchingmatchingunit_witnessunit. (exists ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst. (((gr_unit_product_uniquematchingmatchingunit_witness) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstreal ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond. (((gr_inverse_product_uniquematchingmatchingunit_witnessunit) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondreal ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputreal ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_product_uniquematchingmatchingunit_witnesstransport ge_first_rn_product_uniquematchingmatchingunit_witnesstransport ge_first_ip_product_uniquematchingmatchingunit_witnesstransport ge_first_in_product_uniquematchingmatchingunit_witnesstransport ge_second_rp_product_uniquematchingmatchingunit_witnesstransport ge_second_rn_product_uniquematchingmatchingunit_witnesstransport ge_second_ip_product_uniquematchingmatchingunit_witnesstransport ge_second_in_product_uniquematchingmatchingunit_witnesstransport. ((exists ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst. (((gr_unit_product_uniquematchingmatchingunit_witness) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstreal ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstreal = (ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstimaginary = (ge_first_in_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond. (((gr_match_source_product_uniquematchingmatching) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondreal ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondreal = (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondimaginary = (ge_second_in_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput. (((gr_match_target_product_uniquematchingmatching) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputreal ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rp_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_in_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_in_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_ip_product_uniquematchingmatchingunit_witnesstransport))))))) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rp_product_uniquematchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_ip_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_in_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_in_product_uniquematchingmatchingunit_witnesstransport))))))) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_ip_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_in_product_uniquematchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rp_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_in_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport))))))) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_in_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_ip_product_uniquematchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_in_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rp_product_uniquematchingmatchingunit_witnesstransport))))))) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputimaginary)))))))))))))))))