gaussian_all_irreducible_product_unit_length_zero

Exact expanded first-order arithmetic statement

forall b c l P. (forall gr_factor_index_unit_product_factors gr_factor_value_unit_product_factors. (exists ge_gap_unit_product_factorsindex. ge_gap_unit_product_factorsindex + S (gr_factor_index_unit_product_factors) = (l)) -> (((exists ff_h_gprod_unit_product_factorsentry. ff_h_gprod_unit_product_factorsentry + S (gr_factor_value_unit_product_factors) = S ((S (gr_factor_index_unit_product_factors)) * c)) /\ exists ff_q_gprod_unit_product_factorsentry. b = ff_q_gprod_unit_product_factorsentry * S ((S (gr_factor_index_unit_product_factors)) * c) + (gr_factor_value_unit_product_factors))) -> (((exists ge_real_positive_unit_product_factorsirreduciblecarrier ge_real_negative_unit_product_factorsirreduciblecarrier ge_imaginary_positive_unit_product_factorsirreduciblecarrier ge_imaginary_negative_unit_product_factorsirreduciblecarrier. (exists ge_real_code_unit_product_factorsirreduciblecarrierdecode ge_imaginary_code_unit_product_factorsirreduciblecarrierdecode. (((gr_factor_value_unit_product_factors) = ((ge_real_code_unit_product_factorsirreduciblecarrierdecode) + (ge_imaginary_code_unit_product_factorsirreduciblecarrierdecode)) * S ((ge_real_code_unit_product_factorsirreduciblecarrierdecode) + (ge_imaginary_code_unit_product_factorsirreduciblecarrierdecode)) + ((ge_imaginary_code_unit_product_factorsirreduciblecarrierdecode) + (ge_imaginary_code_unit_product_factorsirreduciblecarrierdecode))) /\ (((((ge_real_code_unit_product_factorsirreduciblecarrierdecode) = 2 * (ge_real_positive_unit_product_factorsirreduciblecarrier) /\ (ge_real_negative_unit_product_factorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unit_product_factorsirreduciblecarrierdecode_real. (((ge_real_code_unit_product_factorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unit_product_factorsirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_unit_product_factorsirreduciblecarrier) = 0) /\ (ge_real_negative_unit_product_factorsirreduciblecarrier) = S ge_signed_half_ge_unit_product_factorsirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_unit_product_factorsirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_unit_product_factorsirreduciblecarrier) /\ (ge_imaginary_negative_unit_product_factorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unit_product_factorsirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_unit_product_factorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unit_product_factorsirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unit_product_factorsirreduciblecarrier) = 0) /\ (ge_imaginary_negative_unit_product_factorsirreduciblecarrier) = S ge_signed_half_ge_unit_product_factorsirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_unit_product_factors)=0)) /\ ((~(exists gr_inverse_unit_product_factorsirreduciblenonunit. (exists ge_first_rp_unit_product_factorsirreduciblenonunitidentity ge_first_rn_unit_product_factorsirreduciblenonunitidentity ge_first_ip_unit_product_factorsirreduciblenonunitidentity ge_first_in_unit_product_factorsirreduciblenonunitidentity ge_second_rp_unit_product_factorsirreduciblenonunitidentity ge_second_rn_unit_product_factorsirreduciblenonunitidentity ge_second_ip_unit_product_factorsirreduciblenonunitidentity ge_second_in_unit_product_factorsirreduciblenonunitidentity. ((exists ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityfirst ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityfirst. (((gr_factor_value_unit_product_factors) = ((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblenonunitidentityfirstreal ge_balance_negative_unit_product_factorsirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unit_product_factorsirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unit_product_factorsirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentityfirstreal) = S ge_signed_half_unit_product_factorsirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_product_factorsirreduciblenonunitidentity) + ge_balance_negative_unit_product_factorsirreduciblenonunitidentityfirstreal = (ge_first_rn_unit_product_factorsirreduciblenonunitidentity) + ge_balance_positive_unit_product_factorsirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblenonunitidentityfirstimaginary ge_balance_negative_unit_product_factorsirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unit_product_factorsirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unit_product_factorsirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_unit_product_factorsirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_factorsirreduciblenonunitidentity) + ge_balance_negative_unit_product_factorsirreduciblenonunitidentityfirstimaginary = (ge_first_in_unit_product_factorsirreduciblenonunitidentity) + ge_balance_positive_unit_product_factorsirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_factorsirreduciblenonunitidentitysecond ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentitysecond. (((gr_inverse_unit_product_factorsirreduciblenonunit) = ((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblenonunitidentitysecondreal ge_balance_negative_unit_product_factorsirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unit_product_factorsirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unit_product_factorsirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentitysecondreal) = S ge_signed_half_unit_product_factorsirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_product_factorsirreduciblenonunitidentity) + ge_balance_negative_unit_product_factorsirreduciblenonunitidentitysecondreal = (ge_second_rn_unit_product_factorsirreduciblenonunitidentity) + ge_balance_positive_unit_product_factorsirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblenonunitidentitysecondimaginary ge_balance_negative_unit_product_factorsirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unit_product_factorsirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unit_product_factorsirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_unit_product_factorsirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_product_factorsirreduciblenonunitidentity) + ge_balance_negative_unit_product_factorsirreduciblenonunitidentitysecondimaginary = (ge_second_in_unit_product_factorsirreduciblenonunitidentity) + ge_balance_positive_unit_product_factorsirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityoutput ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblenonunitidentityoutputreal ge_balance_negative_unit_product_factorsirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unit_product_factorsirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unit_product_factorsirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentityoutputreal) = S ge_signed_half_unit_product_factorsirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_factorsirreduciblenonunitidentity) * (ge_second_rp_unit_product_factorsirreduciblenonunitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblenonunitidentity) * (ge_second_rn_unit_product_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblenonunitidentity) * (ge_second_in_unit_product_factorsirreduciblenonunitidentity))) + (((ge_first_in_unit_product_factorsirreduciblenonunitidentity) * (ge_second_ip_unit_product_factorsirreduciblenonunitidentity))))))) + ge_balance_negative_unit_product_factorsirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_unit_product_factorsirreduciblenonunitidentity) * (ge_second_rn_unit_product_factorsirreduciblenonunitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblenonunitidentity) * (ge_second_rp_unit_product_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblenonunitidentity) * (ge_second_ip_unit_product_factorsirreduciblenonunitidentity))) + (((ge_first_in_unit_product_factorsirreduciblenonunitidentity) * (ge_second_in_unit_product_factorsirreduciblenonunitidentity))))))) + ge_balance_positive_unit_product_factorsirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblenonunitidentityoutputimaginary ge_balance_negative_unit_product_factorsirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unit_product_factorsirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unit_product_factorsirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_unit_product_factorsirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_factorsirreduciblenonunitidentity) * (ge_second_ip_unit_product_factorsirreduciblenonunitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblenonunitidentity) * (ge_second_in_unit_product_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblenonunitidentity) * (ge_second_rp_unit_product_factorsirreduciblenonunitidentity))) + (((ge_first_in_unit_product_factorsirreduciblenonunitidentity) * (ge_second_rn_unit_product_factorsirreduciblenonunitidentity))))))) + ge_balance_negative_unit_product_factorsirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_unit_product_factorsirreduciblenonunitidentity) * (ge_second_in_unit_product_factorsirreduciblenonunitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblenonunitidentity) * (ge_second_ip_unit_product_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblenonunitidentity) * (ge_second_rn_unit_product_factorsirreduciblenonunitidentity))) + (((ge_first_in_unit_product_factorsirreduciblenonunitidentity) * (ge_second_rp_unit_product_factorsirreduciblenonunitidentity))))))) + ge_balance_positive_unit_product_factorsirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unit_product_factorsirreducible gr_second_factor_unit_product_factorsirreducible. (exists ge_first_rp_unit_product_factorsirreduciblefactorization ge_first_rn_unit_product_factorsirreduciblefactorization ge_first_ip_unit_product_factorsirreduciblefactorization ge_first_in_unit_product_factorsirreduciblefactorization ge_second_rp_unit_product_factorsirreduciblefactorization ge_second_rn_unit_product_factorsirreduciblefactorization ge_second_ip_unit_product_factorsirreduciblefactorization ge_second_in_unit_product_factorsirreduciblefactorization. ((exists ge_representation_real_code_unit_product_factorsirreduciblefactorizationfirst ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationfirst. (((gr_first_factor_unit_product_factorsirreducible) = ((ge_representation_real_code_unit_product_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationfirst)) * S ((ge_representation_real_code_unit_product_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblefactorizationfirstreal ge_balance_negative_unit_product_factorsirreduciblefactorizationfirstreal. (((((ge_representation_real_code_unit_product_factorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefactorizationfirstreal) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblefactorizationfirst) = 2 * ge_signed_half_unit_product_factorsirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationfirstreal) = S ge_signed_half_unit_product_factorsirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_unit_product_factorsirreduciblefactorization) + ge_balance_negative_unit_product_factorsirreduciblefactorizationfirstreal = (ge_first_rn_unit_product_factorsirreduciblefactorization) + ge_balance_positive_unit_product_factorsirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblefactorizationfirstimaginary ge_balance_negative_unit_product_factorsirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationfirst) = 2 * ge_signed_half_unit_product_factorsirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationfirstimaginary) = S ge_signed_half_unit_product_factorsirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_factorsirreduciblefactorization) + ge_balance_negative_unit_product_factorsirreduciblefactorizationfirstimaginary = (ge_first_in_unit_product_factorsirreduciblefactorization) + ge_balance_positive_unit_product_factorsirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_factorsirreduciblefactorizationsecond ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationsecond. (((gr_second_factor_unit_product_factorsirreducible) = ((ge_representation_real_code_unit_product_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationsecond)) * S ((ge_representation_real_code_unit_product_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblefactorizationsecondreal ge_balance_negative_unit_product_factorsirreduciblefactorizationsecondreal. (((((ge_representation_real_code_unit_product_factorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefactorizationsecondreal) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblefactorizationsecond) = 2 * ge_signed_half_unit_product_factorsirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationsecondreal) = S ge_signed_half_unit_product_factorsirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_unit_product_factorsirreduciblefactorization) + ge_balance_negative_unit_product_factorsirreduciblefactorizationsecondreal = (ge_second_rn_unit_product_factorsirreduciblefactorization) + ge_balance_positive_unit_product_factorsirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblefactorizationsecondimaginary ge_balance_negative_unit_product_factorsirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationsecond) = 2 * ge_signed_half_unit_product_factorsirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationsecondimaginary) = S ge_signed_half_unit_product_factorsirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_unit_product_factorsirreduciblefactorization) + ge_balance_negative_unit_product_factorsirreduciblefactorizationsecondimaginary = (ge_second_in_unit_product_factorsirreduciblefactorization) + ge_balance_positive_unit_product_factorsirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_factorsirreduciblefactorizationoutput ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationoutput. (((gr_factor_value_unit_product_factors) = ((ge_representation_real_code_unit_product_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationoutput)) * S ((ge_representation_real_code_unit_product_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblefactorizationoutputreal ge_balance_negative_unit_product_factorsirreduciblefactorizationoutputreal. (((((ge_representation_real_code_unit_product_factorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefactorizationoutputreal) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblefactorizationoutput) = 2 * ge_signed_half_unit_product_factorsirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationoutputreal) = S ge_signed_half_unit_product_factorsirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_factorsirreduciblefactorization) * (ge_second_rp_unit_product_factorsirreduciblefactorization))) + (((ge_first_rn_unit_product_factorsirreduciblefactorization) * (ge_second_rn_unit_product_factorsirreduciblefactorization))))) + (((((ge_first_ip_unit_product_factorsirreduciblefactorization) * (ge_second_in_unit_product_factorsirreduciblefactorization))) + (((ge_first_in_unit_product_factorsirreduciblefactorization) * (ge_second_ip_unit_product_factorsirreduciblefactorization))))))) + ge_balance_negative_unit_product_factorsirreduciblefactorizationoutputreal = (((((((ge_first_rp_unit_product_factorsirreduciblefactorization) * (ge_second_rn_unit_product_factorsirreduciblefactorization))) + (((ge_first_rn_unit_product_factorsirreduciblefactorization) * (ge_second_rp_unit_product_factorsirreduciblefactorization))))) + (((((ge_first_ip_unit_product_factorsirreduciblefactorization) * (ge_second_ip_unit_product_factorsirreduciblefactorization))) + (((ge_first_in_unit_product_factorsirreduciblefactorization) * (ge_second_in_unit_product_factorsirreduciblefactorization))))))) + ge_balance_positive_unit_product_factorsirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblefactorizationoutputimaginary ge_balance_negative_unit_product_factorsirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblefactorizationoutput) = 2 * ge_signed_half_unit_product_factorsirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefactorizationoutputimaginary) = S ge_signed_half_unit_product_factorsirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_factorsirreduciblefactorization) * (ge_second_ip_unit_product_factorsirreduciblefactorization))) + (((ge_first_rn_unit_product_factorsirreduciblefactorization) * (ge_second_in_unit_product_factorsirreduciblefactorization))))) + (((((ge_first_ip_unit_product_factorsirreduciblefactorization) * (ge_second_rp_unit_product_factorsirreduciblefactorization))) + (((ge_first_in_unit_product_factorsirreduciblefactorization) * (ge_second_rn_unit_product_factorsirreduciblefactorization))))))) + ge_balance_negative_unit_product_factorsirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_unit_product_factorsirreduciblefactorization) * (ge_second_in_unit_product_factorsirreduciblefactorization))) + (((ge_first_rn_unit_product_factorsirreduciblefactorization) * (ge_second_ip_unit_product_factorsirreduciblefactorization))))) + (((((ge_first_ip_unit_product_factorsirreduciblefactorization) * (ge_second_rn_unit_product_factorsirreduciblefactorization))) + (((ge_first_in_unit_product_factorsirreduciblefactorization) * (ge_second_rp_unit_product_factorsirreduciblefactorization))))))) + ge_balance_positive_unit_product_factorsirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_unit_product_factorsirreduciblefirst_unit. (exists ge_first_rp_unit_product_factorsirreduciblefirst_unitidentity ge_first_rn_unit_product_factorsirreduciblefirst_unitidentity ge_first_ip_unit_product_factorsirreduciblefirst_unitidentity ge_first_in_unit_product_factorsirreduciblefirst_unitidentity ge_second_rp_unit_product_factorsirreduciblefirst_unitidentity ge_second_rn_unit_product_factorsirreduciblefirst_unitidentity ge_second_ip_unit_product_factorsirreduciblefirst_unitidentity ge_second_in_unit_product_factorsirreduciblefirst_unitidentity. ((exists ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityfirst. (((gr_first_factor_unit_product_factorsirreducible) = ((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityfirstreal ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_product_factorsirreduciblefirst_unitidentity) + ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityfirstreal = (ge_first_rn_unit_product_factorsirreduciblefirst_unitidentity) + ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_factorsirreduciblefirst_unitidentity) + ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_unit_product_factorsirreduciblefirst_unitidentity) + ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentitysecond. (((gr_inverse_unit_product_factorsirreduciblefirst_unit) = ((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentitysecondreal ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unit_product_factorsirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_unit_product_factorsirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_product_factorsirreduciblefirst_unitidentity) + ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentitysecondreal = (ge_second_rn_unit_product_factorsirreduciblefirst_unitidentity) + ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unit_product_factorsirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_unit_product_factorsirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_product_factorsirreduciblefirst_unitidentity) + ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_unit_product_factorsirreduciblefirst_unitidentity) + ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityoutputreal ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_rp_unit_product_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_rn_unit_product_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_in_unit_product_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_ip_unit_product_factorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_rn_unit_product_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_rp_unit_product_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_ip_unit_product_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_in_unit_product_factorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_unit_product_factorsirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_ip_unit_product_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_in_unit_product_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_rp_unit_product_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_rn_unit_product_factorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_unit_product_factorsirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_in_unit_product_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_ip_unit_product_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_rn_unit_product_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_unit_product_factorsirreduciblefirst_unitidentity) * (ge_second_rp_unit_product_factorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_unit_product_factorsirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_unit_product_factorsirreduciblesecond_unit. (exists ge_first_rp_unit_product_factorsirreduciblesecond_unitidentity ge_first_rn_unit_product_factorsirreduciblesecond_unitidentity ge_first_ip_unit_product_factorsirreduciblesecond_unitidentity ge_first_in_unit_product_factorsirreduciblesecond_unitidentity ge_second_rp_unit_product_factorsirreduciblesecond_unitidentity ge_second_rn_unit_product_factorsirreduciblesecond_unitidentity ge_second_ip_unit_product_factorsirreduciblesecond_unitidentity ge_second_in_unit_product_factorsirreduciblesecond_unitidentity. ((exists ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityfirst. (((gr_second_factor_unit_product_factorsirreducible) = ((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityfirstreal ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_product_factorsirreduciblesecond_unitidentity) + ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityfirstreal = (ge_first_rn_unit_product_factorsirreduciblesecond_unitidentity) + ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_factorsirreduciblesecond_unitidentity) + ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_unit_product_factorsirreduciblesecond_unitidentity) + ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentitysecond. (((gr_inverse_unit_product_factorsirreduciblesecond_unit) = ((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentitysecondreal ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unit_product_factorsirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_unit_product_factorsirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_product_factorsirreduciblesecond_unitidentity) + ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentitysecondreal = (ge_second_rn_unit_product_factorsirreduciblesecond_unitidentity) + ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unit_product_factorsirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_unit_product_factorsirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_product_factorsirreduciblesecond_unitidentity) + ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_unit_product_factorsirreduciblesecond_unitidentity) + ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityoutputreal ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_unit_product_factorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_rp_unit_product_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_rn_unit_product_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_in_unit_product_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_ip_unit_product_factorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_rn_unit_product_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_rp_unit_product_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_ip_unit_product_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_in_unit_product_factorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_factorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_unit_product_factorsirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_ip_unit_product_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_in_unit_product_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_rp_unit_product_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_rn_unit_product_factorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_unit_product_factorsirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_in_unit_product_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_ip_unit_product_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_rn_unit_product_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_unit_product_factorsirreduciblesecond_unitidentity) * (ge_second_rp_unit_product_factorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_unit_product_factorsirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (exists gr_product_trace_unit_product_trace gr_product_scale_unit_product_trace. ((((exists ff_h_gprod_unit_product_tracestart. ff_h_gprod_unit_product_tracestart + S (6) = S ((S (0)) * gr_product_scale_unit_product_trace)) /\ exists ff_q_gprod_unit_product_tracestart. gr_product_trace_unit_product_trace = ff_q_gprod_unit_product_tracestart * S ((S (0)) * gr_product_scale_unit_product_trace) + (6))) /\ ((((exists ff_h_gprod_unit_product_traceend. ff_h_gprod_unit_product_traceend + S (P) = S ((S (l)) * gr_product_scale_unit_product_trace)) /\ exists ff_q_gprod_unit_product_traceend. gr_product_trace_unit_product_trace = ff_q_gprod_unit_product_traceend * S ((S (l)) * gr_product_scale_unit_product_trace) + (P))) /\ (forall gr_product_index_unit_product_tracesteps. (exists ge_gap_unit_product_tracestepsindex_bound. ge_gap_unit_product_tracestepsindex_bound + S (gr_product_index_unit_product_tracesteps) = (l)) -> exists gr_product_factor_unit_product_tracesteps gr_product_before_unit_product_tracesteps gr_product_after_unit_product_tracesteps. ((((exists ff_h_gprod_unit_product_tracestepsfactor. ff_h_gprod_unit_product_tracestepsfactor + S (gr_product_factor_unit_product_tracesteps) = S ((S (gr_product_index_unit_product_tracesteps)) * c)) /\ exists ff_q_gprod_unit_product_tracestepsfactor. b = ff_q_gprod_unit_product_tracestepsfactor * S ((S (gr_product_index_unit_product_tracesteps)) * c) + (gr_product_factor_unit_product_tracesteps))) /\ ((((exists ff_h_gprod_unit_product_tracestepsbefore. ff_h_gprod_unit_product_tracestepsbefore + S (gr_product_before_unit_product_tracesteps) = S ((S (gr_product_index_unit_product_tracesteps)) * gr_product_scale_unit_product_trace)) /\ exists ff_q_gprod_unit_product_tracestepsbefore. gr_product_trace_unit_product_trace = ff_q_gprod_unit_product_tracestepsbefore * S ((S (gr_product_index_unit_product_tracesteps)) * gr_product_scale_unit_product_trace) + (gr_product_before_unit_product_tracesteps))) /\ ((((exists ff_h_gprod_unit_product_tracestepsafter. ff_h_gprod_unit_product_tracestepsafter + S (gr_product_after_unit_product_tracesteps) = S ((S (S (gr_product_index_unit_product_tracesteps))) * gr_product_scale_unit_product_trace)) /\ exists ff_q_gprod_unit_product_tracestepsafter. gr_product_trace_unit_product_trace = ff_q_gprod_unit_product_tracestepsafter * S ((S (S (gr_product_index_unit_product_tracesteps))) * gr_product_scale_unit_product_trace) + (gr_product_after_unit_product_tracesteps))) /\ (exists ge_first_rp_unit_product_tracestepsmultiply ge_first_rn_unit_product_tracestepsmultiply ge_first_ip_unit_product_tracestepsmultiply ge_first_in_unit_product_tracestepsmultiply ge_second_rp_unit_product_tracestepsmultiply ge_second_rn_unit_product_tracestepsmultiply ge_second_ip_unit_product_tracestepsmultiply ge_second_in_unit_product_tracestepsmultiply. ((exists ge_representation_real_code_unit_product_tracestepsmultiplyfirst ge_representation_imaginary_code_unit_product_tracestepsmultiplyfirst. (((gr_product_before_unit_product_tracesteps) = ((ge_representation_real_code_unit_product_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplyfirst)) * S ((ge_representation_real_code_unit_product_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_unit_product_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_unit_product_tracestepsmultiplyfirstreal ge_balance_negative_unit_product_tracestepsmultiplyfirstreal. (((((ge_representation_real_code_unit_product_tracestepsmultiplyfirst) = 2 * (ge_balance_positive_unit_product_tracestepsmultiplyfirstreal) /\ (ge_balance_negative_unit_product_tracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unit_product_tracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_unit_product_tracestepsmultiplyfirst) = 2 * ge_signed_half_unit_product_tracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_tracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unit_product_tracestepsmultiplyfirstreal) = S ge_signed_half_unit_product_tracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unit_product_tracestepsmultiply) + ge_balance_negative_unit_product_tracestepsmultiplyfirstreal = (ge_first_rn_unit_product_tracestepsmultiply) + ge_balance_positive_unit_product_tracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unit_product_tracestepsmultiplyfirstimaginary ge_balance_negative_unit_product_tracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unit_product_tracestepsmultiplyfirst) = 2 * (ge_balance_positive_unit_product_tracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_unit_product_tracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_tracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_tracestepsmultiplyfirst) = 2 * ge_signed_half_unit_product_tracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_tracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_tracestepsmultiplyfirstimaginary) = S ge_signed_half_unit_product_tracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_tracestepsmultiply) + ge_balance_negative_unit_product_tracestepsmultiplyfirstimaginary = (ge_first_in_unit_product_tracestepsmultiply) + ge_balance_positive_unit_product_tracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_tracestepsmultiplysecond ge_representation_imaginary_code_unit_product_tracestepsmultiplysecond. (((gr_product_factor_unit_product_tracesteps) = ((ge_representation_real_code_unit_product_tracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplysecond)) * S ((ge_representation_real_code_unit_product_tracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplysecond)) + ((ge_representation_imaginary_code_unit_product_tracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplysecond))) /\ ((exists ge_balance_positive_unit_product_tracestepsmultiplysecondreal ge_balance_negative_unit_product_tracestepsmultiplysecondreal. (((((ge_representation_real_code_unit_product_tracestepsmultiplysecond) = 2 * (ge_balance_positive_unit_product_tracestepsmultiplysecondreal) /\ (ge_balance_negative_unit_product_tracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unit_product_tracestepsmultiplysecondrealdecode. (((ge_representation_real_code_unit_product_tracestepsmultiplysecond) = 2 * ge_signed_half_unit_product_tracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unit_product_tracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unit_product_tracestepsmultiplysecondreal) = S ge_signed_half_unit_product_tracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unit_product_tracestepsmultiply) + ge_balance_negative_unit_product_tracestepsmultiplysecondreal = (ge_second_rn_unit_product_tracestepsmultiply) + ge_balance_positive_unit_product_tracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_unit_product_tracestepsmultiplysecondimaginary ge_balance_negative_unit_product_tracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unit_product_tracestepsmultiplysecond) = 2 * (ge_balance_positive_unit_product_tracestepsmultiplysecondimaginary) /\ (ge_balance_negative_unit_product_tracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unit_product_tracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_tracestepsmultiplysecond) = 2 * ge_signed_half_unit_product_tracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_tracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unit_product_tracestepsmultiplysecondimaginary) = S ge_signed_half_unit_product_tracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unit_product_tracestepsmultiply) + ge_balance_negative_unit_product_tracestepsmultiplysecondimaginary = (ge_second_in_unit_product_tracestepsmultiply) + ge_balance_positive_unit_product_tracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_tracestepsmultiplyoutput ge_representation_imaginary_code_unit_product_tracestepsmultiplyoutput. (((gr_product_after_unit_product_tracesteps) = ((ge_representation_real_code_unit_product_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplyoutput)) * S ((ge_representation_real_code_unit_product_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_unit_product_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_product_tracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_unit_product_tracestepsmultiplyoutputreal ge_balance_negative_unit_product_tracestepsmultiplyoutputreal. (((((ge_representation_real_code_unit_product_tracestepsmultiplyoutput) = 2 * (ge_balance_positive_unit_product_tracestepsmultiplyoutputreal) /\ (ge_balance_negative_unit_product_tracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unit_product_tracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_unit_product_tracestepsmultiplyoutput) = 2 * ge_signed_half_unit_product_tracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_tracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unit_product_tracestepsmultiplyoutputreal) = S ge_signed_half_unit_product_tracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_tracestepsmultiply) * (ge_second_rp_unit_product_tracestepsmultiply))) + (((ge_first_rn_unit_product_tracestepsmultiply) * (ge_second_rn_unit_product_tracestepsmultiply))))) + (((((ge_first_ip_unit_product_tracestepsmultiply) * (ge_second_in_unit_product_tracestepsmultiply))) + (((ge_first_in_unit_product_tracestepsmultiply) * (ge_second_ip_unit_product_tracestepsmultiply))))))) + ge_balance_negative_unit_product_tracestepsmultiplyoutputreal = (((((((ge_first_rp_unit_product_tracestepsmultiply) * (ge_second_rn_unit_product_tracestepsmultiply))) + (((ge_first_rn_unit_product_tracestepsmultiply) * (ge_second_rp_unit_product_tracestepsmultiply))))) + (((((ge_first_ip_unit_product_tracestepsmultiply) * (ge_second_ip_unit_product_tracestepsmultiply))) + (((ge_first_in_unit_product_tracestepsmultiply) * (ge_second_in_unit_product_tracestepsmultiply))))))) + ge_balance_positive_unit_product_tracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unit_product_tracestepsmultiplyoutputimaginary ge_balance_negative_unit_product_tracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unit_product_tracestepsmultiplyoutput) = 2 * (ge_balance_positive_unit_product_tracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_unit_product_tracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_tracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_tracestepsmultiplyoutput) = 2 * ge_signed_half_unit_product_tracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_tracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_tracestepsmultiplyoutputimaginary) = S ge_signed_half_unit_product_tracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_tracestepsmultiply) * (ge_second_ip_unit_product_tracestepsmultiply))) + (((ge_first_rn_unit_product_tracestepsmultiply) * (ge_second_in_unit_product_tracestepsmultiply))))) + (((((ge_first_ip_unit_product_tracestepsmultiply) * (ge_second_rp_unit_product_tracestepsmultiply))) + (((ge_first_in_unit_product_tracestepsmultiply) * (ge_second_rn_unit_product_tracestepsmultiply))))))) + ge_balance_negative_unit_product_tracestepsmultiplyoutputimaginary = (((((((ge_first_rp_unit_product_tracestepsmultiply) * (ge_second_in_unit_product_tracestepsmultiply))) + (((ge_first_rn_unit_product_tracestepsmultiply) * (ge_second_ip_unit_product_tracestepsmultiply))))) + (((((ge_first_ip_unit_product_tracestepsmultiply) * (ge_second_rn_unit_product_tracestepsmultiply))) + (((ge_first_in_unit_product_tracestepsmultiply) * (ge_second_rp_unit_product_tracestepsmultiply))))))) + ge_balance_positive_unit_product_tracestepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_inverse_unit_product_unit. (exists ge_first_rp_unit_product_unitidentity ge_first_rn_unit_product_unitidentity ge_first_ip_unit_product_unitidentity ge_first_in_unit_product_unitidentity ge_second_rp_unit_product_unitidentity ge_second_rn_unit_product_unitidentity ge_second_ip_unit_product_unitidentity ge_second_in_unit_product_unitidentity. ((exists ge_representation_real_code_unit_product_unitidentityfirst ge_representation_imaginary_code_unit_product_unitidentityfirst. (((P) = ((ge_representation_real_code_unit_product_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_unitidentityfirst)) * S ((ge_representation_real_code_unit_product_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_unitidentityfirst)) + ((ge_representation_imaginary_code_unit_product_unitidentityfirst) + (ge_representation_imaginary_code_unit_product_unitidentityfirst))) /\ ((exists ge_balance_positive_unit_product_unitidentityfirstreal ge_balance_negative_unit_product_unitidentityfirstreal. (((((ge_representation_real_code_unit_product_unitidentityfirst) = 2 * (ge_balance_positive_unit_product_unitidentityfirstreal) /\ (ge_balance_negative_unit_product_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_product_unitidentityfirstrealdecode. (((ge_representation_real_code_unit_product_unitidentityfirst) = 2 * ge_signed_half_unit_product_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_product_unitidentityfirstreal) = S ge_signed_half_unit_product_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_product_unitidentity) + ge_balance_negative_unit_product_unitidentityfirstreal = (ge_first_rn_unit_product_unitidentity) + ge_balance_positive_unit_product_unitidentityfirstreal))) /\ (exists ge_balance_positive_unit_product_unitidentityfirstimaginary ge_balance_negative_unit_product_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_product_unitidentityfirst) = 2 * (ge_balance_positive_unit_product_unitidentityfirstimaginary) /\ (ge_balance_negative_unit_product_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_unitidentityfirst) = 2 * ge_signed_half_unit_product_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_unitidentityfirstimaginary) = S ge_signed_half_unit_product_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_unitidentity) + ge_balance_negative_unit_product_unitidentityfirstimaginary = (ge_first_in_unit_product_unitidentity) + ge_balance_positive_unit_product_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_unitidentitysecond ge_representation_imaginary_code_unit_product_unitidentitysecond. (((gr_inverse_unit_product_unit) = ((ge_representation_real_code_unit_product_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_unitidentitysecond)) * S ((ge_representation_real_code_unit_product_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_unitidentitysecond)) + ((ge_representation_imaginary_code_unit_product_unitidentitysecond) + (ge_representation_imaginary_code_unit_product_unitidentitysecond))) /\ ((exists ge_balance_positive_unit_product_unitidentitysecondreal ge_balance_negative_unit_product_unitidentitysecondreal. (((((ge_representation_real_code_unit_product_unitidentitysecond) = 2 * (ge_balance_positive_unit_product_unitidentitysecondreal) /\ (ge_balance_negative_unit_product_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_product_unitidentitysecondrealdecode. (((ge_representation_real_code_unit_product_unitidentitysecond) = 2 * ge_signed_half_unit_product_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_product_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_product_unitidentitysecondreal) = S ge_signed_half_unit_product_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_product_unitidentity) + ge_balance_negative_unit_product_unitidentitysecondreal = (ge_second_rn_unit_product_unitidentity) + ge_balance_positive_unit_product_unitidentitysecondreal))) /\ (exists ge_balance_positive_unit_product_unitidentitysecondimaginary ge_balance_negative_unit_product_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_product_unitidentitysecond) = 2 * (ge_balance_positive_unit_product_unitidentitysecondimaginary) /\ (ge_balance_negative_unit_product_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_product_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_unitidentitysecond) = 2 * ge_signed_half_unit_product_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_product_unitidentitysecondimaginary) = S ge_signed_half_unit_product_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_product_unitidentity) + ge_balance_negative_unit_product_unitidentitysecondimaginary = (ge_second_in_unit_product_unitidentity) + ge_balance_positive_unit_product_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_unitidentityoutput ge_representation_imaginary_code_unit_product_unitidentityoutput. (((6) = ((ge_representation_real_code_unit_product_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_unitidentityoutput)) * S ((ge_representation_real_code_unit_product_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_unitidentityoutput)) + ((ge_representation_imaginary_code_unit_product_unitidentityoutput) + (ge_representation_imaginary_code_unit_product_unitidentityoutput))) /\ ((exists ge_balance_positive_unit_product_unitidentityoutputreal ge_balance_negative_unit_product_unitidentityoutputreal. (((((ge_representation_real_code_unit_product_unitidentityoutput) = 2 * (ge_balance_positive_unit_product_unitidentityoutputreal) /\ (ge_balance_negative_unit_product_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_product_unitidentityoutputrealdecode. (((ge_representation_real_code_unit_product_unitidentityoutput) = 2 * ge_signed_half_unit_product_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_product_unitidentityoutputreal) = S ge_signed_half_unit_product_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_unitidentity) * (ge_second_rp_unit_product_unitidentity))) + (((ge_first_rn_unit_product_unitidentity) * (ge_second_rn_unit_product_unitidentity))))) + (((((ge_first_ip_unit_product_unitidentity) * (ge_second_in_unit_product_unitidentity))) + (((ge_first_in_unit_product_unitidentity) * (ge_second_ip_unit_product_unitidentity))))))) + ge_balance_negative_unit_product_unitidentityoutputreal = (((((((ge_first_rp_unit_product_unitidentity) * (ge_second_rn_unit_product_unitidentity))) + (((ge_first_rn_unit_product_unitidentity) * (ge_second_rp_unit_product_unitidentity))))) + (((((ge_first_ip_unit_product_unitidentity) * (ge_second_ip_unit_product_unitidentity))) + (((ge_first_in_unit_product_unitidentity) * (ge_second_in_unit_product_unitidentity))))))) + ge_balance_positive_unit_product_unitidentityoutputreal))) /\ (exists ge_balance_positive_unit_product_unitidentityoutputimaginary ge_balance_negative_unit_product_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_product_unitidentityoutput) = 2 * (ge_balance_positive_unit_product_unitidentityoutputimaginary) /\ (ge_balance_negative_unit_product_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_unitidentityoutput) = 2 * ge_signed_half_unit_product_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_unitidentityoutputimaginary) = S ge_signed_half_unit_product_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_unitidentity) * (ge_second_ip_unit_product_unitidentity))) + (((ge_first_rn_unit_product_unitidentity) * (ge_second_in_unit_product_unitidentity))))) + (((((ge_first_ip_unit_product_unitidentity) * (ge_second_rp_unit_product_unitidentity))) + (((ge_first_in_unit_product_unitidentity) * (ge_second_rn_unit_product_unitidentity))))))) + ge_balance_negative_unit_product_unitidentityoutputimaginary = (((((((ge_first_rp_unit_product_unitidentity) * (ge_second_in_unit_product_unitidentity))) + (((ge_first_rn_unit_product_unitidentity) * (ge_second_ip_unit_product_unitidentity))))) + (((((ge_first_ip_unit_product_unitidentity) * (ge_second_rn_unit_product_unitidentity))) + (((ge_first_in_unit_product_unitidentity) * (ge_second_rp_unit_product_unitidentity))))))) + ge_balance_positive_unit_product_unitidentityoutputimaginary)))))))))) -> l=0