gaussian_multiply_swap_tail

forall a b c ab ac t. (exists ge_first_rp_swap_first ge_first_rn_swap_first ge_first_ip_swap_first ge_first_in_swap_first ge_second_rp_swap_first ge_second_rn_swap_first ge_second_ip_swap_first ge_second_in_swap_first. ((exists ge_representation_real_code_swap_firstfirst ge_representation_imaginary_code_swap_firstfirst. (((a) = ((ge_representation_real_code_swap_firstfirst) + (ge_representation_imaginary_code_swap_firstfirst)) * S ((ge_representation_real_code_swap_firstfirst) + (ge_representation_imaginary_code_swap_firstfirst)) + ((ge_representation_imaginary_code_swap_firstfirst) + (ge_representation_imaginary_code_swap_firstfirst))) /\ ((exists ge_balance_positive_swap_firstfirstreal ge_balance_negative_swap_firstfirstreal. (((((ge_representation_real_code_swap_firstfirst) = 2 * (ge_balance_positive_swap_firstfirstreal) /\ (ge_balance_negative_swap_firstfirstreal) = 0) \/ exists ge_signed_half_swap_firstfirstrealdecode. (((ge_representation_real_code_swap_firstfirst) = 2 * ge_signed_half_swap_firstfirstrealdecode + 1 /\ (ge_balance_positive_swap_firstfirstreal) = 0) /\ (ge_balance_negative_swap_firstfirstreal) = S ge_signed_half_swap_firstfirstrealdecode))) /\ ((ge_first_rp_swap_first) + ge_balance_negative_swap_firstfirstreal = (ge_first_rn_swap_first) + ge_balance_positive_swap_firstfirstreal))) /\ (exists ge_balance_positive_swap_firstfirstimaginary ge_balance_negative_swap_firstfirstimaginary. (((((ge_representation_imaginary_code_swap_firstfirst) = 2 * (ge_balance_positive_swap_firstfirstimaginary) /\ (ge_balance_negative_swap_firstfirstimaginary) = 0) \/ exists ge_signed_half_swap_firstfirstimaginarydecode. (((ge_representation_imaginary_code_swap_firstfirst) = 2 * ge_signed_half_swap_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_firstfirstimaginary) = 0) /\ (ge_balance_negative_swap_firstfirstimaginary) = S ge_signed_half_swap_firstfirstimaginarydecode))) /\ ((ge_first_ip_swap_first) + ge_balance_negative_swap_firstfirstimaginary = (ge_first_in_swap_first) + ge_balance_positive_swap_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_firstsecond ge_representation_imaginary_code_swap_firstsecond. (((b) = ((ge_representation_real_code_swap_firstsecond) + (ge_representation_imaginary_code_swap_firstsecond)) * S ((ge_representation_real_code_swap_firstsecond) + (ge_representation_imaginary_code_swap_firstsecond)) + ((ge_representation_imaginary_code_swap_firstsecond) + (ge_representation_imaginary_code_swap_firstsecond))) /\ ((exists ge_balance_positive_swap_firstsecondreal ge_balance_negative_swap_firstsecondreal. (((((ge_representation_real_code_swap_firstsecond) = 2 * (ge_balance_positive_swap_firstsecondreal) /\ (ge_balance_negative_swap_firstsecondreal) = 0) \/ exists ge_signed_half_swap_firstsecondrealdecode. (((ge_representation_real_code_swap_firstsecond) = 2 * ge_signed_half_swap_firstsecondrealdecode + 1 /\ (ge_balance_positive_swap_firstsecondreal) = 0) /\ (ge_balance_negative_swap_firstsecondreal) = S ge_signed_half_swap_firstsecondrealdecode))) /\ ((ge_second_rp_swap_first) + ge_balance_negative_swap_firstsecondreal = (ge_second_rn_swap_first) + ge_balance_positive_swap_firstsecondreal))) /\ (exists ge_balance_positive_swap_firstsecondimaginary ge_balance_negative_swap_firstsecondimaginary. (((((ge_representation_imaginary_code_swap_firstsecond) = 2 * (ge_balance_positive_swap_firstsecondimaginary) /\ (ge_balance_negative_swap_firstsecondimaginary) = 0) \/ exists ge_signed_half_swap_firstsecondimaginarydecode. (((ge_representation_imaginary_code_swap_firstsecond) = 2 * ge_signed_half_swap_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_firstsecondimaginary) = 0) /\ (ge_balance_negative_swap_firstsecondimaginary) = S ge_signed_half_swap_firstsecondimaginarydecode))) /\ ((ge_second_ip_swap_first) + ge_balance_negative_swap_firstsecondimaginary = (ge_second_in_swap_first) + ge_balance_positive_swap_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_firstoutput ge_representation_imaginary_code_swap_firstoutput. (((ab) = ((ge_representation_real_code_swap_firstoutput) + (ge_representation_imaginary_code_swap_firstoutput)) * S ((ge_representation_real_code_swap_firstoutput) + (ge_representation_imaginary_code_swap_firstoutput)) + ((ge_representation_imaginary_code_swap_firstoutput) + (ge_representation_imaginary_code_swap_firstoutput))) /\ ((exists ge_balance_positive_swap_firstoutputreal ge_balance_negative_swap_firstoutputreal. (((((ge_representation_real_code_swap_firstoutput) = 2 * (ge_balance_positive_swap_firstoutputreal) /\ (ge_balance_negative_swap_firstoutputreal) = 0) \/ exists ge_signed_half_swap_firstoutputrealdecode. (((ge_representation_real_code_swap_firstoutput) = 2 * ge_signed_half_swap_firstoutputrealdecode + 1 /\ (ge_balance_positive_swap_firstoutputreal) = 0) /\ (ge_balance_negative_swap_firstoutputreal) = S ge_signed_half_swap_firstoutputrealdecode))) /\ ((((((((ge_first_rp_swap_first) * (ge_second_rp_swap_first))) + (((ge_first_rn_swap_first) * (ge_second_rn_swap_first))))) + (((((ge_first_ip_swap_first) * (ge_second_in_swap_first))) + (((ge_first_in_swap_first) * (ge_second_ip_swap_first))))))) + ge_balance_negative_swap_firstoutputreal = (((((((ge_first_rp_swap_first) * (ge_second_rn_swap_first))) + (((ge_first_rn_swap_first) * (ge_second_rp_swap_first))))) + (((((ge_first_ip_swap_first) * (ge_second_ip_swap_first))) + (((ge_first_in_swap_first) * (ge_second_in_swap_first))))))) + ge_balance_positive_swap_firstoutputreal))) /\ (exists ge_balance_positive_swap_firstoutputimaginary ge_balance_negative_swap_firstoutputimaginary. (((((ge_representation_imaginary_code_swap_firstoutput) = 2 * (ge_balance_positive_swap_firstoutputimaginary) /\ (ge_balance_negative_swap_firstoutputimaginary) = 0) \/ exists ge_signed_half_swap_firstoutputimaginarydecode. (((ge_representation_imaginary_code_swap_firstoutput) = 2 * ge_signed_half_swap_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_firstoutputimaginary) = 0) /\ (ge_balance_negative_swap_firstoutputimaginary) = S ge_signed_half_swap_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_first) * (ge_second_ip_swap_first))) + (((ge_first_rn_swap_first) * (ge_second_in_swap_first))))) + (((((ge_first_ip_swap_first) * (ge_second_rp_swap_first))) + (((ge_first_in_swap_first) * (ge_second_rn_swap_first))))))) + ge_balance_negative_swap_firstoutputimaginary = (((((((ge_first_rp_swap_first) * (ge_second_in_swap_first))) + (((ge_first_rn_swap_first) * (ge_second_ip_swap_first))))) + (((((ge_first_ip_swap_first) * (ge_second_rn_swap_first))) + (((ge_first_in_swap_first) * (ge_second_rp_swap_first))))))) + ge_balance_positive_swap_firstoutputimaginary))))))))) -> (exists ge_first_rp_swap_second ge_first_rn_swap_second ge_first_ip_swap_second ge_first_in_swap_second ge_second_rp_swap_second ge_second_rn_swap_second ge_second_ip_swap_second ge_second_in_swap_second. ((exists ge_representation_real_code_swap_secondfirst ge_representation_imaginary_code_swap_secondfirst. (((ab) = ((ge_representation_real_code_swap_secondfirst) + (ge_representation_imaginary_code_swap_secondfirst)) * S ((ge_representation_real_code_swap_secondfirst) + (ge_representation_imaginary_code_swap_secondfirst)) + ((ge_representation_imaginary_code_swap_secondfirst) + (ge_representation_imaginary_code_swap_secondfirst))) /\ ((exists ge_balance_positive_swap_secondfirstreal ge_balance_negative_swap_secondfirstreal. (((((ge_representation_real_code_swap_secondfirst) = 2 * (ge_balance_positive_swap_secondfirstreal) /\ (ge_balance_negative_swap_secondfirstreal) = 0) \/ exists ge_signed_half_swap_secondfirstrealdecode. (((ge_representation_real_code_swap_secondfirst) = 2 * ge_signed_half_swap_secondfirstrealdecode + 1 /\ (ge_balance_positive_swap_secondfirstreal) = 0) /\ (ge_balance_negative_swap_secondfirstreal) = S ge_signed_half_swap_secondfirstrealdecode))) /\ ((ge_first_rp_swap_second) + ge_balance_negative_swap_secondfirstreal = (ge_first_rn_swap_second) + ge_balance_positive_swap_secondfirstreal))) /\ (exists ge_balance_positive_swap_secondfirstimaginary ge_balance_negative_swap_secondfirstimaginary. (((((ge_representation_imaginary_code_swap_secondfirst) = 2 * (ge_balance_positive_swap_secondfirstimaginary) /\ (ge_balance_negative_swap_secondfirstimaginary) = 0) \/ exists ge_signed_half_swap_secondfirstimaginarydecode. (((ge_representation_imaginary_code_swap_secondfirst) = 2 * ge_signed_half_swap_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_secondfirstimaginary) = 0) /\ (ge_balance_negative_swap_secondfirstimaginary) = S ge_signed_half_swap_secondfirstimaginarydecode))) /\ ((ge_first_ip_swap_second) + ge_balance_negative_swap_secondfirstimaginary = (ge_first_in_swap_second) + ge_balance_positive_swap_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_secondsecond ge_representation_imaginary_code_swap_secondsecond. (((c) = ((ge_representation_real_code_swap_secondsecond) + (ge_representation_imaginary_code_swap_secondsecond)) * S ((ge_representation_real_code_swap_secondsecond) + (ge_representation_imaginary_code_swap_secondsecond)) + ((ge_representation_imaginary_code_swap_secondsecond) + (ge_representation_imaginary_code_swap_secondsecond))) /\ ((exists ge_balance_positive_swap_secondsecondreal ge_balance_negative_swap_secondsecondreal. (((((ge_representation_real_code_swap_secondsecond) = 2 * (ge_balance_positive_swap_secondsecondreal) /\ (ge_balance_negative_swap_secondsecondreal) = 0) \/ exists ge_signed_half_swap_secondsecondrealdecode. (((ge_representation_real_code_swap_secondsecond) = 2 * ge_signed_half_swap_secondsecondrealdecode + 1 /\ (ge_balance_positive_swap_secondsecondreal) = 0) /\ (ge_balance_negative_swap_secondsecondreal) = S ge_signed_half_swap_secondsecondrealdecode))) /\ ((ge_second_rp_swap_second) + ge_balance_negative_swap_secondsecondreal = (ge_second_rn_swap_second) + ge_balance_positive_swap_secondsecondreal))) /\ (exists ge_balance_positive_swap_secondsecondimaginary ge_balance_negative_swap_secondsecondimaginary. (((((ge_representation_imaginary_code_swap_secondsecond) = 2 * (ge_balance_positive_swap_secondsecondimaginary) /\ (ge_balance_negative_swap_secondsecondimaginary) = 0) \/ exists ge_signed_half_swap_secondsecondimaginarydecode. (((ge_representation_imaginary_code_swap_secondsecond) = 2 * ge_signed_half_swap_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_secondsecondimaginary) = 0) /\ (ge_balance_negative_swap_secondsecondimaginary) = S ge_signed_half_swap_secondsecondimaginarydecode))) /\ ((ge_second_ip_swap_second) + ge_balance_negative_swap_secondsecondimaginary = (ge_second_in_swap_second) + ge_balance_positive_swap_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_secondoutput ge_representation_imaginary_code_swap_secondoutput. (((t) = ((ge_representation_real_code_swap_secondoutput) + (ge_representation_imaginary_code_swap_secondoutput)) * S ((ge_representation_real_code_swap_secondoutput) + (ge_representation_imaginary_code_swap_secondoutput)) + ((ge_representation_imaginary_code_swap_secondoutput) + (ge_representation_imaginary_code_swap_secondoutput))) /\ ((exists ge_balance_positive_swap_secondoutputreal ge_balance_negative_swap_secondoutputreal. (((((ge_representation_real_code_swap_secondoutput) = 2 * (ge_balance_positive_swap_secondoutputreal) /\ (ge_balance_negative_swap_secondoutputreal) = 0) \/ exists ge_signed_half_swap_secondoutputrealdecode. (((ge_representation_real_code_swap_secondoutput) = 2 * ge_signed_half_swap_secondoutputrealdecode + 1 /\ (ge_balance_positive_swap_secondoutputreal) = 0) /\ (ge_balance_negative_swap_secondoutputreal) = S ge_signed_half_swap_secondoutputrealdecode))) /\ ((((((((ge_first_rp_swap_second) * (ge_second_rp_swap_second))) + (((ge_first_rn_swap_second) * (ge_second_rn_swap_second))))) + (((((ge_first_ip_swap_second) * (ge_second_in_swap_second))) + (((ge_first_in_swap_second) * (ge_second_ip_swap_second))))))) + ge_balance_negative_swap_secondoutputreal = (((((((ge_first_rp_swap_second) * (ge_second_rn_swap_second))) + (((ge_first_rn_swap_second) * (ge_second_rp_swap_second))))) + (((((ge_first_ip_swap_second) * (ge_second_ip_swap_second))) + (((ge_first_in_swap_second) * (ge_second_in_swap_second))))))) + ge_balance_positive_swap_secondoutputreal))) /\ (exists ge_balance_positive_swap_secondoutputimaginary ge_balance_negative_swap_secondoutputimaginary. (((((ge_representation_imaginary_code_swap_secondoutput) = 2 * (ge_balance_positive_swap_secondoutputimaginary) /\ (ge_balance_negative_swap_secondoutputimaginary) = 0) \/ exists ge_signed_half_swap_secondoutputimaginarydecode. (((ge_representation_imaginary_code_swap_secondoutput) = 2 * ge_signed_half_swap_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_secondoutputimaginary) = 0) /\ (ge_balance_negative_swap_secondoutputimaginary) = S ge_signed_half_swap_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_second) * (ge_second_ip_swap_second))) + (((ge_first_rn_swap_second) * (ge_second_in_swap_second))))) + (((((ge_first_ip_swap_second) * (ge_second_rp_swap_second))) + (((ge_first_in_swap_second) * (ge_second_rn_swap_second))))))) + ge_balance_negative_swap_secondoutputimaginary = (((((((ge_first_rp_swap_second) * (ge_second_in_swap_second))) + (((ge_first_rn_swap_second) * (ge_second_ip_swap_second))))) + (((((ge_first_ip_swap_second) * (ge_second_rn_swap_second))) + (((ge_first_in_swap_second) * (ge_second_rp_swap_second))))))) + ge_balance_positive_swap_secondoutputimaginary))))))))) -> (exists ge_first_rp_swap_third ge_first_rn_swap_third ge_first_ip_swap_third ge_first_in_swap_third ge_second_rp_swap_third ge_second_rn_swap_third ge_second_ip_swap_third ge_second_in_swap_third. ((exists ge_representation_real_code_swap_thirdfirst ge_representation_imaginary_code_swap_thirdfirst. (((a) = ((ge_representation_real_code_swap_thirdfirst) + (ge_representation_imaginary_code_swap_thirdfirst)) * S ((ge_representation_real_code_swap_thirdfirst) + (ge_representation_imaginary_code_swap_thirdfirst)) + ((ge_representation_imaginary_code_swap_thirdfirst) + (ge_representation_imaginary_code_swap_thirdfirst))) /\ ((exists ge_balance_positive_swap_thirdfirstreal ge_balance_negative_swap_thirdfirstreal. (((((ge_representation_real_code_swap_thirdfirst) = 2 * (ge_balance_positive_swap_thirdfirstreal) /\ (ge_balance_negative_swap_thirdfirstreal) = 0) \/ exists ge_signed_half_swap_thirdfirstrealdecode. (((ge_representation_real_code_swap_thirdfirst) = 2 * ge_signed_half_swap_thirdfirstrealdecode + 1 /\ (ge_balance_positive_swap_thirdfirstreal) = 0) /\ (ge_balance_negative_swap_thirdfirstreal) = S ge_signed_half_swap_thirdfirstrealdecode))) /\ ((ge_first_rp_swap_third) + ge_balance_negative_swap_thirdfirstreal = (ge_first_rn_swap_third) + ge_balance_positive_swap_thirdfirstreal))) /\ (exists ge_balance_positive_swap_thirdfirstimaginary ge_balance_negative_swap_thirdfirstimaginary. (((((ge_representation_imaginary_code_swap_thirdfirst) = 2 * (ge_balance_positive_swap_thirdfirstimaginary) /\ (ge_balance_negative_swap_thirdfirstimaginary) = 0) \/ exists ge_signed_half_swap_thirdfirstimaginarydecode. (((ge_representation_imaginary_code_swap_thirdfirst) = 2 * ge_signed_half_swap_thirdfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_thirdfirstimaginary) = 0) /\ (ge_balance_negative_swap_thirdfirstimaginary) = S ge_signed_half_swap_thirdfirstimaginarydecode))) /\ ((ge_first_ip_swap_third) + ge_balance_negative_swap_thirdfirstimaginary = (ge_first_in_swap_third) + ge_balance_positive_swap_thirdfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_thirdsecond ge_representation_imaginary_code_swap_thirdsecond. (((c) = ((ge_representation_real_code_swap_thirdsecond) + (ge_representation_imaginary_code_swap_thirdsecond)) * S ((ge_representation_real_code_swap_thirdsecond) + (ge_representation_imaginary_code_swap_thirdsecond)) + ((ge_representation_imaginary_code_swap_thirdsecond) + (ge_representation_imaginary_code_swap_thirdsecond))) /\ ((exists ge_balance_positive_swap_thirdsecondreal ge_balance_negative_swap_thirdsecondreal. (((((ge_representation_real_code_swap_thirdsecond) = 2 * (ge_balance_positive_swap_thirdsecondreal) /\ (ge_balance_negative_swap_thirdsecondreal) = 0) \/ exists ge_signed_half_swap_thirdsecondrealdecode. (((ge_representation_real_code_swap_thirdsecond) = 2 * ge_signed_half_swap_thirdsecondrealdecode + 1 /\ (ge_balance_positive_swap_thirdsecondreal) = 0) /\ (ge_balance_negative_swap_thirdsecondreal) = S ge_signed_half_swap_thirdsecondrealdecode))) /\ ((ge_second_rp_swap_third) + ge_balance_negative_swap_thirdsecondreal = (ge_second_rn_swap_third) + ge_balance_positive_swap_thirdsecondreal))) /\ (exists ge_balance_positive_swap_thirdsecondimaginary ge_balance_negative_swap_thirdsecondimaginary. (((((ge_representation_imaginary_code_swap_thirdsecond) = 2 * (ge_balance_positive_swap_thirdsecondimaginary) /\ (ge_balance_negative_swap_thirdsecondimaginary) = 0) \/ exists ge_signed_half_swap_thirdsecondimaginarydecode. (((ge_representation_imaginary_code_swap_thirdsecond) = 2 * ge_signed_half_swap_thirdsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_thirdsecondimaginary) = 0) /\ (ge_balance_negative_swap_thirdsecondimaginary) = S ge_signed_half_swap_thirdsecondimaginarydecode))) /\ ((ge_second_ip_swap_third) + ge_balance_negative_swap_thirdsecondimaginary = (ge_second_in_swap_third) + ge_balance_positive_swap_thirdsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_thirdoutput ge_representation_imaginary_code_swap_thirdoutput. (((ac) = ((ge_representation_real_code_swap_thirdoutput) + (ge_representation_imaginary_code_swap_thirdoutput)) * S ((ge_representation_real_code_swap_thirdoutput) + (ge_representation_imaginary_code_swap_thirdoutput)) + ((ge_representation_imaginary_code_swap_thirdoutput) + (ge_representation_imaginary_code_swap_thirdoutput))) /\ ((exists ge_balance_positive_swap_thirdoutputreal ge_balance_negative_swap_thirdoutputreal. (((((ge_representation_real_code_swap_thirdoutput) = 2 * (ge_balance_positive_swap_thirdoutputreal) /\ (ge_balance_negative_swap_thirdoutputreal) = 0) \/ exists ge_signed_half_swap_thirdoutputrealdecode. (((ge_representation_real_code_swap_thirdoutput) = 2 * ge_signed_half_swap_thirdoutputrealdecode + 1 /\ (ge_balance_positive_swap_thirdoutputreal) = 0) /\ (ge_balance_negative_swap_thirdoutputreal) = S ge_signed_half_swap_thirdoutputrealdecode))) /\ ((((((((ge_first_rp_swap_third) * (ge_second_rp_swap_third))) + (((ge_first_rn_swap_third) * (ge_second_rn_swap_third))))) + (((((ge_first_ip_swap_third) * (ge_second_in_swap_third))) + (((ge_first_in_swap_third) * (ge_second_ip_swap_third))))))) + ge_balance_negative_swap_thirdoutputreal = (((((((ge_first_rp_swap_third) * (ge_second_rn_swap_third))) + (((ge_first_rn_swap_third) * (ge_second_rp_swap_third))))) + (((((ge_first_ip_swap_third) * (ge_second_ip_swap_third))) + (((ge_first_in_swap_third) * (ge_second_in_swap_third))))))) + ge_balance_positive_swap_thirdoutputreal))) /\ (exists ge_balance_positive_swap_thirdoutputimaginary ge_balance_negative_swap_thirdoutputimaginary. (((((ge_representation_imaginary_code_swap_thirdoutput) = 2 * (ge_balance_positive_swap_thirdoutputimaginary) /\ (ge_balance_negative_swap_thirdoutputimaginary) = 0) \/ exists ge_signed_half_swap_thirdoutputimaginarydecode. (((ge_representation_imaginary_code_swap_thirdoutput) = 2 * ge_signed_half_swap_thirdoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_thirdoutputimaginary) = 0) /\ (ge_balance_negative_swap_thirdoutputimaginary) = S ge_signed_half_swap_thirdoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_third) * (ge_second_ip_swap_third))) + (((ge_first_rn_swap_third) * (ge_second_in_swap_third))))) + (((((ge_first_ip_swap_third) * (ge_second_rp_swap_third))) + (((ge_first_in_swap_third) * (ge_second_rn_swap_third))))))) + ge_balance_negative_swap_thirdoutputimaginary = (((((((ge_first_rp_swap_third) * (ge_second_in_swap_third))) + (((ge_first_rn_swap_third) * (ge_second_ip_swap_third))))) + (((((ge_first_ip_swap_third) * (ge_second_rn_swap_third))) + (((ge_first_in_swap_third) * (ge_second_rp_swap_third))))))) + ge_balance_positive_swap_thirdoutputimaginary))))))))) -> (exists ge_first_rp_swap_result ge_first_rn_swap_result ge_first_ip_swap_result ge_first_in_swap_result ge_second_rp_swap_result ge_second_rn_swap_result ge_second_ip_swap_result ge_second_in_swap_result. ((exists ge_representation_real_code_swap_resultfirst ge_representation_imaginary_code_swap_resultfirst. (((ac) = ((ge_representation_real_code_swap_resultfirst) + (ge_representation_imaginary_code_swap_resultfirst)) * S ((ge_representation_real_code_swap_resultfirst) + (ge_representation_imaginary_code_swap_resultfirst)) + ((ge_representation_imaginary_code_swap_resultfirst) + (ge_representation_imaginary_code_swap_resultfirst))) /\ ((exists ge_balance_positive_swap_resultfirstreal ge_balance_negative_swap_resultfirstreal. (((((ge_representation_real_code_swap_resultfirst) = 2 * (ge_balance_positive_swap_resultfirstreal) /\ (ge_balance_negative_swap_resultfirstreal) = 0) \/ exists ge_signed_half_swap_resultfirstrealdecode. (((ge_representation_real_code_swap_resultfirst) = 2 * ge_signed_half_swap_resultfirstrealdecode + 1 /\ (ge_balance_positive_swap_resultfirstreal) = 0) /\ (ge_balance_negative_swap_resultfirstreal) = S ge_signed_half_swap_resultfirstrealdecode))) /\ ((ge_first_rp_swap_result) + ge_balance_negative_swap_resultfirstreal = (ge_first_rn_swap_result) + ge_balance_positive_swap_resultfirstreal))) /\ (exists ge_balance_positive_swap_resultfirstimaginary ge_balance_negative_swap_resultfirstimaginary. (((((ge_representation_imaginary_code_swap_resultfirst) = 2 * (ge_balance_positive_swap_resultfirstimaginary) /\ (ge_balance_negative_swap_resultfirstimaginary) = 0) \/ exists ge_signed_half_swap_resultfirstimaginarydecode. (((ge_representation_imaginary_code_swap_resultfirst) = 2 * ge_signed_half_swap_resultfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_resultfirstimaginary) = 0) /\ (ge_balance_negative_swap_resultfirstimaginary) = S ge_signed_half_swap_resultfirstimaginarydecode))) /\ ((ge_first_ip_swap_result) + ge_balance_negative_swap_resultfirstimaginary = (ge_first_in_swap_result) + ge_balance_positive_swap_resultfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_resultsecond ge_representation_imaginary_code_swap_resultsecond. (((b) = ((ge_representation_real_code_swap_resultsecond) + (ge_representation_imaginary_code_swap_resultsecond)) * S ((ge_representation_real_code_swap_resultsecond) + (ge_representation_imaginary_code_swap_resultsecond)) + ((ge_representation_imaginary_code_swap_resultsecond) + (ge_representation_imaginary_code_swap_resultsecond))) /\ ((exists ge_balance_positive_swap_resultsecondreal ge_balance_negative_swap_resultsecondreal. (((((ge_representation_real_code_swap_resultsecond) = 2 * (ge_balance_positive_swap_resultsecondreal) /\ (ge_balance_negative_swap_resultsecondreal) = 0) \/ exists ge_signed_half_swap_resultsecondrealdecode. (((ge_representation_real_code_swap_resultsecond) = 2 * ge_signed_half_swap_resultsecondrealdecode + 1 /\ (ge_balance_positive_swap_resultsecondreal) = 0) /\ (ge_balance_negative_swap_resultsecondreal) = S ge_signed_half_swap_resultsecondrealdecode))) /\ ((ge_second_rp_swap_result) + ge_balance_negative_swap_resultsecondreal = (ge_second_rn_swap_result) + ge_balance_positive_swap_resultsecondreal))) /\ (exists ge_balance_positive_swap_resultsecondimaginary ge_balance_negative_swap_resultsecondimaginary. (((((ge_representation_imaginary_code_swap_resultsecond) = 2 * (ge_balance_positive_swap_resultsecondimaginary) /\ (ge_balance_negative_swap_resultsecondimaginary) = 0) \/ exists ge_signed_half_swap_resultsecondimaginarydecode. (((ge_representation_imaginary_code_swap_resultsecond) = 2 * ge_signed_half_swap_resultsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_resultsecondimaginary) = 0) /\ (ge_balance_negative_swap_resultsecondimaginary) = S ge_signed_half_swap_resultsecondimaginarydecode))) /\ ((ge_second_ip_swap_result) + ge_balance_negative_swap_resultsecondimaginary = (ge_second_in_swap_result) + ge_balance_positive_swap_resultsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_resultoutput ge_representation_imaginary_code_swap_resultoutput. (((t) = ((ge_representation_real_code_swap_resultoutput) + (ge_representation_imaginary_code_swap_resultoutput)) * S ((ge_representation_real_code_swap_resultoutput) + (ge_representation_imaginary_code_swap_resultoutput)) + ((ge_representation_imaginary_code_swap_resultoutput) + (ge_representation_imaginary_code_swap_resultoutput))) /\ ((exists ge_balance_positive_swap_resultoutputreal ge_balance_negative_swap_resultoutputreal. (((((ge_representation_real_code_swap_resultoutput) = 2 * (ge_balance_positive_swap_resultoutputreal) /\ (ge_balance_negative_swap_resultoutputreal) = 0) \/ exists ge_signed_half_swap_resultoutputrealdecode. (((ge_representation_real_code_swap_resultoutput) = 2 * ge_signed_half_swap_resultoutputrealdecode + 1 /\ (ge_balance_positive_swap_resultoutputreal) = 0) /\ (ge_balance_negative_swap_resultoutputreal) = S ge_signed_half_swap_resultoutputrealdecode))) /\ ((((((((ge_first_rp_swap_result) * (ge_second_rp_swap_result))) + (((ge_first_rn_swap_result) * (ge_second_rn_swap_result))))) + (((((ge_first_ip_swap_result) * (ge_second_in_swap_result))) + (((ge_first_in_swap_result) * (ge_second_ip_swap_result))))))) + ge_balance_negative_swap_resultoutputreal = (((((((ge_first_rp_swap_result) * (ge_second_rn_swap_result))) + (((ge_first_rn_swap_result) * (ge_second_rp_swap_result))))) + (((((ge_first_ip_swap_result) * (ge_second_ip_swap_result))) + (((ge_first_in_swap_result) * (ge_second_in_swap_result))))))) + ge_balance_positive_swap_resultoutputreal))) /\ (exists ge_balance_positive_swap_resultoutputimaginary ge_balance_negative_swap_resultoutputimaginary. (((((ge_representation_imaginary_code_swap_resultoutput) = 2 * (ge_balance_positive_swap_resultoutputimaginary) /\ (ge_balance_negative_swap_resultoutputimaginary) = 0) \/ exists ge_signed_half_swap_resultoutputimaginarydecode. (((ge_representation_imaginary_code_swap_resultoutput) = 2 * ge_signed_half_swap_resultoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_resultoutputimaginary) = 0) /\ (ge_balance_negative_swap_resultoutputimaginary) = S ge_signed_half_swap_resultoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_result) * (ge_second_ip_swap_result))) + (((ge_first_rn_swap_result) * (ge_second_in_swap_result))))) + (((((ge_first_ip_swap_result) * (ge_second_rp_swap_result))) + (((ge_first_in_swap_result) * (ge_second_rn_swap_result))))))) + ge_balance_negative_swap_resultoutputimaginary = (((((((ge_first_rp_swap_result) * (ge_second_in_swap_result))) + (((ge_first_rn_swap_result) * (ge_second_ip_swap_result))))) + (((((ge_first_ip_swap_result) * (ge_second_rn_swap_result))) + (((ge_first_in_swap_result) * (ge_second_rp_swap_result))))))) + ge_balance_positive_swap_resultoutputimaginary)))))))))