gaussian_multiply_of_representations

Exact expanded first-order arithmetic statement

forall ac bc cc a b c d e f g h. (exists ge_representation_real_code_multiply_intro_first ge_representation_imaginary_code_multiply_intro_first. (((ac) = ((ge_representation_real_code_multiply_intro_first) + (ge_representation_imaginary_code_multiply_intro_first)) * S ((ge_representation_real_code_multiply_intro_first) + (ge_representation_imaginary_code_multiply_intro_first)) + ((ge_representation_imaginary_code_multiply_intro_first) + (ge_representation_imaginary_code_multiply_intro_first))) /\ ((exists ge_balance_positive_multiply_intro_firstreal ge_balance_negative_multiply_intro_firstreal. (((((ge_representation_real_code_multiply_intro_first) = 2 * (ge_balance_positive_multiply_intro_firstreal) /\ (ge_balance_negative_multiply_intro_firstreal) = 0) \/ exists ge_signed_half_multiply_intro_firstrealdecode. (((ge_representation_real_code_multiply_intro_first) = 2 * ge_signed_half_multiply_intro_firstrealdecode + 1 /\ (ge_balance_positive_multiply_intro_firstreal) = 0) /\ (ge_balance_negative_multiply_intro_firstreal) = S ge_signed_half_multiply_intro_firstrealdecode))) /\ ((a) + ge_balance_negative_multiply_intro_firstreal = (b) + ge_balance_positive_multiply_intro_firstreal))) /\ (exists ge_balance_positive_multiply_intro_firstimaginary ge_balance_negative_multiply_intro_firstimaginary. (((((ge_representation_imaginary_code_multiply_intro_first) = 2 * (ge_balance_positive_multiply_intro_firstimaginary) /\ (ge_balance_negative_multiply_intro_firstimaginary) = 0) \/ exists ge_signed_half_multiply_intro_firstimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_first) = 2 * ge_signed_half_multiply_intro_firstimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_firstimaginary) = 0) /\ (ge_balance_negative_multiply_intro_firstimaginary) = S ge_signed_half_multiply_intro_firstimaginarydecode))) /\ ((c) + ge_balance_negative_multiply_intro_firstimaginary = (d) + ge_balance_positive_multiply_intro_firstimaginary)))))) -> (exists ge_representation_real_code_multiply_intro_second ge_representation_imaginary_code_multiply_intro_second. (((bc) = ((ge_representation_real_code_multiply_intro_second) + (ge_representation_imaginary_code_multiply_intro_second)) * S ((ge_representation_real_code_multiply_intro_second) + (ge_representation_imaginary_code_multiply_intro_second)) + ((ge_representation_imaginary_code_multiply_intro_second) + (ge_representation_imaginary_code_multiply_intro_second))) /\ ((exists ge_balance_positive_multiply_intro_secondreal ge_balance_negative_multiply_intro_secondreal. (((((ge_representation_real_code_multiply_intro_second) = 2 * (ge_balance_positive_multiply_intro_secondreal) /\ (ge_balance_negative_multiply_intro_secondreal) = 0) \/ exists ge_signed_half_multiply_intro_secondrealdecode. (((ge_representation_real_code_multiply_intro_second) = 2 * ge_signed_half_multiply_intro_secondrealdecode + 1 /\ (ge_balance_positive_multiply_intro_secondreal) = 0) /\ (ge_balance_negative_multiply_intro_secondreal) = S ge_signed_half_multiply_intro_secondrealdecode))) /\ ((e) + ge_balance_negative_multiply_intro_secondreal = (f) + ge_balance_positive_multiply_intro_secondreal))) /\ (exists ge_balance_positive_multiply_intro_secondimaginary ge_balance_negative_multiply_intro_secondimaginary. (((((ge_representation_imaginary_code_multiply_intro_second) = 2 * (ge_balance_positive_multiply_intro_secondimaginary) /\ (ge_balance_negative_multiply_intro_secondimaginary) = 0) \/ exists ge_signed_half_multiply_intro_secondimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_second) = 2 * ge_signed_half_multiply_intro_secondimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_secondimaginary) = 0) /\ (ge_balance_negative_multiply_intro_secondimaginary) = S ge_signed_half_multiply_intro_secondimaginarydecode))) /\ ((g) + ge_balance_negative_multiply_intro_secondimaginary = (h) + ge_balance_positive_multiply_intro_secondimaginary)))))) -> (exists ge_representation_real_code_multiply_intro_output ge_representation_imaginary_code_multiply_intro_output. (((cc) = ((ge_representation_real_code_multiply_intro_output) + (ge_representation_imaginary_code_multiply_intro_output)) * S ((ge_representation_real_code_multiply_intro_output) + (ge_representation_imaginary_code_multiply_intro_output)) + ((ge_representation_imaginary_code_multiply_intro_output) + (ge_representation_imaginary_code_multiply_intro_output))) /\ ((exists ge_balance_positive_multiply_intro_outputreal ge_balance_negative_multiply_intro_outputreal. (((((ge_representation_real_code_multiply_intro_output) = 2 * (ge_balance_positive_multiply_intro_outputreal) /\ (ge_balance_negative_multiply_intro_outputreal) = 0) \/ exists ge_signed_half_multiply_intro_outputrealdecode. (((ge_representation_real_code_multiply_intro_output) = 2 * ge_signed_half_multiply_intro_outputrealdecode + 1 /\ (ge_balance_positive_multiply_intro_outputreal) = 0) /\ (ge_balance_negative_multiply_intro_outputreal) = S ge_signed_half_multiply_intro_outputrealdecode))) /\ ((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + ge_balance_negative_multiply_intro_outputreal = (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + ge_balance_positive_multiply_intro_outputreal))) /\ (exists ge_balance_positive_multiply_intro_outputimaginary ge_balance_negative_multiply_intro_outputimaginary. (((((ge_representation_imaginary_code_multiply_intro_output) = 2 * (ge_balance_positive_multiply_intro_outputimaginary) /\ (ge_balance_negative_multiply_intro_outputimaginary) = 0) \/ exists ge_signed_half_multiply_intro_outputimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_output) = 2 * ge_signed_half_multiply_intro_outputimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_outputimaginary) = 0) /\ (ge_balance_negative_multiply_intro_outputimaginary) = S ge_signed_half_multiply_intro_outputimaginarydecode))) /\ ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + ge_balance_negative_multiply_intro_outputimaginary = (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + ge_balance_positive_multiply_intro_outputimaginary)))))) -> (exists ge_first_rp_multiply_intro_graph ge_first_rn_multiply_intro_graph ge_first_ip_multiply_intro_graph ge_first_in_multiply_intro_graph ge_second_rp_multiply_intro_graph ge_second_rn_multiply_intro_graph ge_second_ip_multiply_intro_graph ge_second_in_multiply_intro_graph. ((exists ge_representation_real_code_multiply_intro_graphfirst ge_representation_imaginary_code_multiply_intro_graphfirst. (((ac) = ((ge_representation_real_code_multiply_intro_graphfirst) + (ge_representation_imaginary_code_multiply_intro_graphfirst)) * S ((ge_representation_real_code_multiply_intro_graphfirst) + (ge_representation_imaginary_code_multiply_intro_graphfirst)) + ((ge_representation_imaginary_code_multiply_intro_graphfirst) + (ge_representation_imaginary_code_multiply_intro_graphfirst))) /\ ((exists ge_balance_positive_multiply_intro_graphfirstreal ge_balance_negative_multiply_intro_graphfirstreal. (((((ge_representation_real_code_multiply_intro_graphfirst) = 2 * (ge_balance_positive_multiply_intro_graphfirstreal) /\ (ge_balance_negative_multiply_intro_graphfirstreal) = 0) \/ exists ge_signed_half_multiply_intro_graphfirstrealdecode. (((ge_representation_real_code_multiply_intro_graphfirst) = 2 * ge_signed_half_multiply_intro_graphfirstrealdecode + 1 /\ (ge_balance_positive_multiply_intro_graphfirstreal) = 0) /\ (ge_balance_negative_multiply_intro_graphfirstreal) = S ge_signed_half_multiply_intro_graphfirstrealdecode))) /\ ((ge_first_rp_multiply_intro_graph) + ge_balance_negative_multiply_intro_graphfirstreal = (ge_first_rn_multiply_intro_graph) + ge_balance_positive_multiply_intro_graphfirstreal))) /\ (exists ge_balance_positive_multiply_intro_graphfirstimaginary ge_balance_negative_multiply_intro_graphfirstimaginary. (((((ge_representation_imaginary_code_multiply_intro_graphfirst) = 2 * (ge_balance_positive_multiply_intro_graphfirstimaginary) /\ (ge_balance_negative_multiply_intro_graphfirstimaginary) = 0) \/ exists ge_signed_half_multiply_intro_graphfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_graphfirst) = 2 * ge_signed_half_multiply_intro_graphfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_graphfirstimaginary) = 0) /\ (ge_balance_negative_multiply_intro_graphfirstimaginary) = S ge_signed_half_multiply_intro_graphfirstimaginarydecode))) /\ ((ge_first_ip_multiply_intro_graph) + ge_balance_negative_multiply_intro_graphfirstimaginary = (ge_first_in_multiply_intro_graph) + ge_balance_positive_multiply_intro_graphfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_intro_graphsecond ge_representation_imaginary_code_multiply_intro_graphsecond. (((bc) = ((ge_representation_real_code_multiply_intro_graphsecond) + (ge_representation_imaginary_code_multiply_intro_graphsecond)) * S ((ge_representation_real_code_multiply_intro_graphsecond) + (ge_representation_imaginary_code_multiply_intro_graphsecond)) + ((ge_representation_imaginary_code_multiply_intro_graphsecond) + (ge_representation_imaginary_code_multiply_intro_graphsecond))) /\ ((exists ge_balance_positive_multiply_intro_graphsecondreal ge_balance_negative_multiply_intro_graphsecondreal. (((((ge_representation_real_code_multiply_intro_graphsecond) = 2 * (ge_balance_positive_multiply_intro_graphsecondreal) /\ (ge_balance_negative_multiply_intro_graphsecondreal) = 0) \/ exists ge_signed_half_multiply_intro_graphsecondrealdecode. (((ge_representation_real_code_multiply_intro_graphsecond) = 2 * ge_signed_half_multiply_intro_graphsecondrealdecode + 1 /\ (ge_balance_positive_multiply_intro_graphsecondreal) = 0) /\ (ge_balance_negative_multiply_intro_graphsecondreal) = S ge_signed_half_multiply_intro_graphsecondrealdecode))) /\ ((ge_second_rp_multiply_intro_graph) + ge_balance_negative_multiply_intro_graphsecondreal = (ge_second_rn_multiply_intro_graph) + ge_balance_positive_multiply_intro_graphsecondreal))) /\ (exists ge_balance_positive_multiply_intro_graphsecondimaginary ge_balance_negative_multiply_intro_graphsecondimaginary. (((((ge_representation_imaginary_code_multiply_intro_graphsecond) = 2 * (ge_balance_positive_multiply_intro_graphsecondimaginary) /\ (ge_balance_negative_multiply_intro_graphsecondimaginary) = 0) \/ exists ge_signed_half_multiply_intro_graphsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_graphsecond) = 2 * ge_signed_half_multiply_intro_graphsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_graphsecondimaginary) = 0) /\ (ge_balance_negative_multiply_intro_graphsecondimaginary) = S ge_signed_half_multiply_intro_graphsecondimaginarydecode))) /\ ((ge_second_ip_multiply_intro_graph) + ge_balance_negative_multiply_intro_graphsecondimaginary = (ge_second_in_multiply_intro_graph) + ge_balance_positive_multiply_intro_graphsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_intro_graphoutput ge_representation_imaginary_code_multiply_intro_graphoutput. (((cc) = ((ge_representation_real_code_multiply_intro_graphoutput) + (ge_representation_imaginary_code_multiply_intro_graphoutput)) * S ((ge_representation_real_code_multiply_intro_graphoutput) + (ge_representation_imaginary_code_multiply_intro_graphoutput)) + ((ge_representation_imaginary_code_multiply_intro_graphoutput) + (ge_representation_imaginary_code_multiply_intro_graphoutput))) /\ ((exists ge_balance_positive_multiply_intro_graphoutputreal ge_balance_negative_multiply_intro_graphoutputreal. (((((ge_representation_real_code_multiply_intro_graphoutput) = 2 * (ge_balance_positive_multiply_intro_graphoutputreal) /\ (ge_balance_negative_multiply_intro_graphoutputreal) = 0) \/ exists ge_signed_half_multiply_intro_graphoutputrealdecode. (((ge_representation_real_code_multiply_intro_graphoutput) = 2 * ge_signed_half_multiply_intro_graphoutputrealdecode + 1 /\ (ge_balance_positive_multiply_intro_graphoutputreal) = 0) /\ (ge_balance_negative_multiply_intro_graphoutputreal) = S ge_signed_half_multiply_intro_graphoutputrealdecode))) /\ ((((((((ge_first_rp_multiply_intro_graph) * (ge_second_rp_multiply_intro_graph))) + (((ge_first_rn_multiply_intro_graph) * (ge_second_rn_multiply_intro_graph))))) + (((((ge_first_ip_multiply_intro_graph) * (ge_second_in_multiply_intro_graph))) + (((ge_first_in_multiply_intro_graph) * (ge_second_ip_multiply_intro_graph))))))) + ge_balance_negative_multiply_intro_graphoutputreal = (((((((ge_first_rp_multiply_intro_graph) * (ge_second_rn_multiply_intro_graph))) + (((ge_first_rn_multiply_intro_graph) * (ge_second_rp_multiply_intro_graph))))) + (((((ge_first_ip_multiply_intro_graph) * (ge_second_ip_multiply_intro_graph))) + (((ge_first_in_multiply_intro_graph) * (ge_second_in_multiply_intro_graph))))))) + ge_balance_positive_multiply_intro_graphoutputreal))) /\ (exists ge_balance_positive_multiply_intro_graphoutputimaginary ge_balance_negative_multiply_intro_graphoutputimaginary. (((((ge_representation_imaginary_code_multiply_intro_graphoutput) = 2 * (ge_balance_positive_multiply_intro_graphoutputimaginary) /\ (ge_balance_negative_multiply_intro_graphoutputimaginary) = 0) \/ exists ge_signed_half_multiply_intro_graphoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_graphoutput) = 2 * ge_signed_half_multiply_intro_graphoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_graphoutputimaginary) = 0) /\ (ge_balance_negative_multiply_intro_graphoutputimaginary) = S ge_signed_half_multiply_intro_graphoutputimaginarydecode))) /\ ((((((((ge_first_rp_multiply_intro_graph) * (ge_second_ip_multiply_intro_graph))) + (((ge_first_rn_multiply_intro_graph) * (ge_second_in_multiply_intro_graph))))) + (((((ge_first_ip_multiply_intro_graph) * (ge_second_rp_multiply_intro_graph))) + (((ge_first_in_multiply_intro_graph) * (ge_second_rn_multiply_intro_graph))))))) + ge_balance_negative_multiply_intro_graphoutputimaginary = (((((((ge_first_rp_multiply_intro_graph) * (ge_second_in_multiply_intro_graph))) + (((ge_first_rn_multiply_intro_graph) * (ge_second_ip_multiply_intro_graph))))) + (((((ge_first_ip_multiply_intro_graph) * (ge_second_rn_multiply_intro_graph))) + (((ge_first_in_multiply_intro_graph) * (ge_second_rp_multiply_intro_graph))))))) + ge_balance_positive_multiply_intro_graphoutputimaginary)))))))))