gaussian_unit_factor_left

Exact expanded first-order arithmetic statement

forall a b c. (exists ge_first_rp_unit_factor_product ge_first_rn_unit_factor_product ge_first_ip_unit_factor_product ge_first_in_unit_factor_product ge_second_rp_unit_factor_product ge_second_rn_unit_factor_product ge_second_ip_unit_factor_product ge_second_in_unit_factor_product. ((exists ge_representation_real_code_unit_factor_productfirst ge_representation_imaginary_code_unit_factor_productfirst. (((a) = ((ge_representation_real_code_unit_factor_productfirst) + (ge_representation_imaginary_code_unit_factor_productfirst)) * S ((ge_representation_real_code_unit_factor_productfirst) + (ge_representation_imaginary_code_unit_factor_productfirst)) + ((ge_representation_imaginary_code_unit_factor_productfirst) + (ge_representation_imaginary_code_unit_factor_productfirst))) /\ ((exists ge_balance_positive_unit_factor_productfirstreal ge_balance_negative_unit_factor_productfirstreal. (((((ge_representation_real_code_unit_factor_productfirst) = 2 * (ge_balance_positive_unit_factor_productfirstreal) /\ (ge_balance_negative_unit_factor_productfirstreal) = 0) \/ exists ge_signed_half_unit_factor_productfirstrealdecode. (((ge_representation_real_code_unit_factor_productfirst) = 2 * ge_signed_half_unit_factor_productfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_productfirstreal) = 0) /\ (ge_balance_negative_unit_factor_productfirstreal) = S ge_signed_half_unit_factor_productfirstrealdecode))) /\ ((ge_first_rp_unit_factor_product) + ge_balance_negative_unit_factor_productfirstreal = (ge_first_rn_unit_factor_product) + ge_balance_positive_unit_factor_productfirstreal))) /\ (exists ge_balance_positive_unit_factor_productfirstimaginary ge_balance_negative_unit_factor_productfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_productfirst) = 2 * (ge_balance_positive_unit_factor_productfirstimaginary) /\ (ge_balance_negative_unit_factor_productfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_productfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_productfirst) = 2 * ge_signed_half_unit_factor_productfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_productfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_productfirstimaginary) = S ge_signed_half_unit_factor_productfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_product) + ge_balance_negative_unit_factor_productfirstimaginary = (ge_first_in_unit_factor_product) + ge_balance_positive_unit_factor_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_productsecond ge_representation_imaginary_code_unit_factor_productsecond. (((b) = ((ge_representation_real_code_unit_factor_productsecond) + (ge_representation_imaginary_code_unit_factor_productsecond)) * S ((ge_representation_real_code_unit_factor_productsecond) + (ge_representation_imaginary_code_unit_factor_productsecond)) + ((ge_representation_imaginary_code_unit_factor_productsecond) + (ge_representation_imaginary_code_unit_factor_productsecond))) /\ ((exists ge_balance_positive_unit_factor_productsecondreal ge_balance_negative_unit_factor_productsecondreal. (((((ge_representation_real_code_unit_factor_productsecond) = 2 * (ge_balance_positive_unit_factor_productsecondreal) /\ (ge_balance_negative_unit_factor_productsecondreal) = 0) \/ exists ge_signed_half_unit_factor_productsecondrealdecode. (((ge_representation_real_code_unit_factor_productsecond) = 2 * ge_signed_half_unit_factor_productsecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_productsecondreal) = 0) /\ (ge_balance_negative_unit_factor_productsecondreal) = S ge_signed_half_unit_factor_productsecondrealdecode))) /\ ((ge_second_rp_unit_factor_product) + ge_balance_negative_unit_factor_productsecondreal = (ge_second_rn_unit_factor_product) + ge_balance_positive_unit_factor_productsecondreal))) /\ (exists ge_balance_positive_unit_factor_productsecondimaginary ge_balance_negative_unit_factor_productsecondimaginary. (((((ge_representation_imaginary_code_unit_factor_productsecond) = 2 * (ge_balance_positive_unit_factor_productsecondimaginary) /\ (ge_balance_negative_unit_factor_productsecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_productsecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_productsecond) = 2 * ge_signed_half_unit_factor_productsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_productsecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_productsecondimaginary) = S ge_signed_half_unit_factor_productsecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_product) + ge_balance_negative_unit_factor_productsecondimaginary = (ge_second_in_unit_factor_product) + ge_balance_positive_unit_factor_productsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_productoutput ge_representation_imaginary_code_unit_factor_productoutput. (((c) = ((ge_representation_real_code_unit_factor_productoutput) + (ge_representation_imaginary_code_unit_factor_productoutput)) * S ((ge_representation_real_code_unit_factor_productoutput) + (ge_representation_imaginary_code_unit_factor_productoutput)) + ((ge_representation_imaginary_code_unit_factor_productoutput) + (ge_representation_imaginary_code_unit_factor_productoutput))) /\ ((exists ge_balance_positive_unit_factor_productoutputreal ge_balance_negative_unit_factor_productoutputreal. (((((ge_representation_real_code_unit_factor_productoutput) = 2 * (ge_balance_positive_unit_factor_productoutputreal) /\ (ge_balance_negative_unit_factor_productoutputreal) = 0) \/ exists ge_signed_half_unit_factor_productoutputrealdecode. (((ge_representation_real_code_unit_factor_productoutput) = 2 * ge_signed_half_unit_factor_productoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_productoutputreal) = 0) /\ (ge_balance_negative_unit_factor_productoutputreal) = S ge_signed_half_unit_factor_productoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_product) * (ge_second_rp_unit_factor_product))) + (((ge_first_rn_unit_factor_product) * (ge_second_rn_unit_factor_product))))) + (((((ge_first_ip_unit_factor_product) * (ge_second_in_unit_factor_product))) + (((ge_first_in_unit_factor_product) * (ge_second_ip_unit_factor_product))))))) + ge_balance_negative_unit_factor_productoutputreal = (((((((ge_first_rp_unit_factor_product) * (ge_second_rn_unit_factor_product))) + (((ge_first_rn_unit_factor_product) * (ge_second_rp_unit_factor_product))))) + (((((ge_first_ip_unit_factor_product) * (ge_second_ip_unit_factor_product))) + (((ge_first_in_unit_factor_product) * (ge_second_in_unit_factor_product))))))) + ge_balance_positive_unit_factor_productoutputreal))) /\ (exists ge_balance_positive_unit_factor_productoutputimaginary ge_balance_negative_unit_factor_productoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_productoutput) = 2 * (ge_balance_positive_unit_factor_productoutputimaginary) /\ (ge_balance_negative_unit_factor_productoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_productoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_productoutput) = 2 * ge_signed_half_unit_factor_productoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_productoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_productoutputimaginary) = S ge_signed_half_unit_factor_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_product) * (ge_second_ip_unit_factor_product))) + (((ge_first_rn_unit_factor_product) * (ge_second_in_unit_factor_product))))) + (((((ge_first_ip_unit_factor_product) * (ge_second_rp_unit_factor_product))) + (((ge_first_in_unit_factor_product) * (ge_second_rn_unit_factor_product))))))) + ge_balance_negative_unit_factor_productoutputimaginary = (((((((ge_first_rp_unit_factor_product) * (ge_second_in_unit_factor_product))) + (((ge_first_rn_unit_factor_product) * (ge_second_ip_unit_factor_product))))) + (((((ge_first_ip_unit_factor_product) * (ge_second_rn_unit_factor_product))) + (((ge_first_in_unit_factor_product) * (ge_second_rp_unit_factor_product))))))) + ge_balance_positive_unit_factor_productoutputimaginary))))))))) -> (exists gr_inverse_unit_factor_whole. (exists ge_first_rp_unit_factor_wholeidentity ge_first_rn_unit_factor_wholeidentity ge_first_ip_unit_factor_wholeidentity ge_first_in_unit_factor_wholeidentity ge_second_rp_unit_factor_wholeidentity ge_second_rn_unit_factor_wholeidentity ge_second_ip_unit_factor_wholeidentity ge_second_in_unit_factor_wholeidentity. ((exists ge_representation_real_code_unit_factor_wholeidentityfirst ge_representation_imaginary_code_unit_factor_wholeidentityfirst. (((c) = ((ge_representation_real_code_unit_factor_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_wholeidentityfirst)) * S ((ge_representation_real_code_unit_factor_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_wholeidentityfirst)) + ((ge_representation_imaginary_code_unit_factor_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_wholeidentityfirst))) /\ ((exists ge_balance_positive_unit_factor_wholeidentityfirstreal ge_balance_negative_unit_factor_wholeidentityfirstreal. (((((ge_representation_real_code_unit_factor_wholeidentityfirst) = 2 * (ge_balance_positive_unit_factor_wholeidentityfirstreal) /\ (ge_balance_negative_unit_factor_wholeidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factor_wholeidentityfirstrealdecode. (((ge_representation_real_code_unit_factor_wholeidentityfirst) = 2 * ge_signed_half_unit_factor_wholeidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factor_wholeidentityfirstreal) = S ge_signed_half_unit_factor_wholeidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factor_wholeidentity) + ge_balance_negative_unit_factor_wholeidentityfirstreal = (ge_first_rn_unit_factor_wholeidentity) + ge_balance_positive_unit_factor_wholeidentityfirstreal))) /\ (exists ge_balance_positive_unit_factor_wholeidentityfirstimaginary ge_balance_negative_unit_factor_wholeidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_wholeidentityfirst) = 2 * (ge_balance_positive_unit_factor_wholeidentityfirstimaginary) /\ (ge_balance_negative_unit_factor_wholeidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_wholeidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_wholeidentityfirst) = 2 * ge_signed_half_unit_factor_wholeidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_wholeidentityfirstimaginary) = S ge_signed_half_unit_factor_wholeidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_wholeidentity) + ge_balance_negative_unit_factor_wholeidentityfirstimaginary = (ge_first_in_unit_factor_wholeidentity) + ge_balance_positive_unit_factor_wholeidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_wholeidentitysecond ge_representation_imaginary_code_unit_factor_wholeidentitysecond. (((gr_inverse_unit_factor_whole) = ((ge_representation_real_code_unit_factor_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_wholeidentitysecond)) * S ((ge_representation_real_code_unit_factor_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_wholeidentitysecond)) + ((ge_representation_imaginary_code_unit_factor_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_wholeidentitysecond))) /\ ((exists ge_balance_positive_unit_factor_wholeidentitysecondreal ge_balance_negative_unit_factor_wholeidentitysecondreal. (((((ge_representation_real_code_unit_factor_wholeidentitysecond) = 2 * (ge_balance_positive_unit_factor_wholeidentitysecondreal) /\ (ge_balance_negative_unit_factor_wholeidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factor_wholeidentitysecondrealdecode. (((ge_representation_real_code_unit_factor_wholeidentitysecond) = 2 * ge_signed_half_unit_factor_wholeidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factor_wholeidentitysecondreal) = S ge_signed_half_unit_factor_wholeidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factor_wholeidentity) + ge_balance_negative_unit_factor_wholeidentitysecondreal = (ge_second_rn_unit_factor_wholeidentity) + ge_balance_positive_unit_factor_wholeidentitysecondreal))) /\ (exists ge_balance_positive_unit_factor_wholeidentitysecondimaginary ge_balance_negative_unit_factor_wholeidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factor_wholeidentitysecond) = 2 * (ge_balance_positive_unit_factor_wholeidentitysecondimaginary) /\ (ge_balance_negative_unit_factor_wholeidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_wholeidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_wholeidentitysecond) = 2 * ge_signed_half_unit_factor_wholeidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_wholeidentitysecondimaginary) = S ge_signed_half_unit_factor_wholeidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_wholeidentity) + ge_balance_negative_unit_factor_wholeidentitysecondimaginary = (ge_second_in_unit_factor_wholeidentity) + ge_balance_positive_unit_factor_wholeidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_wholeidentityoutput ge_representation_imaginary_code_unit_factor_wholeidentityoutput. (((6) = ((ge_representation_real_code_unit_factor_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_wholeidentityoutput)) * S ((ge_representation_real_code_unit_factor_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_wholeidentityoutput)) + ((ge_representation_imaginary_code_unit_factor_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_wholeidentityoutput))) /\ ((exists ge_balance_positive_unit_factor_wholeidentityoutputreal ge_balance_negative_unit_factor_wholeidentityoutputreal. (((((ge_representation_real_code_unit_factor_wholeidentityoutput) = 2 * (ge_balance_positive_unit_factor_wholeidentityoutputreal) /\ (ge_balance_negative_unit_factor_wholeidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factor_wholeidentityoutputrealdecode. (((ge_representation_real_code_unit_factor_wholeidentityoutput) = 2 * ge_signed_half_unit_factor_wholeidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factor_wholeidentityoutputreal) = S ge_signed_half_unit_factor_wholeidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_wholeidentity) * (ge_second_rp_unit_factor_wholeidentity))) + (((ge_first_rn_unit_factor_wholeidentity) * (ge_second_rn_unit_factor_wholeidentity))))) + (((((ge_first_ip_unit_factor_wholeidentity) * (ge_second_in_unit_factor_wholeidentity))) + (((ge_first_in_unit_factor_wholeidentity) * (ge_second_ip_unit_factor_wholeidentity))))))) + ge_balance_negative_unit_factor_wholeidentityoutputreal = (((((((ge_first_rp_unit_factor_wholeidentity) * (ge_second_rn_unit_factor_wholeidentity))) + (((ge_first_rn_unit_factor_wholeidentity) * (ge_second_rp_unit_factor_wholeidentity))))) + (((((ge_first_ip_unit_factor_wholeidentity) * (ge_second_ip_unit_factor_wholeidentity))) + (((ge_first_in_unit_factor_wholeidentity) * (ge_second_in_unit_factor_wholeidentity))))))) + ge_balance_positive_unit_factor_wholeidentityoutputreal))) /\ (exists ge_balance_positive_unit_factor_wholeidentityoutputimaginary ge_balance_negative_unit_factor_wholeidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_wholeidentityoutput) = 2 * (ge_balance_positive_unit_factor_wholeidentityoutputimaginary) /\ (ge_balance_negative_unit_factor_wholeidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_wholeidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_wholeidentityoutput) = 2 * ge_signed_half_unit_factor_wholeidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_wholeidentityoutputimaginary) = S ge_signed_half_unit_factor_wholeidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_wholeidentity) * (ge_second_ip_unit_factor_wholeidentity))) + (((ge_first_rn_unit_factor_wholeidentity) * (ge_second_in_unit_factor_wholeidentity))))) + (((((ge_first_ip_unit_factor_wholeidentity) * (ge_second_rp_unit_factor_wholeidentity))) + (((ge_first_in_unit_factor_wholeidentity) * (ge_second_rn_unit_factor_wholeidentity))))))) + ge_balance_negative_unit_factor_wholeidentityoutputimaginary = (((((((ge_first_rp_unit_factor_wholeidentity) * (ge_second_in_unit_factor_wholeidentity))) + (((ge_first_rn_unit_factor_wholeidentity) * (ge_second_ip_unit_factor_wholeidentity))))) + (((((ge_first_ip_unit_factor_wholeidentity) * (ge_second_rn_unit_factor_wholeidentity))) + (((ge_first_in_unit_factor_wholeidentity) * (ge_second_rp_unit_factor_wholeidentity))))))) + ge_balance_positive_unit_factor_wholeidentityoutputimaginary)))))))))) -> (exists gr_inverse_unit_factor_first. (exists ge_first_rp_unit_factor_firstidentity ge_first_rn_unit_factor_firstidentity ge_first_ip_unit_factor_firstidentity ge_first_in_unit_factor_firstidentity ge_second_rp_unit_factor_firstidentity ge_second_rn_unit_factor_firstidentity ge_second_ip_unit_factor_firstidentity ge_second_in_unit_factor_firstidentity. ((exists ge_representation_real_code_unit_factor_firstidentityfirst ge_representation_imaginary_code_unit_factor_firstidentityfirst. (((a) = ((ge_representation_real_code_unit_factor_firstidentityfirst) + (ge_representation_imaginary_code_unit_factor_firstidentityfirst)) * S ((ge_representation_real_code_unit_factor_firstidentityfirst) + (ge_representation_imaginary_code_unit_factor_firstidentityfirst)) + ((ge_representation_imaginary_code_unit_factor_firstidentityfirst) + (ge_representation_imaginary_code_unit_factor_firstidentityfirst))) /\ ((exists ge_balance_positive_unit_factor_firstidentityfirstreal ge_balance_negative_unit_factor_firstidentityfirstreal. (((((ge_representation_real_code_unit_factor_firstidentityfirst) = 2 * (ge_balance_positive_unit_factor_firstidentityfirstreal) /\ (ge_balance_negative_unit_factor_firstidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factor_firstidentityfirstrealdecode. (((ge_representation_real_code_unit_factor_firstidentityfirst) = 2 * ge_signed_half_unit_factor_firstidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_firstidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factor_firstidentityfirstreal) = S ge_signed_half_unit_factor_firstidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factor_firstidentity) + ge_balance_negative_unit_factor_firstidentityfirstreal = (ge_first_rn_unit_factor_firstidentity) + ge_balance_positive_unit_factor_firstidentityfirstreal))) /\ (exists ge_balance_positive_unit_factor_firstidentityfirstimaginary ge_balance_negative_unit_factor_firstidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_firstidentityfirst) = 2 * (ge_balance_positive_unit_factor_firstidentityfirstimaginary) /\ (ge_balance_negative_unit_factor_firstidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_firstidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_firstidentityfirst) = 2 * ge_signed_half_unit_factor_firstidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_firstidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_firstidentityfirstimaginary) = S ge_signed_half_unit_factor_firstidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_firstidentity) + ge_balance_negative_unit_factor_firstidentityfirstimaginary = (ge_first_in_unit_factor_firstidentity) + ge_balance_positive_unit_factor_firstidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_firstidentitysecond ge_representation_imaginary_code_unit_factor_firstidentitysecond. (((gr_inverse_unit_factor_first) = ((ge_representation_real_code_unit_factor_firstidentitysecond) + (ge_representation_imaginary_code_unit_factor_firstidentitysecond)) * S ((ge_representation_real_code_unit_factor_firstidentitysecond) + (ge_representation_imaginary_code_unit_factor_firstidentitysecond)) + ((ge_representation_imaginary_code_unit_factor_firstidentitysecond) + (ge_representation_imaginary_code_unit_factor_firstidentitysecond))) /\ ((exists ge_balance_positive_unit_factor_firstidentitysecondreal ge_balance_negative_unit_factor_firstidentitysecondreal. (((((ge_representation_real_code_unit_factor_firstidentitysecond) = 2 * (ge_balance_positive_unit_factor_firstidentitysecondreal) /\ (ge_balance_negative_unit_factor_firstidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factor_firstidentitysecondrealdecode. (((ge_representation_real_code_unit_factor_firstidentitysecond) = 2 * ge_signed_half_unit_factor_firstidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_firstidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factor_firstidentitysecondreal) = S ge_signed_half_unit_factor_firstidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factor_firstidentity) + ge_balance_negative_unit_factor_firstidentitysecondreal = (ge_second_rn_unit_factor_firstidentity) + ge_balance_positive_unit_factor_firstidentitysecondreal))) /\ (exists ge_balance_positive_unit_factor_firstidentitysecondimaginary ge_balance_negative_unit_factor_firstidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factor_firstidentitysecond) = 2 * (ge_balance_positive_unit_factor_firstidentitysecondimaginary) /\ (ge_balance_negative_unit_factor_firstidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_firstidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_firstidentitysecond) = 2 * ge_signed_half_unit_factor_firstidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_firstidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_firstidentitysecondimaginary) = S ge_signed_half_unit_factor_firstidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_firstidentity) + ge_balance_negative_unit_factor_firstidentitysecondimaginary = (ge_second_in_unit_factor_firstidentity) + ge_balance_positive_unit_factor_firstidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_firstidentityoutput ge_representation_imaginary_code_unit_factor_firstidentityoutput. (((6) = ((ge_representation_real_code_unit_factor_firstidentityoutput) + (ge_representation_imaginary_code_unit_factor_firstidentityoutput)) * S ((ge_representation_real_code_unit_factor_firstidentityoutput) + (ge_representation_imaginary_code_unit_factor_firstidentityoutput)) + ((ge_representation_imaginary_code_unit_factor_firstidentityoutput) + (ge_representation_imaginary_code_unit_factor_firstidentityoutput))) /\ ((exists ge_balance_positive_unit_factor_firstidentityoutputreal ge_balance_negative_unit_factor_firstidentityoutputreal. (((((ge_representation_real_code_unit_factor_firstidentityoutput) = 2 * (ge_balance_positive_unit_factor_firstidentityoutputreal) /\ (ge_balance_negative_unit_factor_firstidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factor_firstidentityoutputrealdecode. (((ge_representation_real_code_unit_factor_firstidentityoutput) = 2 * ge_signed_half_unit_factor_firstidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_firstidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factor_firstidentityoutputreal) = S ge_signed_half_unit_factor_firstidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_firstidentity) * (ge_second_rp_unit_factor_firstidentity))) + (((ge_first_rn_unit_factor_firstidentity) * (ge_second_rn_unit_factor_firstidentity))))) + (((((ge_first_ip_unit_factor_firstidentity) * (ge_second_in_unit_factor_firstidentity))) + (((ge_first_in_unit_factor_firstidentity) * (ge_second_ip_unit_factor_firstidentity))))))) + ge_balance_negative_unit_factor_firstidentityoutputreal = (((((((ge_first_rp_unit_factor_firstidentity) * (ge_second_rn_unit_factor_firstidentity))) + (((ge_first_rn_unit_factor_firstidentity) * (ge_second_rp_unit_factor_firstidentity))))) + (((((ge_first_ip_unit_factor_firstidentity) * (ge_second_ip_unit_factor_firstidentity))) + (((ge_first_in_unit_factor_firstidentity) * (ge_second_in_unit_factor_firstidentity))))))) + ge_balance_positive_unit_factor_firstidentityoutputreal))) /\ (exists ge_balance_positive_unit_factor_firstidentityoutputimaginary ge_balance_negative_unit_factor_firstidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_firstidentityoutput) = 2 * (ge_balance_positive_unit_factor_firstidentityoutputimaginary) /\ (ge_balance_negative_unit_factor_firstidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_firstidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_firstidentityoutput) = 2 * ge_signed_half_unit_factor_firstidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_firstidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_firstidentityoutputimaginary) = S ge_signed_half_unit_factor_firstidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_firstidentity) * (ge_second_ip_unit_factor_firstidentity))) + (((ge_first_rn_unit_factor_firstidentity) * (ge_second_in_unit_factor_firstidentity))))) + (((((ge_first_ip_unit_factor_firstidentity) * (ge_second_rp_unit_factor_firstidentity))) + (((ge_first_in_unit_factor_firstidentity) * (ge_second_rn_unit_factor_firstidentity))))))) + ge_balance_negative_unit_factor_firstidentityoutputimaginary = (((((((ge_first_rp_unit_factor_firstidentity) * (ge_second_in_unit_factor_firstidentity))) + (((ge_first_rn_unit_factor_firstidentity) * (ge_second_ip_unit_factor_firstidentity))))) + (((((ge_first_ip_unit_factor_firstidentity) * (ge_second_rn_unit_factor_firstidentity))) + (((ge_first_in_unit_factor_firstidentity) * (ge_second_rp_unit_factor_firstidentity))))))) + ge_balance_positive_unit_factor_firstidentityoutputimaginary))))))))))