gaussian_factor_associate_cancel_products

Exact expanded first-order arithmetic statement

forall R p P T q Q. (exists ge_first_rp_cancel_first_product ge_first_rn_cancel_first_product ge_first_ip_cancel_first_product ge_first_in_cancel_first_product ge_second_rp_cancel_first_product ge_second_rn_cancel_first_product ge_second_ip_cancel_first_product ge_second_in_cancel_first_product. ((exists ge_representation_real_code_cancel_first_productfirst ge_representation_imaginary_code_cancel_first_productfirst. (((R) = ((ge_representation_real_code_cancel_first_productfirst) + (ge_representation_imaginary_code_cancel_first_productfirst)) * S ((ge_representation_real_code_cancel_first_productfirst) + (ge_representation_imaginary_code_cancel_first_productfirst)) + ((ge_representation_imaginary_code_cancel_first_productfirst) + (ge_representation_imaginary_code_cancel_first_productfirst))) /\ ((exists ge_balance_positive_cancel_first_productfirstreal ge_balance_negative_cancel_first_productfirstreal. (((((ge_representation_real_code_cancel_first_productfirst) = 2 * (ge_balance_positive_cancel_first_productfirstreal) /\ (ge_balance_negative_cancel_first_productfirstreal) = 0) \/ exists ge_signed_half_cancel_first_productfirstrealdecode. (((ge_representation_real_code_cancel_first_productfirst) = 2 * ge_signed_half_cancel_first_productfirstrealdecode + 1 /\ (ge_balance_positive_cancel_first_productfirstreal) = 0) /\ (ge_balance_negative_cancel_first_productfirstreal) = S ge_signed_half_cancel_first_productfirstrealdecode))) /\ ((ge_first_rp_cancel_first_product) + ge_balance_negative_cancel_first_productfirstreal = (ge_first_rn_cancel_first_product) + ge_balance_positive_cancel_first_productfirstreal))) /\ (exists ge_balance_positive_cancel_first_productfirstimaginary ge_balance_negative_cancel_first_productfirstimaginary. (((((ge_representation_imaginary_code_cancel_first_productfirst) = 2 * (ge_balance_positive_cancel_first_productfirstimaginary) /\ (ge_balance_negative_cancel_first_productfirstimaginary) = 0) \/ exists ge_signed_half_cancel_first_productfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_first_productfirst) = 2 * ge_signed_half_cancel_first_productfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_first_productfirstimaginary) = 0) /\ (ge_balance_negative_cancel_first_productfirstimaginary) = S ge_signed_half_cancel_first_productfirstimaginarydecode))) /\ ((ge_first_ip_cancel_first_product) + ge_balance_negative_cancel_first_productfirstimaginary = (ge_first_in_cancel_first_product) + ge_balance_positive_cancel_first_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_first_productsecond ge_representation_imaginary_code_cancel_first_productsecond. (((p) = ((ge_representation_real_code_cancel_first_productsecond) + (ge_representation_imaginary_code_cancel_first_productsecond)) * S ((ge_representation_real_code_cancel_first_productsecond) + (ge_representation_imaginary_code_cancel_first_productsecond)) + ((ge_representation_imaginary_code_cancel_first_productsecond) + (ge_representation_imaginary_code_cancel_first_productsecond))) /\ ((exists ge_balance_positive_cancel_first_productsecondreal ge_balance_negative_cancel_first_productsecondreal. (((((ge_representation_real_code_cancel_first_productsecond) = 2 * (ge_balance_positive_cancel_first_productsecondreal) /\ (ge_balance_negative_cancel_first_productsecondreal) = 0) \/ exists ge_signed_half_cancel_first_productsecondrealdecode. (((ge_representation_real_code_cancel_first_productsecond) = 2 * ge_signed_half_cancel_first_productsecondrealdecode + 1 /\ (ge_balance_positive_cancel_first_productsecondreal) = 0) /\ (ge_balance_negative_cancel_first_productsecondreal) = S ge_signed_half_cancel_first_productsecondrealdecode))) /\ ((ge_second_rp_cancel_first_product) + ge_balance_negative_cancel_first_productsecondreal = (ge_second_rn_cancel_first_product) + ge_balance_positive_cancel_first_productsecondreal))) /\ (exists ge_balance_positive_cancel_first_productsecondimaginary ge_balance_negative_cancel_first_productsecondimaginary. (((((ge_representation_imaginary_code_cancel_first_productsecond) = 2 * (ge_balance_positive_cancel_first_productsecondimaginary) /\ (ge_balance_negative_cancel_first_productsecondimaginary) = 0) \/ exists ge_signed_half_cancel_first_productsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_first_productsecond) = 2 * ge_signed_half_cancel_first_productsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_first_productsecondimaginary) = 0) /\ (ge_balance_negative_cancel_first_productsecondimaginary) = S ge_signed_half_cancel_first_productsecondimaginarydecode))) /\ ((ge_second_ip_cancel_first_product) + ge_balance_negative_cancel_first_productsecondimaginary = (ge_second_in_cancel_first_product) + ge_balance_positive_cancel_first_productsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_first_productoutput ge_representation_imaginary_code_cancel_first_productoutput. (((P) = ((ge_representation_real_code_cancel_first_productoutput) + (ge_representation_imaginary_code_cancel_first_productoutput)) * S ((ge_representation_real_code_cancel_first_productoutput) + (ge_representation_imaginary_code_cancel_first_productoutput)) + ((ge_representation_imaginary_code_cancel_first_productoutput) + (ge_representation_imaginary_code_cancel_first_productoutput))) /\ ((exists ge_balance_positive_cancel_first_productoutputreal ge_balance_negative_cancel_first_productoutputreal. (((((ge_representation_real_code_cancel_first_productoutput) = 2 * (ge_balance_positive_cancel_first_productoutputreal) /\ (ge_balance_negative_cancel_first_productoutputreal) = 0) \/ exists ge_signed_half_cancel_first_productoutputrealdecode. (((ge_representation_real_code_cancel_first_productoutput) = 2 * ge_signed_half_cancel_first_productoutputrealdecode + 1 /\ (ge_balance_positive_cancel_first_productoutputreal) = 0) /\ (ge_balance_negative_cancel_first_productoutputreal) = S ge_signed_half_cancel_first_productoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_first_product) * (ge_second_rp_cancel_first_product))) + (((ge_first_rn_cancel_first_product) * (ge_second_rn_cancel_first_product))))) + (((((ge_first_ip_cancel_first_product) * (ge_second_in_cancel_first_product))) + (((ge_first_in_cancel_first_product) * (ge_second_ip_cancel_first_product))))))) + ge_balance_negative_cancel_first_productoutputreal = (((((((ge_first_rp_cancel_first_product) * (ge_second_rn_cancel_first_product))) + (((ge_first_rn_cancel_first_product) * (ge_second_rp_cancel_first_product))))) + (((((ge_first_ip_cancel_first_product) * (ge_second_ip_cancel_first_product))) + (((ge_first_in_cancel_first_product) * (ge_second_in_cancel_first_product))))))) + ge_balance_positive_cancel_first_productoutputreal))) /\ (exists ge_balance_positive_cancel_first_productoutputimaginary ge_balance_negative_cancel_first_productoutputimaginary. (((((ge_representation_imaginary_code_cancel_first_productoutput) = 2 * (ge_balance_positive_cancel_first_productoutputimaginary) /\ (ge_balance_negative_cancel_first_productoutputimaginary) = 0) \/ exists ge_signed_half_cancel_first_productoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_first_productoutput) = 2 * ge_signed_half_cancel_first_productoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_first_productoutputimaginary) = 0) /\ (ge_balance_negative_cancel_first_productoutputimaginary) = S ge_signed_half_cancel_first_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_first_product) * (ge_second_ip_cancel_first_product))) + (((ge_first_rn_cancel_first_product) * (ge_second_in_cancel_first_product))))) + (((((ge_first_ip_cancel_first_product) * (ge_second_rp_cancel_first_product))) + (((ge_first_in_cancel_first_product) * (ge_second_rn_cancel_first_product))))))) + ge_balance_negative_cancel_first_productoutputimaginary = (((((((ge_first_rp_cancel_first_product) * (ge_second_in_cancel_first_product))) + (((ge_first_rn_cancel_first_product) * (ge_second_ip_cancel_first_product))))) + (((((ge_first_ip_cancel_first_product) * (ge_second_rn_cancel_first_product))) + (((ge_first_in_cancel_first_product) * (ge_second_rp_cancel_first_product))))))) + ge_balance_positive_cancel_first_productoutputimaginary))))))))) -> (exists ge_first_rp_cancel_second_product ge_first_rn_cancel_second_product ge_first_ip_cancel_second_product ge_first_in_cancel_second_product ge_second_rp_cancel_second_product ge_second_rn_cancel_second_product ge_second_ip_cancel_second_product ge_second_in_cancel_second_product. ((exists ge_representation_real_code_cancel_second_productfirst ge_representation_imaginary_code_cancel_second_productfirst. (((T) = ((ge_representation_real_code_cancel_second_productfirst) + (ge_representation_imaginary_code_cancel_second_productfirst)) * S ((ge_representation_real_code_cancel_second_productfirst) + (ge_representation_imaginary_code_cancel_second_productfirst)) + ((ge_representation_imaginary_code_cancel_second_productfirst) + (ge_representation_imaginary_code_cancel_second_productfirst))) /\ ((exists ge_balance_positive_cancel_second_productfirstreal ge_balance_negative_cancel_second_productfirstreal. (((((ge_representation_real_code_cancel_second_productfirst) = 2 * (ge_balance_positive_cancel_second_productfirstreal) /\ (ge_balance_negative_cancel_second_productfirstreal) = 0) \/ exists ge_signed_half_cancel_second_productfirstrealdecode. (((ge_representation_real_code_cancel_second_productfirst) = 2 * ge_signed_half_cancel_second_productfirstrealdecode + 1 /\ (ge_balance_positive_cancel_second_productfirstreal) = 0) /\ (ge_balance_negative_cancel_second_productfirstreal) = S ge_signed_half_cancel_second_productfirstrealdecode))) /\ ((ge_first_rp_cancel_second_product) + ge_balance_negative_cancel_second_productfirstreal = (ge_first_rn_cancel_second_product) + ge_balance_positive_cancel_second_productfirstreal))) /\ (exists ge_balance_positive_cancel_second_productfirstimaginary ge_balance_negative_cancel_second_productfirstimaginary. (((((ge_representation_imaginary_code_cancel_second_productfirst) = 2 * (ge_balance_positive_cancel_second_productfirstimaginary) /\ (ge_balance_negative_cancel_second_productfirstimaginary) = 0) \/ exists ge_signed_half_cancel_second_productfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_second_productfirst) = 2 * ge_signed_half_cancel_second_productfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_second_productfirstimaginary) = 0) /\ (ge_balance_negative_cancel_second_productfirstimaginary) = S ge_signed_half_cancel_second_productfirstimaginarydecode))) /\ ((ge_first_ip_cancel_second_product) + ge_balance_negative_cancel_second_productfirstimaginary = (ge_first_in_cancel_second_product) + ge_balance_positive_cancel_second_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_second_productsecond ge_representation_imaginary_code_cancel_second_productsecond. (((q) = ((ge_representation_real_code_cancel_second_productsecond) + (ge_representation_imaginary_code_cancel_second_productsecond)) * S ((ge_representation_real_code_cancel_second_productsecond) + (ge_representation_imaginary_code_cancel_second_productsecond)) + ((ge_representation_imaginary_code_cancel_second_productsecond) + (ge_representation_imaginary_code_cancel_second_productsecond))) /\ ((exists ge_balance_positive_cancel_second_productsecondreal ge_balance_negative_cancel_second_productsecondreal. (((((ge_representation_real_code_cancel_second_productsecond) = 2 * (ge_balance_positive_cancel_second_productsecondreal) /\ (ge_balance_negative_cancel_second_productsecondreal) = 0) \/ exists ge_signed_half_cancel_second_productsecondrealdecode. (((ge_representation_real_code_cancel_second_productsecond) = 2 * ge_signed_half_cancel_second_productsecondrealdecode + 1 /\ (ge_balance_positive_cancel_second_productsecondreal) = 0) /\ (ge_balance_negative_cancel_second_productsecondreal) = S ge_signed_half_cancel_second_productsecondrealdecode))) /\ ((ge_second_rp_cancel_second_product) + ge_balance_negative_cancel_second_productsecondreal = (ge_second_rn_cancel_second_product) + ge_balance_positive_cancel_second_productsecondreal))) /\ (exists ge_balance_positive_cancel_second_productsecondimaginary ge_balance_negative_cancel_second_productsecondimaginary. (((((ge_representation_imaginary_code_cancel_second_productsecond) = 2 * (ge_balance_positive_cancel_second_productsecondimaginary) /\ (ge_balance_negative_cancel_second_productsecondimaginary) = 0) \/ exists ge_signed_half_cancel_second_productsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_second_productsecond) = 2 * ge_signed_half_cancel_second_productsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_second_productsecondimaginary) = 0) /\ (ge_balance_negative_cancel_second_productsecondimaginary) = S ge_signed_half_cancel_second_productsecondimaginarydecode))) /\ ((ge_second_ip_cancel_second_product) + ge_balance_negative_cancel_second_productsecondimaginary = (ge_second_in_cancel_second_product) + ge_balance_positive_cancel_second_productsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_second_productoutput ge_representation_imaginary_code_cancel_second_productoutput. (((Q) = ((ge_representation_real_code_cancel_second_productoutput) + (ge_representation_imaginary_code_cancel_second_productoutput)) * S ((ge_representation_real_code_cancel_second_productoutput) + (ge_representation_imaginary_code_cancel_second_productoutput)) + ((ge_representation_imaginary_code_cancel_second_productoutput) + (ge_representation_imaginary_code_cancel_second_productoutput))) /\ ((exists ge_balance_positive_cancel_second_productoutputreal ge_balance_negative_cancel_second_productoutputreal. (((((ge_representation_real_code_cancel_second_productoutput) = 2 * (ge_balance_positive_cancel_second_productoutputreal) /\ (ge_balance_negative_cancel_second_productoutputreal) = 0) \/ exists ge_signed_half_cancel_second_productoutputrealdecode. (((ge_representation_real_code_cancel_second_productoutput) = 2 * ge_signed_half_cancel_second_productoutputrealdecode + 1 /\ (ge_balance_positive_cancel_second_productoutputreal) = 0) /\ (ge_balance_negative_cancel_second_productoutputreal) = S ge_signed_half_cancel_second_productoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_second_product) * (ge_second_rp_cancel_second_product))) + (((ge_first_rn_cancel_second_product) * (ge_second_rn_cancel_second_product))))) + (((((ge_first_ip_cancel_second_product) * (ge_second_in_cancel_second_product))) + (((ge_first_in_cancel_second_product) * (ge_second_ip_cancel_second_product))))))) + ge_balance_negative_cancel_second_productoutputreal = (((((((ge_first_rp_cancel_second_product) * (ge_second_rn_cancel_second_product))) + (((ge_first_rn_cancel_second_product) * (ge_second_rp_cancel_second_product))))) + (((((ge_first_ip_cancel_second_product) * (ge_second_ip_cancel_second_product))) + (((ge_first_in_cancel_second_product) * (ge_second_in_cancel_second_product))))))) + ge_balance_positive_cancel_second_productoutputreal))) /\ (exists ge_balance_positive_cancel_second_productoutputimaginary ge_balance_negative_cancel_second_productoutputimaginary. (((((ge_representation_imaginary_code_cancel_second_productoutput) = 2 * (ge_balance_positive_cancel_second_productoutputimaginary) /\ (ge_balance_negative_cancel_second_productoutputimaginary) = 0) \/ exists ge_signed_half_cancel_second_productoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_second_productoutput) = 2 * ge_signed_half_cancel_second_productoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_second_productoutputimaginary) = 0) /\ (ge_balance_negative_cancel_second_productoutputimaginary) = S ge_signed_half_cancel_second_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_second_product) * (ge_second_ip_cancel_second_product))) + (((ge_first_rn_cancel_second_product) * (ge_second_in_cancel_second_product))))) + (((((ge_first_ip_cancel_second_product) * (ge_second_rp_cancel_second_product))) + (((ge_first_in_cancel_second_product) * (ge_second_rn_cancel_second_product))))))) + ge_balance_negative_cancel_second_productoutputimaginary = (((((((ge_first_rp_cancel_second_product) * (ge_second_in_cancel_second_product))) + (((ge_first_rn_cancel_second_product) * (ge_second_ip_cancel_second_product))))) + (((((ge_first_ip_cancel_second_product) * (ge_second_rn_cancel_second_product))) + (((ge_first_in_cancel_second_product) * (ge_second_rp_cancel_second_product))))))) + ge_balance_positive_cancel_second_productoutputimaginary))))))))) -> (exists gr_unit_cancel_total_associate. ((exists gr_inverse_cancel_total_associateunit. (exists ge_first_rp_cancel_total_associateunitidentity ge_first_rn_cancel_total_associateunitidentity ge_first_ip_cancel_total_associateunitidentity ge_first_in_cancel_total_associateunitidentity ge_second_rp_cancel_total_associateunitidentity ge_second_rn_cancel_total_associateunitidentity ge_second_ip_cancel_total_associateunitidentity ge_second_in_cancel_total_associateunitidentity. ((exists ge_representation_real_code_cancel_total_associateunitidentityfirst ge_representation_imaginary_code_cancel_total_associateunitidentityfirst. (((gr_unit_cancel_total_associate) = ((ge_representation_real_code_cancel_total_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_total_associateunitidentityfirst)) * S ((ge_representation_real_code_cancel_total_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_total_associateunitidentityfirst)) + ((ge_representation_imaginary_code_cancel_total_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_total_associateunitidentityfirst))) /\ ((exists ge_balance_positive_cancel_total_associateunitidentityfirstreal ge_balance_negative_cancel_total_associateunitidentityfirstreal. (((((ge_representation_real_code_cancel_total_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_total_associateunitidentityfirstreal) /\ (ge_balance_negative_cancel_total_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentityfirstrealdecode. (((ge_representation_real_code_cancel_total_associateunitidentityfirst) = 2 * ge_signed_half_cancel_total_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentityfirstreal) = S ge_signed_half_cancel_total_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_cancel_total_associateunitidentity) + ge_balance_negative_cancel_total_associateunitidentityfirstreal = (ge_first_rn_cancel_total_associateunitidentity) + ge_balance_positive_cancel_total_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_cancel_total_associateunitidentityfirstimaginary ge_balance_negative_cancel_total_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_cancel_total_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_total_associateunitidentityfirstimaginary) /\ (ge_balance_negative_cancel_total_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associateunitidentityfirst) = 2 * ge_signed_half_cancel_total_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentityfirstimaginary) = S ge_signed_half_cancel_total_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_cancel_total_associateunitidentity) + ge_balance_negative_cancel_total_associateunitidentityfirstimaginary = (ge_first_in_cancel_total_associateunitidentity) + ge_balance_positive_cancel_total_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_total_associateunitidentitysecond ge_representation_imaginary_code_cancel_total_associateunitidentitysecond. (((gr_inverse_cancel_total_associateunit) = ((ge_representation_real_code_cancel_total_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_total_associateunitidentitysecond)) * S ((ge_representation_real_code_cancel_total_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_total_associateunitidentitysecond)) + ((ge_representation_imaginary_code_cancel_total_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_total_associateunitidentitysecond))) /\ ((exists ge_balance_positive_cancel_total_associateunitidentitysecondreal ge_balance_negative_cancel_total_associateunitidentitysecondreal. (((((ge_representation_real_code_cancel_total_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_total_associateunitidentitysecondreal) /\ (ge_balance_negative_cancel_total_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentitysecondrealdecode. (((ge_representation_real_code_cancel_total_associateunitidentitysecond) = 2 * ge_signed_half_cancel_total_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentitysecondreal) = S ge_signed_half_cancel_total_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_cancel_total_associateunitidentity) + ge_balance_negative_cancel_total_associateunitidentitysecondreal = (ge_second_rn_cancel_total_associateunitidentity) + ge_balance_positive_cancel_total_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_cancel_total_associateunitidentitysecondimaginary ge_balance_negative_cancel_total_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_cancel_total_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_total_associateunitidentitysecondimaginary) /\ (ge_balance_negative_cancel_total_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associateunitidentitysecond) = 2 * ge_signed_half_cancel_total_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentitysecondimaginary) = S ge_signed_half_cancel_total_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_cancel_total_associateunitidentity) + ge_balance_negative_cancel_total_associateunitidentitysecondimaginary = (ge_second_in_cancel_total_associateunitidentity) + ge_balance_positive_cancel_total_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_total_associateunitidentityoutput ge_representation_imaginary_code_cancel_total_associateunitidentityoutput. (((6) = ((ge_representation_real_code_cancel_total_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_total_associateunitidentityoutput)) * S ((ge_representation_real_code_cancel_total_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_total_associateunitidentityoutput)) + ((ge_representation_imaginary_code_cancel_total_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_total_associateunitidentityoutput))) /\ ((exists ge_balance_positive_cancel_total_associateunitidentityoutputreal ge_balance_negative_cancel_total_associateunitidentityoutputreal. (((((ge_representation_real_code_cancel_total_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_total_associateunitidentityoutputreal) /\ (ge_balance_negative_cancel_total_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentityoutputrealdecode. (((ge_representation_real_code_cancel_total_associateunitidentityoutput) = 2 * ge_signed_half_cancel_total_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentityoutputreal) = S ge_signed_half_cancel_total_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_total_associateunitidentity) * (ge_second_rp_cancel_total_associateunitidentity))) + (((ge_first_rn_cancel_total_associateunitidentity) * (ge_second_rn_cancel_total_associateunitidentity))))) + (((((ge_first_ip_cancel_total_associateunitidentity) * (ge_second_in_cancel_total_associateunitidentity))) + (((ge_first_in_cancel_total_associateunitidentity) * (ge_second_ip_cancel_total_associateunitidentity))))))) + ge_balance_negative_cancel_total_associateunitidentityoutputreal = (((((((ge_first_rp_cancel_total_associateunitidentity) * (ge_second_rn_cancel_total_associateunitidentity))) + (((ge_first_rn_cancel_total_associateunitidentity) * (ge_second_rp_cancel_total_associateunitidentity))))) + (((((ge_first_ip_cancel_total_associateunitidentity) * (ge_second_ip_cancel_total_associateunitidentity))) + (((ge_first_in_cancel_total_associateunitidentity) * (ge_second_in_cancel_total_associateunitidentity))))))) + ge_balance_positive_cancel_total_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_cancel_total_associateunitidentityoutputimaginary ge_balance_negative_cancel_total_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_cancel_total_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_total_associateunitidentityoutputimaginary) /\ (ge_balance_negative_cancel_total_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associateunitidentityoutput) = 2 * ge_signed_half_cancel_total_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentityoutputimaginary) = S ge_signed_half_cancel_total_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_total_associateunitidentity) * (ge_second_ip_cancel_total_associateunitidentity))) + (((ge_first_rn_cancel_total_associateunitidentity) * (ge_second_in_cancel_total_associateunitidentity))))) + (((((ge_first_ip_cancel_total_associateunitidentity) * (ge_second_rp_cancel_total_associateunitidentity))) + (((ge_first_in_cancel_total_associateunitidentity) * (ge_second_rn_cancel_total_associateunitidentity))))))) + ge_balance_negative_cancel_total_associateunitidentityoutputimaginary = (((((((ge_first_rp_cancel_total_associateunitidentity) * (ge_second_in_cancel_total_associateunitidentity))) + (((ge_first_rn_cancel_total_associateunitidentity) * (ge_second_ip_cancel_total_associateunitidentity))))) + (((((ge_first_ip_cancel_total_associateunitidentity) * (ge_second_rn_cancel_total_associateunitidentity))) + (((ge_first_in_cancel_total_associateunitidentity) * (ge_second_rp_cancel_total_associateunitidentity))))))) + ge_balance_positive_cancel_total_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_cancel_total_associatetransport ge_first_rn_cancel_total_associatetransport ge_first_ip_cancel_total_associatetransport ge_first_in_cancel_total_associatetransport ge_second_rp_cancel_total_associatetransport ge_second_rn_cancel_total_associatetransport ge_second_ip_cancel_total_associatetransport ge_second_in_cancel_total_associatetransport. ((exists ge_representation_real_code_cancel_total_associatetransportfirst ge_representation_imaginary_code_cancel_total_associatetransportfirst. (((gr_unit_cancel_total_associate) = ((ge_representation_real_code_cancel_total_associatetransportfirst) + (ge_representation_imaginary_code_cancel_total_associatetransportfirst)) * S ((ge_representation_real_code_cancel_total_associatetransportfirst) + (ge_representation_imaginary_code_cancel_total_associatetransportfirst)) + ((ge_representation_imaginary_code_cancel_total_associatetransportfirst) + (ge_representation_imaginary_code_cancel_total_associatetransportfirst))) /\ ((exists ge_balance_positive_cancel_total_associatetransportfirstreal ge_balance_negative_cancel_total_associatetransportfirstreal. (((((ge_representation_real_code_cancel_total_associatetransportfirst) = 2 * (ge_balance_positive_cancel_total_associatetransportfirstreal) /\ (ge_balance_negative_cancel_total_associatetransportfirstreal) = 0) \/ exists ge_signed_half_cancel_total_associatetransportfirstrealdecode. (((ge_representation_real_code_cancel_total_associatetransportfirst) = 2 * ge_signed_half_cancel_total_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportfirstreal) = 0) /\ (ge_balance_negative_cancel_total_associatetransportfirstreal) = S ge_signed_half_cancel_total_associatetransportfirstrealdecode))) /\ ((ge_first_rp_cancel_total_associatetransport) + ge_balance_negative_cancel_total_associatetransportfirstreal = (ge_first_rn_cancel_total_associatetransport) + ge_balance_positive_cancel_total_associatetransportfirstreal))) /\ (exists ge_balance_positive_cancel_total_associatetransportfirstimaginary ge_balance_negative_cancel_total_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_cancel_total_associatetransportfirst) = 2 * (ge_balance_positive_cancel_total_associatetransportfirstimaginary) /\ (ge_balance_negative_cancel_total_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_cancel_total_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associatetransportfirst) = 2 * ge_signed_half_cancel_total_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_cancel_total_associatetransportfirstimaginary) = S ge_signed_half_cancel_total_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_cancel_total_associatetransport) + ge_balance_negative_cancel_total_associatetransportfirstimaginary = (ge_first_in_cancel_total_associatetransport) + ge_balance_positive_cancel_total_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_total_associatetransportsecond ge_representation_imaginary_code_cancel_total_associatetransportsecond. (((P) = ((ge_representation_real_code_cancel_total_associatetransportsecond) + (ge_representation_imaginary_code_cancel_total_associatetransportsecond)) * S ((ge_representation_real_code_cancel_total_associatetransportsecond) + (ge_representation_imaginary_code_cancel_total_associatetransportsecond)) + ((ge_representation_imaginary_code_cancel_total_associatetransportsecond) + (ge_representation_imaginary_code_cancel_total_associatetransportsecond))) /\ ((exists ge_balance_positive_cancel_total_associatetransportsecondreal ge_balance_negative_cancel_total_associatetransportsecondreal. (((((ge_representation_real_code_cancel_total_associatetransportsecond) = 2 * (ge_balance_positive_cancel_total_associatetransportsecondreal) /\ (ge_balance_negative_cancel_total_associatetransportsecondreal) = 0) \/ exists ge_signed_half_cancel_total_associatetransportsecondrealdecode. (((ge_representation_real_code_cancel_total_associatetransportsecond) = 2 * ge_signed_half_cancel_total_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportsecondreal) = 0) /\ (ge_balance_negative_cancel_total_associatetransportsecondreal) = S ge_signed_half_cancel_total_associatetransportsecondrealdecode))) /\ ((ge_second_rp_cancel_total_associatetransport) + ge_balance_negative_cancel_total_associatetransportsecondreal = (ge_second_rn_cancel_total_associatetransport) + ge_balance_positive_cancel_total_associatetransportsecondreal))) /\ (exists ge_balance_positive_cancel_total_associatetransportsecondimaginary ge_balance_negative_cancel_total_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_cancel_total_associatetransportsecond) = 2 * (ge_balance_positive_cancel_total_associatetransportsecondimaginary) /\ (ge_balance_negative_cancel_total_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_cancel_total_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associatetransportsecond) = 2 * ge_signed_half_cancel_total_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_cancel_total_associatetransportsecondimaginary) = S ge_signed_half_cancel_total_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_cancel_total_associatetransport) + ge_balance_negative_cancel_total_associatetransportsecondimaginary = (ge_second_in_cancel_total_associatetransport) + ge_balance_positive_cancel_total_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_total_associatetransportoutput ge_representation_imaginary_code_cancel_total_associatetransportoutput. (((Q) = ((ge_representation_real_code_cancel_total_associatetransportoutput) + (ge_representation_imaginary_code_cancel_total_associatetransportoutput)) * S ((ge_representation_real_code_cancel_total_associatetransportoutput) + (ge_representation_imaginary_code_cancel_total_associatetransportoutput)) + ((ge_representation_imaginary_code_cancel_total_associatetransportoutput) + (ge_representation_imaginary_code_cancel_total_associatetransportoutput))) /\ ((exists ge_balance_positive_cancel_total_associatetransportoutputreal ge_balance_negative_cancel_total_associatetransportoutputreal. (((((ge_representation_real_code_cancel_total_associatetransportoutput) = 2 * (ge_balance_positive_cancel_total_associatetransportoutputreal) /\ (ge_balance_negative_cancel_total_associatetransportoutputreal) = 0) \/ exists ge_signed_half_cancel_total_associatetransportoutputrealdecode. (((ge_representation_real_code_cancel_total_associatetransportoutput) = 2 * ge_signed_half_cancel_total_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportoutputreal) = 0) /\ (ge_balance_negative_cancel_total_associatetransportoutputreal) = S ge_signed_half_cancel_total_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_total_associatetransport) * (ge_second_rp_cancel_total_associatetransport))) + (((ge_first_rn_cancel_total_associatetransport) * (ge_second_rn_cancel_total_associatetransport))))) + (((((ge_first_ip_cancel_total_associatetransport) * (ge_second_in_cancel_total_associatetransport))) + (((ge_first_in_cancel_total_associatetransport) * (ge_second_ip_cancel_total_associatetransport))))))) + ge_balance_negative_cancel_total_associatetransportoutputreal = (((((((ge_first_rp_cancel_total_associatetransport) * (ge_second_rn_cancel_total_associatetransport))) + (((ge_first_rn_cancel_total_associatetransport) * (ge_second_rp_cancel_total_associatetransport))))) + (((((ge_first_ip_cancel_total_associatetransport) * (ge_second_ip_cancel_total_associatetransport))) + (((ge_first_in_cancel_total_associatetransport) * (ge_second_in_cancel_total_associatetransport))))))) + ge_balance_positive_cancel_total_associatetransportoutputreal))) /\ (exists ge_balance_positive_cancel_total_associatetransportoutputimaginary ge_balance_negative_cancel_total_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_cancel_total_associatetransportoutput) = 2 * (ge_balance_positive_cancel_total_associatetransportoutputimaginary) /\ (ge_balance_negative_cancel_total_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_cancel_total_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associatetransportoutput) = 2 * ge_signed_half_cancel_total_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_cancel_total_associatetransportoutputimaginary) = S ge_signed_half_cancel_total_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_total_associatetransport) * (ge_second_ip_cancel_total_associatetransport))) + (((ge_first_rn_cancel_total_associatetransport) * (ge_second_in_cancel_total_associatetransport))))) + (((((ge_first_ip_cancel_total_associatetransport) * (ge_second_rp_cancel_total_associatetransport))) + (((ge_first_in_cancel_total_associatetransport) * (ge_second_rn_cancel_total_associatetransport))))))) + ge_balance_negative_cancel_total_associatetransportoutputimaginary = (((((((ge_first_rp_cancel_total_associatetransport) * (ge_second_in_cancel_total_associatetransport))) + (((ge_first_rn_cancel_total_associatetransport) * (ge_second_ip_cancel_total_associatetransport))))) + (((((ge_first_ip_cancel_total_associatetransport) * (ge_second_rn_cancel_total_associatetransport))) + (((ge_first_in_cancel_total_associatetransport) * (ge_second_rp_cancel_total_associatetransport))))))) + ge_balance_positive_cancel_total_associatetransportoutputimaginary))))))))))) -> (exists gr_unit_cancel_factor_associate. ((exists gr_inverse_cancel_factor_associateunit. (exists ge_first_rp_cancel_factor_associateunitidentity ge_first_rn_cancel_factor_associateunitidentity ge_first_ip_cancel_factor_associateunitidentity ge_first_in_cancel_factor_associateunitidentity ge_second_rp_cancel_factor_associateunitidentity ge_second_rn_cancel_factor_associateunitidentity ge_second_ip_cancel_factor_associateunitidentity ge_second_in_cancel_factor_associateunitidentity. ((exists ge_representation_real_code_cancel_factor_associateunitidentityfirst ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst. (((gr_unit_cancel_factor_associate) = ((ge_representation_real_code_cancel_factor_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst)) * S ((ge_representation_real_code_cancel_factor_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst)) + ((ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst))) /\ ((exists ge_balance_positive_cancel_factor_associateunitidentityfirstreal ge_balance_negative_cancel_factor_associateunitidentityfirstreal. (((((ge_representation_real_code_cancel_factor_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_factor_associateunitidentityfirstreal) /\ (ge_balance_negative_cancel_factor_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentityfirstrealdecode. (((ge_representation_real_code_cancel_factor_associateunitidentityfirst) = 2 * ge_signed_half_cancel_factor_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentityfirstreal) = S ge_signed_half_cancel_factor_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_cancel_factor_associateunitidentity) + ge_balance_negative_cancel_factor_associateunitidentityfirstreal = (ge_first_rn_cancel_factor_associateunitidentity) + ge_balance_positive_cancel_factor_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_cancel_factor_associateunitidentityfirstimaginary ge_balance_negative_cancel_factor_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_factor_associateunitidentityfirstimaginary) /\ (ge_balance_negative_cancel_factor_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst) = 2 * ge_signed_half_cancel_factor_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentityfirstimaginary) = S ge_signed_half_cancel_factor_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_cancel_factor_associateunitidentity) + ge_balance_negative_cancel_factor_associateunitidentityfirstimaginary = (ge_first_in_cancel_factor_associateunitidentity) + ge_balance_positive_cancel_factor_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_factor_associateunitidentitysecond ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond. (((gr_inverse_cancel_factor_associateunit) = ((ge_representation_real_code_cancel_factor_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond)) * S ((ge_representation_real_code_cancel_factor_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond)) + ((ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond))) /\ ((exists ge_balance_positive_cancel_factor_associateunitidentitysecondreal ge_balance_negative_cancel_factor_associateunitidentitysecondreal. (((((ge_representation_real_code_cancel_factor_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_factor_associateunitidentitysecondreal) /\ (ge_balance_negative_cancel_factor_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentitysecondrealdecode. (((ge_representation_real_code_cancel_factor_associateunitidentitysecond) = 2 * ge_signed_half_cancel_factor_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentitysecondreal) = S ge_signed_half_cancel_factor_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_cancel_factor_associateunitidentity) + ge_balance_negative_cancel_factor_associateunitidentitysecondreal = (ge_second_rn_cancel_factor_associateunitidentity) + ge_balance_positive_cancel_factor_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_cancel_factor_associateunitidentitysecondimaginary ge_balance_negative_cancel_factor_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_factor_associateunitidentitysecondimaginary) /\ (ge_balance_negative_cancel_factor_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond) = 2 * ge_signed_half_cancel_factor_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentitysecondimaginary) = S ge_signed_half_cancel_factor_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_cancel_factor_associateunitidentity) + ge_balance_negative_cancel_factor_associateunitidentitysecondimaginary = (ge_second_in_cancel_factor_associateunitidentity) + ge_balance_positive_cancel_factor_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_factor_associateunitidentityoutput ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput. (((6) = ((ge_representation_real_code_cancel_factor_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput)) * S ((ge_representation_real_code_cancel_factor_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput)) + ((ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput))) /\ ((exists ge_balance_positive_cancel_factor_associateunitidentityoutputreal ge_balance_negative_cancel_factor_associateunitidentityoutputreal. (((((ge_representation_real_code_cancel_factor_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_factor_associateunitidentityoutputreal) /\ (ge_balance_negative_cancel_factor_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentityoutputrealdecode. (((ge_representation_real_code_cancel_factor_associateunitidentityoutput) = 2 * ge_signed_half_cancel_factor_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentityoutputreal) = S ge_signed_half_cancel_factor_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_factor_associateunitidentity) * (ge_second_rp_cancel_factor_associateunitidentity))) + (((ge_first_rn_cancel_factor_associateunitidentity) * (ge_second_rn_cancel_factor_associateunitidentity))))) + (((((ge_first_ip_cancel_factor_associateunitidentity) * (ge_second_in_cancel_factor_associateunitidentity))) + (((ge_first_in_cancel_factor_associateunitidentity) * (ge_second_ip_cancel_factor_associateunitidentity))))))) + ge_balance_negative_cancel_factor_associateunitidentityoutputreal = (((((((ge_first_rp_cancel_factor_associateunitidentity) * (ge_second_rn_cancel_factor_associateunitidentity))) + (((ge_first_rn_cancel_factor_associateunitidentity) * (ge_second_rp_cancel_factor_associateunitidentity))))) + (((((ge_first_ip_cancel_factor_associateunitidentity) * (ge_second_ip_cancel_factor_associateunitidentity))) + (((ge_first_in_cancel_factor_associateunitidentity) * (ge_second_in_cancel_factor_associateunitidentity))))))) + ge_balance_positive_cancel_factor_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_cancel_factor_associateunitidentityoutputimaginary ge_balance_negative_cancel_factor_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_factor_associateunitidentityoutputimaginary) /\ (ge_balance_negative_cancel_factor_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput) = 2 * ge_signed_half_cancel_factor_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentityoutputimaginary) = S ge_signed_half_cancel_factor_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_factor_associateunitidentity) * (ge_second_ip_cancel_factor_associateunitidentity))) + (((ge_first_rn_cancel_factor_associateunitidentity) * (ge_second_in_cancel_factor_associateunitidentity))))) + (((((ge_first_ip_cancel_factor_associateunitidentity) * (ge_second_rp_cancel_factor_associateunitidentity))) + (((ge_first_in_cancel_factor_associateunitidentity) * (ge_second_rn_cancel_factor_associateunitidentity))))))) + ge_balance_negative_cancel_factor_associateunitidentityoutputimaginary = (((((((ge_first_rp_cancel_factor_associateunitidentity) * (ge_second_in_cancel_factor_associateunitidentity))) + (((ge_first_rn_cancel_factor_associateunitidentity) * (ge_second_ip_cancel_factor_associateunitidentity))))) + (((((ge_first_ip_cancel_factor_associateunitidentity) * (ge_second_rn_cancel_factor_associateunitidentity))) + (((ge_first_in_cancel_factor_associateunitidentity) * (ge_second_rp_cancel_factor_associateunitidentity))))))) + ge_balance_positive_cancel_factor_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_cancel_factor_associatetransport ge_first_rn_cancel_factor_associatetransport ge_first_ip_cancel_factor_associatetransport ge_first_in_cancel_factor_associatetransport ge_second_rp_cancel_factor_associatetransport ge_second_rn_cancel_factor_associatetransport ge_second_ip_cancel_factor_associatetransport ge_second_in_cancel_factor_associatetransport. ((exists ge_representation_real_code_cancel_factor_associatetransportfirst ge_representation_imaginary_code_cancel_factor_associatetransportfirst. (((gr_unit_cancel_factor_associate) = ((ge_representation_real_code_cancel_factor_associatetransportfirst) + (ge_representation_imaginary_code_cancel_factor_associatetransportfirst)) * S ((ge_representation_real_code_cancel_factor_associatetransportfirst) + (ge_representation_imaginary_code_cancel_factor_associatetransportfirst)) + ((ge_representation_imaginary_code_cancel_factor_associatetransportfirst) + (ge_representation_imaginary_code_cancel_factor_associatetransportfirst))) /\ ((exists ge_balance_positive_cancel_factor_associatetransportfirstreal ge_balance_negative_cancel_factor_associatetransportfirstreal. (((((ge_representation_real_code_cancel_factor_associatetransportfirst) = 2 * (ge_balance_positive_cancel_factor_associatetransportfirstreal) /\ (ge_balance_negative_cancel_factor_associatetransportfirstreal) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportfirstrealdecode. (((ge_representation_real_code_cancel_factor_associatetransportfirst) = 2 * ge_signed_half_cancel_factor_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportfirstreal) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportfirstreal) = S ge_signed_half_cancel_factor_associatetransportfirstrealdecode))) /\ ((ge_first_rp_cancel_factor_associatetransport) + ge_balance_negative_cancel_factor_associatetransportfirstreal = (ge_first_rn_cancel_factor_associatetransport) + ge_balance_positive_cancel_factor_associatetransportfirstreal))) /\ (exists ge_balance_positive_cancel_factor_associatetransportfirstimaginary ge_balance_negative_cancel_factor_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_cancel_factor_associatetransportfirst) = 2 * (ge_balance_positive_cancel_factor_associatetransportfirstimaginary) /\ (ge_balance_negative_cancel_factor_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associatetransportfirst) = 2 * ge_signed_half_cancel_factor_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportfirstimaginary) = S ge_signed_half_cancel_factor_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_cancel_factor_associatetransport) + ge_balance_negative_cancel_factor_associatetransportfirstimaginary = (ge_first_in_cancel_factor_associatetransport) + ge_balance_positive_cancel_factor_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_factor_associatetransportsecond ge_representation_imaginary_code_cancel_factor_associatetransportsecond. (((p) = ((ge_representation_real_code_cancel_factor_associatetransportsecond) + (ge_representation_imaginary_code_cancel_factor_associatetransportsecond)) * S ((ge_representation_real_code_cancel_factor_associatetransportsecond) + (ge_representation_imaginary_code_cancel_factor_associatetransportsecond)) + ((ge_representation_imaginary_code_cancel_factor_associatetransportsecond) + (ge_representation_imaginary_code_cancel_factor_associatetransportsecond))) /\ ((exists ge_balance_positive_cancel_factor_associatetransportsecondreal ge_balance_negative_cancel_factor_associatetransportsecondreal. (((((ge_representation_real_code_cancel_factor_associatetransportsecond) = 2 * (ge_balance_positive_cancel_factor_associatetransportsecondreal) /\ (ge_balance_negative_cancel_factor_associatetransportsecondreal) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportsecondrealdecode. (((ge_representation_real_code_cancel_factor_associatetransportsecond) = 2 * ge_signed_half_cancel_factor_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportsecondreal) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportsecondreal) = S ge_signed_half_cancel_factor_associatetransportsecondrealdecode))) /\ ((ge_second_rp_cancel_factor_associatetransport) + ge_balance_negative_cancel_factor_associatetransportsecondreal = (ge_second_rn_cancel_factor_associatetransport) + ge_balance_positive_cancel_factor_associatetransportsecondreal))) /\ (exists ge_balance_positive_cancel_factor_associatetransportsecondimaginary ge_balance_negative_cancel_factor_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_cancel_factor_associatetransportsecond) = 2 * (ge_balance_positive_cancel_factor_associatetransportsecondimaginary) /\ (ge_balance_negative_cancel_factor_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associatetransportsecond) = 2 * ge_signed_half_cancel_factor_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportsecondimaginary) = S ge_signed_half_cancel_factor_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_cancel_factor_associatetransport) + ge_balance_negative_cancel_factor_associatetransportsecondimaginary = (ge_second_in_cancel_factor_associatetransport) + ge_balance_positive_cancel_factor_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_factor_associatetransportoutput ge_representation_imaginary_code_cancel_factor_associatetransportoutput. (((q) = ((ge_representation_real_code_cancel_factor_associatetransportoutput) + (ge_representation_imaginary_code_cancel_factor_associatetransportoutput)) * S ((ge_representation_real_code_cancel_factor_associatetransportoutput) + (ge_representation_imaginary_code_cancel_factor_associatetransportoutput)) + ((ge_representation_imaginary_code_cancel_factor_associatetransportoutput) + (ge_representation_imaginary_code_cancel_factor_associatetransportoutput))) /\ ((exists ge_balance_positive_cancel_factor_associatetransportoutputreal ge_balance_negative_cancel_factor_associatetransportoutputreal. (((((ge_representation_real_code_cancel_factor_associatetransportoutput) = 2 * (ge_balance_positive_cancel_factor_associatetransportoutputreal) /\ (ge_balance_negative_cancel_factor_associatetransportoutputreal) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportoutputrealdecode. (((ge_representation_real_code_cancel_factor_associatetransportoutput) = 2 * ge_signed_half_cancel_factor_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportoutputreal) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportoutputreal) = S ge_signed_half_cancel_factor_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_factor_associatetransport) * (ge_second_rp_cancel_factor_associatetransport))) + (((ge_first_rn_cancel_factor_associatetransport) * (ge_second_rn_cancel_factor_associatetransport))))) + (((((ge_first_ip_cancel_factor_associatetransport) * (ge_second_in_cancel_factor_associatetransport))) + (((ge_first_in_cancel_factor_associatetransport) * (ge_second_ip_cancel_factor_associatetransport))))))) + ge_balance_negative_cancel_factor_associatetransportoutputreal = (((((((ge_first_rp_cancel_factor_associatetransport) * (ge_second_rn_cancel_factor_associatetransport))) + (((ge_first_rn_cancel_factor_associatetransport) * (ge_second_rp_cancel_factor_associatetransport))))) + (((((ge_first_ip_cancel_factor_associatetransport) * (ge_second_ip_cancel_factor_associatetransport))) + (((ge_first_in_cancel_factor_associatetransport) * (ge_second_in_cancel_factor_associatetransport))))))) + ge_balance_positive_cancel_factor_associatetransportoutputreal))) /\ (exists ge_balance_positive_cancel_factor_associatetransportoutputimaginary ge_balance_negative_cancel_factor_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_cancel_factor_associatetransportoutput) = 2 * (ge_balance_positive_cancel_factor_associatetransportoutputimaginary) /\ (ge_balance_negative_cancel_factor_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associatetransportoutput) = 2 * ge_signed_half_cancel_factor_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportoutputimaginary) = S ge_signed_half_cancel_factor_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_factor_associatetransport) * (ge_second_ip_cancel_factor_associatetransport))) + (((ge_first_rn_cancel_factor_associatetransport) * (ge_second_in_cancel_factor_associatetransport))))) + (((((ge_first_ip_cancel_factor_associatetransport) * (ge_second_rp_cancel_factor_associatetransport))) + (((ge_first_in_cancel_factor_associatetransport) * (ge_second_rn_cancel_factor_associatetransport))))))) + ge_balance_negative_cancel_factor_associatetransportoutputimaginary = (((((((ge_first_rp_cancel_factor_associatetransport) * (ge_second_in_cancel_factor_associatetransport))) + (((ge_first_rn_cancel_factor_associatetransport) * (ge_second_ip_cancel_factor_associatetransport))))) + (((((ge_first_ip_cancel_factor_associatetransport) * (ge_second_rn_cancel_factor_associatetransport))) + (((ge_first_in_cancel_factor_associatetransport) * (ge_second_rp_cancel_factor_associatetransport))))))) + ge_balance_positive_cancel_factor_associatetransportoutputimaginary))))))))))) -> ~(p=0) -> (exists gr_unit_cancel_prefix_associate. ((exists gr_inverse_cancel_prefix_associateunit. (exists ge_first_rp_cancel_prefix_associateunitidentity ge_first_rn_cancel_prefix_associateunitidentity ge_first_ip_cancel_prefix_associateunitidentity ge_first_in_cancel_prefix_associateunitidentity ge_second_rp_cancel_prefix_associateunitidentity ge_second_rn_cancel_prefix_associateunitidentity ge_second_ip_cancel_prefix_associateunitidentity ge_second_in_cancel_prefix_associateunitidentity. ((exists ge_representation_real_code_cancel_prefix_associateunitidentityfirst ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst. (((gr_unit_cancel_prefix_associate) = ((ge_representation_real_code_cancel_prefix_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst)) * S ((ge_representation_real_code_cancel_prefix_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst)) + ((ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst))) /\ ((exists ge_balance_positive_cancel_prefix_associateunitidentityfirstreal ge_balance_negative_cancel_prefix_associateunitidentityfirstreal. (((((ge_representation_real_code_cancel_prefix_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentityfirstreal) /\ (ge_balance_negative_cancel_prefix_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentityfirstrealdecode. (((ge_representation_real_code_cancel_prefix_associateunitidentityfirst) = 2 * ge_signed_half_cancel_prefix_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentityfirstreal) = S ge_signed_half_cancel_prefix_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_cancel_prefix_associateunitidentity) + ge_balance_negative_cancel_prefix_associateunitidentityfirstreal = (ge_first_rn_cancel_prefix_associateunitidentity) + ge_balance_positive_cancel_prefix_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_cancel_prefix_associateunitidentityfirstimaginary ge_balance_negative_cancel_prefix_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentityfirstimaginary) /\ (ge_balance_negative_cancel_prefix_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst) = 2 * ge_signed_half_cancel_prefix_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentityfirstimaginary) = S ge_signed_half_cancel_prefix_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_cancel_prefix_associateunitidentity) + ge_balance_negative_cancel_prefix_associateunitidentityfirstimaginary = (ge_first_in_cancel_prefix_associateunitidentity) + ge_balance_positive_cancel_prefix_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_prefix_associateunitidentitysecond ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond. (((gr_inverse_cancel_prefix_associateunit) = ((ge_representation_real_code_cancel_prefix_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond)) * S ((ge_representation_real_code_cancel_prefix_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond)) + ((ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond))) /\ ((exists ge_balance_positive_cancel_prefix_associateunitidentitysecondreal ge_balance_negative_cancel_prefix_associateunitidentitysecondreal. (((((ge_representation_real_code_cancel_prefix_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentitysecondreal) /\ (ge_balance_negative_cancel_prefix_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentitysecondrealdecode. (((ge_representation_real_code_cancel_prefix_associateunitidentitysecond) = 2 * ge_signed_half_cancel_prefix_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentitysecondreal) = S ge_signed_half_cancel_prefix_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_cancel_prefix_associateunitidentity) + ge_balance_negative_cancel_prefix_associateunitidentitysecondreal = (ge_second_rn_cancel_prefix_associateunitidentity) + ge_balance_positive_cancel_prefix_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_cancel_prefix_associateunitidentitysecondimaginary ge_balance_negative_cancel_prefix_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentitysecondimaginary) /\ (ge_balance_negative_cancel_prefix_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond) = 2 * ge_signed_half_cancel_prefix_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentitysecondimaginary) = S ge_signed_half_cancel_prefix_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_cancel_prefix_associateunitidentity) + ge_balance_negative_cancel_prefix_associateunitidentitysecondimaginary = (ge_second_in_cancel_prefix_associateunitidentity) + ge_balance_positive_cancel_prefix_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_prefix_associateunitidentityoutput ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput. (((6) = ((ge_representation_real_code_cancel_prefix_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput)) * S ((ge_representation_real_code_cancel_prefix_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput)) + ((ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput))) /\ ((exists ge_balance_positive_cancel_prefix_associateunitidentityoutputreal ge_balance_negative_cancel_prefix_associateunitidentityoutputreal. (((((ge_representation_real_code_cancel_prefix_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentityoutputreal) /\ (ge_balance_negative_cancel_prefix_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentityoutputrealdecode. (((ge_representation_real_code_cancel_prefix_associateunitidentityoutput) = 2 * ge_signed_half_cancel_prefix_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentityoutputreal) = S ge_signed_half_cancel_prefix_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_prefix_associateunitidentity) * (ge_second_rp_cancel_prefix_associateunitidentity))) + (((ge_first_rn_cancel_prefix_associateunitidentity) * (ge_second_rn_cancel_prefix_associateunitidentity))))) + (((((ge_first_ip_cancel_prefix_associateunitidentity) * (ge_second_in_cancel_prefix_associateunitidentity))) + (((ge_first_in_cancel_prefix_associateunitidentity) * (ge_second_ip_cancel_prefix_associateunitidentity))))))) + ge_balance_negative_cancel_prefix_associateunitidentityoutputreal = (((((((ge_first_rp_cancel_prefix_associateunitidentity) * (ge_second_rn_cancel_prefix_associateunitidentity))) + (((ge_first_rn_cancel_prefix_associateunitidentity) * (ge_second_rp_cancel_prefix_associateunitidentity))))) + (((((ge_first_ip_cancel_prefix_associateunitidentity) * (ge_second_ip_cancel_prefix_associateunitidentity))) + (((ge_first_in_cancel_prefix_associateunitidentity) * (ge_second_in_cancel_prefix_associateunitidentity))))))) + ge_balance_positive_cancel_prefix_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_cancel_prefix_associateunitidentityoutputimaginary ge_balance_negative_cancel_prefix_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentityoutputimaginary) /\ (ge_balance_negative_cancel_prefix_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput) = 2 * ge_signed_half_cancel_prefix_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentityoutputimaginary) = S ge_signed_half_cancel_prefix_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_prefix_associateunitidentity) * (ge_second_ip_cancel_prefix_associateunitidentity))) + (((ge_first_rn_cancel_prefix_associateunitidentity) * (ge_second_in_cancel_prefix_associateunitidentity))))) + (((((ge_first_ip_cancel_prefix_associateunitidentity) * (ge_second_rp_cancel_prefix_associateunitidentity))) + (((ge_first_in_cancel_prefix_associateunitidentity) * (ge_second_rn_cancel_prefix_associateunitidentity))))))) + ge_balance_negative_cancel_prefix_associateunitidentityoutputimaginary = (((((((ge_first_rp_cancel_prefix_associateunitidentity) * (ge_second_in_cancel_prefix_associateunitidentity))) + (((ge_first_rn_cancel_prefix_associateunitidentity) * (ge_second_ip_cancel_prefix_associateunitidentity))))) + (((((ge_first_ip_cancel_prefix_associateunitidentity) * (ge_second_rn_cancel_prefix_associateunitidentity))) + (((ge_first_in_cancel_prefix_associateunitidentity) * (ge_second_rp_cancel_prefix_associateunitidentity))))))) + ge_balance_positive_cancel_prefix_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_cancel_prefix_associatetransport ge_first_rn_cancel_prefix_associatetransport ge_first_ip_cancel_prefix_associatetransport ge_first_in_cancel_prefix_associatetransport ge_second_rp_cancel_prefix_associatetransport ge_second_rn_cancel_prefix_associatetransport ge_second_ip_cancel_prefix_associatetransport ge_second_in_cancel_prefix_associatetransport. ((exists ge_representation_real_code_cancel_prefix_associatetransportfirst ge_representation_imaginary_code_cancel_prefix_associatetransportfirst. (((gr_unit_cancel_prefix_associate) = ((ge_representation_real_code_cancel_prefix_associatetransportfirst) + (ge_representation_imaginary_code_cancel_prefix_associatetransportfirst)) * S ((ge_representation_real_code_cancel_prefix_associatetransportfirst) + (ge_representation_imaginary_code_cancel_prefix_associatetransportfirst)) + ((ge_representation_imaginary_code_cancel_prefix_associatetransportfirst) + (ge_representation_imaginary_code_cancel_prefix_associatetransportfirst))) /\ ((exists ge_balance_positive_cancel_prefix_associatetransportfirstreal ge_balance_negative_cancel_prefix_associatetransportfirstreal. (((((ge_representation_real_code_cancel_prefix_associatetransportfirst) = 2 * (ge_balance_positive_cancel_prefix_associatetransportfirstreal) /\ (ge_balance_negative_cancel_prefix_associatetransportfirstreal) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportfirstrealdecode. (((ge_representation_real_code_cancel_prefix_associatetransportfirst) = 2 * ge_signed_half_cancel_prefix_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportfirstreal) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportfirstreal) = S ge_signed_half_cancel_prefix_associatetransportfirstrealdecode))) /\ ((ge_first_rp_cancel_prefix_associatetransport) + ge_balance_negative_cancel_prefix_associatetransportfirstreal = (ge_first_rn_cancel_prefix_associatetransport) + ge_balance_positive_cancel_prefix_associatetransportfirstreal))) /\ (exists ge_balance_positive_cancel_prefix_associatetransportfirstimaginary ge_balance_negative_cancel_prefix_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associatetransportfirst) = 2 * (ge_balance_positive_cancel_prefix_associatetransportfirstimaginary) /\ (ge_balance_negative_cancel_prefix_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associatetransportfirst) = 2 * ge_signed_half_cancel_prefix_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportfirstimaginary) = S ge_signed_half_cancel_prefix_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_cancel_prefix_associatetransport) + ge_balance_negative_cancel_prefix_associatetransportfirstimaginary = (ge_first_in_cancel_prefix_associatetransport) + ge_balance_positive_cancel_prefix_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_prefix_associatetransportsecond ge_representation_imaginary_code_cancel_prefix_associatetransportsecond. (((R) = ((ge_representation_real_code_cancel_prefix_associatetransportsecond) + (ge_representation_imaginary_code_cancel_prefix_associatetransportsecond)) * S ((ge_representation_real_code_cancel_prefix_associatetransportsecond) + (ge_representation_imaginary_code_cancel_prefix_associatetransportsecond)) + ((ge_representation_imaginary_code_cancel_prefix_associatetransportsecond) + (ge_representation_imaginary_code_cancel_prefix_associatetransportsecond))) /\ ((exists ge_balance_positive_cancel_prefix_associatetransportsecondreal ge_balance_negative_cancel_prefix_associatetransportsecondreal. (((((ge_representation_real_code_cancel_prefix_associatetransportsecond) = 2 * (ge_balance_positive_cancel_prefix_associatetransportsecondreal) /\ (ge_balance_negative_cancel_prefix_associatetransportsecondreal) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportsecondrealdecode. (((ge_representation_real_code_cancel_prefix_associatetransportsecond) = 2 * ge_signed_half_cancel_prefix_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportsecondreal) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportsecondreal) = S ge_signed_half_cancel_prefix_associatetransportsecondrealdecode))) /\ ((ge_second_rp_cancel_prefix_associatetransport) + ge_balance_negative_cancel_prefix_associatetransportsecondreal = (ge_second_rn_cancel_prefix_associatetransport) + ge_balance_positive_cancel_prefix_associatetransportsecondreal))) /\ (exists ge_balance_positive_cancel_prefix_associatetransportsecondimaginary ge_balance_negative_cancel_prefix_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associatetransportsecond) = 2 * (ge_balance_positive_cancel_prefix_associatetransportsecondimaginary) /\ (ge_balance_negative_cancel_prefix_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associatetransportsecond) = 2 * ge_signed_half_cancel_prefix_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportsecondimaginary) = S ge_signed_half_cancel_prefix_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_cancel_prefix_associatetransport) + ge_balance_negative_cancel_prefix_associatetransportsecondimaginary = (ge_second_in_cancel_prefix_associatetransport) + ge_balance_positive_cancel_prefix_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_prefix_associatetransportoutput ge_representation_imaginary_code_cancel_prefix_associatetransportoutput. (((T) = ((ge_representation_real_code_cancel_prefix_associatetransportoutput) + (ge_representation_imaginary_code_cancel_prefix_associatetransportoutput)) * S ((ge_representation_real_code_cancel_prefix_associatetransportoutput) + (ge_representation_imaginary_code_cancel_prefix_associatetransportoutput)) + ((ge_representation_imaginary_code_cancel_prefix_associatetransportoutput) + (ge_representation_imaginary_code_cancel_prefix_associatetransportoutput))) /\ ((exists ge_balance_positive_cancel_prefix_associatetransportoutputreal ge_balance_negative_cancel_prefix_associatetransportoutputreal. (((((ge_representation_real_code_cancel_prefix_associatetransportoutput) = 2 * (ge_balance_positive_cancel_prefix_associatetransportoutputreal) /\ (ge_balance_negative_cancel_prefix_associatetransportoutputreal) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportoutputrealdecode. (((ge_representation_real_code_cancel_prefix_associatetransportoutput) = 2 * ge_signed_half_cancel_prefix_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportoutputreal) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportoutputreal) = S ge_signed_half_cancel_prefix_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_prefix_associatetransport) * (ge_second_rp_cancel_prefix_associatetransport))) + (((ge_first_rn_cancel_prefix_associatetransport) * (ge_second_rn_cancel_prefix_associatetransport))))) + (((((ge_first_ip_cancel_prefix_associatetransport) * (ge_second_in_cancel_prefix_associatetransport))) + (((ge_first_in_cancel_prefix_associatetransport) * (ge_second_ip_cancel_prefix_associatetransport))))))) + ge_balance_negative_cancel_prefix_associatetransportoutputreal = (((((((ge_first_rp_cancel_prefix_associatetransport) * (ge_second_rn_cancel_prefix_associatetransport))) + (((ge_first_rn_cancel_prefix_associatetransport) * (ge_second_rp_cancel_prefix_associatetransport))))) + (((((ge_first_ip_cancel_prefix_associatetransport) * (ge_second_ip_cancel_prefix_associatetransport))) + (((ge_first_in_cancel_prefix_associatetransport) * (ge_second_in_cancel_prefix_associatetransport))))))) + ge_balance_positive_cancel_prefix_associatetransportoutputreal))) /\ (exists ge_balance_positive_cancel_prefix_associatetransportoutputimaginary ge_balance_negative_cancel_prefix_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associatetransportoutput) = 2 * (ge_balance_positive_cancel_prefix_associatetransportoutputimaginary) /\ (ge_balance_negative_cancel_prefix_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associatetransportoutput) = 2 * ge_signed_half_cancel_prefix_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportoutputimaginary) = S ge_signed_half_cancel_prefix_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_prefix_associatetransport) * (ge_second_ip_cancel_prefix_associatetransport))) + (((ge_first_rn_cancel_prefix_associatetransport) * (ge_second_in_cancel_prefix_associatetransport))))) + (((((ge_first_ip_cancel_prefix_associatetransport) * (ge_second_rp_cancel_prefix_associatetransport))) + (((ge_first_in_cancel_prefix_associatetransport) * (ge_second_rn_cancel_prefix_associatetransport))))))) + ge_balance_negative_cancel_prefix_associatetransportoutputimaginary = (((((((ge_first_rp_cancel_prefix_associatetransport) * (ge_second_in_cancel_prefix_associatetransport))) + (((ge_first_rn_cancel_prefix_associatetransport) * (ge_second_ip_cancel_prefix_associatetransport))))) + (((((ge_first_ip_cancel_prefix_associatetransport) * (ge_second_rn_cancel_prefix_associatetransport))) + (((ge_first_in_cancel_prefix_associatetransport) * (ge_second_rp_cancel_prefix_associatetransport))))))) + ge_balance_positive_cancel_prefix_associatetransportoutputimaginary)))))))))))