gaussian_multiply_functional

Exact expanded first-order arithmetic statement

forall ac bc cc dd. (exists ge_first_rp_multiply_unique_first ge_first_rn_multiply_unique_first ge_first_ip_multiply_unique_first ge_first_in_multiply_unique_first ge_second_rp_multiply_unique_first ge_second_rn_multiply_unique_first ge_second_ip_multiply_unique_first ge_second_in_multiply_unique_first. ((exists ge_representation_real_code_multiply_unique_firstfirst ge_representation_imaginary_code_multiply_unique_firstfirst. (((ac) = ((ge_representation_real_code_multiply_unique_firstfirst) + (ge_representation_imaginary_code_multiply_unique_firstfirst)) * S ((ge_representation_real_code_multiply_unique_firstfirst) + (ge_representation_imaginary_code_multiply_unique_firstfirst)) + ((ge_representation_imaginary_code_multiply_unique_firstfirst) + (ge_representation_imaginary_code_multiply_unique_firstfirst))) /\ ((exists ge_balance_positive_multiply_unique_firstfirstreal ge_balance_negative_multiply_unique_firstfirstreal. (((((ge_representation_real_code_multiply_unique_firstfirst) = 2 * (ge_balance_positive_multiply_unique_firstfirstreal) /\ (ge_balance_negative_multiply_unique_firstfirstreal) = 0) \/ exists ge_signed_half_multiply_unique_firstfirstrealdecode. (((ge_representation_real_code_multiply_unique_firstfirst) = 2 * ge_signed_half_multiply_unique_firstfirstrealdecode + 1 /\ (ge_balance_positive_multiply_unique_firstfirstreal) = 0) /\ (ge_balance_negative_multiply_unique_firstfirstreal) = S ge_signed_half_multiply_unique_firstfirstrealdecode))) /\ ((ge_first_rp_multiply_unique_first) + ge_balance_negative_multiply_unique_firstfirstreal = (ge_first_rn_multiply_unique_first) + ge_balance_positive_multiply_unique_firstfirstreal))) /\ (exists ge_balance_positive_multiply_unique_firstfirstimaginary ge_balance_negative_multiply_unique_firstfirstimaginary. (((((ge_representation_imaginary_code_multiply_unique_firstfirst) = 2 * (ge_balance_positive_multiply_unique_firstfirstimaginary) /\ (ge_balance_negative_multiply_unique_firstfirstimaginary) = 0) \/ exists ge_signed_half_multiply_unique_firstfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_unique_firstfirst) = 2 * ge_signed_half_multiply_unique_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_unique_firstfirstimaginary) = 0) /\ (ge_balance_negative_multiply_unique_firstfirstimaginary) = S ge_signed_half_multiply_unique_firstfirstimaginarydecode))) /\ ((ge_first_ip_multiply_unique_first) + ge_balance_negative_multiply_unique_firstfirstimaginary = (ge_first_in_multiply_unique_first) + ge_balance_positive_multiply_unique_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_unique_firstsecond ge_representation_imaginary_code_multiply_unique_firstsecond. (((bc) = ((ge_representation_real_code_multiply_unique_firstsecond) + (ge_representation_imaginary_code_multiply_unique_firstsecond)) * S ((ge_representation_real_code_multiply_unique_firstsecond) + (ge_representation_imaginary_code_multiply_unique_firstsecond)) + ((ge_representation_imaginary_code_multiply_unique_firstsecond) + (ge_representation_imaginary_code_multiply_unique_firstsecond))) /\ ((exists ge_balance_positive_multiply_unique_firstsecondreal ge_balance_negative_multiply_unique_firstsecondreal. (((((ge_representation_real_code_multiply_unique_firstsecond) = 2 * (ge_balance_positive_multiply_unique_firstsecondreal) /\ (ge_balance_negative_multiply_unique_firstsecondreal) = 0) \/ exists ge_signed_half_multiply_unique_firstsecondrealdecode. (((ge_representation_real_code_multiply_unique_firstsecond) = 2 * ge_signed_half_multiply_unique_firstsecondrealdecode + 1 /\ (ge_balance_positive_multiply_unique_firstsecondreal) = 0) /\ (ge_balance_negative_multiply_unique_firstsecondreal) = S ge_signed_half_multiply_unique_firstsecondrealdecode))) /\ ((ge_second_rp_multiply_unique_first) + ge_balance_negative_multiply_unique_firstsecondreal = (ge_second_rn_multiply_unique_first) + ge_balance_positive_multiply_unique_firstsecondreal))) /\ (exists ge_balance_positive_multiply_unique_firstsecondimaginary ge_balance_negative_multiply_unique_firstsecondimaginary. (((((ge_representation_imaginary_code_multiply_unique_firstsecond) = 2 * (ge_balance_positive_multiply_unique_firstsecondimaginary) /\ (ge_balance_negative_multiply_unique_firstsecondimaginary) = 0) \/ exists ge_signed_half_multiply_unique_firstsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_unique_firstsecond) = 2 * ge_signed_half_multiply_unique_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_unique_firstsecondimaginary) = 0) /\ (ge_balance_negative_multiply_unique_firstsecondimaginary) = S ge_signed_half_multiply_unique_firstsecondimaginarydecode))) /\ ((ge_second_ip_multiply_unique_first) + ge_balance_negative_multiply_unique_firstsecondimaginary = (ge_second_in_multiply_unique_first) + ge_balance_positive_multiply_unique_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_unique_firstoutput ge_representation_imaginary_code_multiply_unique_firstoutput. (((cc) = ((ge_representation_real_code_multiply_unique_firstoutput) + (ge_representation_imaginary_code_multiply_unique_firstoutput)) * S ((ge_representation_real_code_multiply_unique_firstoutput) + (ge_representation_imaginary_code_multiply_unique_firstoutput)) + ((ge_representation_imaginary_code_multiply_unique_firstoutput) + (ge_representation_imaginary_code_multiply_unique_firstoutput))) /\ ((exists ge_balance_positive_multiply_unique_firstoutputreal ge_balance_negative_multiply_unique_firstoutputreal. (((((ge_representation_real_code_multiply_unique_firstoutput) = 2 * (ge_balance_positive_multiply_unique_firstoutputreal) /\ (ge_balance_negative_multiply_unique_firstoutputreal) = 0) \/ exists ge_signed_half_multiply_unique_firstoutputrealdecode. (((ge_representation_real_code_multiply_unique_firstoutput) = 2 * ge_signed_half_multiply_unique_firstoutputrealdecode + 1 /\ (ge_balance_positive_multiply_unique_firstoutputreal) = 0) /\ (ge_balance_negative_multiply_unique_firstoutputreal) = S ge_signed_half_multiply_unique_firstoutputrealdecode))) /\ ((((((((ge_first_rp_multiply_unique_first) * (ge_second_rp_multiply_unique_first))) + (((ge_first_rn_multiply_unique_first) * (ge_second_rn_multiply_unique_first))))) + (((((ge_first_ip_multiply_unique_first) * (ge_second_in_multiply_unique_first))) + (((ge_first_in_multiply_unique_first) * (ge_second_ip_multiply_unique_first))))))) + ge_balance_negative_multiply_unique_firstoutputreal = (((((((ge_first_rp_multiply_unique_first) * (ge_second_rn_multiply_unique_first))) + (((ge_first_rn_multiply_unique_first) * (ge_second_rp_multiply_unique_first))))) + (((((ge_first_ip_multiply_unique_first) * (ge_second_ip_multiply_unique_first))) + (((ge_first_in_multiply_unique_first) * (ge_second_in_multiply_unique_first))))))) + ge_balance_positive_multiply_unique_firstoutputreal))) /\ (exists ge_balance_positive_multiply_unique_firstoutputimaginary ge_balance_negative_multiply_unique_firstoutputimaginary. (((((ge_representation_imaginary_code_multiply_unique_firstoutput) = 2 * (ge_balance_positive_multiply_unique_firstoutputimaginary) /\ (ge_balance_negative_multiply_unique_firstoutputimaginary) = 0) \/ exists ge_signed_half_multiply_unique_firstoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_unique_firstoutput) = 2 * ge_signed_half_multiply_unique_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_unique_firstoutputimaginary) = 0) /\ (ge_balance_negative_multiply_unique_firstoutputimaginary) = S ge_signed_half_multiply_unique_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_multiply_unique_first) * (ge_second_ip_multiply_unique_first))) + (((ge_first_rn_multiply_unique_first) * (ge_second_in_multiply_unique_first))))) + (((((ge_first_ip_multiply_unique_first) * (ge_second_rp_multiply_unique_first))) + (((ge_first_in_multiply_unique_first) * (ge_second_rn_multiply_unique_first))))))) + ge_balance_negative_multiply_unique_firstoutputimaginary = (((((((ge_first_rp_multiply_unique_first) * (ge_second_in_multiply_unique_first))) + (((ge_first_rn_multiply_unique_first) * (ge_second_ip_multiply_unique_first))))) + (((((ge_first_ip_multiply_unique_first) * (ge_second_rn_multiply_unique_first))) + (((ge_first_in_multiply_unique_first) * (ge_second_rp_multiply_unique_first))))))) + ge_balance_positive_multiply_unique_firstoutputimaginary))))))))) -> (exists ge_first_rp_multiply_unique_second ge_first_rn_multiply_unique_second ge_first_ip_multiply_unique_second ge_first_in_multiply_unique_second ge_second_rp_multiply_unique_second ge_second_rn_multiply_unique_second ge_second_ip_multiply_unique_second ge_second_in_multiply_unique_second. ((exists ge_representation_real_code_multiply_unique_secondfirst ge_representation_imaginary_code_multiply_unique_secondfirst. (((ac) = ((ge_representation_real_code_multiply_unique_secondfirst) + (ge_representation_imaginary_code_multiply_unique_secondfirst)) * S ((ge_representation_real_code_multiply_unique_secondfirst) + (ge_representation_imaginary_code_multiply_unique_secondfirst)) + ((ge_representation_imaginary_code_multiply_unique_secondfirst) + (ge_representation_imaginary_code_multiply_unique_secondfirst))) /\ ((exists ge_balance_positive_multiply_unique_secondfirstreal ge_balance_negative_multiply_unique_secondfirstreal. (((((ge_representation_real_code_multiply_unique_secondfirst) = 2 * (ge_balance_positive_multiply_unique_secondfirstreal) /\ (ge_balance_negative_multiply_unique_secondfirstreal) = 0) \/ exists ge_signed_half_multiply_unique_secondfirstrealdecode. (((ge_representation_real_code_multiply_unique_secondfirst) = 2 * ge_signed_half_multiply_unique_secondfirstrealdecode + 1 /\ (ge_balance_positive_multiply_unique_secondfirstreal) = 0) /\ (ge_balance_negative_multiply_unique_secondfirstreal) = S ge_signed_half_multiply_unique_secondfirstrealdecode))) /\ ((ge_first_rp_multiply_unique_second) + ge_balance_negative_multiply_unique_secondfirstreal = (ge_first_rn_multiply_unique_second) + ge_balance_positive_multiply_unique_secondfirstreal))) /\ (exists ge_balance_positive_multiply_unique_secondfirstimaginary ge_balance_negative_multiply_unique_secondfirstimaginary. (((((ge_representation_imaginary_code_multiply_unique_secondfirst) = 2 * (ge_balance_positive_multiply_unique_secondfirstimaginary) /\ (ge_balance_negative_multiply_unique_secondfirstimaginary) = 0) \/ exists ge_signed_half_multiply_unique_secondfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_unique_secondfirst) = 2 * ge_signed_half_multiply_unique_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_unique_secondfirstimaginary) = 0) /\ (ge_balance_negative_multiply_unique_secondfirstimaginary) = S ge_signed_half_multiply_unique_secondfirstimaginarydecode))) /\ ((ge_first_ip_multiply_unique_second) + ge_balance_negative_multiply_unique_secondfirstimaginary = (ge_first_in_multiply_unique_second) + ge_balance_positive_multiply_unique_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_unique_secondsecond ge_representation_imaginary_code_multiply_unique_secondsecond. (((bc) = ((ge_representation_real_code_multiply_unique_secondsecond) + (ge_representation_imaginary_code_multiply_unique_secondsecond)) * S ((ge_representation_real_code_multiply_unique_secondsecond) + (ge_representation_imaginary_code_multiply_unique_secondsecond)) + ((ge_representation_imaginary_code_multiply_unique_secondsecond) + (ge_representation_imaginary_code_multiply_unique_secondsecond))) /\ ((exists ge_balance_positive_multiply_unique_secondsecondreal ge_balance_negative_multiply_unique_secondsecondreal. (((((ge_representation_real_code_multiply_unique_secondsecond) = 2 * (ge_balance_positive_multiply_unique_secondsecondreal) /\ (ge_balance_negative_multiply_unique_secondsecondreal) = 0) \/ exists ge_signed_half_multiply_unique_secondsecondrealdecode. (((ge_representation_real_code_multiply_unique_secondsecond) = 2 * ge_signed_half_multiply_unique_secondsecondrealdecode + 1 /\ (ge_balance_positive_multiply_unique_secondsecondreal) = 0) /\ (ge_balance_negative_multiply_unique_secondsecondreal) = S ge_signed_half_multiply_unique_secondsecondrealdecode))) /\ ((ge_second_rp_multiply_unique_second) + ge_balance_negative_multiply_unique_secondsecondreal = (ge_second_rn_multiply_unique_second) + ge_balance_positive_multiply_unique_secondsecondreal))) /\ (exists ge_balance_positive_multiply_unique_secondsecondimaginary ge_balance_negative_multiply_unique_secondsecondimaginary. (((((ge_representation_imaginary_code_multiply_unique_secondsecond) = 2 * (ge_balance_positive_multiply_unique_secondsecondimaginary) /\ (ge_balance_negative_multiply_unique_secondsecondimaginary) = 0) \/ exists ge_signed_half_multiply_unique_secondsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_unique_secondsecond) = 2 * ge_signed_half_multiply_unique_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_unique_secondsecondimaginary) = 0) /\ (ge_balance_negative_multiply_unique_secondsecondimaginary) = S ge_signed_half_multiply_unique_secondsecondimaginarydecode))) /\ ((ge_second_ip_multiply_unique_second) + ge_balance_negative_multiply_unique_secondsecondimaginary = (ge_second_in_multiply_unique_second) + ge_balance_positive_multiply_unique_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_unique_secondoutput ge_representation_imaginary_code_multiply_unique_secondoutput. (((dd) = ((ge_representation_real_code_multiply_unique_secondoutput) + (ge_representation_imaginary_code_multiply_unique_secondoutput)) * S ((ge_representation_real_code_multiply_unique_secondoutput) + (ge_representation_imaginary_code_multiply_unique_secondoutput)) + ((ge_representation_imaginary_code_multiply_unique_secondoutput) + (ge_representation_imaginary_code_multiply_unique_secondoutput))) /\ ((exists ge_balance_positive_multiply_unique_secondoutputreal ge_balance_negative_multiply_unique_secondoutputreal. (((((ge_representation_real_code_multiply_unique_secondoutput) = 2 * (ge_balance_positive_multiply_unique_secondoutputreal) /\ (ge_balance_negative_multiply_unique_secondoutputreal) = 0) \/ exists ge_signed_half_multiply_unique_secondoutputrealdecode. (((ge_representation_real_code_multiply_unique_secondoutput) = 2 * ge_signed_half_multiply_unique_secondoutputrealdecode + 1 /\ (ge_balance_positive_multiply_unique_secondoutputreal) = 0) /\ (ge_balance_negative_multiply_unique_secondoutputreal) = S ge_signed_half_multiply_unique_secondoutputrealdecode))) /\ ((((((((ge_first_rp_multiply_unique_second) * (ge_second_rp_multiply_unique_second))) + (((ge_first_rn_multiply_unique_second) * (ge_second_rn_multiply_unique_second))))) + (((((ge_first_ip_multiply_unique_second) * (ge_second_in_multiply_unique_second))) + (((ge_first_in_multiply_unique_second) * (ge_second_ip_multiply_unique_second))))))) + ge_balance_negative_multiply_unique_secondoutputreal = (((((((ge_first_rp_multiply_unique_second) * (ge_second_rn_multiply_unique_second))) + (((ge_first_rn_multiply_unique_second) * (ge_second_rp_multiply_unique_second))))) + (((((ge_first_ip_multiply_unique_second) * (ge_second_ip_multiply_unique_second))) + (((ge_first_in_multiply_unique_second) * (ge_second_in_multiply_unique_second))))))) + ge_balance_positive_multiply_unique_secondoutputreal))) /\ (exists ge_balance_positive_multiply_unique_secondoutputimaginary ge_balance_negative_multiply_unique_secondoutputimaginary. (((((ge_representation_imaginary_code_multiply_unique_secondoutput) = 2 * (ge_balance_positive_multiply_unique_secondoutputimaginary) /\ (ge_balance_negative_multiply_unique_secondoutputimaginary) = 0) \/ exists ge_signed_half_multiply_unique_secondoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_unique_secondoutput) = 2 * ge_signed_half_multiply_unique_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_unique_secondoutputimaginary) = 0) /\ (ge_balance_negative_multiply_unique_secondoutputimaginary) = S ge_signed_half_multiply_unique_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_multiply_unique_second) * (ge_second_ip_multiply_unique_second))) + (((ge_first_rn_multiply_unique_second) * (ge_second_in_multiply_unique_second))))) + (((((ge_first_ip_multiply_unique_second) * (ge_second_rp_multiply_unique_second))) + (((ge_first_in_multiply_unique_second) * (ge_second_rn_multiply_unique_second))))))) + ge_balance_negative_multiply_unique_secondoutputimaginary = (((((((ge_first_rp_multiply_unique_second) * (ge_second_in_multiply_unique_second))) + (((ge_first_rn_multiply_unique_second) * (ge_second_ip_multiply_unique_second))))) + (((((ge_first_ip_multiply_unique_second) * (ge_second_rn_multiply_unique_second))) + (((ge_first_in_multiply_unique_second) * (ge_second_rp_multiply_unique_second))))))) + ge_balance_positive_multiply_unique_secondoutputimaginary))))))))) -> cc = dd