gaussian_all_irreducible_product_exists

Exact expanded first-order arithmetic statement

forall l b c. (forall gr_factor_index_all_irreducible_product_input gr_factor_value_all_irreducible_product_input. (exists ge_gap_all_irreducible_product_inputindex. ge_gap_all_irreducible_product_inputindex + S (gr_factor_index_all_irreducible_product_input) = (l)) -> (((exists ff_h_gprod_all_irreducible_product_inputentry. ff_h_gprod_all_irreducible_product_inputentry + S (gr_factor_value_all_irreducible_product_input) = S ((S (gr_factor_index_all_irreducible_product_input)) * c)) /\ exists ff_q_gprod_all_irreducible_product_inputentry. b = ff_q_gprod_all_irreducible_product_inputentry * S ((S (gr_factor_index_all_irreducible_product_input)) * c) + (gr_factor_value_all_irreducible_product_input))) -> (((exists ge_real_positive_all_irreducible_product_inputirreduciblecarrier ge_real_negative_all_irreducible_product_inputirreduciblecarrier ge_imaginary_positive_all_irreducible_product_inputirreduciblecarrier ge_imaginary_negative_all_irreducible_product_inputirreduciblecarrier. (exists ge_real_code_all_irreducible_product_inputirreduciblecarrierdecode ge_imaginary_code_all_irreducible_product_inputirreduciblecarrierdecode. (((gr_factor_value_all_irreducible_product_input) = ((ge_real_code_all_irreducible_product_inputirreduciblecarrierdecode) + (ge_imaginary_code_all_irreducible_product_inputirreduciblecarrierdecode)) * S ((ge_real_code_all_irreducible_product_inputirreduciblecarrierdecode) + (ge_imaginary_code_all_irreducible_product_inputirreduciblecarrierdecode)) + ((ge_imaginary_code_all_irreducible_product_inputirreduciblecarrierdecode) + (ge_imaginary_code_all_irreducible_product_inputirreduciblecarrierdecode))) /\ (((((ge_real_code_all_irreducible_product_inputirreduciblecarrierdecode) = 2 * (ge_real_positive_all_irreducible_product_inputirreduciblecarrier) /\ (ge_real_negative_all_irreducible_product_inputirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_all_irreducible_product_inputirreduciblecarrierdecode_real. (((ge_real_code_all_irreducible_product_inputirreduciblecarrierdecode) = 2 * ge_signed_half_ge_all_irreducible_product_inputirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_all_irreducible_product_inputirreduciblecarrier) = 0) /\ (ge_real_negative_all_irreducible_product_inputirreduciblecarrier) = S ge_signed_half_ge_all_irreducible_product_inputirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_all_irreducible_product_inputirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_all_irreducible_product_inputirreduciblecarrier) /\ (ge_imaginary_negative_all_irreducible_product_inputirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_all_irreducible_product_inputirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_all_irreducible_product_inputirreduciblecarrierdecode) = 2 * ge_signed_half_ge_all_irreducible_product_inputirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_all_irreducible_product_inputirreduciblecarrier) = 0) /\ (ge_imaginary_negative_all_irreducible_product_inputirreduciblecarrier) = S ge_signed_half_ge_all_irreducible_product_inputirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_all_irreducible_product_input)=0)) /\ ((~(exists gr_inverse_all_irreducible_product_inputirreduciblenonunit. (exists ge_first_rp_all_irreducible_product_inputirreduciblenonunitidentity ge_first_rn_all_irreducible_product_inputirreduciblenonunitidentity ge_first_ip_all_irreducible_product_inputirreduciblenonunitidentity ge_first_in_all_irreducible_product_inputirreduciblenonunitidentity ge_second_rp_all_irreducible_product_inputirreduciblenonunitidentity ge_second_rn_all_irreducible_product_inputirreduciblenonunitidentity ge_second_ip_all_irreducible_product_inputirreduciblenonunitidentity ge_second_in_all_irreducible_product_inputirreduciblenonunitidentity. ((exists ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityfirst ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityfirst. (((gr_factor_value_all_irreducible_product_input) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityfirstreal ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityfirst) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityfirstreal) = S ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_all_irreducible_product_inputirreduciblenonunitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityfirstreal = (ge_first_rn_all_irreducible_product_inputirreduciblenonunitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginary ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityfirst) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_all_irreducible_product_inputirreduciblenonunitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginary = (ge_first_in_all_irreducible_product_inputirreduciblenonunitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentitysecond ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentitysecond. (((gr_inverse_all_irreducible_product_inputirreduciblenonunit) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentitysecondreal ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentitysecond) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentitysecondreal) = S ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_all_irreducible_product_inputirreduciblenonunitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentitysecondreal = (ge_second_rn_all_irreducible_product_inputirreduciblenonunitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginary ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentitysecond) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_all_irreducible_product_inputirreduciblenonunitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginary = (ge_second_in_all_irreducible_product_inputirreduciblenonunitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityoutput ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityoutputreal ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblenonunitidentityoutput) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityoutputreal) = S ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblenonunitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblenonunitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblenonunitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblenonunitidentity))))))) + ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblenonunitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblenonunitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblenonunitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblenonunitidentity))))))) + ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginary ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblenonunitidentityoutput) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblenonunitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblenonunitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblenonunitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblenonunitidentity))))))) + ge_balance_negative_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblenonunitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblenonunitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblenonunitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblenonunitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblenonunitidentity))))))) + ge_balance_positive_all_irreducible_product_inputirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_all_irreducible_product_inputirreducible gr_second_factor_all_irreducible_product_inputirreducible. (exists ge_first_rp_all_irreducible_product_inputirreduciblefactorization ge_first_rn_all_irreducible_product_inputirreduciblefactorization ge_first_ip_all_irreducible_product_inputirreduciblefactorization ge_first_in_all_irreducible_product_inputirreduciblefactorization ge_second_rp_all_irreducible_product_inputirreduciblefactorization ge_second_rn_all_irreducible_product_inputirreduciblefactorization ge_second_ip_all_irreducible_product_inputirreduciblefactorization ge_second_in_all_irreducible_product_inputirreduciblefactorization. ((exists ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationfirst ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationfirst. (((gr_first_factor_all_irreducible_product_inputirreducible) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationfirst)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationfirstreal ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationfirstreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationfirst) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationfirstreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationfirst) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationfirstreal) = S ge_signed_half_all_irreducible_product_inputirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_all_irreducible_product_inputirreduciblefactorization) + ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationfirstreal = (ge_first_rn_all_irreducible_product_inputirreduciblefactorization) + ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationfirstimaginary ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationfirst) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationfirst) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationfirstimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_all_irreducible_product_inputirreduciblefactorization) + ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationfirstimaginary = (ge_first_in_all_irreducible_product_inputirreduciblefactorization) + ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationsecond ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationsecond. (((gr_second_factor_all_irreducible_product_inputirreducible) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationsecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationsecond)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationsecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationsecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationsecondreal ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationsecondreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationsecond) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationsecondreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationsecond) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationsecondreal) = S ge_signed_half_all_irreducible_product_inputirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_all_irreducible_product_inputirreduciblefactorization) + ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationsecondreal = (ge_second_rn_all_irreducible_product_inputirreduciblefactorization) + ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationsecondimaginary ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationsecond) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationsecond) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationsecondimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_all_irreducible_product_inputirreduciblefactorization) + ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationsecondimaginary = (ge_second_in_all_irreducible_product_inputirreduciblefactorization) + ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationoutput ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationoutput. (((gr_factor_value_all_irreducible_product_input) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationoutput)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationoutputreal ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationoutputreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationoutput) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationoutputreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblefactorizationoutput) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationoutputreal) = S ge_signed_half_all_irreducible_product_inputirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_all_irreducible_product_inputirreduciblefactorization) * (ge_second_rp_all_irreducible_product_inputirreduciblefactorization))) + (((ge_first_rn_all_irreducible_product_inputirreduciblefactorization) * (ge_second_rn_all_irreducible_product_inputirreduciblefactorization))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblefactorization) * (ge_second_in_all_irreducible_product_inputirreduciblefactorization))) + (((ge_first_in_all_irreducible_product_inputirreduciblefactorization) * (ge_second_ip_all_irreducible_product_inputirreduciblefactorization))))))) + ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationoutputreal = (((((((ge_first_rp_all_irreducible_product_inputirreduciblefactorization) * (ge_second_rn_all_irreducible_product_inputirreduciblefactorization))) + (((ge_first_rn_all_irreducible_product_inputirreduciblefactorization) * (ge_second_rp_all_irreducible_product_inputirreduciblefactorization))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblefactorization) * (ge_second_ip_all_irreducible_product_inputirreduciblefactorization))) + (((ge_first_in_all_irreducible_product_inputirreduciblefactorization) * (ge_second_in_all_irreducible_product_inputirreduciblefactorization))))))) + ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationoutputimaginary ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationoutput) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefactorizationoutput) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationoutputimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_all_irreducible_product_inputirreduciblefactorization) * (ge_second_ip_all_irreducible_product_inputirreduciblefactorization))) + (((ge_first_rn_all_irreducible_product_inputirreduciblefactorization) * (ge_second_in_all_irreducible_product_inputirreduciblefactorization))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblefactorization) * (ge_second_rp_all_irreducible_product_inputirreduciblefactorization))) + (((ge_first_in_all_irreducible_product_inputirreduciblefactorization) * (ge_second_rn_all_irreducible_product_inputirreduciblefactorization))))))) + ge_balance_negative_all_irreducible_product_inputirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_all_irreducible_product_inputirreduciblefactorization) * (ge_second_in_all_irreducible_product_inputirreduciblefactorization))) + (((ge_first_rn_all_irreducible_product_inputirreduciblefactorization) * (ge_second_ip_all_irreducible_product_inputirreduciblefactorization))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblefactorization) * (ge_second_rn_all_irreducible_product_inputirreduciblefactorization))) + (((ge_first_in_all_irreducible_product_inputirreduciblefactorization) * (ge_second_rp_all_irreducible_product_inputirreduciblefactorization))))))) + ge_balance_positive_all_irreducible_product_inputirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_all_irreducible_product_inputirreduciblefirst_unit. (exists ge_first_rp_all_irreducible_product_inputirreduciblefirst_unitidentity ge_first_rn_all_irreducible_product_inputirreduciblefirst_unitidentity ge_first_ip_all_irreducible_product_inputirreduciblefirst_unitidentity ge_first_in_all_irreducible_product_inputirreduciblefirst_unitidentity ge_second_rp_all_irreducible_product_inputirreduciblefirst_unitidentity ge_second_rn_all_irreducible_product_inputirreduciblefirst_unitidentity ge_second_ip_all_irreducible_product_inputirreduciblefirst_unitidentity ge_second_in_all_irreducible_product_inputirreduciblefirst_unitidentity. ((exists ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst. (((gr_first_factor_all_irreducible_product_inputirreducible) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityfirstreal ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_all_irreducible_product_inputirreduciblefirst_unitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityfirstreal = (ge_first_rn_all_irreducible_product_inputirreduciblefirst_unitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_all_irreducible_product_inputirreduciblefirst_unitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_all_irreducible_product_inputirreduciblefirst_unitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond. (((gr_inverse_all_irreducible_product_inputirreduciblefirst_unit) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentitysecondreal ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_all_irreducible_product_inputirreduciblefirst_unitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentitysecondreal = (ge_second_rn_all_irreducible_product_inputirreduciblefirst_unitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_all_irreducible_product_inputirreduciblefirst_unitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_all_irreducible_product_inputirreduciblefirst_unitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityoutputreal ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblefirst_unitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblefirst_unitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblefirst_unitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblefirst_unitidentity))))))) + ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblefirst_unitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblefirst_unitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblefirst_unitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblefirst_unitidentity))))))) + ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblefirst_unitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblefirst_unitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblefirst_unitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblefirst_unitidentity))))))) + ge_balance_negative_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblefirst_unitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblefirst_unitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblefirst_unitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblefirst_unitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblefirst_unitidentity))))))) + ge_balance_positive_all_irreducible_product_inputirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_all_irreducible_product_inputirreduciblesecond_unit. (exists ge_first_rp_all_irreducible_product_inputirreduciblesecond_unitidentity ge_first_rn_all_irreducible_product_inputirreduciblesecond_unitidentity ge_first_ip_all_irreducible_product_inputirreduciblesecond_unitidentity ge_first_in_all_irreducible_product_inputirreduciblesecond_unitidentity ge_second_rp_all_irreducible_product_inputirreduciblesecond_unitidentity ge_second_rn_all_irreducible_product_inputirreduciblesecond_unitidentity ge_second_ip_all_irreducible_product_inputirreduciblesecond_unitidentity ge_second_in_all_irreducible_product_inputirreduciblesecond_unitidentity. ((exists ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst. (((gr_second_factor_all_irreducible_product_inputirreducible) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityfirstreal ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_all_irreducible_product_inputirreduciblesecond_unitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityfirstreal = (ge_first_rn_all_irreducible_product_inputirreduciblesecond_unitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_all_irreducible_product_inputirreduciblesecond_unitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_all_irreducible_product_inputirreduciblesecond_unitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond. (((gr_inverse_all_irreducible_product_inputirreduciblesecond_unit) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentitysecondreal ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_all_irreducible_product_inputirreduciblesecond_unitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentitysecondreal = (ge_second_rn_all_irreducible_product_inputirreduciblesecond_unitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_all_irreducible_product_inputirreduciblesecond_unitidentity) + ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_all_irreducible_product_inputirreduciblesecond_unitidentity) + ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityoutputreal ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblesecond_unitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblesecond_unitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblesecond_unitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblesecond_unitidentity))))))) + ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblesecond_unitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblesecond_unitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblesecond_unitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblesecond_unitidentity))))))) + ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_inputirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblesecond_unitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblesecond_unitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblesecond_unitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblesecond_unitidentity))))))) + ge_balance_negative_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_in_all_irreducible_product_inputirreduciblesecond_unitidentity))) + (((ge_first_rn_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_ip_all_irreducible_product_inputirreduciblesecond_unitidentity))))) + (((((ge_first_ip_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_rn_all_irreducible_product_inputirreduciblesecond_unitidentity))) + (((ge_first_in_all_irreducible_product_inputirreduciblesecond_unitidentity) * (ge_second_rp_all_irreducible_product_inputirreduciblesecond_unitidentity))))))) + ge_balance_positive_all_irreducible_product_inputirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> exists P. (exists gr_product_trace_all_irreducible_product_exists gr_product_scale_all_irreducible_product_exists. ((((exists ff_h_gprod_all_irreducible_product_existsstart. ff_h_gprod_all_irreducible_product_existsstart + S (6) = S ((S (0)) * gr_product_scale_all_irreducible_product_exists)) /\ exists ff_q_gprod_all_irreducible_product_existsstart. gr_product_trace_all_irreducible_product_exists = ff_q_gprod_all_irreducible_product_existsstart * S ((S (0)) * gr_product_scale_all_irreducible_product_exists) + (6))) /\ ((((exists ff_h_gprod_all_irreducible_product_existsend. ff_h_gprod_all_irreducible_product_existsend + S (P) = S ((S (l)) * gr_product_scale_all_irreducible_product_exists)) /\ exists ff_q_gprod_all_irreducible_product_existsend. gr_product_trace_all_irreducible_product_exists = ff_q_gprod_all_irreducible_product_existsend * S ((S (l)) * gr_product_scale_all_irreducible_product_exists) + (P))) /\ (forall gr_product_index_all_irreducible_product_existssteps. (exists ge_gap_all_irreducible_product_existsstepsindex_bound. ge_gap_all_irreducible_product_existsstepsindex_bound + S (gr_product_index_all_irreducible_product_existssteps) = (l)) -> exists gr_product_factor_all_irreducible_product_existssteps gr_product_before_all_irreducible_product_existssteps gr_product_after_all_irreducible_product_existssteps. ((((exists ff_h_gprod_all_irreducible_product_existsstepsfactor. ff_h_gprod_all_irreducible_product_existsstepsfactor + S (gr_product_factor_all_irreducible_product_existssteps) = S ((S (gr_product_index_all_irreducible_product_existssteps)) * c)) /\ exists ff_q_gprod_all_irreducible_product_existsstepsfactor. b = ff_q_gprod_all_irreducible_product_existsstepsfactor * S ((S (gr_product_index_all_irreducible_product_existssteps)) * c) + (gr_product_factor_all_irreducible_product_existssteps))) /\ ((((exists ff_h_gprod_all_irreducible_product_existsstepsbefore. ff_h_gprod_all_irreducible_product_existsstepsbefore + S (gr_product_before_all_irreducible_product_existssteps) = S ((S (gr_product_index_all_irreducible_product_existssteps)) * gr_product_scale_all_irreducible_product_exists)) /\ exists ff_q_gprod_all_irreducible_product_existsstepsbefore. gr_product_trace_all_irreducible_product_exists = ff_q_gprod_all_irreducible_product_existsstepsbefore * S ((S (gr_product_index_all_irreducible_product_existssteps)) * gr_product_scale_all_irreducible_product_exists) + (gr_product_before_all_irreducible_product_existssteps))) /\ ((((exists ff_h_gprod_all_irreducible_product_existsstepsafter. ff_h_gprod_all_irreducible_product_existsstepsafter + S (gr_product_after_all_irreducible_product_existssteps) = S ((S (S (gr_product_index_all_irreducible_product_existssteps))) * gr_product_scale_all_irreducible_product_exists)) /\ exists ff_q_gprod_all_irreducible_product_existsstepsafter. gr_product_trace_all_irreducible_product_exists = ff_q_gprod_all_irreducible_product_existsstepsafter * S ((S (S (gr_product_index_all_irreducible_product_existssteps))) * gr_product_scale_all_irreducible_product_exists) + (gr_product_after_all_irreducible_product_existssteps))) /\ (exists ge_first_rp_all_irreducible_product_existsstepsmultiply ge_first_rn_all_irreducible_product_existsstepsmultiply ge_first_ip_all_irreducible_product_existsstepsmultiply ge_first_in_all_irreducible_product_existsstepsmultiply ge_second_rp_all_irreducible_product_existsstepsmultiply ge_second_rn_all_irreducible_product_existsstepsmultiply ge_second_ip_all_irreducible_product_existsstepsmultiply ge_second_in_all_irreducible_product_existsstepsmultiply. ((exists ge_representation_real_code_all_irreducible_product_existsstepsmultiplyfirst ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyfirst. (((gr_product_before_all_irreducible_product_existssteps) = ((ge_representation_real_code_all_irreducible_product_existsstepsmultiplyfirst) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyfirst)) * S ((ge_representation_real_code_all_irreducible_product_existsstepsmultiplyfirst) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyfirst)) + ((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyfirst) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyfirst))) /\ ((exists ge_balance_positive_all_irreducible_product_existsstepsmultiplyfirstreal ge_balance_negative_all_irreducible_product_existsstepsmultiplyfirstreal. (((((ge_representation_real_code_all_irreducible_product_existsstepsmultiplyfirst) = 2 * (ge_balance_positive_all_irreducible_product_existsstepsmultiplyfirstreal) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_all_irreducible_product_existsstepsmultiplyfirstrealdecode. (((ge_representation_real_code_all_irreducible_product_existsstepsmultiplyfirst) = 2 * ge_signed_half_all_irreducible_product_existsstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_existsstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplyfirstreal) = S ge_signed_half_all_irreducible_product_existsstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_all_irreducible_product_existsstepsmultiply) + ge_balance_negative_all_irreducible_product_existsstepsmultiplyfirstreal = (ge_first_rn_all_irreducible_product_existsstepsmultiply) + ge_balance_positive_all_irreducible_product_existsstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_all_irreducible_product_existsstepsmultiplyfirstimaginary ge_balance_negative_all_irreducible_product_existsstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyfirst) = 2 * (ge_balance_positive_all_irreducible_product_existsstepsmultiplyfirstimaginary) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_existsstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyfirst) = 2 * ge_signed_half_all_irreducible_product_existsstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_existsstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplyfirstimaginary) = S ge_signed_half_all_irreducible_product_existsstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_all_irreducible_product_existsstepsmultiply) + ge_balance_negative_all_irreducible_product_existsstepsmultiplyfirstimaginary = (ge_first_in_all_irreducible_product_existsstepsmultiply) + ge_balance_positive_all_irreducible_product_existsstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_all_irreducible_product_existsstepsmultiplysecond ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplysecond. (((gr_product_factor_all_irreducible_product_existssteps) = ((ge_representation_real_code_all_irreducible_product_existsstepsmultiplysecond) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplysecond)) * S ((ge_representation_real_code_all_irreducible_product_existsstepsmultiplysecond) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplysecond)) + ((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplysecond) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplysecond))) /\ ((exists ge_balance_positive_all_irreducible_product_existsstepsmultiplysecondreal ge_balance_negative_all_irreducible_product_existsstepsmultiplysecondreal. (((((ge_representation_real_code_all_irreducible_product_existsstepsmultiplysecond) = 2 * (ge_balance_positive_all_irreducible_product_existsstepsmultiplysecondreal) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_all_irreducible_product_existsstepsmultiplysecondrealdecode. (((ge_representation_real_code_all_irreducible_product_existsstepsmultiplysecond) = 2 * ge_signed_half_all_irreducible_product_existsstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_existsstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplysecondreal) = S ge_signed_half_all_irreducible_product_existsstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_all_irreducible_product_existsstepsmultiply) + ge_balance_negative_all_irreducible_product_existsstepsmultiplysecondreal = (ge_second_rn_all_irreducible_product_existsstepsmultiply) + ge_balance_positive_all_irreducible_product_existsstepsmultiplysecondreal))) /\ (exists ge_balance_positive_all_irreducible_product_existsstepsmultiplysecondimaginary ge_balance_negative_all_irreducible_product_existsstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplysecond) = 2 * (ge_balance_positive_all_irreducible_product_existsstepsmultiplysecondimaginary) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_existsstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplysecond) = 2 * ge_signed_half_all_irreducible_product_existsstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_existsstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplysecondimaginary) = S ge_signed_half_all_irreducible_product_existsstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_all_irreducible_product_existsstepsmultiply) + ge_balance_negative_all_irreducible_product_existsstepsmultiplysecondimaginary = (ge_second_in_all_irreducible_product_existsstepsmultiply) + ge_balance_positive_all_irreducible_product_existsstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_all_irreducible_product_existsstepsmultiplyoutput ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyoutput. (((gr_product_after_all_irreducible_product_existssteps) = ((ge_representation_real_code_all_irreducible_product_existsstepsmultiplyoutput) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyoutput)) * S ((ge_representation_real_code_all_irreducible_product_existsstepsmultiplyoutput) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyoutput)) + ((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyoutput) + (ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyoutput))) /\ ((exists ge_balance_positive_all_irreducible_product_existsstepsmultiplyoutputreal ge_balance_negative_all_irreducible_product_existsstepsmultiplyoutputreal. (((((ge_representation_real_code_all_irreducible_product_existsstepsmultiplyoutput) = 2 * (ge_balance_positive_all_irreducible_product_existsstepsmultiplyoutputreal) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_all_irreducible_product_existsstepsmultiplyoutputrealdecode. (((ge_representation_real_code_all_irreducible_product_existsstepsmultiplyoutput) = 2 * ge_signed_half_all_irreducible_product_existsstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_all_irreducible_product_existsstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplyoutputreal) = S ge_signed_half_all_irreducible_product_existsstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_all_irreducible_product_existsstepsmultiply) * (ge_second_rp_all_irreducible_product_existsstepsmultiply))) + (((ge_first_rn_all_irreducible_product_existsstepsmultiply) * (ge_second_rn_all_irreducible_product_existsstepsmultiply))))) + (((((ge_first_ip_all_irreducible_product_existsstepsmultiply) * (ge_second_in_all_irreducible_product_existsstepsmultiply))) + (((ge_first_in_all_irreducible_product_existsstepsmultiply) * (ge_second_ip_all_irreducible_product_existsstepsmultiply))))))) + ge_balance_negative_all_irreducible_product_existsstepsmultiplyoutputreal = (((((((ge_first_rp_all_irreducible_product_existsstepsmultiply) * (ge_second_rn_all_irreducible_product_existsstepsmultiply))) + (((ge_first_rn_all_irreducible_product_existsstepsmultiply) * (ge_second_rp_all_irreducible_product_existsstepsmultiply))))) + (((((ge_first_ip_all_irreducible_product_existsstepsmultiply) * (ge_second_ip_all_irreducible_product_existsstepsmultiply))) + (((ge_first_in_all_irreducible_product_existsstepsmultiply) * (ge_second_in_all_irreducible_product_existsstepsmultiply))))))) + ge_balance_positive_all_irreducible_product_existsstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_all_irreducible_product_existsstepsmultiplyoutputimaginary ge_balance_negative_all_irreducible_product_existsstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyoutput) = 2 * (ge_balance_positive_all_irreducible_product_existsstepsmultiplyoutputimaginary) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_all_irreducible_product_existsstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_all_irreducible_product_existsstepsmultiplyoutput) = 2 * ge_signed_half_all_irreducible_product_existsstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_all_irreducible_product_existsstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_all_irreducible_product_existsstepsmultiplyoutputimaginary) = S ge_signed_half_all_irreducible_product_existsstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_all_irreducible_product_existsstepsmultiply) * (ge_second_ip_all_irreducible_product_existsstepsmultiply))) + (((ge_first_rn_all_irreducible_product_existsstepsmultiply) * (ge_second_in_all_irreducible_product_existsstepsmultiply))))) + (((((ge_first_ip_all_irreducible_product_existsstepsmultiply) * (ge_second_rp_all_irreducible_product_existsstepsmultiply))) + (((ge_first_in_all_irreducible_product_existsstepsmultiply) * (ge_second_rn_all_irreducible_product_existsstepsmultiply))))))) + ge_balance_negative_all_irreducible_product_existsstepsmultiplyoutputimaginary = (((((((ge_first_rp_all_irreducible_product_existsstepsmultiply) * (ge_second_in_all_irreducible_product_existsstepsmultiply))) + (((ge_first_rn_all_irreducible_product_existsstepsmultiply) * (ge_second_ip_all_irreducible_product_existsstepsmultiply))))) + (((((ge_first_ip_all_irreducible_product_existsstepsmultiply) * (ge_second_rn_all_irreducible_product_existsstepsmultiply))) + (((ge_first_in_all_irreducible_product_existsstepsmultiply) * (ge_second_rp_all_irreducible_product_existsstepsmultiply))))))) + ge_balance_positive_all_irreducible_product_existsstepsmultiplyoutputimaginary))))))))))))))))