gaussian_unit_factor_right

Exact expanded first-order arithmetic statement

forall a b c. (exists ge_first_rp_unit_factor_right_product ge_first_rn_unit_factor_right_product ge_first_ip_unit_factor_right_product ge_first_in_unit_factor_right_product ge_second_rp_unit_factor_right_product ge_second_rn_unit_factor_right_product ge_second_ip_unit_factor_right_product ge_second_in_unit_factor_right_product. ((exists ge_representation_real_code_unit_factor_right_productfirst ge_representation_imaginary_code_unit_factor_right_productfirst. (((a) = ((ge_representation_real_code_unit_factor_right_productfirst) + (ge_representation_imaginary_code_unit_factor_right_productfirst)) * S ((ge_representation_real_code_unit_factor_right_productfirst) + (ge_representation_imaginary_code_unit_factor_right_productfirst)) + ((ge_representation_imaginary_code_unit_factor_right_productfirst) + (ge_representation_imaginary_code_unit_factor_right_productfirst))) /\ ((exists ge_balance_positive_unit_factor_right_productfirstreal ge_balance_negative_unit_factor_right_productfirstreal. (((((ge_representation_real_code_unit_factor_right_productfirst) = 2 * (ge_balance_positive_unit_factor_right_productfirstreal) /\ (ge_balance_negative_unit_factor_right_productfirstreal) = 0) \/ exists ge_signed_half_unit_factor_right_productfirstrealdecode. (((ge_representation_real_code_unit_factor_right_productfirst) = 2 * ge_signed_half_unit_factor_right_productfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_right_productfirstreal) = 0) /\ (ge_balance_negative_unit_factor_right_productfirstreal) = S ge_signed_half_unit_factor_right_productfirstrealdecode))) /\ ((ge_first_rp_unit_factor_right_product) + ge_balance_negative_unit_factor_right_productfirstreal = (ge_first_rn_unit_factor_right_product) + ge_balance_positive_unit_factor_right_productfirstreal))) /\ (exists ge_balance_positive_unit_factor_right_productfirstimaginary ge_balance_negative_unit_factor_right_productfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_right_productfirst) = 2 * (ge_balance_positive_unit_factor_right_productfirstimaginary) /\ (ge_balance_negative_unit_factor_right_productfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_right_productfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_right_productfirst) = 2 * ge_signed_half_unit_factor_right_productfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_right_productfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_right_productfirstimaginary) = S ge_signed_half_unit_factor_right_productfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_right_product) + ge_balance_negative_unit_factor_right_productfirstimaginary = (ge_first_in_unit_factor_right_product) + ge_balance_positive_unit_factor_right_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_right_productsecond ge_representation_imaginary_code_unit_factor_right_productsecond. (((b) = ((ge_representation_real_code_unit_factor_right_productsecond) + (ge_representation_imaginary_code_unit_factor_right_productsecond)) * S ((ge_representation_real_code_unit_factor_right_productsecond) + (ge_representation_imaginary_code_unit_factor_right_productsecond)) + ((ge_representation_imaginary_code_unit_factor_right_productsecond) + (ge_representation_imaginary_code_unit_factor_right_productsecond))) /\ ((exists ge_balance_positive_unit_factor_right_productsecondreal ge_balance_negative_unit_factor_right_productsecondreal. (((((ge_representation_real_code_unit_factor_right_productsecond) = 2 * (ge_balance_positive_unit_factor_right_productsecondreal) /\ (ge_balance_negative_unit_factor_right_productsecondreal) = 0) \/ exists ge_signed_half_unit_factor_right_productsecondrealdecode. (((ge_representation_real_code_unit_factor_right_productsecond) = 2 * ge_signed_half_unit_factor_right_productsecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_right_productsecondreal) = 0) /\ (ge_balance_negative_unit_factor_right_productsecondreal) = S ge_signed_half_unit_factor_right_productsecondrealdecode))) /\ ((ge_second_rp_unit_factor_right_product) + ge_balance_negative_unit_factor_right_productsecondreal = (ge_second_rn_unit_factor_right_product) + ge_balance_positive_unit_factor_right_productsecondreal))) /\ (exists ge_balance_positive_unit_factor_right_productsecondimaginary ge_balance_negative_unit_factor_right_productsecondimaginary. (((((ge_representation_imaginary_code_unit_factor_right_productsecond) = 2 * (ge_balance_positive_unit_factor_right_productsecondimaginary) /\ (ge_balance_negative_unit_factor_right_productsecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_right_productsecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_right_productsecond) = 2 * ge_signed_half_unit_factor_right_productsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_right_productsecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_right_productsecondimaginary) = S ge_signed_half_unit_factor_right_productsecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_right_product) + ge_balance_negative_unit_factor_right_productsecondimaginary = (ge_second_in_unit_factor_right_product) + ge_balance_positive_unit_factor_right_productsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_right_productoutput ge_representation_imaginary_code_unit_factor_right_productoutput. (((c) = ((ge_representation_real_code_unit_factor_right_productoutput) + (ge_representation_imaginary_code_unit_factor_right_productoutput)) * S ((ge_representation_real_code_unit_factor_right_productoutput) + (ge_representation_imaginary_code_unit_factor_right_productoutput)) + ((ge_representation_imaginary_code_unit_factor_right_productoutput) + (ge_representation_imaginary_code_unit_factor_right_productoutput))) /\ ((exists ge_balance_positive_unit_factor_right_productoutputreal ge_balance_negative_unit_factor_right_productoutputreal. (((((ge_representation_real_code_unit_factor_right_productoutput) = 2 * (ge_balance_positive_unit_factor_right_productoutputreal) /\ (ge_balance_negative_unit_factor_right_productoutputreal) = 0) \/ exists ge_signed_half_unit_factor_right_productoutputrealdecode. (((ge_representation_real_code_unit_factor_right_productoutput) = 2 * ge_signed_half_unit_factor_right_productoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_right_productoutputreal) = 0) /\ (ge_balance_negative_unit_factor_right_productoutputreal) = S ge_signed_half_unit_factor_right_productoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_right_product) * (ge_second_rp_unit_factor_right_product))) + (((ge_first_rn_unit_factor_right_product) * (ge_second_rn_unit_factor_right_product))))) + (((((ge_first_ip_unit_factor_right_product) * (ge_second_in_unit_factor_right_product))) + (((ge_first_in_unit_factor_right_product) * (ge_second_ip_unit_factor_right_product))))))) + ge_balance_negative_unit_factor_right_productoutputreal = (((((((ge_first_rp_unit_factor_right_product) * (ge_second_rn_unit_factor_right_product))) + (((ge_first_rn_unit_factor_right_product) * (ge_second_rp_unit_factor_right_product))))) + (((((ge_first_ip_unit_factor_right_product) * (ge_second_ip_unit_factor_right_product))) + (((ge_first_in_unit_factor_right_product) * (ge_second_in_unit_factor_right_product))))))) + ge_balance_positive_unit_factor_right_productoutputreal))) /\ (exists ge_balance_positive_unit_factor_right_productoutputimaginary ge_balance_negative_unit_factor_right_productoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_right_productoutput) = 2 * (ge_balance_positive_unit_factor_right_productoutputimaginary) /\ (ge_balance_negative_unit_factor_right_productoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_right_productoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_right_productoutput) = 2 * ge_signed_half_unit_factor_right_productoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_right_productoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_right_productoutputimaginary) = S ge_signed_half_unit_factor_right_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_right_product) * (ge_second_ip_unit_factor_right_product))) + (((ge_first_rn_unit_factor_right_product) * (ge_second_in_unit_factor_right_product))))) + (((((ge_first_ip_unit_factor_right_product) * (ge_second_rp_unit_factor_right_product))) + (((ge_first_in_unit_factor_right_product) * (ge_second_rn_unit_factor_right_product))))))) + ge_balance_negative_unit_factor_right_productoutputimaginary = (((((((ge_first_rp_unit_factor_right_product) * (ge_second_in_unit_factor_right_product))) + (((ge_first_rn_unit_factor_right_product) * (ge_second_ip_unit_factor_right_product))))) + (((((ge_first_ip_unit_factor_right_product) * (ge_second_rn_unit_factor_right_product))) + (((ge_first_in_unit_factor_right_product) * (ge_second_rp_unit_factor_right_product))))))) + ge_balance_positive_unit_factor_right_productoutputimaginary))))))))) -> (exists gr_inverse_unit_factor_right_whole. (exists ge_first_rp_unit_factor_right_wholeidentity ge_first_rn_unit_factor_right_wholeidentity ge_first_ip_unit_factor_right_wholeidentity ge_first_in_unit_factor_right_wholeidentity ge_second_rp_unit_factor_right_wholeidentity ge_second_rn_unit_factor_right_wholeidentity ge_second_ip_unit_factor_right_wholeidentity ge_second_in_unit_factor_right_wholeidentity. ((exists ge_representation_real_code_unit_factor_right_wholeidentityfirst ge_representation_imaginary_code_unit_factor_right_wholeidentityfirst. (((c) = ((ge_representation_real_code_unit_factor_right_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_right_wholeidentityfirst)) * S ((ge_representation_real_code_unit_factor_right_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_right_wholeidentityfirst)) + ((ge_representation_imaginary_code_unit_factor_right_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_right_wholeidentityfirst))) /\ ((exists ge_balance_positive_unit_factor_right_wholeidentityfirstreal ge_balance_negative_unit_factor_right_wholeidentityfirstreal. (((((ge_representation_real_code_unit_factor_right_wholeidentityfirst) = 2 * (ge_balance_positive_unit_factor_right_wholeidentityfirstreal) /\ (ge_balance_negative_unit_factor_right_wholeidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factor_right_wholeidentityfirstrealdecode. (((ge_representation_real_code_unit_factor_right_wholeidentityfirst) = 2 * ge_signed_half_unit_factor_right_wholeidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_right_wholeidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factor_right_wholeidentityfirstreal) = S ge_signed_half_unit_factor_right_wholeidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factor_right_wholeidentity) + ge_balance_negative_unit_factor_right_wholeidentityfirstreal = (ge_first_rn_unit_factor_right_wholeidentity) + ge_balance_positive_unit_factor_right_wholeidentityfirstreal))) /\ (exists ge_balance_positive_unit_factor_right_wholeidentityfirstimaginary ge_balance_negative_unit_factor_right_wholeidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_right_wholeidentityfirst) = 2 * (ge_balance_positive_unit_factor_right_wholeidentityfirstimaginary) /\ (ge_balance_negative_unit_factor_right_wholeidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_right_wholeidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_right_wholeidentityfirst) = 2 * ge_signed_half_unit_factor_right_wholeidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_right_wholeidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_right_wholeidentityfirstimaginary) = S ge_signed_half_unit_factor_right_wholeidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_right_wholeidentity) + ge_balance_negative_unit_factor_right_wholeidentityfirstimaginary = (ge_first_in_unit_factor_right_wholeidentity) + ge_balance_positive_unit_factor_right_wholeidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_right_wholeidentitysecond ge_representation_imaginary_code_unit_factor_right_wholeidentitysecond. (((gr_inverse_unit_factor_right_whole) = ((ge_representation_real_code_unit_factor_right_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_right_wholeidentitysecond)) * S ((ge_representation_real_code_unit_factor_right_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_right_wholeidentitysecond)) + ((ge_representation_imaginary_code_unit_factor_right_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_right_wholeidentitysecond))) /\ ((exists ge_balance_positive_unit_factor_right_wholeidentitysecondreal ge_balance_negative_unit_factor_right_wholeidentitysecondreal. (((((ge_representation_real_code_unit_factor_right_wholeidentitysecond) = 2 * (ge_balance_positive_unit_factor_right_wholeidentitysecondreal) /\ (ge_balance_negative_unit_factor_right_wholeidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factor_right_wholeidentitysecondrealdecode. (((ge_representation_real_code_unit_factor_right_wholeidentitysecond) = 2 * ge_signed_half_unit_factor_right_wholeidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_right_wholeidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factor_right_wholeidentitysecondreal) = S ge_signed_half_unit_factor_right_wholeidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factor_right_wholeidentity) + ge_balance_negative_unit_factor_right_wholeidentitysecondreal = (ge_second_rn_unit_factor_right_wholeidentity) + ge_balance_positive_unit_factor_right_wholeidentitysecondreal))) /\ (exists ge_balance_positive_unit_factor_right_wholeidentitysecondimaginary ge_balance_negative_unit_factor_right_wholeidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factor_right_wholeidentitysecond) = 2 * (ge_balance_positive_unit_factor_right_wholeidentitysecondimaginary) /\ (ge_balance_negative_unit_factor_right_wholeidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_right_wholeidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_right_wholeidentitysecond) = 2 * ge_signed_half_unit_factor_right_wholeidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_right_wholeidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_right_wholeidentitysecondimaginary) = S ge_signed_half_unit_factor_right_wholeidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_right_wholeidentity) + ge_balance_negative_unit_factor_right_wholeidentitysecondimaginary = (ge_second_in_unit_factor_right_wholeidentity) + ge_balance_positive_unit_factor_right_wholeidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_right_wholeidentityoutput ge_representation_imaginary_code_unit_factor_right_wholeidentityoutput. (((6) = ((ge_representation_real_code_unit_factor_right_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_right_wholeidentityoutput)) * S ((ge_representation_real_code_unit_factor_right_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_right_wholeidentityoutput)) + ((ge_representation_imaginary_code_unit_factor_right_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_right_wholeidentityoutput))) /\ ((exists ge_balance_positive_unit_factor_right_wholeidentityoutputreal ge_balance_negative_unit_factor_right_wholeidentityoutputreal. (((((ge_representation_real_code_unit_factor_right_wholeidentityoutput) = 2 * (ge_balance_positive_unit_factor_right_wholeidentityoutputreal) /\ (ge_balance_negative_unit_factor_right_wholeidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factor_right_wholeidentityoutputrealdecode. (((ge_representation_real_code_unit_factor_right_wholeidentityoutput) = 2 * ge_signed_half_unit_factor_right_wholeidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_right_wholeidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factor_right_wholeidentityoutputreal) = S ge_signed_half_unit_factor_right_wholeidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_right_wholeidentity) * (ge_second_rp_unit_factor_right_wholeidentity))) + (((ge_first_rn_unit_factor_right_wholeidentity) * (ge_second_rn_unit_factor_right_wholeidentity))))) + (((((ge_first_ip_unit_factor_right_wholeidentity) * (ge_second_in_unit_factor_right_wholeidentity))) + (((ge_first_in_unit_factor_right_wholeidentity) * (ge_second_ip_unit_factor_right_wholeidentity))))))) + ge_balance_negative_unit_factor_right_wholeidentityoutputreal = (((((((ge_first_rp_unit_factor_right_wholeidentity) * (ge_second_rn_unit_factor_right_wholeidentity))) + (((ge_first_rn_unit_factor_right_wholeidentity) * (ge_second_rp_unit_factor_right_wholeidentity))))) + (((((ge_first_ip_unit_factor_right_wholeidentity) * (ge_second_ip_unit_factor_right_wholeidentity))) + (((ge_first_in_unit_factor_right_wholeidentity) * (ge_second_in_unit_factor_right_wholeidentity))))))) + ge_balance_positive_unit_factor_right_wholeidentityoutputreal))) /\ (exists ge_balance_positive_unit_factor_right_wholeidentityoutputimaginary ge_balance_negative_unit_factor_right_wholeidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_right_wholeidentityoutput) = 2 * (ge_balance_positive_unit_factor_right_wholeidentityoutputimaginary) /\ (ge_balance_negative_unit_factor_right_wholeidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_right_wholeidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_right_wholeidentityoutput) = 2 * ge_signed_half_unit_factor_right_wholeidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_right_wholeidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_right_wholeidentityoutputimaginary) = S ge_signed_half_unit_factor_right_wholeidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_right_wholeidentity) * (ge_second_ip_unit_factor_right_wholeidentity))) + (((ge_first_rn_unit_factor_right_wholeidentity) * (ge_second_in_unit_factor_right_wholeidentity))))) + (((((ge_first_ip_unit_factor_right_wholeidentity) * (ge_second_rp_unit_factor_right_wholeidentity))) + (((ge_first_in_unit_factor_right_wholeidentity) * (ge_second_rn_unit_factor_right_wholeidentity))))))) + ge_balance_negative_unit_factor_right_wholeidentityoutputimaginary = (((((((ge_first_rp_unit_factor_right_wholeidentity) * (ge_second_in_unit_factor_right_wholeidentity))) + (((ge_first_rn_unit_factor_right_wholeidentity) * (ge_second_ip_unit_factor_right_wholeidentity))))) + (((((ge_first_ip_unit_factor_right_wholeidentity) * (ge_second_rn_unit_factor_right_wholeidentity))) + (((ge_first_in_unit_factor_right_wholeidentity) * (ge_second_rp_unit_factor_right_wholeidentity))))))) + ge_balance_positive_unit_factor_right_wholeidentityoutputimaginary)))))))))) -> (exists gr_inverse_unit_factor_second. (exists ge_first_rp_unit_factor_secondidentity ge_first_rn_unit_factor_secondidentity ge_first_ip_unit_factor_secondidentity ge_first_in_unit_factor_secondidentity ge_second_rp_unit_factor_secondidentity ge_second_rn_unit_factor_secondidentity ge_second_ip_unit_factor_secondidentity ge_second_in_unit_factor_secondidentity. ((exists ge_representation_real_code_unit_factor_secondidentityfirst ge_representation_imaginary_code_unit_factor_secondidentityfirst. (((b) = ((ge_representation_real_code_unit_factor_secondidentityfirst) + (ge_representation_imaginary_code_unit_factor_secondidentityfirst)) * S ((ge_representation_real_code_unit_factor_secondidentityfirst) + (ge_representation_imaginary_code_unit_factor_secondidentityfirst)) + ((ge_representation_imaginary_code_unit_factor_secondidentityfirst) + (ge_representation_imaginary_code_unit_factor_secondidentityfirst))) /\ ((exists ge_balance_positive_unit_factor_secondidentityfirstreal ge_balance_negative_unit_factor_secondidentityfirstreal. (((((ge_representation_real_code_unit_factor_secondidentityfirst) = 2 * (ge_balance_positive_unit_factor_secondidentityfirstreal) /\ (ge_balance_negative_unit_factor_secondidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factor_secondidentityfirstrealdecode. (((ge_representation_real_code_unit_factor_secondidentityfirst) = 2 * ge_signed_half_unit_factor_secondidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_secondidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factor_secondidentityfirstreal) = S ge_signed_half_unit_factor_secondidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factor_secondidentity) + ge_balance_negative_unit_factor_secondidentityfirstreal = (ge_first_rn_unit_factor_secondidentity) + ge_balance_positive_unit_factor_secondidentityfirstreal))) /\ (exists ge_balance_positive_unit_factor_secondidentityfirstimaginary ge_balance_negative_unit_factor_secondidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_secondidentityfirst) = 2 * (ge_balance_positive_unit_factor_secondidentityfirstimaginary) /\ (ge_balance_negative_unit_factor_secondidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_secondidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_secondidentityfirst) = 2 * ge_signed_half_unit_factor_secondidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_secondidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_secondidentityfirstimaginary) = S ge_signed_half_unit_factor_secondidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_secondidentity) + ge_balance_negative_unit_factor_secondidentityfirstimaginary = (ge_first_in_unit_factor_secondidentity) + ge_balance_positive_unit_factor_secondidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_secondidentitysecond ge_representation_imaginary_code_unit_factor_secondidentitysecond. (((gr_inverse_unit_factor_second) = ((ge_representation_real_code_unit_factor_secondidentitysecond) + (ge_representation_imaginary_code_unit_factor_secondidentitysecond)) * S ((ge_representation_real_code_unit_factor_secondidentitysecond) + (ge_representation_imaginary_code_unit_factor_secondidentitysecond)) + ((ge_representation_imaginary_code_unit_factor_secondidentitysecond) + (ge_representation_imaginary_code_unit_factor_secondidentitysecond))) /\ ((exists ge_balance_positive_unit_factor_secondidentitysecondreal ge_balance_negative_unit_factor_secondidentitysecondreal. (((((ge_representation_real_code_unit_factor_secondidentitysecond) = 2 * (ge_balance_positive_unit_factor_secondidentitysecondreal) /\ (ge_balance_negative_unit_factor_secondidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factor_secondidentitysecondrealdecode. (((ge_representation_real_code_unit_factor_secondidentitysecond) = 2 * ge_signed_half_unit_factor_secondidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_secondidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factor_secondidentitysecondreal) = S ge_signed_half_unit_factor_secondidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factor_secondidentity) + ge_balance_negative_unit_factor_secondidentitysecondreal = (ge_second_rn_unit_factor_secondidentity) + ge_balance_positive_unit_factor_secondidentitysecondreal))) /\ (exists ge_balance_positive_unit_factor_secondidentitysecondimaginary ge_balance_negative_unit_factor_secondidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factor_secondidentitysecond) = 2 * (ge_balance_positive_unit_factor_secondidentitysecondimaginary) /\ (ge_balance_negative_unit_factor_secondidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_secondidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_secondidentitysecond) = 2 * ge_signed_half_unit_factor_secondidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_secondidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_secondidentitysecondimaginary) = S ge_signed_half_unit_factor_secondidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_secondidentity) + ge_balance_negative_unit_factor_secondidentitysecondimaginary = (ge_second_in_unit_factor_secondidentity) + ge_balance_positive_unit_factor_secondidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_secondidentityoutput ge_representation_imaginary_code_unit_factor_secondidentityoutput. (((6) = ((ge_representation_real_code_unit_factor_secondidentityoutput) + (ge_representation_imaginary_code_unit_factor_secondidentityoutput)) * S ((ge_representation_real_code_unit_factor_secondidentityoutput) + (ge_representation_imaginary_code_unit_factor_secondidentityoutput)) + ((ge_representation_imaginary_code_unit_factor_secondidentityoutput) + (ge_representation_imaginary_code_unit_factor_secondidentityoutput))) /\ ((exists ge_balance_positive_unit_factor_secondidentityoutputreal ge_balance_negative_unit_factor_secondidentityoutputreal. (((((ge_representation_real_code_unit_factor_secondidentityoutput) = 2 * (ge_balance_positive_unit_factor_secondidentityoutputreal) /\ (ge_balance_negative_unit_factor_secondidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factor_secondidentityoutputrealdecode. (((ge_representation_real_code_unit_factor_secondidentityoutput) = 2 * ge_signed_half_unit_factor_secondidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_secondidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factor_secondidentityoutputreal) = S ge_signed_half_unit_factor_secondidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_secondidentity) * (ge_second_rp_unit_factor_secondidentity))) + (((ge_first_rn_unit_factor_secondidentity) * (ge_second_rn_unit_factor_secondidentity))))) + (((((ge_first_ip_unit_factor_secondidentity) * (ge_second_in_unit_factor_secondidentity))) + (((ge_first_in_unit_factor_secondidentity) * (ge_second_ip_unit_factor_secondidentity))))))) + ge_balance_negative_unit_factor_secondidentityoutputreal = (((((((ge_first_rp_unit_factor_secondidentity) * (ge_second_rn_unit_factor_secondidentity))) + (((ge_first_rn_unit_factor_secondidentity) * (ge_second_rp_unit_factor_secondidentity))))) + (((((ge_first_ip_unit_factor_secondidentity) * (ge_second_ip_unit_factor_secondidentity))) + (((ge_first_in_unit_factor_secondidentity) * (ge_second_in_unit_factor_secondidentity))))))) + ge_balance_positive_unit_factor_secondidentityoutputreal))) /\ (exists ge_balance_positive_unit_factor_secondidentityoutputimaginary ge_balance_negative_unit_factor_secondidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_secondidentityoutput) = 2 * (ge_balance_positive_unit_factor_secondidentityoutputimaginary) /\ (ge_balance_negative_unit_factor_secondidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_secondidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_secondidentityoutput) = 2 * ge_signed_half_unit_factor_secondidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_secondidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_secondidentityoutputimaginary) = S ge_signed_half_unit_factor_secondidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_secondidentity) * (ge_second_ip_unit_factor_secondidentity))) + (((ge_first_rn_unit_factor_secondidentity) * (ge_second_in_unit_factor_secondidentity))))) + (((((ge_first_ip_unit_factor_secondidentity) * (ge_second_rp_unit_factor_secondidentity))) + (((ge_first_in_unit_factor_secondidentity) * (ge_second_rn_unit_factor_secondidentity))))))) + ge_balance_negative_unit_factor_secondidentityoutputimaginary = (((((((ge_first_rp_unit_factor_secondidentity) * (ge_second_in_unit_factor_secondidentity))) + (((ge_first_rn_unit_factor_secondidentity) * (ge_second_ip_unit_factor_secondidentity))))) + (((((ge_first_ip_unit_factor_secondidentity) * (ge_second_rn_unit_factor_secondidentity))) + (((ge_first_in_unit_factor_secondidentity) * (ge_second_rp_unit_factor_secondidentity))))))) + ge_balance_positive_unit_factor_secondidentityoutputimaginary))))))))))