gaussian_add_for_representations

Exact expanded first-order arithmetic statement

forall ac bc cc a b c d e f g h. (exists ge_representation_real_code_add_fixed_first ge_representation_imaginary_code_add_fixed_first. (((ac) = ((ge_representation_real_code_add_fixed_first) + (ge_representation_imaginary_code_add_fixed_first)) * S ((ge_representation_real_code_add_fixed_first) + (ge_representation_imaginary_code_add_fixed_first)) + ((ge_representation_imaginary_code_add_fixed_first) + (ge_representation_imaginary_code_add_fixed_first))) /\ ((exists ge_balance_positive_add_fixed_firstreal ge_balance_negative_add_fixed_firstreal. (((((ge_representation_real_code_add_fixed_first) = 2 * (ge_balance_positive_add_fixed_firstreal) /\ (ge_balance_negative_add_fixed_firstreal) = 0) \/ exists ge_signed_half_add_fixed_firstrealdecode. (((ge_representation_real_code_add_fixed_first) = 2 * ge_signed_half_add_fixed_firstrealdecode + 1 /\ (ge_balance_positive_add_fixed_firstreal) = 0) /\ (ge_balance_negative_add_fixed_firstreal) = S ge_signed_half_add_fixed_firstrealdecode))) /\ ((a) + ge_balance_negative_add_fixed_firstreal = (b) + ge_balance_positive_add_fixed_firstreal))) /\ (exists ge_balance_positive_add_fixed_firstimaginary ge_balance_negative_add_fixed_firstimaginary. (((((ge_representation_imaginary_code_add_fixed_first) = 2 * (ge_balance_positive_add_fixed_firstimaginary) /\ (ge_balance_negative_add_fixed_firstimaginary) = 0) \/ exists ge_signed_half_add_fixed_firstimaginarydecode. (((ge_representation_imaginary_code_add_fixed_first) = 2 * ge_signed_half_add_fixed_firstimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_firstimaginary) = 0) /\ (ge_balance_negative_add_fixed_firstimaginary) = S ge_signed_half_add_fixed_firstimaginarydecode))) /\ ((c) + ge_balance_negative_add_fixed_firstimaginary = (d) + ge_balance_positive_add_fixed_firstimaginary)))))) -> (exists ge_representation_real_code_add_fixed_second ge_representation_imaginary_code_add_fixed_second. (((bc) = ((ge_representation_real_code_add_fixed_second) + (ge_representation_imaginary_code_add_fixed_second)) * S ((ge_representation_real_code_add_fixed_second) + (ge_representation_imaginary_code_add_fixed_second)) + ((ge_representation_imaginary_code_add_fixed_second) + (ge_representation_imaginary_code_add_fixed_second))) /\ ((exists ge_balance_positive_add_fixed_secondreal ge_balance_negative_add_fixed_secondreal. (((((ge_representation_real_code_add_fixed_second) = 2 * (ge_balance_positive_add_fixed_secondreal) /\ (ge_balance_negative_add_fixed_secondreal) = 0) \/ exists ge_signed_half_add_fixed_secondrealdecode. (((ge_representation_real_code_add_fixed_second) = 2 * ge_signed_half_add_fixed_secondrealdecode + 1 /\ (ge_balance_positive_add_fixed_secondreal) = 0) /\ (ge_balance_negative_add_fixed_secondreal) = S ge_signed_half_add_fixed_secondrealdecode))) /\ ((e) + ge_balance_negative_add_fixed_secondreal = (f) + ge_balance_positive_add_fixed_secondreal))) /\ (exists ge_balance_positive_add_fixed_secondimaginary ge_balance_negative_add_fixed_secondimaginary. (((((ge_representation_imaginary_code_add_fixed_second) = 2 * (ge_balance_positive_add_fixed_secondimaginary) /\ (ge_balance_negative_add_fixed_secondimaginary) = 0) \/ exists ge_signed_half_add_fixed_secondimaginarydecode. (((ge_representation_imaginary_code_add_fixed_second) = 2 * ge_signed_half_add_fixed_secondimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_secondimaginary) = 0) /\ (ge_balance_negative_add_fixed_secondimaginary) = S ge_signed_half_add_fixed_secondimaginarydecode))) /\ ((g) + ge_balance_negative_add_fixed_secondimaginary = (h) + ge_balance_positive_add_fixed_secondimaginary)))))) -> (exists ge_first_rp_add_fixed_graph ge_first_rn_add_fixed_graph ge_first_ip_add_fixed_graph ge_first_in_add_fixed_graph ge_second_rp_add_fixed_graph ge_second_rn_add_fixed_graph ge_second_ip_add_fixed_graph ge_second_in_add_fixed_graph. ((exists ge_representation_real_code_add_fixed_graphfirst ge_representation_imaginary_code_add_fixed_graphfirst. (((ac) = ((ge_representation_real_code_add_fixed_graphfirst) + (ge_representation_imaginary_code_add_fixed_graphfirst)) * S ((ge_representation_real_code_add_fixed_graphfirst) + (ge_representation_imaginary_code_add_fixed_graphfirst)) + ((ge_representation_imaginary_code_add_fixed_graphfirst) + (ge_representation_imaginary_code_add_fixed_graphfirst))) /\ ((exists ge_balance_positive_add_fixed_graphfirstreal ge_balance_negative_add_fixed_graphfirstreal. (((((ge_representation_real_code_add_fixed_graphfirst) = 2 * (ge_balance_positive_add_fixed_graphfirstreal) /\ (ge_balance_negative_add_fixed_graphfirstreal) = 0) \/ exists ge_signed_half_add_fixed_graphfirstrealdecode. (((ge_representation_real_code_add_fixed_graphfirst) = 2 * ge_signed_half_add_fixed_graphfirstrealdecode + 1 /\ (ge_balance_positive_add_fixed_graphfirstreal) = 0) /\ (ge_balance_negative_add_fixed_graphfirstreal) = S ge_signed_half_add_fixed_graphfirstrealdecode))) /\ ((ge_first_rp_add_fixed_graph) + ge_balance_negative_add_fixed_graphfirstreal = (ge_first_rn_add_fixed_graph) + ge_balance_positive_add_fixed_graphfirstreal))) /\ (exists ge_balance_positive_add_fixed_graphfirstimaginary ge_balance_negative_add_fixed_graphfirstimaginary. (((((ge_representation_imaginary_code_add_fixed_graphfirst) = 2 * (ge_balance_positive_add_fixed_graphfirstimaginary) /\ (ge_balance_negative_add_fixed_graphfirstimaginary) = 0) \/ exists ge_signed_half_add_fixed_graphfirstimaginarydecode. (((ge_representation_imaginary_code_add_fixed_graphfirst) = 2 * ge_signed_half_add_fixed_graphfirstimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_graphfirstimaginary) = 0) /\ (ge_balance_negative_add_fixed_graphfirstimaginary) = S ge_signed_half_add_fixed_graphfirstimaginarydecode))) /\ ((ge_first_ip_add_fixed_graph) + ge_balance_negative_add_fixed_graphfirstimaginary = (ge_first_in_add_fixed_graph) + ge_balance_positive_add_fixed_graphfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_fixed_graphsecond ge_representation_imaginary_code_add_fixed_graphsecond. (((bc) = ((ge_representation_real_code_add_fixed_graphsecond) + (ge_representation_imaginary_code_add_fixed_graphsecond)) * S ((ge_representation_real_code_add_fixed_graphsecond) + (ge_representation_imaginary_code_add_fixed_graphsecond)) + ((ge_representation_imaginary_code_add_fixed_graphsecond) + (ge_representation_imaginary_code_add_fixed_graphsecond))) /\ ((exists ge_balance_positive_add_fixed_graphsecondreal ge_balance_negative_add_fixed_graphsecondreal. (((((ge_representation_real_code_add_fixed_graphsecond) = 2 * (ge_balance_positive_add_fixed_graphsecondreal) /\ (ge_balance_negative_add_fixed_graphsecondreal) = 0) \/ exists ge_signed_half_add_fixed_graphsecondrealdecode. (((ge_representation_real_code_add_fixed_graphsecond) = 2 * ge_signed_half_add_fixed_graphsecondrealdecode + 1 /\ (ge_balance_positive_add_fixed_graphsecondreal) = 0) /\ (ge_balance_negative_add_fixed_graphsecondreal) = S ge_signed_half_add_fixed_graphsecondrealdecode))) /\ ((ge_second_rp_add_fixed_graph) + ge_balance_negative_add_fixed_graphsecondreal = (ge_second_rn_add_fixed_graph) + ge_balance_positive_add_fixed_graphsecondreal))) /\ (exists ge_balance_positive_add_fixed_graphsecondimaginary ge_balance_negative_add_fixed_graphsecondimaginary. (((((ge_representation_imaginary_code_add_fixed_graphsecond) = 2 * (ge_balance_positive_add_fixed_graphsecondimaginary) /\ (ge_balance_negative_add_fixed_graphsecondimaginary) = 0) \/ exists ge_signed_half_add_fixed_graphsecondimaginarydecode. (((ge_representation_imaginary_code_add_fixed_graphsecond) = 2 * ge_signed_half_add_fixed_graphsecondimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_graphsecondimaginary) = 0) /\ (ge_balance_negative_add_fixed_graphsecondimaginary) = S ge_signed_half_add_fixed_graphsecondimaginarydecode))) /\ ((ge_second_ip_add_fixed_graph) + ge_balance_negative_add_fixed_graphsecondimaginary = (ge_second_in_add_fixed_graph) + ge_balance_positive_add_fixed_graphsecondimaginary)))))) /\ (exists ge_representation_real_code_add_fixed_graphoutput ge_representation_imaginary_code_add_fixed_graphoutput. (((cc) = ((ge_representation_real_code_add_fixed_graphoutput) + (ge_representation_imaginary_code_add_fixed_graphoutput)) * S ((ge_representation_real_code_add_fixed_graphoutput) + (ge_representation_imaginary_code_add_fixed_graphoutput)) + ((ge_representation_imaginary_code_add_fixed_graphoutput) + (ge_representation_imaginary_code_add_fixed_graphoutput))) /\ ((exists ge_balance_positive_add_fixed_graphoutputreal ge_balance_negative_add_fixed_graphoutputreal. (((((ge_representation_real_code_add_fixed_graphoutput) = 2 * (ge_balance_positive_add_fixed_graphoutputreal) /\ (ge_balance_negative_add_fixed_graphoutputreal) = 0) \/ exists ge_signed_half_add_fixed_graphoutputrealdecode. (((ge_representation_real_code_add_fixed_graphoutput) = 2 * ge_signed_half_add_fixed_graphoutputrealdecode + 1 /\ (ge_balance_positive_add_fixed_graphoutputreal) = 0) /\ (ge_balance_negative_add_fixed_graphoutputreal) = S ge_signed_half_add_fixed_graphoutputrealdecode))) /\ ((((ge_first_rp_add_fixed_graph) + (ge_second_rp_add_fixed_graph))) + ge_balance_negative_add_fixed_graphoutputreal = (((ge_first_rn_add_fixed_graph) + (ge_second_rn_add_fixed_graph))) + ge_balance_positive_add_fixed_graphoutputreal))) /\ (exists ge_balance_positive_add_fixed_graphoutputimaginary ge_balance_negative_add_fixed_graphoutputimaginary. (((((ge_representation_imaginary_code_add_fixed_graphoutput) = 2 * (ge_balance_positive_add_fixed_graphoutputimaginary) /\ (ge_balance_negative_add_fixed_graphoutputimaginary) = 0) \/ exists ge_signed_half_add_fixed_graphoutputimaginarydecode. (((ge_representation_imaginary_code_add_fixed_graphoutput) = 2 * ge_signed_half_add_fixed_graphoutputimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_graphoutputimaginary) = 0) /\ (ge_balance_negative_add_fixed_graphoutputimaginary) = S ge_signed_half_add_fixed_graphoutputimaginarydecode))) /\ ((((ge_first_ip_add_fixed_graph) + (ge_second_ip_add_fixed_graph))) + ge_balance_negative_add_fixed_graphoutputimaginary = (((ge_first_in_add_fixed_graph) + (ge_second_in_add_fixed_graph))) + ge_balance_positive_add_fixed_graphoutputimaginary))))))))) -> (exists ge_representation_real_code_add_fixed_output ge_representation_imaginary_code_add_fixed_output. (((cc) = ((ge_representation_real_code_add_fixed_output) + (ge_representation_imaginary_code_add_fixed_output)) * S ((ge_representation_real_code_add_fixed_output) + (ge_representation_imaginary_code_add_fixed_output)) + ((ge_representation_imaginary_code_add_fixed_output) + (ge_representation_imaginary_code_add_fixed_output))) /\ ((exists ge_balance_positive_add_fixed_outputreal ge_balance_negative_add_fixed_outputreal. (((((ge_representation_real_code_add_fixed_output) = 2 * (ge_balance_positive_add_fixed_outputreal) /\ (ge_balance_negative_add_fixed_outputreal) = 0) \/ exists ge_signed_half_add_fixed_outputrealdecode. (((ge_representation_real_code_add_fixed_output) = 2 * ge_signed_half_add_fixed_outputrealdecode + 1 /\ (ge_balance_positive_add_fixed_outputreal) = 0) /\ (ge_balance_negative_add_fixed_outputreal) = S ge_signed_half_add_fixed_outputrealdecode))) /\ ((((a) + (e))) + ge_balance_negative_add_fixed_outputreal = (((b) + (f))) + ge_balance_positive_add_fixed_outputreal))) /\ (exists ge_balance_positive_add_fixed_outputimaginary ge_balance_negative_add_fixed_outputimaginary. (((((ge_representation_imaginary_code_add_fixed_output) = 2 * (ge_balance_positive_add_fixed_outputimaginary) /\ (ge_balance_negative_add_fixed_outputimaginary) = 0) \/ exists ge_signed_half_add_fixed_outputimaginarydecode. (((ge_representation_imaginary_code_add_fixed_output) = 2 * ge_signed_half_add_fixed_outputimaginarydecode + 1 /\ (ge_balance_positive_add_fixed_outputimaginary) = 0) /\ (ge_balance_negative_add_fixed_outputimaginary) = S ge_signed_half_add_fixed_outputimaginarydecode))) /\ ((((c) + (g))) + ge_balance_negative_add_fixed_outputimaginary = (((d) + (h))) + ge_balance_positive_add_fixed_outputimaginary))))))