gaussian_multiply_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_multiply_fixed_first ge_representation_imaginary_code_multiply_fixed_first. (((ac) = ((ge_representation_real_code_multiply_fixed_first) + (ge_representation_imaginary_code_multiply_fixed_first)) * S ((ge_representation_real_code_multiply_fixed_first) + (ge_representation_imaginary_code_multiply_fixed_first)) + ((ge_representation_imaginary_code_multiply_fixed_first) + (ge_representation_imaginary_code_multiply_fixed_first))) /\ ((exists ge_balance_positive_multiply_fixed_firstreal ge_balance_negative_multiply_fixed_firstreal. (((((ge_representation_real_code_multiply_fixed_first) = 2 * (ge_balance_positive_multiply_fixed_firstreal) /\ (ge_balance_negative_multiply_fixed_firstreal) = 0) \/ exists ge_signed_half_multiply_fixed_firstrealdecode. (((ge_representation_real_code_multiply_fixed_first) = 2 * ge_signed_half_multiply_fixed_firstrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_firstreal) = 0) /\ (ge_balance_negative_multiply_fixed_firstreal) = S ge_signed_half_multiply_fixed_firstrealdecode))) /\ ((a) + ge_balance_negative_multiply_fixed_firstreal = (b) + ge_balance_positive_multiply_fixed_firstreal))) /\ (exists ge_balance_positive_multiply_fixed_firstimaginary ge_balance_negative_multiply_fixed_firstimaginary. (((((ge_representation_imaginary_code_multiply_fixed_first) = 2 * (ge_balance_positive_multiply_fixed_firstimaginary) /\ (ge_balance_negative_multiply_fixed_firstimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_firstimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_first) = 2 * ge_signed_half_multiply_fixed_firstimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_firstimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_firstimaginary) = S ge_signed_half_multiply_fixed_firstimaginarydecode))) /\ ((c) + ge_balance_negative_multiply_fixed_firstimaginary = (d) + ge_balance_positive_multiply_fixed_firstimaginary)))))) -> (exists ge_representation_real_code_multiply_fixed_second ge_representation_imaginary_code_multiply_fixed_second. (((bc) = ((ge_representation_real_code_multiply_fixed_second) + (ge_representation_imaginary_code_multiply_fixed_second)) * S ((ge_representation_real_code_multiply_fixed_second) + (ge_representation_imaginary_code_multiply_fixed_second)) + ((ge_representation_imaginary_code_multiply_fixed_second) + (ge_representation_imaginary_code_multiply_fixed_second))) /\ ((exists ge_balance_positive_multiply_fixed_secondreal ge_balance_negative_multiply_fixed_secondreal. (((((ge_representation_real_code_multiply_fixed_second) = 2 * (ge_balance_positive_multiply_fixed_secondreal) /\ (ge_balance_negative_multiply_fixed_secondreal) = 0) \/ exists ge_signed_half_multiply_fixed_secondrealdecode. (((ge_representation_real_code_multiply_fixed_second) = 2 * ge_signed_half_multiply_fixed_secondrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_secondreal) = 0) /\ (ge_balance_negative_multiply_fixed_secondreal) = S ge_signed_half_multiply_fixed_secondrealdecode))) /\ ((e) + ge_balance_negative_multiply_fixed_secondreal = (f) + ge_balance_positive_multiply_fixed_secondreal))) /\ (exists ge_balance_positive_multiply_fixed_secondimaginary ge_balance_negative_multiply_fixed_secondimaginary. (((((ge_representation_imaginary_code_multiply_fixed_second) = 2 * (ge_balance_positive_multiply_fixed_secondimaginary) /\ (ge_balance_negative_multiply_fixed_secondimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_secondimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_second) = 2 * ge_signed_half_multiply_fixed_secondimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_secondimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_secondimaginary) = S ge_signed_half_multiply_fixed_secondimaginarydecode))) /\ ((g) + ge_balance_negative_multiply_fixed_secondimaginary = (h) + ge_balance_positive_multiply_fixed_secondimaginary)))))) -> (exists ge_first_rp_multiply_fixed_graph ge_first_rn_multiply_fixed_graph ge_first_ip_multiply_fixed_graph ge_first_in_multiply_fixed_graph ge_second_rp_multiply_fixed_graph ge_second_rn_multiply_fixed_graph ge_second_ip_multiply_fixed_graph ge_second_in_multiply_fixed_graph. ((exists ge_representation_real_code_multiply_fixed_graphfirst ge_representation_imaginary_code_multiply_fixed_graphfirst. (((ac) = ((ge_representation_real_code_multiply_fixed_graphfirst) + (ge_representation_imaginary_code_multiply_fixed_graphfirst)) * S ((ge_representation_real_code_multiply_fixed_graphfirst) + (ge_representation_imaginary_code_multiply_fixed_graphfirst)) + ((ge_representation_imaginary_code_multiply_fixed_graphfirst) + (ge_representation_imaginary_code_multiply_fixed_graphfirst))) /\ ((exists ge_balance_positive_multiply_fixed_graphfirstreal ge_balance_negative_multiply_fixed_graphfirstreal. (((((ge_representation_real_code_multiply_fixed_graphfirst) = 2 * (ge_balance_positive_multiply_fixed_graphfirstreal) /\ (ge_balance_negative_multiply_fixed_graphfirstreal) = 0) \/ exists ge_signed_half_multiply_fixed_graphfirstrealdecode. (((ge_representation_real_code_multiply_fixed_graphfirst) = 2 * ge_signed_half_multiply_fixed_graphfirstrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_graphfirstreal) = 0) /\ (ge_balance_negative_multiply_fixed_graphfirstreal) = S ge_signed_half_multiply_fixed_graphfirstrealdecode))) /\ ((ge_first_rp_multiply_fixed_graph) + ge_balance_negative_multiply_fixed_graphfirstreal = (ge_first_rn_multiply_fixed_graph) + ge_balance_positive_multiply_fixed_graphfirstreal))) /\ (exists ge_balance_positive_multiply_fixed_graphfirstimaginary ge_balance_negative_multiply_fixed_graphfirstimaginary. (((((ge_representation_imaginary_code_multiply_fixed_graphfirst) = 2 * (ge_balance_positive_multiply_fixed_graphfirstimaginary) /\ (ge_balance_negative_multiply_fixed_graphfirstimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_graphfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_graphfirst) = 2 * ge_signed_half_multiply_fixed_graphfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_graphfirstimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_graphfirstimaginary) = S ge_signed_half_multiply_fixed_graphfirstimaginarydecode))) /\ ((ge_first_ip_multiply_fixed_graph) + ge_balance_negative_multiply_fixed_graphfirstimaginary = (ge_first_in_multiply_fixed_graph) + ge_balance_positive_multiply_fixed_graphfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_fixed_graphsecond ge_representation_imaginary_code_multiply_fixed_graphsecond. (((bc) = ((ge_representation_real_code_multiply_fixed_graphsecond) + (ge_representation_imaginary_code_multiply_fixed_graphsecond)) * S ((ge_representation_real_code_multiply_fixed_graphsecond) + (ge_representation_imaginary_code_multiply_fixed_graphsecond)) + ((ge_representation_imaginary_code_multiply_fixed_graphsecond) + (ge_representation_imaginary_code_multiply_fixed_graphsecond))) /\ ((exists ge_balance_positive_multiply_fixed_graphsecondreal ge_balance_negative_multiply_fixed_graphsecondreal. (((((ge_representation_real_code_multiply_fixed_graphsecond) = 2 * (ge_balance_positive_multiply_fixed_graphsecondreal) /\ (ge_balance_negative_multiply_fixed_graphsecondreal) = 0) \/ exists ge_signed_half_multiply_fixed_graphsecondrealdecode. (((ge_representation_real_code_multiply_fixed_graphsecond) = 2 * ge_signed_half_multiply_fixed_graphsecondrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_graphsecondreal) = 0) /\ (ge_balance_negative_multiply_fixed_graphsecondreal) = S ge_signed_half_multiply_fixed_graphsecondrealdecode))) /\ ((ge_second_rp_multiply_fixed_graph) + ge_balance_negative_multiply_fixed_graphsecondreal = (ge_second_rn_multiply_fixed_graph) + ge_balance_positive_multiply_fixed_graphsecondreal))) /\ (exists ge_balance_positive_multiply_fixed_graphsecondimaginary ge_balance_negative_multiply_fixed_graphsecondimaginary. (((((ge_representation_imaginary_code_multiply_fixed_graphsecond) = 2 * (ge_balance_positive_multiply_fixed_graphsecondimaginary) /\ (ge_balance_negative_multiply_fixed_graphsecondimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_graphsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_graphsecond) = 2 * ge_signed_half_multiply_fixed_graphsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_graphsecondimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_graphsecondimaginary) = S ge_signed_half_multiply_fixed_graphsecondimaginarydecode))) /\ ((ge_second_ip_multiply_fixed_graph) + ge_balance_negative_multiply_fixed_graphsecondimaginary = (ge_second_in_multiply_fixed_graph) + ge_balance_positive_multiply_fixed_graphsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_fixed_graphoutput ge_representation_imaginary_code_multiply_fixed_graphoutput. (((cc) = ((ge_representation_real_code_multiply_fixed_graphoutput) + (ge_representation_imaginary_code_multiply_fixed_graphoutput)) * S ((ge_representation_real_code_multiply_fixed_graphoutput) + (ge_representation_imaginary_code_multiply_fixed_graphoutput)) + ((ge_representation_imaginary_code_multiply_fixed_graphoutput) + (ge_representation_imaginary_code_multiply_fixed_graphoutput))) /\ ((exists ge_balance_positive_multiply_fixed_graphoutputreal ge_balance_negative_multiply_fixed_graphoutputreal. (((((ge_representation_real_code_multiply_fixed_graphoutput) = 2 * (ge_balance_positive_multiply_fixed_graphoutputreal) /\ (ge_balance_negative_multiply_fixed_graphoutputreal) = 0) \/ exists ge_signed_half_multiply_fixed_graphoutputrealdecode. (((ge_representation_real_code_multiply_fixed_graphoutput) = 2 * ge_signed_half_multiply_fixed_graphoutputrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_graphoutputreal) = 0) /\ (ge_balance_negative_multiply_fixed_graphoutputreal) = S ge_signed_half_multiply_fixed_graphoutputrealdecode))) /\ ((((((((ge_first_rp_multiply_fixed_graph) * (ge_second_rp_multiply_fixed_graph))) + (((ge_first_rn_multiply_fixed_graph) * (ge_second_rn_multiply_fixed_graph))))) + (((((ge_first_ip_multiply_fixed_graph) * (ge_second_in_multiply_fixed_graph))) + (((ge_first_in_multiply_fixed_graph) * (ge_second_ip_multiply_fixed_graph))))))) + ge_balance_negative_multiply_fixed_graphoutputreal = (((((((ge_first_rp_multiply_fixed_graph) * (ge_second_rn_multiply_fixed_graph))) + (((ge_first_rn_multiply_fixed_graph) * (ge_second_rp_multiply_fixed_graph))))) + (((((ge_first_ip_multiply_fixed_graph) * (ge_second_ip_multiply_fixed_graph))) + (((ge_first_in_multiply_fixed_graph) * (ge_second_in_multiply_fixed_graph))))))) + ge_balance_positive_multiply_fixed_graphoutputreal))) /\ (exists ge_balance_positive_multiply_fixed_graphoutputimaginary ge_balance_negative_multiply_fixed_graphoutputimaginary. (((((ge_representation_imaginary_code_multiply_fixed_graphoutput) = 2 * (ge_balance_positive_multiply_fixed_graphoutputimaginary) /\ (ge_balance_negative_multiply_fixed_graphoutputimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_graphoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_graphoutput) = 2 * ge_signed_half_multiply_fixed_graphoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_graphoutputimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_graphoutputimaginary) = S ge_signed_half_multiply_fixed_graphoutputimaginarydecode))) /\ ((((((((ge_first_rp_multiply_fixed_graph) * (ge_second_ip_multiply_fixed_graph))) + (((ge_first_rn_multiply_fixed_graph) * (ge_second_in_multiply_fixed_graph))))) + (((((ge_first_ip_multiply_fixed_graph) * (ge_second_rp_multiply_fixed_graph))) + (((ge_first_in_multiply_fixed_graph) * (ge_second_rn_multiply_fixed_graph))))))) + ge_balance_negative_multiply_fixed_graphoutputimaginary = (((((((ge_first_rp_multiply_fixed_graph) * (ge_second_in_multiply_fixed_graph))) + (((ge_first_rn_multiply_fixed_graph) * (ge_second_ip_multiply_fixed_graph))))) + (((((ge_first_ip_multiply_fixed_graph) * (ge_second_rn_multiply_fixed_graph))) + (((ge_first_in_multiply_fixed_graph) * (ge_second_rp_multiply_fixed_graph))))))) + ge_balance_positive_multiply_fixed_graphoutputimaginary))))))))) -> (exists ge_representation_real_code_multiply_fixed_output ge_representation_imaginary_code_multiply_fixed_output. (((cc) = ((ge_representation_real_code_multiply_fixed_output) + (ge_representation_imaginary_code_multiply_fixed_output)) * S ((ge_representation_real_code_multiply_fixed_output) + (ge_representation_imaginary_code_multiply_fixed_output)) + ((ge_representation_imaginary_code_multiply_fixed_output) + (ge_representation_imaginary_code_multiply_fixed_output))) /\ ((exists ge_balance_positive_multiply_fixed_outputreal ge_balance_negative_multiply_fixed_outputreal. (((((ge_representation_real_code_multiply_fixed_output) = 2 * (ge_balance_positive_multiply_fixed_outputreal) /\ (ge_balance_negative_multiply_fixed_outputreal) = 0) \/ exists ge_signed_half_multiply_fixed_outputrealdecode. (((ge_representation_real_code_multiply_fixed_output) = 2 * ge_signed_half_multiply_fixed_outputrealdecode + 1 /\ (ge_balance_positive_multiply_fixed_outputreal) = 0) /\ (ge_balance_negative_multiply_fixed_outputreal) = S ge_signed_half_multiply_fixed_outputrealdecode))) /\ ((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + ge_balance_negative_multiply_fixed_outputreal = (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + ge_balance_positive_multiply_fixed_outputreal))) /\ (exists ge_balance_positive_multiply_fixed_outputimaginary ge_balance_negative_multiply_fixed_outputimaginary. (((((ge_representation_imaginary_code_multiply_fixed_output) = 2 * (ge_balance_positive_multiply_fixed_outputimaginary) /\ (ge_balance_negative_multiply_fixed_outputimaginary) = 0) \/ exists ge_signed_half_multiply_fixed_outputimaginarydecode. (((ge_representation_imaginary_code_multiply_fixed_output) = 2 * ge_signed_half_multiply_fixed_outputimaginarydecode + 1 /\ (ge_balance_positive_multiply_fixed_outputimaginary) = 0) /\ (ge_balance_negative_multiply_fixed_outputimaginary) = S ge_signed_half_multiply_fixed_outputimaginarydecode))) /\ ((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + ge_balance_negative_multiply_fixed_outputimaginary = (((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + ge_balance_positive_multiply_fixed_outputimaginary))))))