gaussian_unit_inverse

Exact expanded first-order arithmetic statement

forall u. (exists gr_inverse_inverse_given. (exists ge_first_rp_inverse_givenidentity ge_first_rn_inverse_givenidentity ge_first_ip_inverse_givenidentity ge_first_in_inverse_givenidentity ge_second_rp_inverse_givenidentity ge_second_rn_inverse_givenidentity ge_second_ip_inverse_givenidentity ge_second_in_inverse_givenidentity. ((exists ge_representation_real_code_inverse_givenidentityfirst ge_representation_imaginary_code_inverse_givenidentityfirst. (((u) = ((ge_representation_real_code_inverse_givenidentityfirst) + (ge_representation_imaginary_code_inverse_givenidentityfirst)) * S ((ge_representation_real_code_inverse_givenidentityfirst) + (ge_representation_imaginary_code_inverse_givenidentityfirst)) + ((ge_representation_imaginary_code_inverse_givenidentityfirst) + (ge_representation_imaginary_code_inverse_givenidentityfirst))) /\ ((exists ge_balance_positive_inverse_givenidentityfirstreal ge_balance_negative_inverse_givenidentityfirstreal. (((((ge_representation_real_code_inverse_givenidentityfirst) = 2 * (ge_balance_positive_inverse_givenidentityfirstreal) /\ (ge_balance_negative_inverse_givenidentityfirstreal) = 0) \/ exists ge_signed_half_inverse_givenidentityfirstrealdecode. (((ge_representation_real_code_inverse_givenidentityfirst) = 2 * ge_signed_half_inverse_givenidentityfirstrealdecode + 1 /\ (ge_balance_positive_inverse_givenidentityfirstreal) = 0) /\ (ge_balance_negative_inverse_givenidentityfirstreal) = S ge_signed_half_inverse_givenidentityfirstrealdecode))) /\ ((ge_first_rp_inverse_givenidentity) + ge_balance_negative_inverse_givenidentityfirstreal = (ge_first_rn_inverse_givenidentity) + ge_balance_positive_inverse_givenidentityfirstreal))) /\ (exists ge_balance_positive_inverse_givenidentityfirstimaginary ge_balance_negative_inverse_givenidentityfirstimaginary. (((((ge_representation_imaginary_code_inverse_givenidentityfirst) = 2 * (ge_balance_positive_inverse_givenidentityfirstimaginary) /\ (ge_balance_negative_inverse_givenidentityfirstimaginary) = 0) \/ exists ge_signed_half_inverse_givenidentityfirstimaginarydecode. (((ge_representation_imaginary_code_inverse_givenidentityfirst) = 2 * ge_signed_half_inverse_givenidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_inverse_givenidentityfirstimaginary) = 0) /\ (ge_balance_negative_inverse_givenidentityfirstimaginary) = S ge_signed_half_inverse_givenidentityfirstimaginarydecode))) /\ ((ge_first_ip_inverse_givenidentity) + ge_balance_negative_inverse_givenidentityfirstimaginary = (ge_first_in_inverse_givenidentity) + ge_balance_positive_inverse_givenidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_inverse_givenidentitysecond ge_representation_imaginary_code_inverse_givenidentitysecond. (((gr_inverse_inverse_given) = ((ge_representation_real_code_inverse_givenidentitysecond) + (ge_representation_imaginary_code_inverse_givenidentitysecond)) * S ((ge_representation_real_code_inverse_givenidentitysecond) + (ge_representation_imaginary_code_inverse_givenidentitysecond)) + ((ge_representation_imaginary_code_inverse_givenidentitysecond) + (ge_representation_imaginary_code_inverse_givenidentitysecond))) /\ ((exists ge_balance_positive_inverse_givenidentitysecondreal ge_balance_negative_inverse_givenidentitysecondreal. (((((ge_representation_real_code_inverse_givenidentitysecond) = 2 * (ge_balance_positive_inverse_givenidentitysecondreal) /\ (ge_balance_negative_inverse_givenidentitysecondreal) = 0) \/ exists ge_signed_half_inverse_givenidentitysecondrealdecode. (((ge_representation_real_code_inverse_givenidentitysecond) = 2 * ge_signed_half_inverse_givenidentitysecondrealdecode + 1 /\ (ge_balance_positive_inverse_givenidentitysecondreal) = 0) /\ (ge_balance_negative_inverse_givenidentitysecondreal) = S ge_signed_half_inverse_givenidentitysecondrealdecode))) /\ ((ge_second_rp_inverse_givenidentity) + ge_balance_negative_inverse_givenidentitysecondreal = (ge_second_rn_inverse_givenidentity) + ge_balance_positive_inverse_givenidentitysecondreal))) /\ (exists ge_balance_positive_inverse_givenidentitysecondimaginary ge_balance_negative_inverse_givenidentitysecondimaginary. (((((ge_representation_imaginary_code_inverse_givenidentitysecond) = 2 * (ge_balance_positive_inverse_givenidentitysecondimaginary) /\ (ge_balance_negative_inverse_givenidentitysecondimaginary) = 0) \/ exists ge_signed_half_inverse_givenidentitysecondimaginarydecode. (((ge_representation_imaginary_code_inverse_givenidentitysecond) = 2 * ge_signed_half_inverse_givenidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_inverse_givenidentitysecondimaginary) = 0) /\ (ge_balance_negative_inverse_givenidentitysecondimaginary) = S ge_signed_half_inverse_givenidentitysecondimaginarydecode))) /\ ((ge_second_ip_inverse_givenidentity) + ge_balance_negative_inverse_givenidentitysecondimaginary = (ge_second_in_inverse_givenidentity) + ge_balance_positive_inverse_givenidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_inverse_givenidentityoutput ge_representation_imaginary_code_inverse_givenidentityoutput. (((6) = ((ge_representation_real_code_inverse_givenidentityoutput) + (ge_representation_imaginary_code_inverse_givenidentityoutput)) * S ((ge_representation_real_code_inverse_givenidentityoutput) + (ge_representation_imaginary_code_inverse_givenidentityoutput)) + ((ge_representation_imaginary_code_inverse_givenidentityoutput) + (ge_representation_imaginary_code_inverse_givenidentityoutput))) /\ ((exists ge_balance_positive_inverse_givenidentityoutputreal ge_balance_negative_inverse_givenidentityoutputreal. (((((ge_representation_real_code_inverse_givenidentityoutput) = 2 * (ge_balance_positive_inverse_givenidentityoutputreal) /\ (ge_balance_negative_inverse_givenidentityoutputreal) = 0) \/ exists ge_signed_half_inverse_givenidentityoutputrealdecode. (((ge_representation_real_code_inverse_givenidentityoutput) = 2 * ge_signed_half_inverse_givenidentityoutputrealdecode + 1 /\ (ge_balance_positive_inverse_givenidentityoutputreal) = 0) /\ (ge_balance_negative_inverse_givenidentityoutputreal) = S ge_signed_half_inverse_givenidentityoutputrealdecode))) /\ ((((((((ge_first_rp_inverse_givenidentity) * (ge_second_rp_inverse_givenidentity))) + (((ge_first_rn_inverse_givenidentity) * (ge_second_rn_inverse_givenidentity))))) + (((((ge_first_ip_inverse_givenidentity) * (ge_second_in_inverse_givenidentity))) + (((ge_first_in_inverse_givenidentity) * (ge_second_ip_inverse_givenidentity))))))) + ge_balance_negative_inverse_givenidentityoutputreal = (((((((ge_first_rp_inverse_givenidentity) * (ge_second_rn_inverse_givenidentity))) + (((ge_first_rn_inverse_givenidentity) * (ge_second_rp_inverse_givenidentity))))) + (((((ge_first_ip_inverse_givenidentity) * (ge_second_ip_inverse_givenidentity))) + (((ge_first_in_inverse_givenidentity) * (ge_second_in_inverse_givenidentity))))))) + ge_balance_positive_inverse_givenidentityoutputreal))) /\ (exists ge_balance_positive_inverse_givenidentityoutputimaginary ge_balance_negative_inverse_givenidentityoutputimaginary. (((((ge_representation_imaginary_code_inverse_givenidentityoutput) = 2 * (ge_balance_positive_inverse_givenidentityoutputimaginary) /\ (ge_balance_negative_inverse_givenidentityoutputimaginary) = 0) \/ exists ge_signed_half_inverse_givenidentityoutputimaginarydecode. (((ge_representation_imaginary_code_inverse_givenidentityoutput) = 2 * ge_signed_half_inverse_givenidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_inverse_givenidentityoutputimaginary) = 0) /\ (ge_balance_negative_inverse_givenidentityoutputimaginary) = S ge_signed_half_inverse_givenidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_inverse_givenidentity) * (ge_second_ip_inverse_givenidentity))) + (((ge_first_rn_inverse_givenidentity) * (ge_second_in_inverse_givenidentity))))) + (((((ge_first_ip_inverse_givenidentity) * (ge_second_rp_inverse_givenidentity))) + (((ge_first_in_inverse_givenidentity) * (ge_second_rn_inverse_givenidentity))))))) + ge_balance_negative_inverse_givenidentityoutputimaginary = (((((((ge_first_rp_inverse_givenidentity) * (ge_second_in_inverse_givenidentity))) + (((ge_first_rn_inverse_givenidentity) * (ge_second_ip_inverse_givenidentity))))) + (((((ge_first_ip_inverse_givenidentity) * (ge_second_rn_inverse_givenidentity))) + (((ge_first_in_inverse_givenidentity) * (ge_second_rp_inverse_givenidentity))))))) + ge_balance_positive_inverse_givenidentityoutputimaginary)))))))))) -> exists v. (exists gr_inverse_inverse_unit. (exists ge_first_rp_inverse_unitidentity ge_first_rn_inverse_unitidentity ge_first_ip_inverse_unitidentity ge_first_in_inverse_unitidentity ge_second_rp_inverse_unitidentity ge_second_rn_inverse_unitidentity ge_second_ip_inverse_unitidentity ge_second_in_inverse_unitidentity. ((exists ge_representation_real_code_inverse_unitidentityfirst ge_representation_imaginary_code_inverse_unitidentityfirst. (((v) = ((ge_representation_real_code_inverse_unitidentityfirst) + (ge_representation_imaginary_code_inverse_unitidentityfirst)) * S ((ge_representation_real_code_inverse_unitidentityfirst) + (ge_representation_imaginary_code_inverse_unitidentityfirst)) + ((ge_representation_imaginary_code_inverse_unitidentityfirst) + (ge_representation_imaginary_code_inverse_unitidentityfirst))) /\ ((exists ge_balance_positive_inverse_unitidentityfirstreal ge_balance_negative_inverse_unitidentityfirstreal. (((((ge_representation_real_code_inverse_unitidentityfirst) = 2 * (ge_balance_positive_inverse_unitidentityfirstreal) /\ (ge_balance_negative_inverse_unitidentityfirstreal) = 0) \/ exists ge_signed_half_inverse_unitidentityfirstrealdecode. (((ge_representation_real_code_inverse_unitidentityfirst) = 2 * ge_signed_half_inverse_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_inverse_unitidentityfirstreal) = 0) /\ (ge_balance_negative_inverse_unitidentityfirstreal) = S ge_signed_half_inverse_unitidentityfirstrealdecode))) /\ ((ge_first_rp_inverse_unitidentity) + ge_balance_negative_inverse_unitidentityfirstreal = (ge_first_rn_inverse_unitidentity) + ge_balance_positive_inverse_unitidentityfirstreal))) /\ (exists ge_balance_positive_inverse_unitidentityfirstimaginary ge_balance_negative_inverse_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_inverse_unitidentityfirst) = 2 * (ge_balance_positive_inverse_unitidentityfirstimaginary) /\ (ge_balance_negative_inverse_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_inverse_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_inverse_unitidentityfirst) = 2 * ge_signed_half_inverse_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_inverse_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_inverse_unitidentityfirstimaginary) = S ge_signed_half_inverse_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_inverse_unitidentity) + ge_balance_negative_inverse_unitidentityfirstimaginary = (ge_first_in_inverse_unitidentity) + ge_balance_positive_inverse_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_inverse_unitidentitysecond ge_representation_imaginary_code_inverse_unitidentitysecond. (((gr_inverse_inverse_unit) = ((ge_representation_real_code_inverse_unitidentitysecond) + (ge_representation_imaginary_code_inverse_unitidentitysecond)) * S ((ge_representation_real_code_inverse_unitidentitysecond) + (ge_representation_imaginary_code_inverse_unitidentitysecond)) + ((ge_representation_imaginary_code_inverse_unitidentitysecond) + (ge_representation_imaginary_code_inverse_unitidentitysecond))) /\ ((exists ge_balance_positive_inverse_unitidentitysecondreal ge_balance_negative_inverse_unitidentitysecondreal. (((((ge_representation_real_code_inverse_unitidentitysecond) = 2 * (ge_balance_positive_inverse_unitidentitysecondreal) /\ (ge_balance_negative_inverse_unitidentitysecondreal) = 0) \/ exists ge_signed_half_inverse_unitidentitysecondrealdecode. (((ge_representation_real_code_inverse_unitidentitysecond) = 2 * ge_signed_half_inverse_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_inverse_unitidentitysecondreal) = 0) /\ (ge_balance_negative_inverse_unitidentitysecondreal) = S ge_signed_half_inverse_unitidentitysecondrealdecode))) /\ ((ge_second_rp_inverse_unitidentity) + ge_balance_negative_inverse_unitidentitysecondreal = (ge_second_rn_inverse_unitidentity) + ge_balance_positive_inverse_unitidentitysecondreal))) /\ (exists ge_balance_positive_inverse_unitidentitysecondimaginary ge_balance_negative_inverse_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_inverse_unitidentitysecond) = 2 * (ge_balance_positive_inverse_unitidentitysecondimaginary) /\ (ge_balance_negative_inverse_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_inverse_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_inverse_unitidentitysecond) = 2 * ge_signed_half_inverse_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_inverse_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_inverse_unitidentitysecondimaginary) = S ge_signed_half_inverse_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_inverse_unitidentity) + ge_balance_negative_inverse_unitidentitysecondimaginary = (ge_second_in_inverse_unitidentity) + ge_balance_positive_inverse_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_inverse_unitidentityoutput ge_representation_imaginary_code_inverse_unitidentityoutput. (((6) = ((ge_representation_real_code_inverse_unitidentityoutput) + (ge_representation_imaginary_code_inverse_unitidentityoutput)) * S ((ge_representation_real_code_inverse_unitidentityoutput) + (ge_representation_imaginary_code_inverse_unitidentityoutput)) + ((ge_representation_imaginary_code_inverse_unitidentityoutput) + (ge_representation_imaginary_code_inverse_unitidentityoutput))) /\ ((exists ge_balance_positive_inverse_unitidentityoutputreal ge_balance_negative_inverse_unitidentityoutputreal. (((((ge_representation_real_code_inverse_unitidentityoutput) = 2 * (ge_balance_positive_inverse_unitidentityoutputreal) /\ (ge_balance_negative_inverse_unitidentityoutputreal) = 0) \/ exists ge_signed_half_inverse_unitidentityoutputrealdecode. (((ge_representation_real_code_inverse_unitidentityoutput) = 2 * ge_signed_half_inverse_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_inverse_unitidentityoutputreal) = 0) /\ (ge_balance_negative_inverse_unitidentityoutputreal) = S ge_signed_half_inverse_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_inverse_unitidentity) * (ge_second_rp_inverse_unitidentity))) + (((ge_first_rn_inverse_unitidentity) * (ge_second_rn_inverse_unitidentity))))) + (((((ge_first_ip_inverse_unitidentity) * (ge_second_in_inverse_unitidentity))) + (((ge_first_in_inverse_unitidentity) * (ge_second_ip_inverse_unitidentity))))))) + ge_balance_negative_inverse_unitidentityoutputreal = (((((((ge_first_rp_inverse_unitidentity) * (ge_second_rn_inverse_unitidentity))) + (((ge_first_rn_inverse_unitidentity) * (ge_second_rp_inverse_unitidentity))))) + (((((ge_first_ip_inverse_unitidentity) * (ge_second_ip_inverse_unitidentity))) + (((ge_first_in_inverse_unitidentity) * (ge_second_in_inverse_unitidentity))))))) + ge_balance_positive_inverse_unitidentityoutputreal))) /\ (exists ge_balance_positive_inverse_unitidentityoutputimaginary ge_balance_negative_inverse_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_inverse_unitidentityoutput) = 2 * (ge_balance_positive_inverse_unitidentityoutputimaginary) /\ (ge_balance_negative_inverse_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_inverse_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_inverse_unitidentityoutput) = 2 * ge_signed_half_inverse_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_inverse_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_inverse_unitidentityoutputimaginary) = S ge_signed_half_inverse_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_inverse_unitidentity) * (ge_second_ip_inverse_unitidentity))) + (((ge_first_rn_inverse_unitidentity) * (ge_second_in_inverse_unitidentity))))) + (((((ge_first_ip_inverse_unitidentity) * (ge_second_rp_inverse_unitidentity))) + (((ge_first_in_inverse_unitidentity) * (ge_second_rn_inverse_unitidentity))))))) + ge_balance_negative_inverse_unitidentityoutputimaginary = (((((((ge_first_rp_inverse_unitidentity) * (ge_second_in_inverse_unitidentity))) + (((ge_first_rn_inverse_unitidentity) * (ge_second_ip_inverse_unitidentity))))) + (((((ge_first_ip_inverse_unitidentity) * (ge_second_rn_inverse_unitidentity))) + (((ge_first_in_inverse_unitidentity) * (ge_second_rp_inverse_unitidentity))))))) + ge_balance_positive_inverse_unitidentityoutputimaginary)))))))))) /\ ((exists ge_first_rp_inverse_first ge_first_rn_inverse_first ge_first_ip_inverse_first ge_first_in_inverse_first ge_second_rp_inverse_first ge_second_rn_inverse_first ge_second_ip_inverse_first ge_second_in_inverse_first. ((exists ge_representation_real_code_inverse_firstfirst ge_representation_imaginary_code_inverse_firstfirst. (((u) = ((ge_representation_real_code_inverse_firstfirst) + (ge_representation_imaginary_code_inverse_firstfirst)) * S ((ge_representation_real_code_inverse_firstfirst) + (ge_representation_imaginary_code_inverse_firstfirst)) + ((ge_representation_imaginary_code_inverse_firstfirst) + (ge_representation_imaginary_code_inverse_firstfirst))) /\ ((exists ge_balance_positive_inverse_firstfirstreal ge_balance_negative_inverse_firstfirstreal. (((((ge_representation_real_code_inverse_firstfirst) = 2 * (ge_balance_positive_inverse_firstfirstreal) /\ (ge_balance_negative_inverse_firstfirstreal) = 0) \/ exists ge_signed_half_inverse_firstfirstrealdecode. (((ge_representation_real_code_inverse_firstfirst) = 2 * ge_signed_half_inverse_firstfirstrealdecode + 1 /\ (ge_balance_positive_inverse_firstfirstreal) = 0) /\ (ge_balance_negative_inverse_firstfirstreal) = S ge_signed_half_inverse_firstfirstrealdecode))) /\ ((ge_first_rp_inverse_first) + ge_balance_negative_inverse_firstfirstreal = (ge_first_rn_inverse_first) + ge_balance_positive_inverse_firstfirstreal))) /\ (exists ge_balance_positive_inverse_firstfirstimaginary ge_balance_negative_inverse_firstfirstimaginary. (((((ge_representation_imaginary_code_inverse_firstfirst) = 2 * (ge_balance_positive_inverse_firstfirstimaginary) /\ (ge_balance_negative_inverse_firstfirstimaginary) = 0) \/ exists ge_signed_half_inverse_firstfirstimaginarydecode. (((ge_representation_imaginary_code_inverse_firstfirst) = 2 * ge_signed_half_inverse_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_inverse_firstfirstimaginary) = 0) /\ (ge_balance_negative_inverse_firstfirstimaginary) = S ge_signed_half_inverse_firstfirstimaginarydecode))) /\ ((ge_first_ip_inverse_first) + ge_balance_negative_inverse_firstfirstimaginary = (ge_first_in_inverse_first) + ge_balance_positive_inverse_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_inverse_firstsecond ge_representation_imaginary_code_inverse_firstsecond. (((v) = ((ge_representation_real_code_inverse_firstsecond) + (ge_representation_imaginary_code_inverse_firstsecond)) * S ((ge_representation_real_code_inverse_firstsecond) + (ge_representation_imaginary_code_inverse_firstsecond)) + ((ge_representation_imaginary_code_inverse_firstsecond) + (ge_representation_imaginary_code_inverse_firstsecond))) /\ ((exists ge_balance_positive_inverse_firstsecondreal ge_balance_negative_inverse_firstsecondreal. (((((ge_representation_real_code_inverse_firstsecond) = 2 * (ge_balance_positive_inverse_firstsecondreal) /\ (ge_balance_negative_inverse_firstsecondreal) = 0) \/ exists ge_signed_half_inverse_firstsecondrealdecode. (((ge_representation_real_code_inverse_firstsecond) = 2 * ge_signed_half_inverse_firstsecondrealdecode + 1 /\ (ge_balance_positive_inverse_firstsecondreal) = 0) /\ (ge_balance_negative_inverse_firstsecondreal) = S ge_signed_half_inverse_firstsecondrealdecode))) /\ ((ge_second_rp_inverse_first) + ge_balance_negative_inverse_firstsecondreal = (ge_second_rn_inverse_first) + ge_balance_positive_inverse_firstsecondreal))) /\ (exists ge_balance_positive_inverse_firstsecondimaginary ge_balance_negative_inverse_firstsecondimaginary. (((((ge_representation_imaginary_code_inverse_firstsecond) = 2 * (ge_balance_positive_inverse_firstsecondimaginary) /\ (ge_balance_negative_inverse_firstsecondimaginary) = 0) \/ exists ge_signed_half_inverse_firstsecondimaginarydecode. (((ge_representation_imaginary_code_inverse_firstsecond) = 2 * ge_signed_half_inverse_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_inverse_firstsecondimaginary) = 0) /\ (ge_balance_negative_inverse_firstsecondimaginary) = S ge_signed_half_inverse_firstsecondimaginarydecode))) /\ ((ge_second_ip_inverse_first) + ge_balance_negative_inverse_firstsecondimaginary = (ge_second_in_inverse_first) + ge_balance_positive_inverse_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_inverse_firstoutput ge_representation_imaginary_code_inverse_firstoutput. (((6) = ((ge_representation_real_code_inverse_firstoutput) + (ge_representation_imaginary_code_inverse_firstoutput)) * S ((ge_representation_real_code_inverse_firstoutput) + (ge_representation_imaginary_code_inverse_firstoutput)) + ((ge_representation_imaginary_code_inverse_firstoutput) + (ge_representation_imaginary_code_inverse_firstoutput))) /\ ((exists ge_balance_positive_inverse_firstoutputreal ge_balance_negative_inverse_firstoutputreal. (((((ge_representation_real_code_inverse_firstoutput) = 2 * (ge_balance_positive_inverse_firstoutputreal) /\ (ge_balance_negative_inverse_firstoutputreal) = 0) \/ exists ge_signed_half_inverse_firstoutputrealdecode. (((ge_representation_real_code_inverse_firstoutput) = 2 * ge_signed_half_inverse_firstoutputrealdecode + 1 /\ (ge_balance_positive_inverse_firstoutputreal) = 0) /\ (ge_balance_negative_inverse_firstoutputreal) = S ge_signed_half_inverse_firstoutputrealdecode))) /\ ((((((((ge_first_rp_inverse_first) * (ge_second_rp_inverse_first))) + (((ge_first_rn_inverse_first) * (ge_second_rn_inverse_first))))) + (((((ge_first_ip_inverse_first) * (ge_second_in_inverse_first))) + (((ge_first_in_inverse_first) * (ge_second_ip_inverse_first))))))) + ge_balance_negative_inverse_firstoutputreal = (((((((ge_first_rp_inverse_first) * (ge_second_rn_inverse_first))) + (((ge_first_rn_inverse_first) * (ge_second_rp_inverse_first))))) + (((((ge_first_ip_inverse_first) * (ge_second_ip_inverse_first))) + (((ge_first_in_inverse_first) * (ge_second_in_inverse_first))))))) + ge_balance_positive_inverse_firstoutputreal))) /\ (exists ge_balance_positive_inverse_firstoutputimaginary ge_balance_negative_inverse_firstoutputimaginary. (((((ge_representation_imaginary_code_inverse_firstoutput) = 2 * (ge_balance_positive_inverse_firstoutputimaginary) /\ (ge_balance_negative_inverse_firstoutputimaginary) = 0) \/ exists ge_signed_half_inverse_firstoutputimaginarydecode. (((ge_representation_imaginary_code_inverse_firstoutput) = 2 * ge_signed_half_inverse_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_inverse_firstoutputimaginary) = 0) /\ (ge_balance_negative_inverse_firstoutputimaginary) = S ge_signed_half_inverse_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_inverse_first) * (ge_second_ip_inverse_first))) + (((ge_first_rn_inverse_first) * (ge_second_in_inverse_first))))) + (((((ge_first_ip_inverse_first) * (ge_second_rp_inverse_first))) + (((ge_first_in_inverse_first) * (ge_second_rn_inverse_first))))))) + ge_balance_negative_inverse_firstoutputimaginary = (((((((ge_first_rp_inverse_first) * (ge_second_in_inverse_first))) + (((ge_first_rn_inverse_first) * (ge_second_ip_inverse_first))))) + (((((ge_first_ip_inverse_first) * (ge_second_rn_inverse_first))) + (((ge_first_in_inverse_first) * (ge_second_rp_inverse_first))))))) + ge_balance_positive_inverse_firstoutputimaginary))))))))) /\ (exists ge_first_rp_inverse_second ge_first_rn_inverse_second ge_first_ip_inverse_second ge_first_in_inverse_second ge_second_rp_inverse_second ge_second_rn_inverse_second ge_second_ip_inverse_second ge_second_in_inverse_second. ((exists ge_representation_real_code_inverse_secondfirst ge_representation_imaginary_code_inverse_secondfirst. (((v) = ((ge_representation_real_code_inverse_secondfirst) + (ge_representation_imaginary_code_inverse_secondfirst)) * S ((ge_representation_real_code_inverse_secondfirst) + (ge_representation_imaginary_code_inverse_secondfirst)) + ((ge_representation_imaginary_code_inverse_secondfirst) + (ge_representation_imaginary_code_inverse_secondfirst))) /\ ((exists ge_balance_positive_inverse_secondfirstreal ge_balance_negative_inverse_secondfirstreal. (((((ge_representation_real_code_inverse_secondfirst) = 2 * (ge_balance_positive_inverse_secondfirstreal) /\ (ge_balance_negative_inverse_secondfirstreal) = 0) \/ exists ge_signed_half_inverse_secondfirstrealdecode. (((ge_representation_real_code_inverse_secondfirst) = 2 * ge_signed_half_inverse_secondfirstrealdecode + 1 /\ (ge_balance_positive_inverse_secondfirstreal) = 0) /\ (ge_balance_negative_inverse_secondfirstreal) = S ge_signed_half_inverse_secondfirstrealdecode))) /\ ((ge_first_rp_inverse_second) + ge_balance_negative_inverse_secondfirstreal = (ge_first_rn_inverse_second) + ge_balance_positive_inverse_secondfirstreal))) /\ (exists ge_balance_positive_inverse_secondfirstimaginary ge_balance_negative_inverse_secondfirstimaginary. (((((ge_representation_imaginary_code_inverse_secondfirst) = 2 * (ge_balance_positive_inverse_secondfirstimaginary) /\ (ge_balance_negative_inverse_secondfirstimaginary) = 0) \/ exists ge_signed_half_inverse_secondfirstimaginarydecode. (((ge_representation_imaginary_code_inverse_secondfirst) = 2 * ge_signed_half_inverse_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_inverse_secondfirstimaginary) = 0) /\ (ge_balance_negative_inverse_secondfirstimaginary) = S ge_signed_half_inverse_secondfirstimaginarydecode))) /\ ((ge_first_ip_inverse_second) + ge_balance_negative_inverse_secondfirstimaginary = (ge_first_in_inverse_second) + ge_balance_positive_inverse_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_inverse_secondsecond ge_representation_imaginary_code_inverse_secondsecond. (((u) = ((ge_representation_real_code_inverse_secondsecond) + (ge_representation_imaginary_code_inverse_secondsecond)) * S ((ge_representation_real_code_inverse_secondsecond) + (ge_representation_imaginary_code_inverse_secondsecond)) + ((ge_representation_imaginary_code_inverse_secondsecond) + (ge_representation_imaginary_code_inverse_secondsecond))) /\ ((exists ge_balance_positive_inverse_secondsecondreal ge_balance_negative_inverse_secondsecondreal. (((((ge_representation_real_code_inverse_secondsecond) = 2 * (ge_balance_positive_inverse_secondsecondreal) /\ (ge_balance_negative_inverse_secondsecondreal) = 0) \/ exists ge_signed_half_inverse_secondsecondrealdecode. (((ge_representation_real_code_inverse_secondsecond) = 2 * ge_signed_half_inverse_secondsecondrealdecode + 1 /\ (ge_balance_positive_inverse_secondsecondreal) = 0) /\ (ge_balance_negative_inverse_secondsecondreal) = S ge_signed_half_inverse_secondsecondrealdecode))) /\ ((ge_second_rp_inverse_second) + ge_balance_negative_inverse_secondsecondreal = (ge_second_rn_inverse_second) + ge_balance_positive_inverse_secondsecondreal))) /\ (exists ge_balance_positive_inverse_secondsecondimaginary ge_balance_negative_inverse_secondsecondimaginary. (((((ge_representation_imaginary_code_inverse_secondsecond) = 2 * (ge_balance_positive_inverse_secondsecondimaginary) /\ (ge_balance_negative_inverse_secondsecondimaginary) = 0) \/ exists ge_signed_half_inverse_secondsecondimaginarydecode. (((ge_representation_imaginary_code_inverse_secondsecond) = 2 * ge_signed_half_inverse_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_inverse_secondsecondimaginary) = 0) /\ (ge_balance_negative_inverse_secondsecondimaginary) = S ge_signed_half_inverse_secondsecondimaginarydecode))) /\ ((ge_second_ip_inverse_second) + ge_balance_negative_inverse_secondsecondimaginary = (ge_second_in_inverse_second) + ge_balance_positive_inverse_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_inverse_secondoutput ge_representation_imaginary_code_inverse_secondoutput. (((6) = ((ge_representation_real_code_inverse_secondoutput) + (ge_representation_imaginary_code_inverse_secondoutput)) * S ((ge_representation_real_code_inverse_secondoutput) + (ge_representation_imaginary_code_inverse_secondoutput)) + ((ge_representation_imaginary_code_inverse_secondoutput) + (ge_representation_imaginary_code_inverse_secondoutput))) /\ ((exists ge_balance_positive_inverse_secondoutputreal ge_balance_negative_inverse_secondoutputreal. (((((ge_representation_real_code_inverse_secondoutput) = 2 * (ge_balance_positive_inverse_secondoutputreal) /\ (ge_balance_negative_inverse_secondoutputreal) = 0) \/ exists ge_signed_half_inverse_secondoutputrealdecode. (((ge_representation_real_code_inverse_secondoutput) = 2 * ge_signed_half_inverse_secondoutputrealdecode + 1 /\ (ge_balance_positive_inverse_secondoutputreal) = 0) /\ (ge_balance_negative_inverse_secondoutputreal) = S ge_signed_half_inverse_secondoutputrealdecode))) /\ ((((((((ge_first_rp_inverse_second) * (ge_second_rp_inverse_second))) + (((ge_first_rn_inverse_second) * (ge_second_rn_inverse_second))))) + (((((ge_first_ip_inverse_second) * (ge_second_in_inverse_second))) + (((ge_first_in_inverse_second) * (ge_second_ip_inverse_second))))))) + ge_balance_negative_inverse_secondoutputreal = (((((((ge_first_rp_inverse_second) * (ge_second_rn_inverse_second))) + (((ge_first_rn_inverse_second) * (ge_second_rp_inverse_second))))) + (((((ge_first_ip_inverse_second) * (ge_second_ip_inverse_second))) + (((ge_first_in_inverse_second) * (ge_second_in_inverse_second))))))) + ge_balance_positive_inverse_secondoutputreal))) /\ (exists ge_balance_positive_inverse_secondoutputimaginary ge_balance_negative_inverse_secondoutputimaginary. (((((ge_representation_imaginary_code_inverse_secondoutput) = 2 * (ge_balance_positive_inverse_secondoutputimaginary) /\ (ge_balance_negative_inverse_secondoutputimaginary) = 0) \/ exists ge_signed_half_inverse_secondoutputimaginarydecode. (((ge_representation_imaginary_code_inverse_secondoutput) = 2 * ge_signed_half_inverse_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_inverse_secondoutputimaginary) = 0) /\ (ge_balance_negative_inverse_secondoutputimaginary) = S ge_signed_half_inverse_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_inverse_second) * (ge_second_ip_inverse_second))) + (((ge_first_rn_inverse_second) * (ge_second_in_inverse_second))))) + (((((ge_first_ip_inverse_second) * (ge_second_rp_inverse_second))) + (((ge_first_in_inverse_second) * (ge_second_rn_inverse_second))))))) + ge_balance_negative_inverse_secondoutputimaginary = (((((((ge_first_rp_inverse_second) * (ge_second_in_inverse_second))) + (((ge_first_rn_inverse_second) * (ge_second_ip_inverse_second))))) + (((((ge_first_ip_inverse_second) * (ge_second_rn_inverse_second))) + (((ge_first_in_inverse_second) * (ge_second_rp_inverse_second))))))) + ge_balance_positive_inverse_secondoutputimaginary))))))))))