gaussian_associate_of_unit_cofactor

Exact expanded first-order arithmetic statement

forall a u b. (exists gr_inverse_associate_cofactor_unit. (exists ge_first_rp_associate_cofactor_unitidentity ge_first_rn_associate_cofactor_unitidentity ge_first_ip_associate_cofactor_unitidentity ge_first_in_associate_cofactor_unitidentity ge_second_rp_associate_cofactor_unitidentity ge_second_rn_associate_cofactor_unitidentity ge_second_ip_associate_cofactor_unitidentity ge_second_in_associate_cofactor_unitidentity. ((exists ge_representation_real_code_associate_cofactor_unitidentityfirst ge_representation_imaginary_code_associate_cofactor_unitidentityfirst. (((u) = ((ge_representation_real_code_associate_cofactor_unitidentityfirst) + (ge_representation_imaginary_code_associate_cofactor_unitidentityfirst)) * S ((ge_representation_real_code_associate_cofactor_unitidentityfirst) + (ge_representation_imaginary_code_associate_cofactor_unitidentityfirst)) + ((ge_representation_imaginary_code_associate_cofactor_unitidentityfirst) + (ge_representation_imaginary_code_associate_cofactor_unitidentityfirst))) /\ ((exists ge_balance_positive_associate_cofactor_unitidentityfirstreal ge_balance_negative_associate_cofactor_unitidentityfirstreal. (((((ge_representation_real_code_associate_cofactor_unitidentityfirst) = 2 * (ge_balance_positive_associate_cofactor_unitidentityfirstreal) /\ (ge_balance_negative_associate_cofactor_unitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_cofactor_unitidentityfirstrealdecode. (((ge_representation_real_code_associate_cofactor_unitidentityfirst) = 2 * ge_signed_half_associate_cofactor_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_cofactor_unitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_cofactor_unitidentityfirstreal) = S ge_signed_half_associate_cofactor_unitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_cofactor_unitidentity) + ge_balance_negative_associate_cofactor_unitidentityfirstreal = (ge_first_rn_associate_cofactor_unitidentity) + ge_balance_positive_associate_cofactor_unitidentityfirstreal))) /\ (exists ge_balance_positive_associate_cofactor_unitidentityfirstimaginary ge_balance_negative_associate_cofactor_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_cofactor_unitidentityfirst) = 2 * (ge_balance_positive_associate_cofactor_unitidentityfirstimaginary) /\ (ge_balance_negative_associate_cofactor_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_cofactor_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_cofactor_unitidentityfirst) = 2 * ge_signed_half_associate_cofactor_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactor_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_cofactor_unitidentityfirstimaginary) = S ge_signed_half_associate_cofactor_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_cofactor_unitidentity) + ge_balance_negative_associate_cofactor_unitidentityfirstimaginary = (ge_first_in_associate_cofactor_unitidentity) + ge_balance_positive_associate_cofactor_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_cofactor_unitidentitysecond ge_representation_imaginary_code_associate_cofactor_unitidentitysecond. (((gr_inverse_associate_cofactor_unit) = ((ge_representation_real_code_associate_cofactor_unitidentitysecond) + (ge_representation_imaginary_code_associate_cofactor_unitidentitysecond)) * S ((ge_representation_real_code_associate_cofactor_unitidentitysecond) + (ge_representation_imaginary_code_associate_cofactor_unitidentitysecond)) + ((ge_representation_imaginary_code_associate_cofactor_unitidentitysecond) + (ge_representation_imaginary_code_associate_cofactor_unitidentitysecond))) /\ ((exists ge_balance_positive_associate_cofactor_unitidentitysecondreal ge_balance_negative_associate_cofactor_unitidentitysecondreal. (((((ge_representation_real_code_associate_cofactor_unitidentitysecond) = 2 * (ge_balance_positive_associate_cofactor_unitidentitysecondreal) /\ (ge_balance_negative_associate_cofactor_unitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_cofactor_unitidentitysecondrealdecode. (((ge_representation_real_code_associate_cofactor_unitidentitysecond) = 2 * ge_signed_half_associate_cofactor_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_cofactor_unitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_cofactor_unitidentitysecondreal) = S ge_signed_half_associate_cofactor_unitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_cofactor_unitidentity) + ge_balance_negative_associate_cofactor_unitidentitysecondreal = (ge_second_rn_associate_cofactor_unitidentity) + ge_balance_positive_associate_cofactor_unitidentitysecondreal))) /\ (exists ge_balance_positive_associate_cofactor_unitidentitysecondimaginary ge_balance_negative_associate_cofactor_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_cofactor_unitidentitysecond) = 2 * (ge_balance_positive_associate_cofactor_unitidentitysecondimaginary) /\ (ge_balance_negative_associate_cofactor_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_cofactor_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_cofactor_unitidentitysecond) = 2 * ge_signed_half_associate_cofactor_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactor_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_cofactor_unitidentitysecondimaginary) = S ge_signed_half_associate_cofactor_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_cofactor_unitidentity) + ge_balance_negative_associate_cofactor_unitidentitysecondimaginary = (ge_second_in_associate_cofactor_unitidentity) + ge_balance_positive_associate_cofactor_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_cofactor_unitidentityoutput ge_representation_imaginary_code_associate_cofactor_unitidentityoutput. (((6) = ((ge_representation_real_code_associate_cofactor_unitidentityoutput) + (ge_representation_imaginary_code_associate_cofactor_unitidentityoutput)) * S ((ge_representation_real_code_associate_cofactor_unitidentityoutput) + (ge_representation_imaginary_code_associate_cofactor_unitidentityoutput)) + ((ge_representation_imaginary_code_associate_cofactor_unitidentityoutput) + (ge_representation_imaginary_code_associate_cofactor_unitidentityoutput))) /\ ((exists ge_balance_positive_associate_cofactor_unitidentityoutputreal ge_balance_negative_associate_cofactor_unitidentityoutputreal. (((((ge_representation_real_code_associate_cofactor_unitidentityoutput) = 2 * (ge_balance_positive_associate_cofactor_unitidentityoutputreal) /\ (ge_balance_negative_associate_cofactor_unitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_cofactor_unitidentityoutputrealdecode. (((ge_representation_real_code_associate_cofactor_unitidentityoutput) = 2 * ge_signed_half_associate_cofactor_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_cofactor_unitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_cofactor_unitidentityoutputreal) = S ge_signed_half_associate_cofactor_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_cofactor_unitidentity) * (ge_second_rp_associate_cofactor_unitidentity))) + (((ge_first_rn_associate_cofactor_unitidentity) * (ge_second_rn_associate_cofactor_unitidentity))))) + (((((ge_first_ip_associate_cofactor_unitidentity) * (ge_second_in_associate_cofactor_unitidentity))) + (((ge_first_in_associate_cofactor_unitidentity) * (ge_second_ip_associate_cofactor_unitidentity))))))) + ge_balance_negative_associate_cofactor_unitidentityoutputreal = (((((((ge_first_rp_associate_cofactor_unitidentity) * (ge_second_rn_associate_cofactor_unitidentity))) + (((ge_first_rn_associate_cofactor_unitidentity) * (ge_second_rp_associate_cofactor_unitidentity))))) + (((((ge_first_ip_associate_cofactor_unitidentity) * (ge_second_ip_associate_cofactor_unitidentity))) + (((ge_first_in_associate_cofactor_unitidentity) * (ge_second_in_associate_cofactor_unitidentity))))))) + ge_balance_positive_associate_cofactor_unitidentityoutputreal))) /\ (exists ge_balance_positive_associate_cofactor_unitidentityoutputimaginary ge_balance_negative_associate_cofactor_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_cofactor_unitidentityoutput) = 2 * (ge_balance_positive_associate_cofactor_unitidentityoutputimaginary) /\ (ge_balance_negative_associate_cofactor_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_cofactor_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_cofactor_unitidentityoutput) = 2 * ge_signed_half_associate_cofactor_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactor_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_cofactor_unitidentityoutputimaginary) = S ge_signed_half_associate_cofactor_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_cofactor_unitidentity) * (ge_second_ip_associate_cofactor_unitidentity))) + (((ge_first_rn_associate_cofactor_unitidentity) * (ge_second_in_associate_cofactor_unitidentity))))) + (((((ge_first_ip_associate_cofactor_unitidentity) * (ge_second_rp_associate_cofactor_unitidentity))) + (((ge_first_in_associate_cofactor_unitidentity) * (ge_second_rn_associate_cofactor_unitidentity))))))) + ge_balance_negative_associate_cofactor_unitidentityoutputimaginary = (((((((ge_first_rp_associate_cofactor_unitidentity) * (ge_second_in_associate_cofactor_unitidentity))) + (((ge_first_rn_associate_cofactor_unitidentity) * (ge_second_ip_associate_cofactor_unitidentity))))) + (((((ge_first_ip_associate_cofactor_unitidentity) * (ge_second_rn_associate_cofactor_unitidentity))) + (((ge_first_in_associate_cofactor_unitidentity) * (ge_second_rp_associate_cofactor_unitidentity))))))) + ge_balance_positive_associate_cofactor_unitidentityoutputimaginary)))))))))) -> (exists ge_first_rp_associate_cofactor_product ge_first_rn_associate_cofactor_product ge_first_ip_associate_cofactor_product ge_first_in_associate_cofactor_product ge_second_rp_associate_cofactor_product ge_second_rn_associate_cofactor_product ge_second_ip_associate_cofactor_product ge_second_in_associate_cofactor_product. ((exists ge_representation_real_code_associate_cofactor_productfirst ge_representation_imaginary_code_associate_cofactor_productfirst. (((a) = ((ge_representation_real_code_associate_cofactor_productfirst) + (ge_representation_imaginary_code_associate_cofactor_productfirst)) * S ((ge_representation_real_code_associate_cofactor_productfirst) + (ge_representation_imaginary_code_associate_cofactor_productfirst)) + ((ge_representation_imaginary_code_associate_cofactor_productfirst) + (ge_representation_imaginary_code_associate_cofactor_productfirst))) /\ ((exists ge_balance_positive_associate_cofactor_productfirstreal ge_balance_negative_associate_cofactor_productfirstreal. (((((ge_representation_real_code_associate_cofactor_productfirst) = 2 * (ge_balance_positive_associate_cofactor_productfirstreal) /\ (ge_balance_negative_associate_cofactor_productfirstreal) = 0) \/ exists ge_signed_half_associate_cofactor_productfirstrealdecode. (((ge_representation_real_code_associate_cofactor_productfirst) = 2 * ge_signed_half_associate_cofactor_productfirstrealdecode + 1 /\ (ge_balance_positive_associate_cofactor_productfirstreal) = 0) /\ (ge_balance_negative_associate_cofactor_productfirstreal) = S ge_signed_half_associate_cofactor_productfirstrealdecode))) /\ ((ge_first_rp_associate_cofactor_product) + ge_balance_negative_associate_cofactor_productfirstreal = (ge_first_rn_associate_cofactor_product) + ge_balance_positive_associate_cofactor_productfirstreal))) /\ (exists ge_balance_positive_associate_cofactor_productfirstimaginary ge_balance_negative_associate_cofactor_productfirstimaginary. (((((ge_representation_imaginary_code_associate_cofactor_productfirst) = 2 * (ge_balance_positive_associate_cofactor_productfirstimaginary) /\ (ge_balance_negative_associate_cofactor_productfirstimaginary) = 0) \/ exists ge_signed_half_associate_cofactor_productfirstimaginarydecode. (((ge_representation_imaginary_code_associate_cofactor_productfirst) = 2 * ge_signed_half_associate_cofactor_productfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactor_productfirstimaginary) = 0) /\ (ge_balance_negative_associate_cofactor_productfirstimaginary) = S ge_signed_half_associate_cofactor_productfirstimaginarydecode))) /\ ((ge_first_ip_associate_cofactor_product) + ge_balance_negative_associate_cofactor_productfirstimaginary = (ge_first_in_associate_cofactor_product) + ge_balance_positive_associate_cofactor_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_cofactor_productsecond ge_representation_imaginary_code_associate_cofactor_productsecond. (((u) = ((ge_representation_real_code_associate_cofactor_productsecond) + (ge_representation_imaginary_code_associate_cofactor_productsecond)) * S ((ge_representation_real_code_associate_cofactor_productsecond) + (ge_representation_imaginary_code_associate_cofactor_productsecond)) + ((ge_representation_imaginary_code_associate_cofactor_productsecond) + (ge_representation_imaginary_code_associate_cofactor_productsecond))) /\ ((exists ge_balance_positive_associate_cofactor_productsecondreal ge_balance_negative_associate_cofactor_productsecondreal. (((((ge_representation_real_code_associate_cofactor_productsecond) = 2 * (ge_balance_positive_associate_cofactor_productsecondreal) /\ (ge_balance_negative_associate_cofactor_productsecondreal) = 0) \/ exists ge_signed_half_associate_cofactor_productsecondrealdecode. (((ge_representation_real_code_associate_cofactor_productsecond) = 2 * ge_signed_half_associate_cofactor_productsecondrealdecode + 1 /\ (ge_balance_positive_associate_cofactor_productsecondreal) = 0) /\ (ge_balance_negative_associate_cofactor_productsecondreal) = S ge_signed_half_associate_cofactor_productsecondrealdecode))) /\ ((ge_second_rp_associate_cofactor_product) + ge_balance_negative_associate_cofactor_productsecondreal = (ge_second_rn_associate_cofactor_product) + ge_balance_positive_associate_cofactor_productsecondreal))) /\ (exists ge_balance_positive_associate_cofactor_productsecondimaginary ge_balance_negative_associate_cofactor_productsecondimaginary. (((((ge_representation_imaginary_code_associate_cofactor_productsecond) = 2 * (ge_balance_positive_associate_cofactor_productsecondimaginary) /\ (ge_balance_negative_associate_cofactor_productsecondimaginary) = 0) \/ exists ge_signed_half_associate_cofactor_productsecondimaginarydecode. (((ge_representation_imaginary_code_associate_cofactor_productsecond) = 2 * ge_signed_half_associate_cofactor_productsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactor_productsecondimaginary) = 0) /\ (ge_balance_negative_associate_cofactor_productsecondimaginary) = S ge_signed_half_associate_cofactor_productsecondimaginarydecode))) /\ ((ge_second_ip_associate_cofactor_product) + ge_balance_negative_associate_cofactor_productsecondimaginary = (ge_second_in_associate_cofactor_product) + ge_balance_positive_associate_cofactor_productsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_cofactor_productoutput ge_representation_imaginary_code_associate_cofactor_productoutput. (((b) = ((ge_representation_real_code_associate_cofactor_productoutput) + (ge_representation_imaginary_code_associate_cofactor_productoutput)) * S ((ge_representation_real_code_associate_cofactor_productoutput) + (ge_representation_imaginary_code_associate_cofactor_productoutput)) + ((ge_representation_imaginary_code_associate_cofactor_productoutput) + (ge_representation_imaginary_code_associate_cofactor_productoutput))) /\ ((exists ge_balance_positive_associate_cofactor_productoutputreal ge_balance_negative_associate_cofactor_productoutputreal. (((((ge_representation_real_code_associate_cofactor_productoutput) = 2 * (ge_balance_positive_associate_cofactor_productoutputreal) /\ (ge_balance_negative_associate_cofactor_productoutputreal) = 0) \/ exists ge_signed_half_associate_cofactor_productoutputrealdecode. (((ge_representation_real_code_associate_cofactor_productoutput) = 2 * ge_signed_half_associate_cofactor_productoutputrealdecode + 1 /\ (ge_balance_positive_associate_cofactor_productoutputreal) = 0) /\ (ge_balance_negative_associate_cofactor_productoutputreal) = S ge_signed_half_associate_cofactor_productoutputrealdecode))) /\ ((((((((ge_first_rp_associate_cofactor_product) * (ge_second_rp_associate_cofactor_product))) + (((ge_first_rn_associate_cofactor_product) * (ge_second_rn_associate_cofactor_product))))) + (((((ge_first_ip_associate_cofactor_product) * (ge_second_in_associate_cofactor_product))) + (((ge_first_in_associate_cofactor_product) * (ge_second_ip_associate_cofactor_product))))))) + ge_balance_negative_associate_cofactor_productoutputreal = (((((((ge_first_rp_associate_cofactor_product) * (ge_second_rn_associate_cofactor_product))) + (((ge_first_rn_associate_cofactor_product) * (ge_second_rp_associate_cofactor_product))))) + (((((ge_first_ip_associate_cofactor_product) * (ge_second_ip_associate_cofactor_product))) + (((ge_first_in_associate_cofactor_product) * (ge_second_in_associate_cofactor_product))))))) + ge_balance_positive_associate_cofactor_productoutputreal))) /\ (exists ge_balance_positive_associate_cofactor_productoutputimaginary ge_balance_negative_associate_cofactor_productoutputimaginary. (((((ge_representation_imaginary_code_associate_cofactor_productoutput) = 2 * (ge_balance_positive_associate_cofactor_productoutputimaginary) /\ (ge_balance_negative_associate_cofactor_productoutputimaginary) = 0) \/ exists ge_signed_half_associate_cofactor_productoutputimaginarydecode. (((ge_representation_imaginary_code_associate_cofactor_productoutput) = 2 * ge_signed_half_associate_cofactor_productoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactor_productoutputimaginary) = 0) /\ (ge_balance_negative_associate_cofactor_productoutputimaginary) = S ge_signed_half_associate_cofactor_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_cofactor_product) * (ge_second_ip_associate_cofactor_product))) + (((ge_first_rn_associate_cofactor_product) * (ge_second_in_associate_cofactor_product))))) + (((((ge_first_ip_associate_cofactor_product) * (ge_second_rp_associate_cofactor_product))) + (((ge_first_in_associate_cofactor_product) * (ge_second_rn_associate_cofactor_product))))))) + ge_balance_negative_associate_cofactor_productoutputimaginary = (((((((ge_first_rp_associate_cofactor_product) * (ge_second_in_associate_cofactor_product))) + (((ge_first_rn_associate_cofactor_product) * (ge_second_ip_associate_cofactor_product))))) + (((((ge_first_ip_associate_cofactor_product) * (ge_second_rn_associate_cofactor_product))) + (((ge_first_in_associate_cofactor_product) * (ge_second_rp_associate_cofactor_product))))))) + ge_balance_positive_associate_cofactor_productoutputimaginary))))))))) -> (exists gr_unit_associate_cofactor. ((exists gr_inverse_associate_cofactorunit. (exists ge_first_rp_associate_cofactorunitidentity ge_first_rn_associate_cofactorunitidentity ge_first_ip_associate_cofactorunitidentity ge_first_in_associate_cofactorunitidentity ge_second_rp_associate_cofactorunitidentity ge_second_rn_associate_cofactorunitidentity ge_second_ip_associate_cofactorunitidentity ge_second_in_associate_cofactorunitidentity. ((exists ge_representation_real_code_associate_cofactorunitidentityfirst ge_representation_imaginary_code_associate_cofactorunitidentityfirst. (((gr_unit_associate_cofactor) = ((ge_representation_real_code_associate_cofactorunitidentityfirst) + (ge_representation_imaginary_code_associate_cofactorunitidentityfirst)) * S ((ge_representation_real_code_associate_cofactorunitidentityfirst) + (ge_representation_imaginary_code_associate_cofactorunitidentityfirst)) + ((ge_representation_imaginary_code_associate_cofactorunitidentityfirst) + (ge_representation_imaginary_code_associate_cofactorunitidentityfirst))) /\ ((exists ge_balance_positive_associate_cofactorunitidentityfirstreal ge_balance_negative_associate_cofactorunitidentityfirstreal. (((((ge_representation_real_code_associate_cofactorunitidentityfirst) = 2 * (ge_balance_positive_associate_cofactorunitidentityfirstreal) /\ (ge_balance_negative_associate_cofactorunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_cofactorunitidentityfirstrealdecode. (((ge_representation_real_code_associate_cofactorunitidentityfirst) = 2 * ge_signed_half_associate_cofactorunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_cofactorunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_cofactorunitidentityfirstreal) = S ge_signed_half_associate_cofactorunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_cofactorunitidentity) + ge_balance_negative_associate_cofactorunitidentityfirstreal = (ge_first_rn_associate_cofactorunitidentity) + ge_balance_positive_associate_cofactorunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_cofactorunitidentityfirstimaginary ge_balance_negative_associate_cofactorunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_cofactorunitidentityfirst) = 2 * (ge_balance_positive_associate_cofactorunitidentityfirstimaginary) /\ (ge_balance_negative_associate_cofactorunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_cofactorunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_cofactorunitidentityfirst) = 2 * ge_signed_half_associate_cofactorunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactorunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_cofactorunitidentityfirstimaginary) = S ge_signed_half_associate_cofactorunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_cofactorunitidentity) + ge_balance_negative_associate_cofactorunitidentityfirstimaginary = (ge_first_in_associate_cofactorunitidentity) + ge_balance_positive_associate_cofactorunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_cofactorunitidentitysecond ge_representation_imaginary_code_associate_cofactorunitidentitysecond. (((gr_inverse_associate_cofactorunit) = ((ge_representation_real_code_associate_cofactorunitidentitysecond) + (ge_representation_imaginary_code_associate_cofactorunitidentitysecond)) * S ((ge_representation_real_code_associate_cofactorunitidentitysecond) + (ge_representation_imaginary_code_associate_cofactorunitidentitysecond)) + ((ge_representation_imaginary_code_associate_cofactorunitidentitysecond) + (ge_representation_imaginary_code_associate_cofactorunitidentitysecond))) /\ ((exists ge_balance_positive_associate_cofactorunitidentitysecondreal ge_balance_negative_associate_cofactorunitidentitysecondreal. (((((ge_representation_real_code_associate_cofactorunitidentitysecond) = 2 * (ge_balance_positive_associate_cofactorunitidentitysecondreal) /\ (ge_balance_negative_associate_cofactorunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_cofactorunitidentitysecondrealdecode. (((ge_representation_real_code_associate_cofactorunitidentitysecond) = 2 * ge_signed_half_associate_cofactorunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_cofactorunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_cofactorunitidentitysecondreal) = S ge_signed_half_associate_cofactorunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_cofactorunitidentity) + ge_balance_negative_associate_cofactorunitidentitysecondreal = (ge_second_rn_associate_cofactorunitidentity) + ge_balance_positive_associate_cofactorunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_cofactorunitidentitysecondimaginary ge_balance_negative_associate_cofactorunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_cofactorunitidentitysecond) = 2 * (ge_balance_positive_associate_cofactorunitidentitysecondimaginary) /\ (ge_balance_negative_associate_cofactorunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_cofactorunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_cofactorunitidentitysecond) = 2 * ge_signed_half_associate_cofactorunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactorunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_cofactorunitidentitysecondimaginary) = S ge_signed_half_associate_cofactorunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_cofactorunitidentity) + ge_balance_negative_associate_cofactorunitidentitysecondimaginary = (ge_second_in_associate_cofactorunitidentity) + ge_balance_positive_associate_cofactorunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_cofactorunitidentityoutput ge_representation_imaginary_code_associate_cofactorunitidentityoutput. (((6) = ((ge_representation_real_code_associate_cofactorunitidentityoutput) + (ge_representation_imaginary_code_associate_cofactorunitidentityoutput)) * S ((ge_representation_real_code_associate_cofactorunitidentityoutput) + (ge_representation_imaginary_code_associate_cofactorunitidentityoutput)) + ((ge_representation_imaginary_code_associate_cofactorunitidentityoutput) + (ge_representation_imaginary_code_associate_cofactorunitidentityoutput))) /\ ((exists ge_balance_positive_associate_cofactorunitidentityoutputreal ge_balance_negative_associate_cofactorunitidentityoutputreal. (((((ge_representation_real_code_associate_cofactorunitidentityoutput) = 2 * (ge_balance_positive_associate_cofactorunitidentityoutputreal) /\ (ge_balance_negative_associate_cofactorunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_cofactorunitidentityoutputrealdecode. (((ge_representation_real_code_associate_cofactorunitidentityoutput) = 2 * ge_signed_half_associate_cofactorunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_cofactorunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_cofactorunitidentityoutputreal) = S ge_signed_half_associate_cofactorunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_cofactorunitidentity) * (ge_second_rp_associate_cofactorunitidentity))) + (((ge_first_rn_associate_cofactorunitidentity) * (ge_second_rn_associate_cofactorunitidentity))))) + (((((ge_first_ip_associate_cofactorunitidentity) * (ge_second_in_associate_cofactorunitidentity))) + (((ge_first_in_associate_cofactorunitidentity) * (ge_second_ip_associate_cofactorunitidentity))))))) + ge_balance_negative_associate_cofactorunitidentityoutputreal = (((((((ge_first_rp_associate_cofactorunitidentity) * (ge_second_rn_associate_cofactorunitidentity))) + (((ge_first_rn_associate_cofactorunitidentity) * (ge_second_rp_associate_cofactorunitidentity))))) + (((((ge_first_ip_associate_cofactorunitidentity) * (ge_second_ip_associate_cofactorunitidentity))) + (((ge_first_in_associate_cofactorunitidentity) * (ge_second_in_associate_cofactorunitidentity))))))) + ge_balance_positive_associate_cofactorunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_cofactorunitidentityoutputimaginary ge_balance_negative_associate_cofactorunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_cofactorunitidentityoutput) = 2 * (ge_balance_positive_associate_cofactorunitidentityoutputimaginary) /\ (ge_balance_negative_associate_cofactorunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_cofactorunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_cofactorunitidentityoutput) = 2 * ge_signed_half_associate_cofactorunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactorunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_cofactorunitidentityoutputimaginary) = S ge_signed_half_associate_cofactorunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_cofactorunitidentity) * (ge_second_ip_associate_cofactorunitidentity))) + (((ge_first_rn_associate_cofactorunitidentity) * (ge_second_in_associate_cofactorunitidentity))))) + (((((ge_first_ip_associate_cofactorunitidentity) * (ge_second_rp_associate_cofactorunitidentity))) + (((ge_first_in_associate_cofactorunitidentity) * (ge_second_rn_associate_cofactorunitidentity))))))) + ge_balance_negative_associate_cofactorunitidentityoutputimaginary = (((((((ge_first_rp_associate_cofactorunitidentity) * (ge_second_in_associate_cofactorunitidentity))) + (((ge_first_rn_associate_cofactorunitidentity) * (ge_second_ip_associate_cofactorunitidentity))))) + (((((ge_first_ip_associate_cofactorunitidentity) * (ge_second_rn_associate_cofactorunitidentity))) + (((ge_first_in_associate_cofactorunitidentity) * (ge_second_rp_associate_cofactorunitidentity))))))) + ge_balance_positive_associate_cofactorunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_cofactortransport ge_first_rn_associate_cofactortransport ge_first_ip_associate_cofactortransport ge_first_in_associate_cofactortransport ge_second_rp_associate_cofactortransport ge_second_rn_associate_cofactortransport ge_second_ip_associate_cofactortransport ge_second_in_associate_cofactortransport. ((exists ge_representation_real_code_associate_cofactortransportfirst ge_representation_imaginary_code_associate_cofactortransportfirst. (((gr_unit_associate_cofactor) = ((ge_representation_real_code_associate_cofactortransportfirst) + (ge_representation_imaginary_code_associate_cofactortransportfirst)) * S ((ge_representation_real_code_associate_cofactortransportfirst) + (ge_representation_imaginary_code_associate_cofactortransportfirst)) + ((ge_representation_imaginary_code_associate_cofactortransportfirst) + (ge_representation_imaginary_code_associate_cofactortransportfirst))) /\ ((exists ge_balance_positive_associate_cofactortransportfirstreal ge_balance_negative_associate_cofactortransportfirstreal. (((((ge_representation_real_code_associate_cofactortransportfirst) = 2 * (ge_balance_positive_associate_cofactortransportfirstreal) /\ (ge_balance_negative_associate_cofactortransportfirstreal) = 0) \/ exists ge_signed_half_associate_cofactortransportfirstrealdecode. (((ge_representation_real_code_associate_cofactortransportfirst) = 2 * ge_signed_half_associate_cofactortransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_cofactortransportfirstreal) = 0) /\ (ge_balance_negative_associate_cofactortransportfirstreal) = S ge_signed_half_associate_cofactortransportfirstrealdecode))) /\ ((ge_first_rp_associate_cofactortransport) + ge_balance_negative_associate_cofactortransportfirstreal = (ge_first_rn_associate_cofactortransport) + ge_balance_positive_associate_cofactortransportfirstreal))) /\ (exists ge_balance_positive_associate_cofactortransportfirstimaginary ge_balance_negative_associate_cofactortransportfirstimaginary. (((((ge_representation_imaginary_code_associate_cofactortransportfirst) = 2 * (ge_balance_positive_associate_cofactortransportfirstimaginary) /\ (ge_balance_negative_associate_cofactortransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_cofactortransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_cofactortransportfirst) = 2 * ge_signed_half_associate_cofactortransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactortransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_cofactortransportfirstimaginary) = S ge_signed_half_associate_cofactortransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_cofactortransport) + ge_balance_negative_associate_cofactortransportfirstimaginary = (ge_first_in_associate_cofactortransport) + ge_balance_positive_associate_cofactortransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_cofactortransportsecond ge_representation_imaginary_code_associate_cofactortransportsecond. (((a) = ((ge_representation_real_code_associate_cofactortransportsecond) + (ge_representation_imaginary_code_associate_cofactortransportsecond)) * S ((ge_representation_real_code_associate_cofactortransportsecond) + (ge_representation_imaginary_code_associate_cofactortransportsecond)) + ((ge_representation_imaginary_code_associate_cofactortransportsecond) + (ge_representation_imaginary_code_associate_cofactortransportsecond))) /\ ((exists ge_balance_positive_associate_cofactortransportsecondreal ge_balance_negative_associate_cofactortransportsecondreal. (((((ge_representation_real_code_associate_cofactortransportsecond) = 2 * (ge_balance_positive_associate_cofactortransportsecondreal) /\ (ge_balance_negative_associate_cofactortransportsecondreal) = 0) \/ exists ge_signed_half_associate_cofactortransportsecondrealdecode. (((ge_representation_real_code_associate_cofactortransportsecond) = 2 * ge_signed_half_associate_cofactortransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_cofactortransportsecondreal) = 0) /\ (ge_balance_negative_associate_cofactortransportsecondreal) = S ge_signed_half_associate_cofactortransportsecondrealdecode))) /\ ((ge_second_rp_associate_cofactortransport) + ge_balance_negative_associate_cofactortransportsecondreal = (ge_second_rn_associate_cofactortransport) + ge_balance_positive_associate_cofactortransportsecondreal))) /\ (exists ge_balance_positive_associate_cofactortransportsecondimaginary ge_balance_negative_associate_cofactortransportsecondimaginary. (((((ge_representation_imaginary_code_associate_cofactortransportsecond) = 2 * (ge_balance_positive_associate_cofactortransportsecondimaginary) /\ (ge_balance_negative_associate_cofactortransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_cofactortransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_cofactortransportsecond) = 2 * ge_signed_half_associate_cofactortransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactortransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_cofactortransportsecondimaginary) = S ge_signed_half_associate_cofactortransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_cofactortransport) + ge_balance_negative_associate_cofactortransportsecondimaginary = (ge_second_in_associate_cofactortransport) + ge_balance_positive_associate_cofactortransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_cofactortransportoutput ge_representation_imaginary_code_associate_cofactortransportoutput. (((b) = ((ge_representation_real_code_associate_cofactortransportoutput) + (ge_representation_imaginary_code_associate_cofactortransportoutput)) * S ((ge_representation_real_code_associate_cofactortransportoutput) + (ge_representation_imaginary_code_associate_cofactortransportoutput)) + ((ge_representation_imaginary_code_associate_cofactortransportoutput) + (ge_representation_imaginary_code_associate_cofactortransportoutput))) /\ ((exists ge_balance_positive_associate_cofactortransportoutputreal ge_balance_negative_associate_cofactortransportoutputreal. (((((ge_representation_real_code_associate_cofactortransportoutput) = 2 * (ge_balance_positive_associate_cofactortransportoutputreal) /\ (ge_balance_negative_associate_cofactortransportoutputreal) = 0) \/ exists ge_signed_half_associate_cofactortransportoutputrealdecode. (((ge_representation_real_code_associate_cofactortransportoutput) = 2 * ge_signed_half_associate_cofactortransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_cofactortransportoutputreal) = 0) /\ (ge_balance_negative_associate_cofactortransportoutputreal) = S ge_signed_half_associate_cofactortransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_cofactortransport) * (ge_second_rp_associate_cofactortransport))) + (((ge_first_rn_associate_cofactortransport) * (ge_second_rn_associate_cofactortransport))))) + (((((ge_first_ip_associate_cofactortransport) * (ge_second_in_associate_cofactortransport))) + (((ge_first_in_associate_cofactortransport) * (ge_second_ip_associate_cofactortransport))))))) + ge_balance_negative_associate_cofactortransportoutputreal = (((((((ge_first_rp_associate_cofactortransport) * (ge_second_rn_associate_cofactortransport))) + (((ge_first_rn_associate_cofactortransport) * (ge_second_rp_associate_cofactortransport))))) + (((((ge_first_ip_associate_cofactortransport) * (ge_second_ip_associate_cofactortransport))) + (((ge_first_in_associate_cofactortransport) * (ge_second_in_associate_cofactortransport))))))) + ge_balance_positive_associate_cofactortransportoutputreal))) /\ (exists ge_balance_positive_associate_cofactortransportoutputimaginary ge_balance_negative_associate_cofactortransportoutputimaginary. (((((ge_representation_imaginary_code_associate_cofactortransportoutput) = 2 * (ge_balance_positive_associate_cofactortransportoutputimaginary) /\ (ge_balance_negative_associate_cofactortransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_cofactortransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_cofactortransportoutput) = 2 * ge_signed_half_associate_cofactortransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_cofactortransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_cofactortransportoutputimaginary) = S ge_signed_half_associate_cofactortransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_cofactortransport) * (ge_second_ip_associate_cofactortransport))) + (((ge_first_rn_associate_cofactortransport) * (ge_second_in_associate_cofactortransport))))) + (((((ge_first_ip_associate_cofactortransport) * (ge_second_rp_associate_cofactortransport))) + (((ge_first_in_associate_cofactortransport) * (ge_second_rn_associate_cofactortransport))))))) + ge_balance_negative_associate_cofactortransportoutputimaginary = (((((((ge_first_rp_associate_cofactortransport) * (ge_second_in_associate_cofactortransport))) + (((ge_first_rn_associate_cofactortransport) * (ge_second_ip_associate_cofactortransport))))) + (((((ge_first_ip_associate_cofactortransport) * (ge_second_rn_associate_cofactortransport))) + (((ge_first_in_associate_cofactortransport) * (ge_second_rp_associate_cofactortransport))))))) + ge_balance_positive_associate_cofactortransportoutputimaginary)))))))))))