eisenstein_add_functional

Exact expanded first-order arithmetic statement

forall ac bc cc dd. (exists ge_first_rp_add_unique_first ge_first_rn_add_unique_first ge_first_ip_add_unique_first ge_first_in_add_unique_first ge_second_rp_add_unique_first ge_second_rn_add_unique_first ge_second_ip_add_unique_first ge_second_in_add_unique_first. ((exists ge_representation_real_code_add_unique_firstfirst ge_representation_imaginary_code_add_unique_firstfirst. (((ac) = ((ge_representation_real_code_add_unique_firstfirst) + (ge_representation_imaginary_code_add_unique_firstfirst)) * S ((ge_representation_real_code_add_unique_firstfirst) + (ge_representation_imaginary_code_add_unique_firstfirst)) + ((ge_representation_imaginary_code_add_unique_firstfirst) + (ge_representation_imaginary_code_add_unique_firstfirst))) /\ ((exists ge_balance_positive_add_unique_firstfirstreal ge_balance_negative_add_unique_firstfirstreal. (((((ge_representation_real_code_add_unique_firstfirst) = 2 * (ge_balance_positive_add_unique_firstfirstreal) /\ (ge_balance_negative_add_unique_firstfirstreal) = 0) \/ exists ge_signed_half_add_unique_firstfirstrealdecode. (((ge_representation_real_code_add_unique_firstfirst) = 2 * ge_signed_half_add_unique_firstfirstrealdecode + 1 /\ (ge_balance_positive_add_unique_firstfirstreal) = 0) /\ (ge_balance_negative_add_unique_firstfirstreal) = S ge_signed_half_add_unique_firstfirstrealdecode))) /\ ((ge_first_rp_add_unique_first) + ge_balance_negative_add_unique_firstfirstreal = (ge_first_rn_add_unique_first) + ge_balance_positive_add_unique_firstfirstreal))) /\ (exists ge_balance_positive_add_unique_firstfirstimaginary ge_balance_negative_add_unique_firstfirstimaginary. (((((ge_representation_imaginary_code_add_unique_firstfirst) = 2 * (ge_balance_positive_add_unique_firstfirstimaginary) /\ (ge_balance_negative_add_unique_firstfirstimaginary) = 0) \/ exists ge_signed_half_add_unique_firstfirstimaginarydecode. (((ge_representation_imaginary_code_add_unique_firstfirst) = 2 * ge_signed_half_add_unique_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_add_unique_firstfirstimaginary) = 0) /\ (ge_balance_negative_add_unique_firstfirstimaginary) = S ge_signed_half_add_unique_firstfirstimaginarydecode))) /\ ((ge_first_ip_add_unique_first) + ge_balance_negative_add_unique_firstfirstimaginary = (ge_first_in_add_unique_first) + ge_balance_positive_add_unique_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_unique_firstsecond ge_representation_imaginary_code_add_unique_firstsecond. (((bc) = ((ge_representation_real_code_add_unique_firstsecond) + (ge_representation_imaginary_code_add_unique_firstsecond)) * S ((ge_representation_real_code_add_unique_firstsecond) + (ge_representation_imaginary_code_add_unique_firstsecond)) + ((ge_representation_imaginary_code_add_unique_firstsecond) + (ge_representation_imaginary_code_add_unique_firstsecond))) /\ ((exists ge_balance_positive_add_unique_firstsecondreal ge_balance_negative_add_unique_firstsecondreal. (((((ge_representation_real_code_add_unique_firstsecond) = 2 * (ge_balance_positive_add_unique_firstsecondreal) /\ (ge_balance_negative_add_unique_firstsecondreal) = 0) \/ exists ge_signed_half_add_unique_firstsecondrealdecode. (((ge_representation_real_code_add_unique_firstsecond) = 2 * ge_signed_half_add_unique_firstsecondrealdecode + 1 /\ (ge_balance_positive_add_unique_firstsecondreal) = 0) /\ (ge_balance_negative_add_unique_firstsecondreal) = S ge_signed_half_add_unique_firstsecondrealdecode))) /\ ((ge_second_rp_add_unique_first) + ge_balance_negative_add_unique_firstsecondreal = (ge_second_rn_add_unique_first) + ge_balance_positive_add_unique_firstsecondreal))) /\ (exists ge_balance_positive_add_unique_firstsecondimaginary ge_balance_negative_add_unique_firstsecondimaginary. (((((ge_representation_imaginary_code_add_unique_firstsecond) = 2 * (ge_balance_positive_add_unique_firstsecondimaginary) /\ (ge_balance_negative_add_unique_firstsecondimaginary) = 0) \/ exists ge_signed_half_add_unique_firstsecondimaginarydecode. (((ge_representation_imaginary_code_add_unique_firstsecond) = 2 * ge_signed_half_add_unique_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_add_unique_firstsecondimaginary) = 0) /\ (ge_balance_negative_add_unique_firstsecondimaginary) = S ge_signed_half_add_unique_firstsecondimaginarydecode))) /\ ((ge_second_ip_add_unique_first) + ge_balance_negative_add_unique_firstsecondimaginary = (ge_second_in_add_unique_first) + ge_balance_positive_add_unique_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_add_unique_firstoutput ge_representation_imaginary_code_add_unique_firstoutput. (((cc) = ((ge_representation_real_code_add_unique_firstoutput) + (ge_representation_imaginary_code_add_unique_firstoutput)) * S ((ge_representation_real_code_add_unique_firstoutput) + (ge_representation_imaginary_code_add_unique_firstoutput)) + ((ge_representation_imaginary_code_add_unique_firstoutput) + (ge_representation_imaginary_code_add_unique_firstoutput))) /\ ((exists ge_balance_positive_add_unique_firstoutputreal ge_balance_negative_add_unique_firstoutputreal. (((((ge_representation_real_code_add_unique_firstoutput) = 2 * (ge_balance_positive_add_unique_firstoutputreal) /\ (ge_balance_negative_add_unique_firstoutputreal) = 0) \/ exists ge_signed_half_add_unique_firstoutputrealdecode. (((ge_representation_real_code_add_unique_firstoutput) = 2 * ge_signed_half_add_unique_firstoutputrealdecode + 1 /\ (ge_balance_positive_add_unique_firstoutputreal) = 0) /\ (ge_balance_negative_add_unique_firstoutputreal) = S ge_signed_half_add_unique_firstoutputrealdecode))) /\ ((((ge_first_rp_add_unique_first) + (ge_second_rp_add_unique_first))) + ge_balance_negative_add_unique_firstoutputreal = (((ge_first_rn_add_unique_first) + (ge_second_rn_add_unique_first))) + ge_balance_positive_add_unique_firstoutputreal))) /\ (exists ge_balance_positive_add_unique_firstoutputimaginary ge_balance_negative_add_unique_firstoutputimaginary. (((((ge_representation_imaginary_code_add_unique_firstoutput) = 2 * (ge_balance_positive_add_unique_firstoutputimaginary) /\ (ge_balance_negative_add_unique_firstoutputimaginary) = 0) \/ exists ge_signed_half_add_unique_firstoutputimaginarydecode. (((ge_representation_imaginary_code_add_unique_firstoutput) = 2 * ge_signed_half_add_unique_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_add_unique_firstoutputimaginary) = 0) /\ (ge_balance_negative_add_unique_firstoutputimaginary) = S ge_signed_half_add_unique_firstoutputimaginarydecode))) /\ ((((ge_first_ip_add_unique_first) + (ge_second_ip_add_unique_first))) + ge_balance_negative_add_unique_firstoutputimaginary = (((ge_first_in_add_unique_first) + (ge_second_in_add_unique_first))) + ge_balance_positive_add_unique_firstoutputimaginary))))))))) -> (exists ge_first_rp_add_unique_second ge_first_rn_add_unique_second ge_first_ip_add_unique_second ge_first_in_add_unique_second ge_second_rp_add_unique_second ge_second_rn_add_unique_second ge_second_ip_add_unique_second ge_second_in_add_unique_second. ((exists ge_representation_real_code_add_unique_secondfirst ge_representation_imaginary_code_add_unique_secondfirst. (((ac) = ((ge_representation_real_code_add_unique_secondfirst) + (ge_representation_imaginary_code_add_unique_secondfirst)) * S ((ge_representation_real_code_add_unique_secondfirst) + (ge_representation_imaginary_code_add_unique_secondfirst)) + ((ge_representation_imaginary_code_add_unique_secondfirst) + (ge_representation_imaginary_code_add_unique_secondfirst))) /\ ((exists ge_balance_positive_add_unique_secondfirstreal ge_balance_negative_add_unique_secondfirstreal. (((((ge_representation_real_code_add_unique_secondfirst) = 2 * (ge_balance_positive_add_unique_secondfirstreal) /\ (ge_balance_negative_add_unique_secondfirstreal) = 0) \/ exists ge_signed_half_add_unique_secondfirstrealdecode. (((ge_representation_real_code_add_unique_secondfirst) = 2 * ge_signed_half_add_unique_secondfirstrealdecode + 1 /\ (ge_balance_positive_add_unique_secondfirstreal) = 0) /\ (ge_balance_negative_add_unique_secondfirstreal) = S ge_signed_half_add_unique_secondfirstrealdecode))) /\ ((ge_first_rp_add_unique_second) + ge_balance_negative_add_unique_secondfirstreal = (ge_first_rn_add_unique_second) + ge_balance_positive_add_unique_secondfirstreal))) /\ (exists ge_balance_positive_add_unique_secondfirstimaginary ge_balance_negative_add_unique_secondfirstimaginary. (((((ge_representation_imaginary_code_add_unique_secondfirst) = 2 * (ge_balance_positive_add_unique_secondfirstimaginary) /\ (ge_balance_negative_add_unique_secondfirstimaginary) = 0) \/ exists ge_signed_half_add_unique_secondfirstimaginarydecode. (((ge_representation_imaginary_code_add_unique_secondfirst) = 2 * ge_signed_half_add_unique_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_add_unique_secondfirstimaginary) = 0) /\ (ge_balance_negative_add_unique_secondfirstimaginary) = S ge_signed_half_add_unique_secondfirstimaginarydecode))) /\ ((ge_first_ip_add_unique_second) + ge_balance_negative_add_unique_secondfirstimaginary = (ge_first_in_add_unique_second) + ge_balance_positive_add_unique_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_unique_secondsecond ge_representation_imaginary_code_add_unique_secondsecond. (((bc) = ((ge_representation_real_code_add_unique_secondsecond) + (ge_representation_imaginary_code_add_unique_secondsecond)) * S ((ge_representation_real_code_add_unique_secondsecond) + (ge_representation_imaginary_code_add_unique_secondsecond)) + ((ge_representation_imaginary_code_add_unique_secondsecond) + (ge_representation_imaginary_code_add_unique_secondsecond))) /\ ((exists ge_balance_positive_add_unique_secondsecondreal ge_balance_negative_add_unique_secondsecondreal. (((((ge_representation_real_code_add_unique_secondsecond) = 2 * (ge_balance_positive_add_unique_secondsecondreal) /\ (ge_balance_negative_add_unique_secondsecondreal) = 0) \/ exists ge_signed_half_add_unique_secondsecondrealdecode. (((ge_representation_real_code_add_unique_secondsecond) = 2 * ge_signed_half_add_unique_secondsecondrealdecode + 1 /\ (ge_balance_positive_add_unique_secondsecondreal) = 0) /\ (ge_balance_negative_add_unique_secondsecondreal) = S ge_signed_half_add_unique_secondsecondrealdecode))) /\ ((ge_second_rp_add_unique_second) + ge_balance_negative_add_unique_secondsecondreal = (ge_second_rn_add_unique_second) + ge_balance_positive_add_unique_secondsecondreal))) /\ (exists ge_balance_positive_add_unique_secondsecondimaginary ge_balance_negative_add_unique_secondsecondimaginary. (((((ge_representation_imaginary_code_add_unique_secondsecond) = 2 * (ge_balance_positive_add_unique_secondsecondimaginary) /\ (ge_balance_negative_add_unique_secondsecondimaginary) = 0) \/ exists ge_signed_half_add_unique_secondsecondimaginarydecode. (((ge_representation_imaginary_code_add_unique_secondsecond) = 2 * ge_signed_half_add_unique_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_add_unique_secondsecondimaginary) = 0) /\ (ge_balance_negative_add_unique_secondsecondimaginary) = S ge_signed_half_add_unique_secondsecondimaginarydecode))) /\ ((ge_second_ip_add_unique_second) + ge_balance_negative_add_unique_secondsecondimaginary = (ge_second_in_add_unique_second) + ge_balance_positive_add_unique_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_add_unique_secondoutput ge_representation_imaginary_code_add_unique_secondoutput. (((dd) = ((ge_representation_real_code_add_unique_secondoutput) + (ge_representation_imaginary_code_add_unique_secondoutput)) * S ((ge_representation_real_code_add_unique_secondoutput) + (ge_representation_imaginary_code_add_unique_secondoutput)) + ((ge_representation_imaginary_code_add_unique_secondoutput) + (ge_representation_imaginary_code_add_unique_secondoutput))) /\ ((exists ge_balance_positive_add_unique_secondoutputreal ge_balance_negative_add_unique_secondoutputreal. (((((ge_representation_real_code_add_unique_secondoutput) = 2 * (ge_balance_positive_add_unique_secondoutputreal) /\ (ge_balance_negative_add_unique_secondoutputreal) = 0) \/ exists ge_signed_half_add_unique_secondoutputrealdecode. (((ge_representation_real_code_add_unique_secondoutput) = 2 * ge_signed_half_add_unique_secondoutputrealdecode + 1 /\ (ge_balance_positive_add_unique_secondoutputreal) = 0) /\ (ge_balance_negative_add_unique_secondoutputreal) = S ge_signed_half_add_unique_secondoutputrealdecode))) /\ ((((ge_first_rp_add_unique_second) + (ge_second_rp_add_unique_second))) + ge_balance_negative_add_unique_secondoutputreal = (((ge_first_rn_add_unique_second) + (ge_second_rn_add_unique_second))) + ge_balance_positive_add_unique_secondoutputreal))) /\ (exists ge_balance_positive_add_unique_secondoutputimaginary ge_balance_negative_add_unique_secondoutputimaginary. (((((ge_representation_imaginary_code_add_unique_secondoutput) = 2 * (ge_balance_positive_add_unique_secondoutputimaginary) /\ (ge_balance_negative_add_unique_secondoutputimaginary) = 0) \/ exists ge_signed_half_add_unique_secondoutputimaginarydecode. (((ge_representation_imaginary_code_add_unique_secondoutput) = 2 * ge_signed_half_add_unique_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_add_unique_secondoutputimaginary) = 0) /\ (ge_balance_negative_add_unique_secondoutputimaginary) = S ge_signed_half_add_unique_secondoutputimaginarydecode))) /\ ((((ge_first_ip_add_unique_second) + (ge_second_ip_add_unique_second))) + ge_balance_negative_add_unique_secondoutputimaginary = (((ge_first_in_add_unique_second) + (ge_second_in_add_unique_second))) + ge_balance_positive_add_unique_secondoutputimaginary))))))))) -> cc = dd