gaussian_multiply_cancel_right

Exact expanded first-order arithmetic statement

forall a b c t. ~(c=0) -> (exists ge_first_rp_cancel_right_product_first ge_first_rn_cancel_right_product_first ge_first_ip_cancel_right_product_first ge_first_in_cancel_right_product_first ge_second_rp_cancel_right_product_first ge_second_rn_cancel_right_product_first ge_second_ip_cancel_right_product_first ge_second_in_cancel_right_product_first. ((exists ge_representation_real_code_cancel_right_product_firstfirst ge_representation_imaginary_code_cancel_right_product_firstfirst. (((a) = ((ge_representation_real_code_cancel_right_product_firstfirst) + (ge_representation_imaginary_code_cancel_right_product_firstfirst)) * S ((ge_representation_real_code_cancel_right_product_firstfirst) + (ge_representation_imaginary_code_cancel_right_product_firstfirst)) + ((ge_representation_imaginary_code_cancel_right_product_firstfirst) + (ge_representation_imaginary_code_cancel_right_product_firstfirst))) /\ ((exists ge_balance_positive_cancel_right_product_firstfirstreal ge_balance_negative_cancel_right_product_firstfirstreal. (((((ge_representation_real_code_cancel_right_product_firstfirst) = 2 * (ge_balance_positive_cancel_right_product_firstfirstreal) /\ (ge_balance_negative_cancel_right_product_firstfirstreal) = 0) \/ exists ge_signed_half_cancel_right_product_firstfirstrealdecode. (((ge_representation_real_code_cancel_right_product_firstfirst) = 2 * ge_signed_half_cancel_right_product_firstfirstrealdecode + 1 /\ (ge_balance_positive_cancel_right_product_firstfirstreal) = 0) /\ (ge_balance_negative_cancel_right_product_firstfirstreal) = S ge_signed_half_cancel_right_product_firstfirstrealdecode))) /\ ((ge_first_rp_cancel_right_product_first) + ge_balance_negative_cancel_right_product_firstfirstreal = (ge_first_rn_cancel_right_product_first) + ge_balance_positive_cancel_right_product_firstfirstreal))) /\ (exists ge_balance_positive_cancel_right_product_firstfirstimaginary ge_balance_negative_cancel_right_product_firstfirstimaginary. (((((ge_representation_imaginary_code_cancel_right_product_firstfirst) = 2 * (ge_balance_positive_cancel_right_product_firstfirstimaginary) /\ (ge_balance_negative_cancel_right_product_firstfirstimaginary) = 0) \/ exists ge_signed_half_cancel_right_product_firstfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_right_product_firstfirst) = 2 * ge_signed_half_cancel_right_product_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_product_firstfirstimaginary) = 0) /\ (ge_balance_negative_cancel_right_product_firstfirstimaginary) = S ge_signed_half_cancel_right_product_firstfirstimaginarydecode))) /\ ((ge_first_ip_cancel_right_product_first) + ge_balance_negative_cancel_right_product_firstfirstimaginary = (ge_first_in_cancel_right_product_first) + ge_balance_positive_cancel_right_product_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_right_product_firstsecond ge_representation_imaginary_code_cancel_right_product_firstsecond. (((c) = ((ge_representation_real_code_cancel_right_product_firstsecond) + (ge_representation_imaginary_code_cancel_right_product_firstsecond)) * S ((ge_representation_real_code_cancel_right_product_firstsecond) + (ge_representation_imaginary_code_cancel_right_product_firstsecond)) + ((ge_representation_imaginary_code_cancel_right_product_firstsecond) + (ge_representation_imaginary_code_cancel_right_product_firstsecond))) /\ ((exists ge_balance_positive_cancel_right_product_firstsecondreal ge_balance_negative_cancel_right_product_firstsecondreal. (((((ge_representation_real_code_cancel_right_product_firstsecond) = 2 * (ge_balance_positive_cancel_right_product_firstsecondreal) /\ (ge_balance_negative_cancel_right_product_firstsecondreal) = 0) \/ exists ge_signed_half_cancel_right_product_firstsecondrealdecode. (((ge_representation_real_code_cancel_right_product_firstsecond) = 2 * ge_signed_half_cancel_right_product_firstsecondrealdecode + 1 /\ (ge_balance_positive_cancel_right_product_firstsecondreal) = 0) /\ (ge_balance_negative_cancel_right_product_firstsecondreal) = S ge_signed_half_cancel_right_product_firstsecondrealdecode))) /\ ((ge_second_rp_cancel_right_product_first) + ge_balance_negative_cancel_right_product_firstsecondreal = (ge_second_rn_cancel_right_product_first) + ge_balance_positive_cancel_right_product_firstsecondreal))) /\ (exists ge_balance_positive_cancel_right_product_firstsecondimaginary ge_balance_negative_cancel_right_product_firstsecondimaginary. (((((ge_representation_imaginary_code_cancel_right_product_firstsecond) = 2 * (ge_balance_positive_cancel_right_product_firstsecondimaginary) /\ (ge_balance_negative_cancel_right_product_firstsecondimaginary) = 0) \/ exists ge_signed_half_cancel_right_product_firstsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_right_product_firstsecond) = 2 * ge_signed_half_cancel_right_product_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_product_firstsecondimaginary) = 0) /\ (ge_balance_negative_cancel_right_product_firstsecondimaginary) = S ge_signed_half_cancel_right_product_firstsecondimaginarydecode))) /\ ((ge_second_ip_cancel_right_product_first) + ge_balance_negative_cancel_right_product_firstsecondimaginary = (ge_second_in_cancel_right_product_first) + ge_balance_positive_cancel_right_product_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_right_product_firstoutput ge_representation_imaginary_code_cancel_right_product_firstoutput. (((t) = ((ge_representation_real_code_cancel_right_product_firstoutput) + (ge_representation_imaginary_code_cancel_right_product_firstoutput)) * S ((ge_representation_real_code_cancel_right_product_firstoutput) + (ge_representation_imaginary_code_cancel_right_product_firstoutput)) + ((ge_representation_imaginary_code_cancel_right_product_firstoutput) + (ge_representation_imaginary_code_cancel_right_product_firstoutput))) /\ ((exists ge_balance_positive_cancel_right_product_firstoutputreal ge_balance_negative_cancel_right_product_firstoutputreal. (((((ge_representation_real_code_cancel_right_product_firstoutput) = 2 * (ge_balance_positive_cancel_right_product_firstoutputreal) /\ (ge_balance_negative_cancel_right_product_firstoutputreal) = 0) \/ exists ge_signed_half_cancel_right_product_firstoutputrealdecode. (((ge_representation_real_code_cancel_right_product_firstoutput) = 2 * ge_signed_half_cancel_right_product_firstoutputrealdecode + 1 /\ (ge_balance_positive_cancel_right_product_firstoutputreal) = 0) /\ (ge_balance_negative_cancel_right_product_firstoutputreal) = S ge_signed_half_cancel_right_product_firstoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_right_product_first) * (ge_second_rp_cancel_right_product_first))) + (((ge_first_rn_cancel_right_product_first) * (ge_second_rn_cancel_right_product_first))))) + (((((ge_first_ip_cancel_right_product_first) * (ge_second_in_cancel_right_product_first))) + (((ge_first_in_cancel_right_product_first) * (ge_second_ip_cancel_right_product_first))))))) + ge_balance_negative_cancel_right_product_firstoutputreal = (((((((ge_first_rp_cancel_right_product_first) * (ge_second_rn_cancel_right_product_first))) + (((ge_first_rn_cancel_right_product_first) * (ge_second_rp_cancel_right_product_first))))) + (((((ge_first_ip_cancel_right_product_first) * (ge_second_ip_cancel_right_product_first))) + (((ge_first_in_cancel_right_product_first) * (ge_second_in_cancel_right_product_first))))))) + ge_balance_positive_cancel_right_product_firstoutputreal))) /\ (exists ge_balance_positive_cancel_right_product_firstoutputimaginary ge_balance_negative_cancel_right_product_firstoutputimaginary. (((((ge_representation_imaginary_code_cancel_right_product_firstoutput) = 2 * (ge_balance_positive_cancel_right_product_firstoutputimaginary) /\ (ge_balance_negative_cancel_right_product_firstoutputimaginary) = 0) \/ exists ge_signed_half_cancel_right_product_firstoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_right_product_firstoutput) = 2 * ge_signed_half_cancel_right_product_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_product_firstoutputimaginary) = 0) /\ (ge_balance_negative_cancel_right_product_firstoutputimaginary) = S ge_signed_half_cancel_right_product_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_right_product_first) * (ge_second_ip_cancel_right_product_first))) + (((ge_first_rn_cancel_right_product_first) * (ge_second_in_cancel_right_product_first))))) + (((((ge_first_ip_cancel_right_product_first) * (ge_second_rp_cancel_right_product_first))) + (((ge_first_in_cancel_right_product_first) * (ge_second_rn_cancel_right_product_first))))))) + ge_balance_negative_cancel_right_product_firstoutputimaginary = (((((((ge_first_rp_cancel_right_product_first) * (ge_second_in_cancel_right_product_first))) + (((ge_first_rn_cancel_right_product_first) * (ge_second_ip_cancel_right_product_first))))) + (((((ge_first_ip_cancel_right_product_first) * (ge_second_rn_cancel_right_product_first))) + (((ge_first_in_cancel_right_product_first) * (ge_second_rp_cancel_right_product_first))))))) + ge_balance_positive_cancel_right_product_firstoutputimaginary))))))))) -> (exists ge_first_rp_cancel_right_product_second ge_first_rn_cancel_right_product_second ge_first_ip_cancel_right_product_second ge_first_in_cancel_right_product_second ge_second_rp_cancel_right_product_second ge_second_rn_cancel_right_product_second ge_second_ip_cancel_right_product_second ge_second_in_cancel_right_product_second. ((exists ge_representation_real_code_cancel_right_product_secondfirst ge_representation_imaginary_code_cancel_right_product_secondfirst. (((b) = ((ge_representation_real_code_cancel_right_product_secondfirst) + (ge_representation_imaginary_code_cancel_right_product_secondfirst)) * S ((ge_representation_real_code_cancel_right_product_secondfirst) + (ge_representation_imaginary_code_cancel_right_product_secondfirst)) + ((ge_representation_imaginary_code_cancel_right_product_secondfirst) + (ge_representation_imaginary_code_cancel_right_product_secondfirst))) /\ ((exists ge_balance_positive_cancel_right_product_secondfirstreal ge_balance_negative_cancel_right_product_secondfirstreal. (((((ge_representation_real_code_cancel_right_product_secondfirst) = 2 * (ge_balance_positive_cancel_right_product_secondfirstreal) /\ (ge_balance_negative_cancel_right_product_secondfirstreal) = 0) \/ exists ge_signed_half_cancel_right_product_secondfirstrealdecode. (((ge_representation_real_code_cancel_right_product_secondfirst) = 2 * ge_signed_half_cancel_right_product_secondfirstrealdecode + 1 /\ (ge_balance_positive_cancel_right_product_secondfirstreal) = 0) /\ (ge_balance_negative_cancel_right_product_secondfirstreal) = S ge_signed_half_cancel_right_product_secondfirstrealdecode))) /\ ((ge_first_rp_cancel_right_product_second) + ge_balance_negative_cancel_right_product_secondfirstreal = (ge_first_rn_cancel_right_product_second) + ge_balance_positive_cancel_right_product_secondfirstreal))) /\ (exists ge_balance_positive_cancel_right_product_secondfirstimaginary ge_balance_negative_cancel_right_product_secondfirstimaginary. (((((ge_representation_imaginary_code_cancel_right_product_secondfirst) = 2 * (ge_balance_positive_cancel_right_product_secondfirstimaginary) /\ (ge_balance_negative_cancel_right_product_secondfirstimaginary) = 0) \/ exists ge_signed_half_cancel_right_product_secondfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_right_product_secondfirst) = 2 * ge_signed_half_cancel_right_product_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_product_secondfirstimaginary) = 0) /\ (ge_balance_negative_cancel_right_product_secondfirstimaginary) = S ge_signed_half_cancel_right_product_secondfirstimaginarydecode))) /\ ((ge_first_ip_cancel_right_product_second) + ge_balance_negative_cancel_right_product_secondfirstimaginary = (ge_first_in_cancel_right_product_second) + ge_balance_positive_cancel_right_product_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_right_product_secondsecond ge_representation_imaginary_code_cancel_right_product_secondsecond. (((c) = ((ge_representation_real_code_cancel_right_product_secondsecond) + (ge_representation_imaginary_code_cancel_right_product_secondsecond)) * S ((ge_representation_real_code_cancel_right_product_secondsecond) + (ge_representation_imaginary_code_cancel_right_product_secondsecond)) + ((ge_representation_imaginary_code_cancel_right_product_secondsecond) + (ge_representation_imaginary_code_cancel_right_product_secondsecond))) /\ ((exists ge_balance_positive_cancel_right_product_secondsecondreal ge_balance_negative_cancel_right_product_secondsecondreal. (((((ge_representation_real_code_cancel_right_product_secondsecond) = 2 * (ge_balance_positive_cancel_right_product_secondsecondreal) /\ (ge_balance_negative_cancel_right_product_secondsecondreal) = 0) \/ exists ge_signed_half_cancel_right_product_secondsecondrealdecode. (((ge_representation_real_code_cancel_right_product_secondsecond) = 2 * ge_signed_half_cancel_right_product_secondsecondrealdecode + 1 /\ (ge_balance_positive_cancel_right_product_secondsecondreal) = 0) /\ (ge_balance_negative_cancel_right_product_secondsecondreal) = S ge_signed_half_cancel_right_product_secondsecondrealdecode))) /\ ((ge_second_rp_cancel_right_product_second) + ge_balance_negative_cancel_right_product_secondsecondreal = (ge_second_rn_cancel_right_product_second) + ge_balance_positive_cancel_right_product_secondsecondreal))) /\ (exists ge_balance_positive_cancel_right_product_secondsecondimaginary ge_balance_negative_cancel_right_product_secondsecondimaginary. (((((ge_representation_imaginary_code_cancel_right_product_secondsecond) = 2 * (ge_balance_positive_cancel_right_product_secondsecondimaginary) /\ (ge_balance_negative_cancel_right_product_secondsecondimaginary) = 0) \/ exists ge_signed_half_cancel_right_product_secondsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_right_product_secondsecond) = 2 * ge_signed_half_cancel_right_product_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_product_secondsecondimaginary) = 0) /\ (ge_balance_negative_cancel_right_product_secondsecondimaginary) = S ge_signed_half_cancel_right_product_secondsecondimaginarydecode))) /\ ((ge_second_ip_cancel_right_product_second) + ge_balance_negative_cancel_right_product_secondsecondimaginary = (ge_second_in_cancel_right_product_second) + ge_balance_positive_cancel_right_product_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_right_product_secondoutput ge_representation_imaginary_code_cancel_right_product_secondoutput. (((t) = ((ge_representation_real_code_cancel_right_product_secondoutput) + (ge_representation_imaginary_code_cancel_right_product_secondoutput)) * S ((ge_representation_real_code_cancel_right_product_secondoutput) + (ge_representation_imaginary_code_cancel_right_product_secondoutput)) + ((ge_representation_imaginary_code_cancel_right_product_secondoutput) + (ge_representation_imaginary_code_cancel_right_product_secondoutput))) /\ ((exists ge_balance_positive_cancel_right_product_secondoutputreal ge_balance_negative_cancel_right_product_secondoutputreal. (((((ge_representation_real_code_cancel_right_product_secondoutput) = 2 * (ge_balance_positive_cancel_right_product_secondoutputreal) /\ (ge_balance_negative_cancel_right_product_secondoutputreal) = 0) \/ exists ge_signed_half_cancel_right_product_secondoutputrealdecode. (((ge_representation_real_code_cancel_right_product_secondoutput) = 2 * ge_signed_half_cancel_right_product_secondoutputrealdecode + 1 /\ (ge_balance_positive_cancel_right_product_secondoutputreal) = 0) /\ (ge_balance_negative_cancel_right_product_secondoutputreal) = S ge_signed_half_cancel_right_product_secondoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_right_product_second) * (ge_second_rp_cancel_right_product_second))) + (((ge_first_rn_cancel_right_product_second) * (ge_second_rn_cancel_right_product_second))))) + (((((ge_first_ip_cancel_right_product_second) * (ge_second_in_cancel_right_product_second))) + (((ge_first_in_cancel_right_product_second) * (ge_second_ip_cancel_right_product_second))))))) + ge_balance_negative_cancel_right_product_secondoutputreal = (((((((ge_first_rp_cancel_right_product_second) * (ge_second_rn_cancel_right_product_second))) + (((ge_first_rn_cancel_right_product_second) * (ge_second_rp_cancel_right_product_second))))) + (((((ge_first_ip_cancel_right_product_second) * (ge_second_ip_cancel_right_product_second))) + (((ge_first_in_cancel_right_product_second) * (ge_second_in_cancel_right_product_second))))))) + ge_balance_positive_cancel_right_product_secondoutputreal))) /\ (exists ge_balance_positive_cancel_right_product_secondoutputimaginary ge_balance_negative_cancel_right_product_secondoutputimaginary. (((((ge_representation_imaginary_code_cancel_right_product_secondoutput) = 2 * (ge_balance_positive_cancel_right_product_secondoutputimaginary) /\ (ge_balance_negative_cancel_right_product_secondoutputimaginary) = 0) \/ exists ge_signed_half_cancel_right_product_secondoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_right_product_secondoutput) = 2 * ge_signed_half_cancel_right_product_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_product_secondoutputimaginary) = 0) /\ (ge_balance_negative_cancel_right_product_secondoutputimaginary) = S ge_signed_half_cancel_right_product_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_right_product_second) * (ge_second_ip_cancel_right_product_second))) + (((ge_first_rn_cancel_right_product_second) * (ge_second_in_cancel_right_product_second))))) + (((((ge_first_ip_cancel_right_product_second) * (ge_second_rp_cancel_right_product_second))) + (((ge_first_in_cancel_right_product_second) * (ge_second_rn_cancel_right_product_second))))))) + ge_balance_negative_cancel_right_product_secondoutputimaginary = (((((((ge_first_rp_cancel_right_product_second) * (ge_second_in_cancel_right_product_second))) + (((ge_first_rn_cancel_right_product_second) * (ge_second_ip_cancel_right_product_second))))) + (((((ge_first_ip_cancel_right_product_second) * (ge_second_rn_cancel_right_product_second))) + (((ge_first_in_cancel_right_product_second) * (ge_second_rp_cancel_right_product_second))))))) + ge_balance_positive_cancel_right_product_secondoutputimaginary))))))))) -> a=b