gaussian_multiply_associative_reverse

Exact expanded first-order arithmetic statement

forall a b c ab bc t. (exists ge_first_rp_reverse_assoc_first ge_first_rn_reverse_assoc_first ge_first_ip_reverse_assoc_first ge_first_in_reverse_assoc_first ge_second_rp_reverse_assoc_first ge_second_rn_reverse_assoc_first ge_second_ip_reverse_assoc_first ge_second_in_reverse_assoc_first. ((exists ge_representation_real_code_reverse_assoc_firstfirst ge_representation_imaginary_code_reverse_assoc_firstfirst. (((a) = ((ge_representation_real_code_reverse_assoc_firstfirst) + (ge_representation_imaginary_code_reverse_assoc_firstfirst)) * S ((ge_representation_real_code_reverse_assoc_firstfirst) + (ge_representation_imaginary_code_reverse_assoc_firstfirst)) + ((ge_representation_imaginary_code_reverse_assoc_firstfirst) + (ge_representation_imaginary_code_reverse_assoc_firstfirst))) /\ ((exists ge_balance_positive_reverse_assoc_firstfirstreal ge_balance_negative_reverse_assoc_firstfirstreal. (((((ge_representation_real_code_reverse_assoc_firstfirst) = 2 * (ge_balance_positive_reverse_assoc_firstfirstreal) /\ (ge_balance_negative_reverse_assoc_firstfirstreal) = 0) \/ exists ge_signed_half_reverse_assoc_firstfirstrealdecode. (((ge_representation_real_code_reverse_assoc_firstfirst) = 2 * ge_signed_half_reverse_assoc_firstfirstrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_firstfirstreal) = 0) /\ (ge_balance_negative_reverse_assoc_firstfirstreal) = S ge_signed_half_reverse_assoc_firstfirstrealdecode))) /\ ((ge_first_rp_reverse_assoc_first) + ge_balance_negative_reverse_assoc_firstfirstreal = (ge_first_rn_reverse_assoc_first) + ge_balance_positive_reverse_assoc_firstfirstreal))) /\ (exists ge_balance_positive_reverse_assoc_firstfirstimaginary ge_balance_negative_reverse_assoc_firstfirstimaginary. (((((ge_representation_imaginary_code_reverse_assoc_firstfirst) = 2 * (ge_balance_positive_reverse_assoc_firstfirstimaginary) /\ (ge_balance_negative_reverse_assoc_firstfirstimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_firstfirstimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_firstfirst) = 2 * ge_signed_half_reverse_assoc_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_firstfirstimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_firstfirstimaginary) = S ge_signed_half_reverse_assoc_firstfirstimaginarydecode))) /\ ((ge_first_ip_reverse_assoc_first) + ge_balance_negative_reverse_assoc_firstfirstimaginary = (ge_first_in_reverse_assoc_first) + ge_balance_positive_reverse_assoc_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_reverse_assoc_firstsecond ge_representation_imaginary_code_reverse_assoc_firstsecond. (((b) = ((ge_representation_real_code_reverse_assoc_firstsecond) + (ge_representation_imaginary_code_reverse_assoc_firstsecond)) * S ((ge_representation_real_code_reverse_assoc_firstsecond) + (ge_representation_imaginary_code_reverse_assoc_firstsecond)) + ((ge_representation_imaginary_code_reverse_assoc_firstsecond) + (ge_representation_imaginary_code_reverse_assoc_firstsecond))) /\ ((exists ge_balance_positive_reverse_assoc_firstsecondreal ge_balance_negative_reverse_assoc_firstsecondreal. (((((ge_representation_real_code_reverse_assoc_firstsecond) = 2 * (ge_balance_positive_reverse_assoc_firstsecondreal) /\ (ge_balance_negative_reverse_assoc_firstsecondreal) = 0) \/ exists ge_signed_half_reverse_assoc_firstsecondrealdecode. (((ge_representation_real_code_reverse_assoc_firstsecond) = 2 * ge_signed_half_reverse_assoc_firstsecondrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_firstsecondreal) = 0) /\ (ge_balance_negative_reverse_assoc_firstsecondreal) = S ge_signed_half_reverse_assoc_firstsecondrealdecode))) /\ ((ge_second_rp_reverse_assoc_first) + ge_balance_negative_reverse_assoc_firstsecondreal = (ge_second_rn_reverse_assoc_first) + ge_balance_positive_reverse_assoc_firstsecondreal))) /\ (exists ge_balance_positive_reverse_assoc_firstsecondimaginary ge_balance_negative_reverse_assoc_firstsecondimaginary. (((((ge_representation_imaginary_code_reverse_assoc_firstsecond) = 2 * (ge_balance_positive_reverse_assoc_firstsecondimaginary) /\ (ge_balance_negative_reverse_assoc_firstsecondimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_firstsecondimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_firstsecond) = 2 * ge_signed_half_reverse_assoc_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_firstsecondimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_firstsecondimaginary) = S ge_signed_half_reverse_assoc_firstsecondimaginarydecode))) /\ ((ge_second_ip_reverse_assoc_first) + ge_balance_negative_reverse_assoc_firstsecondimaginary = (ge_second_in_reverse_assoc_first) + ge_balance_positive_reverse_assoc_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_reverse_assoc_firstoutput ge_representation_imaginary_code_reverse_assoc_firstoutput. (((ab) = ((ge_representation_real_code_reverse_assoc_firstoutput) + (ge_representation_imaginary_code_reverse_assoc_firstoutput)) * S ((ge_representation_real_code_reverse_assoc_firstoutput) + (ge_representation_imaginary_code_reverse_assoc_firstoutput)) + ((ge_representation_imaginary_code_reverse_assoc_firstoutput) + (ge_representation_imaginary_code_reverse_assoc_firstoutput))) /\ ((exists ge_balance_positive_reverse_assoc_firstoutputreal ge_balance_negative_reverse_assoc_firstoutputreal. (((((ge_representation_real_code_reverse_assoc_firstoutput) = 2 * (ge_balance_positive_reverse_assoc_firstoutputreal) /\ (ge_balance_negative_reverse_assoc_firstoutputreal) = 0) \/ exists ge_signed_half_reverse_assoc_firstoutputrealdecode. (((ge_representation_real_code_reverse_assoc_firstoutput) = 2 * ge_signed_half_reverse_assoc_firstoutputrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_firstoutputreal) = 0) /\ (ge_balance_negative_reverse_assoc_firstoutputreal) = S ge_signed_half_reverse_assoc_firstoutputrealdecode))) /\ ((((((((ge_first_rp_reverse_assoc_first) * (ge_second_rp_reverse_assoc_first))) + (((ge_first_rn_reverse_assoc_first) * (ge_second_rn_reverse_assoc_first))))) + (((((ge_first_ip_reverse_assoc_first) * (ge_second_in_reverse_assoc_first))) + (((ge_first_in_reverse_assoc_first) * (ge_second_ip_reverse_assoc_first))))))) + ge_balance_negative_reverse_assoc_firstoutputreal = (((((((ge_first_rp_reverse_assoc_first) * (ge_second_rn_reverse_assoc_first))) + (((ge_first_rn_reverse_assoc_first) * (ge_second_rp_reverse_assoc_first))))) + (((((ge_first_ip_reverse_assoc_first) * (ge_second_ip_reverse_assoc_first))) + (((ge_first_in_reverse_assoc_first) * (ge_second_in_reverse_assoc_first))))))) + ge_balance_positive_reverse_assoc_firstoutputreal))) /\ (exists ge_balance_positive_reverse_assoc_firstoutputimaginary ge_balance_negative_reverse_assoc_firstoutputimaginary. (((((ge_representation_imaginary_code_reverse_assoc_firstoutput) = 2 * (ge_balance_positive_reverse_assoc_firstoutputimaginary) /\ (ge_balance_negative_reverse_assoc_firstoutputimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_firstoutputimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_firstoutput) = 2 * ge_signed_half_reverse_assoc_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_firstoutputimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_firstoutputimaginary) = S ge_signed_half_reverse_assoc_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_reverse_assoc_first) * (ge_second_ip_reverse_assoc_first))) + (((ge_first_rn_reverse_assoc_first) * (ge_second_in_reverse_assoc_first))))) + (((((ge_first_ip_reverse_assoc_first) * (ge_second_rp_reverse_assoc_first))) + (((ge_first_in_reverse_assoc_first) * (ge_second_rn_reverse_assoc_first))))))) + ge_balance_negative_reverse_assoc_firstoutputimaginary = (((((((ge_first_rp_reverse_assoc_first) * (ge_second_in_reverse_assoc_first))) + (((ge_first_rn_reverse_assoc_first) * (ge_second_ip_reverse_assoc_first))))) + (((((ge_first_ip_reverse_assoc_first) * (ge_second_rn_reverse_assoc_first))) + (((ge_first_in_reverse_assoc_first) * (ge_second_rp_reverse_assoc_first))))))) + ge_balance_positive_reverse_assoc_firstoutputimaginary))))))))) -> (exists ge_first_rp_reverse_assoc_second ge_first_rn_reverse_assoc_second ge_first_ip_reverse_assoc_second ge_first_in_reverse_assoc_second ge_second_rp_reverse_assoc_second ge_second_rn_reverse_assoc_second ge_second_ip_reverse_assoc_second ge_second_in_reverse_assoc_second. ((exists ge_representation_real_code_reverse_assoc_secondfirst ge_representation_imaginary_code_reverse_assoc_secondfirst. (((b) = ((ge_representation_real_code_reverse_assoc_secondfirst) + (ge_representation_imaginary_code_reverse_assoc_secondfirst)) * S ((ge_representation_real_code_reverse_assoc_secondfirst) + (ge_representation_imaginary_code_reverse_assoc_secondfirst)) + ((ge_representation_imaginary_code_reverse_assoc_secondfirst) + (ge_representation_imaginary_code_reverse_assoc_secondfirst))) /\ ((exists ge_balance_positive_reverse_assoc_secondfirstreal ge_balance_negative_reverse_assoc_secondfirstreal. (((((ge_representation_real_code_reverse_assoc_secondfirst) = 2 * (ge_balance_positive_reverse_assoc_secondfirstreal) /\ (ge_balance_negative_reverse_assoc_secondfirstreal) = 0) \/ exists ge_signed_half_reverse_assoc_secondfirstrealdecode. (((ge_representation_real_code_reverse_assoc_secondfirst) = 2 * ge_signed_half_reverse_assoc_secondfirstrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_secondfirstreal) = 0) /\ (ge_balance_negative_reverse_assoc_secondfirstreal) = S ge_signed_half_reverse_assoc_secondfirstrealdecode))) /\ ((ge_first_rp_reverse_assoc_second) + ge_balance_negative_reverse_assoc_secondfirstreal = (ge_first_rn_reverse_assoc_second) + ge_balance_positive_reverse_assoc_secondfirstreal))) /\ (exists ge_balance_positive_reverse_assoc_secondfirstimaginary ge_balance_negative_reverse_assoc_secondfirstimaginary. (((((ge_representation_imaginary_code_reverse_assoc_secondfirst) = 2 * (ge_balance_positive_reverse_assoc_secondfirstimaginary) /\ (ge_balance_negative_reverse_assoc_secondfirstimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_secondfirstimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_secondfirst) = 2 * ge_signed_half_reverse_assoc_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_secondfirstimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_secondfirstimaginary) = S ge_signed_half_reverse_assoc_secondfirstimaginarydecode))) /\ ((ge_first_ip_reverse_assoc_second) + ge_balance_negative_reverse_assoc_secondfirstimaginary = (ge_first_in_reverse_assoc_second) + ge_balance_positive_reverse_assoc_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_reverse_assoc_secondsecond ge_representation_imaginary_code_reverse_assoc_secondsecond. (((c) = ((ge_representation_real_code_reverse_assoc_secondsecond) + (ge_representation_imaginary_code_reverse_assoc_secondsecond)) * S ((ge_representation_real_code_reverse_assoc_secondsecond) + (ge_representation_imaginary_code_reverse_assoc_secondsecond)) + ((ge_representation_imaginary_code_reverse_assoc_secondsecond) + (ge_representation_imaginary_code_reverse_assoc_secondsecond))) /\ ((exists ge_balance_positive_reverse_assoc_secondsecondreal ge_balance_negative_reverse_assoc_secondsecondreal. (((((ge_representation_real_code_reverse_assoc_secondsecond) = 2 * (ge_balance_positive_reverse_assoc_secondsecondreal) /\ (ge_balance_negative_reverse_assoc_secondsecondreal) = 0) \/ exists ge_signed_half_reverse_assoc_secondsecondrealdecode. (((ge_representation_real_code_reverse_assoc_secondsecond) = 2 * ge_signed_half_reverse_assoc_secondsecondrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_secondsecondreal) = 0) /\ (ge_balance_negative_reverse_assoc_secondsecondreal) = S ge_signed_half_reverse_assoc_secondsecondrealdecode))) /\ ((ge_second_rp_reverse_assoc_second) + ge_balance_negative_reverse_assoc_secondsecondreal = (ge_second_rn_reverse_assoc_second) + ge_balance_positive_reverse_assoc_secondsecondreal))) /\ (exists ge_balance_positive_reverse_assoc_secondsecondimaginary ge_balance_negative_reverse_assoc_secondsecondimaginary. (((((ge_representation_imaginary_code_reverse_assoc_secondsecond) = 2 * (ge_balance_positive_reverse_assoc_secondsecondimaginary) /\ (ge_balance_negative_reverse_assoc_secondsecondimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_secondsecondimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_secondsecond) = 2 * ge_signed_half_reverse_assoc_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_secondsecondimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_secondsecondimaginary) = S ge_signed_half_reverse_assoc_secondsecondimaginarydecode))) /\ ((ge_second_ip_reverse_assoc_second) + ge_balance_negative_reverse_assoc_secondsecondimaginary = (ge_second_in_reverse_assoc_second) + ge_balance_positive_reverse_assoc_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_reverse_assoc_secondoutput ge_representation_imaginary_code_reverse_assoc_secondoutput. (((bc) = ((ge_representation_real_code_reverse_assoc_secondoutput) + (ge_representation_imaginary_code_reverse_assoc_secondoutput)) * S ((ge_representation_real_code_reverse_assoc_secondoutput) + (ge_representation_imaginary_code_reverse_assoc_secondoutput)) + ((ge_representation_imaginary_code_reverse_assoc_secondoutput) + (ge_representation_imaginary_code_reverse_assoc_secondoutput))) /\ ((exists ge_balance_positive_reverse_assoc_secondoutputreal ge_balance_negative_reverse_assoc_secondoutputreal. (((((ge_representation_real_code_reverse_assoc_secondoutput) = 2 * (ge_balance_positive_reverse_assoc_secondoutputreal) /\ (ge_balance_negative_reverse_assoc_secondoutputreal) = 0) \/ exists ge_signed_half_reverse_assoc_secondoutputrealdecode. (((ge_representation_real_code_reverse_assoc_secondoutput) = 2 * ge_signed_half_reverse_assoc_secondoutputrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_secondoutputreal) = 0) /\ (ge_balance_negative_reverse_assoc_secondoutputreal) = S ge_signed_half_reverse_assoc_secondoutputrealdecode))) /\ ((((((((ge_first_rp_reverse_assoc_second) * (ge_second_rp_reverse_assoc_second))) + (((ge_first_rn_reverse_assoc_second) * (ge_second_rn_reverse_assoc_second))))) + (((((ge_first_ip_reverse_assoc_second) * (ge_second_in_reverse_assoc_second))) + (((ge_first_in_reverse_assoc_second) * (ge_second_ip_reverse_assoc_second))))))) + ge_balance_negative_reverse_assoc_secondoutputreal = (((((((ge_first_rp_reverse_assoc_second) * (ge_second_rn_reverse_assoc_second))) + (((ge_first_rn_reverse_assoc_second) * (ge_second_rp_reverse_assoc_second))))) + (((((ge_first_ip_reverse_assoc_second) * (ge_second_ip_reverse_assoc_second))) + (((ge_first_in_reverse_assoc_second) * (ge_second_in_reverse_assoc_second))))))) + ge_balance_positive_reverse_assoc_secondoutputreal))) /\ (exists ge_balance_positive_reverse_assoc_secondoutputimaginary ge_balance_negative_reverse_assoc_secondoutputimaginary. (((((ge_representation_imaginary_code_reverse_assoc_secondoutput) = 2 * (ge_balance_positive_reverse_assoc_secondoutputimaginary) /\ (ge_balance_negative_reverse_assoc_secondoutputimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_secondoutputimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_secondoutput) = 2 * ge_signed_half_reverse_assoc_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_secondoutputimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_secondoutputimaginary) = S ge_signed_half_reverse_assoc_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_reverse_assoc_second) * (ge_second_ip_reverse_assoc_second))) + (((ge_first_rn_reverse_assoc_second) * (ge_second_in_reverse_assoc_second))))) + (((((ge_first_ip_reverse_assoc_second) * (ge_second_rp_reverse_assoc_second))) + (((ge_first_in_reverse_assoc_second) * (ge_second_rn_reverse_assoc_second))))))) + ge_balance_negative_reverse_assoc_secondoutputimaginary = (((((((ge_first_rp_reverse_assoc_second) * (ge_second_in_reverse_assoc_second))) + (((ge_first_rn_reverse_assoc_second) * (ge_second_ip_reverse_assoc_second))))) + (((((ge_first_ip_reverse_assoc_second) * (ge_second_rn_reverse_assoc_second))) + (((ge_first_in_reverse_assoc_second) * (ge_second_rp_reverse_assoc_second))))))) + ge_balance_positive_reverse_assoc_secondoutputimaginary))))))))) -> (exists ge_first_rp_reverse_assoc_third ge_first_rn_reverse_assoc_third ge_first_ip_reverse_assoc_third ge_first_in_reverse_assoc_third ge_second_rp_reverse_assoc_third ge_second_rn_reverse_assoc_third ge_second_ip_reverse_assoc_third ge_second_in_reverse_assoc_third. ((exists ge_representation_real_code_reverse_assoc_thirdfirst ge_representation_imaginary_code_reverse_assoc_thirdfirst. (((a) = ((ge_representation_real_code_reverse_assoc_thirdfirst) + (ge_representation_imaginary_code_reverse_assoc_thirdfirst)) * S ((ge_representation_real_code_reverse_assoc_thirdfirst) + (ge_representation_imaginary_code_reverse_assoc_thirdfirst)) + ((ge_representation_imaginary_code_reverse_assoc_thirdfirst) + (ge_representation_imaginary_code_reverse_assoc_thirdfirst))) /\ ((exists ge_balance_positive_reverse_assoc_thirdfirstreal ge_balance_negative_reverse_assoc_thirdfirstreal. (((((ge_representation_real_code_reverse_assoc_thirdfirst) = 2 * (ge_balance_positive_reverse_assoc_thirdfirstreal) /\ (ge_balance_negative_reverse_assoc_thirdfirstreal) = 0) \/ exists ge_signed_half_reverse_assoc_thirdfirstrealdecode. (((ge_representation_real_code_reverse_assoc_thirdfirst) = 2 * ge_signed_half_reverse_assoc_thirdfirstrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_thirdfirstreal) = 0) /\ (ge_balance_negative_reverse_assoc_thirdfirstreal) = S ge_signed_half_reverse_assoc_thirdfirstrealdecode))) /\ ((ge_first_rp_reverse_assoc_third) + ge_balance_negative_reverse_assoc_thirdfirstreal = (ge_first_rn_reverse_assoc_third) + ge_balance_positive_reverse_assoc_thirdfirstreal))) /\ (exists ge_balance_positive_reverse_assoc_thirdfirstimaginary ge_balance_negative_reverse_assoc_thirdfirstimaginary. (((((ge_representation_imaginary_code_reverse_assoc_thirdfirst) = 2 * (ge_balance_positive_reverse_assoc_thirdfirstimaginary) /\ (ge_balance_negative_reverse_assoc_thirdfirstimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_thirdfirstimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_thirdfirst) = 2 * ge_signed_half_reverse_assoc_thirdfirstimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_thirdfirstimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_thirdfirstimaginary) = S ge_signed_half_reverse_assoc_thirdfirstimaginarydecode))) /\ ((ge_first_ip_reverse_assoc_third) + ge_balance_negative_reverse_assoc_thirdfirstimaginary = (ge_first_in_reverse_assoc_third) + ge_balance_positive_reverse_assoc_thirdfirstimaginary)))))) /\ ((exists ge_representation_real_code_reverse_assoc_thirdsecond ge_representation_imaginary_code_reverse_assoc_thirdsecond. (((bc) = ((ge_representation_real_code_reverse_assoc_thirdsecond) + (ge_representation_imaginary_code_reverse_assoc_thirdsecond)) * S ((ge_representation_real_code_reverse_assoc_thirdsecond) + (ge_representation_imaginary_code_reverse_assoc_thirdsecond)) + ((ge_representation_imaginary_code_reverse_assoc_thirdsecond) + (ge_representation_imaginary_code_reverse_assoc_thirdsecond))) /\ ((exists ge_balance_positive_reverse_assoc_thirdsecondreal ge_balance_negative_reverse_assoc_thirdsecondreal. (((((ge_representation_real_code_reverse_assoc_thirdsecond) = 2 * (ge_balance_positive_reverse_assoc_thirdsecondreal) /\ (ge_balance_negative_reverse_assoc_thirdsecondreal) = 0) \/ exists ge_signed_half_reverse_assoc_thirdsecondrealdecode. (((ge_representation_real_code_reverse_assoc_thirdsecond) = 2 * ge_signed_half_reverse_assoc_thirdsecondrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_thirdsecondreal) = 0) /\ (ge_balance_negative_reverse_assoc_thirdsecondreal) = S ge_signed_half_reverse_assoc_thirdsecondrealdecode))) /\ ((ge_second_rp_reverse_assoc_third) + ge_balance_negative_reverse_assoc_thirdsecondreal = (ge_second_rn_reverse_assoc_third) + ge_balance_positive_reverse_assoc_thirdsecondreal))) /\ (exists ge_balance_positive_reverse_assoc_thirdsecondimaginary ge_balance_negative_reverse_assoc_thirdsecondimaginary. (((((ge_representation_imaginary_code_reverse_assoc_thirdsecond) = 2 * (ge_balance_positive_reverse_assoc_thirdsecondimaginary) /\ (ge_balance_negative_reverse_assoc_thirdsecondimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_thirdsecondimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_thirdsecond) = 2 * ge_signed_half_reverse_assoc_thirdsecondimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_thirdsecondimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_thirdsecondimaginary) = S ge_signed_half_reverse_assoc_thirdsecondimaginarydecode))) /\ ((ge_second_ip_reverse_assoc_third) + ge_balance_negative_reverse_assoc_thirdsecondimaginary = (ge_second_in_reverse_assoc_third) + ge_balance_positive_reverse_assoc_thirdsecondimaginary)))))) /\ (exists ge_representation_real_code_reverse_assoc_thirdoutput ge_representation_imaginary_code_reverse_assoc_thirdoutput. (((t) = ((ge_representation_real_code_reverse_assoc_thirdoutput) + (ge_representation_imaginary_code_reverse_assoc_thirdoutput)) * S ((ge_representation_real_code_reverse_assoc_thirdoutput) + (ge_representation_imaginary_code_reverse_assoc_thirdoutput)) + ((ge_representation_imaginary_code_reverse_assoc_thirdoutput) + (ge_representation_imaginary_code_reverse_assoc_thirdoutput))) /\ ((exists ge_balance_positive_reverse_assoc_thirdoutputreal ge_balance_negative_reverse_assoc_thirdoutputreal. (((((ge_representation_real_code_reverse_assoc_thirdoutput) = 2 * (ge_balance_positive_reverse_assoc_thirdoutputreal) /\ (ge_balance_negative_reverse_assoc_thirdoutputreal) = 0) \/ exists ge_signed_half_reverse_assoc_thirdoutputrealdecode. (((ge_representation_real_code_reverse_assoc_thirdoutput) = 2 * ge_signed_half_reverse_assoc_thirdoutputrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_thirdoutputreal) = 0) /\ (ge_balance_negative_reverse_assoc_thirdoutputreal) = S ge_signed_half_reverse_assoc_thirdoutputrealdecode))) /\ ((((((((ge_first_rp_reverse_assoc_third) * (ge_second_rp_reverse_assoc_third))) + (((ge_first_rn_reverse_assoc_third) * (ge_second_rn_reverse_assoc_third))))) + (((((ge_first_ip_reverse_assoc_third) * (ge_second_in_reverse_assoc_third))) + (((ge_first_in_reverse_assoc_third) * (ge_second_ip_reverse_assoc_third))))))) + ge_balance_negative_reverse_assoc_thirdoutputreal = (((((((ge_first_rp_reverse_assoc_third) * (ge_second_rn_reverse_assoc_third))) + (((ge_first_rn_reverse_assoc_third) * (ge_second_rp_reverse_assoc_third))))) + (((((ge_first_ip_reverse_assoc_third) * (ge_second_ip_reverse_assoc_third))) + (((ge_first_in_reverse_assoc_third) * (ge_second_in_reverse_assoc_third))))))) + ge_balance_positive_reverse_assoc_thirdoutputreal))) /\ (exists ge_balance_positive_reverse_assoc_thirdoutputimaginary ge_balance_negative_reverse_assoc_thirdoutputimaginary. (((((ge_representation_imaginary_code_reverse_assoc_thirdoutput) = 2 * (ge_balance_positive_reverse_assoc_thirdoutputimaginary) /\ (ge_balance_negative_reverse_assoc_thirdoutputimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_thirdoutputimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_thirdoutput) = 2 * ge_signed_half_reverse_assoc_thirdoutputimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_thirdoutputimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_thirdoutputimaginary) = S ge_signed_half_reverse_assoc_thirdoutputimaginarydecode))) /\ ((((((((ge_first_rp_reverse_assoc_third) * (ge_second_ip_reverse_assoc_third))) + (((ge_first_rn_reverse_assoc_third) * (ge_second_in_reverse_assoc_third))))) + (((((ge_first_ip_reverse_assoc_third) * (ge_second_rp_reverse_assoc_third))) + (((ge_first_in_reverse_assoc_third) * (ge_second_rn_reverse_assoc_third))))))) + ge_balance_negative_reverse_assoc_thirdoutputimaginary = (((((((ge_first_rp_reverse_assoc_third) * (ge_second_in_reverse_assoc_third))) + (((ge_first_rn_reverse_assoc_third) * (ge_second_ip_reverse_assoc_third))))) + (((((ge_first_ip_reverse_assoc_third) * (ge_second_rn_reverse_assoc_third))) + (((ge_first_in_reverse_assoc_third) * (ge_second_rp_reverse_assoc_third))))))) + ge_balance_positive_reverse_assoc_thirdoutputimaginary))))))))) -> (exists ge_first_rp_reverse_assoc_result ge_first_rn_reverse_assoc_result ge_first_ip_reverse_assoc_result ge_first_in_reverse_assoc_result ge_second_rp_reverse_assoc_result ge_second_rn_reverse_assoc_result ge_second_ip_reverse_assoc_result ge_second_in_reverse_assoc_result. ((exists ge_representation_real_code_reverse_assoc_resultfirst ge_representation_imaginary_code_reverse_assoc_resultfirst. (((ab) = ((ge_representation_real_code_reverse_assoc_resultfirst) + (ge_representation_imaginary_code_reverse_assoc_resultfirst)) * S ((ge_representation_real_code_reverse_assoc_resultfirst) + (ge_representation_imaginary_code_reverse_assoc_resultfirst)) + ((ge_representation_imaginary_code_reverse_assoc_resultfirst) + (ge_representation_imaginary_code_reverse_assoc_resultfirst))) /\ ((exists ge_balance_positive_reverse_assoc_resultfirstreal ge_balance_negative_reverse_assoc_resultfirstreal. (((((ge_representation_real_code_reverse_assoc_resultfirst) = 2 * (ge_balance_positive_reverse_assoc_resultfirstreal) /\ (ge_balance_negative_reverse_assoc_resultfirstreal) = 0) \/ exists ge_signed_half_reverse_assoc_resultfirstrealdecode. (((ge_representation_real_code_reverse_assoc_resultfirst) = 2 * ge_signed_half_reverse_assoc_resultfirstrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_resultfirstreal) = 0) /\ (ge_balance_negative_reverse_assoc_resultfirstreal) = S ge_signed_half_reverse_assoc_resultfirstrealdecode))) /\ ((ge_first_rp_reverse_assoc_result) + ge_balance_negative_reverse_assoc_resultfirstreal = (ge_first_rn_reverse_assoc_result) + ge_balance_positive_reverse_assoc_resultfirstreal))) /\ (exists ge_balance_positive_reverse_assoc_resultfirstimaginary ge_balance_negative_reverse_assoc_resultfirstimaginary. (((((ge_representation_imaginary_code_reverse_assoc_resultfirst) = 2 * (ge_balance_positive_reverse_assoc_resultfirstimaginary) /\ (ge_balance_negative_reverse_assoc_resultfirstimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_resultfirstimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_resultfirst) = 2 * ge_signed_half_reverse_assoc_resultfirstimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_resultfirstimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_resultfirstimaginary) = S ge_signed_half_reverse_assoc_resultfirstimaginarydecode))) /\ ((ge_first_ip_reverse_assoc_result) + ge_balance_negative_reverse_assoc_resultfirstimaginary = (ge_first_in_reverse_assoc_result) + ge_balance_positive_reverse_assoc_resultfirstimaginary)))))) /\ ((exists ge_representation_real_code_reverse_assoc_resultsecond ge_representation_imaginary_code_reverse_assoc_resultsecond. (((c) = ((ge_representation_real_code_reverse_assoc_resultsecond) + (ge_representation_imaginary_code_reverse_assoc_resultsecond)) * S ((ge_representation_real_code_reverse_assoc_resultsecond) + (ge_representation_imaginary_code_reverse_assoc_resultsecond)) + ((ge_representation_imaginary_code_reverse_assoc_resultsecond) + (ge_representation_imaginary_code_reverse_assoc_resultsecond))) /\ ((exists ge_balance_positive_reverse_assoc_resultsecondreal ge_balance_negative_reverse_assoc_resultsecondreal. (((((ge_representation_real_code_reverse_assoc_resultsecond) = 2 * (ge_balance_positive_reverse_assoc_resultsecondreal) /\ (ge_balance_negative_reverse_assoc_resultsecondreal) = 0) \/ exists ge_signed_half_reverse_assoc_resultsecondrealdecode. (((ge_representation_real_code_reverse_assoc_resultsecond) = 2 * ge_signed_half_reverse_assoc_resultsecondrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_resultsecondreal) = 0) /\ (ge_balance_negative_reverse_assoc_resultsecondreal) = S ge_signed_half_reverse_assoc_resultsecondrealdecode))) /\ ((ge_second_rp_reverse_assoc_result) + ge_balance_negative_reverse_assoc_resultsecondreal = (ge_second_rn_reverse_assoc_result) + ge_balance_positive_reverse_assoc_resultsecondreal))) /\ (exists ge_balance_positive_reverse_assoc_resultsecondimaginary ge_balance_negative_reverse_assoc_resultsecondimaginary. (((((ge_representation_imaginary_code_reverse_assoc_resultsecond) = 2 * (ge_balance_positive_reverse_assoc_resultsecondimaginary) /\ (ge_balance_negative_reverse_assoc_resultsecondimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_resultsecondimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_resultsecond) = 2 * ge_signed_half_reverse_assoc_resultsecondimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_resultsecondimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_resultsecondimaginary) = S ge_signed_half_reverse_assoc_resultsecondimaginarydecode))) /\ ((ge_second_ip_reverse_assoc_result) + ge_balance_negative_reverse_assoc_resultsecondimaginary = (ge_second_in_reverse_assoc_result) + ge_balance_positive_reverse_assoc_resultsecondimaginary)))))) /\ (exists ge_representation_real_code_reverse_assoc_resultoutput ge_representation_imaginary_code_reverse_assoc_resultoutput. (((t) = ((ge_representation_real_code_reverse_assoc_resultoutput) + (ge_representation_imaginary_code_reverse_assoc_resultoutput)) * S ((ge_representation_real_code_reverse_assoc_resultoutput) + (ge_representation_imaginary_code_reverse_assoc_resultoutput)) + ((ge_representation_imaginary_code_reverse_assoc_resultoutput) + (ge_representation_imaginary_code_reverse_assoc_resultoutput))) /\ ((exists ge_balance_positive_reverse_assoc_resultoutputreal ge_balance_negative_reverse_assoc_resultoutputreal. (((((ge_representation_real_code_reverse_assoc_resultoutput) = 2 * (ge_balance_positive_reverse_assoc_resultoutputreal) /\ (ge_balance_negative_reverse_assoc_resultoutputreal) = 0) \/ exists ge_signed_half_reverse_assoc_resultoutputrealdecode. (((ge_representation_real_code_reverse_assoc_resultoutput) = 2 * ge_signed_half_reverse_assoc_resultoutputrealdecode + 1 /\ (ge_balance_positive_reverse_assoc_resultoutputreal) = 0) /\ (ge_balance_negative_reverse_assoc_resultoutputreal) = S ge_signed_half_reverse_assoc_resultoutputrealdecode))) /\ ((((((((ge_first_rp_reverse_assoc_result) * (ge_second_rp_reverse_assoc_result))) + (((ge_first_rn_reverse_assoc_result) * (ge_second_rn_reverse_assoc_result))))) + (((((ge_first_ip_reverse_assoc_result) * (ge_second_in_reverse_assoc_result))) + (((ge_first_in_reverse_assoc_result) * (ge_second_ip_reverse_assoc_result))))))) + ge_balance_negative_reverse_assoc_resultoutputreal = (((((((ge_first_rp_reverse_assoc_result) * (ge_second_rn_reverse_assoc_result))) + (((ge_first_rn_reverse_assoc_result) * (ge_second_rp_reverse_assoc_result))))) + (((((ge_first_ip_reverse_assoc_result) * (ge_second_ip_reverse_assoc_result))) + (((ge_first_in_reverse_assoc_result) * (ge_second_in_reverse_assoc_result))))))) + ge_balance_positive_reverse_assoc_resultoutputreal))) /\ (exists ge_balance_positive_reverse_assoc_resultoutputimaginary ge_balance_negative_reverse_assoc_resultoutputimaginary. (((((ge_representation_imaginary_code_reverse_assoc_resultoutput) = 2 * (ge_balance_positive_reverse_assoc_resultoutputimaginary) /\ (ge_balance_negative_reverse_assoc_resultoutputimaginary) = 0) \/ exists ge_signed_half_reverse_assoc_resultoutputimaginarydecode. (((ge_representation_imaginary_code_reverse_assoc_resultoutput) = 2 * ge_signed_half_reverse_assoc_resultoutputimaginarydecode + 1 /\ (ge_balance_positive_reverse_assoc_resultoutputimaginary) = 0) /\ (ge_balance_negative_reverse_assoc_resultoutputimaginary) = S ge_signed_half_reverse_assoc_resultoutputimaginarydecode))) /\ ((((((((ge_first_rp_reverse_assoc_result) * (ge_second_ip_reverse_assoc_result))) + (((ge_first_rn_reverse_assoc_result) * (ge_second_in_reverse_assoc_result))))) + (((((ge_first_ip_reverse_assoc_result) * (ge_second_rp_reverse_assoc_result))) + (((ge_first_in_reverse_assoc_result) * (ge_second_rn_reverse_assoc_result))))))) + ge_balance_negative_reverse_assoc_resultoutputimaginary = (((((((ge_first_rp_reverse_assoc_result) * (ge_second_in_reverse_assoc_result))) + (((ge_first_rn_reverse_assoc_result) * (ge_second_ip_reverse_assoc_result))))) + (((((ge_first_ip_reverse_assoc_result) * (ge_second_rn_reverse_assoc_result))) + (((ge_first_in_reverse_assoc_result) * (ge_second_rp_reverse_assoc_result))))))) + ge_balance_positive_reverse_assoc_resultoutputimaginary)))))))))