gaussian_norm_multiply

Exact expanded first-order arithmetic statement

forall ac bc cc N M. (exists ge_norm_rp_norm_product_first ge_norm_rn_norm_product_first ge_norm_ip_norm_product_first ge_norm_in_norm_product_first. ((exists ge_representation_real_code_norm_product_firstrepresentation ge_representation_imaginary_code_norm_product_firstrepresentation. (((ac) = ((ge_representation_real_code_norm_product_firstrepresentation) + (ge_representation_imaginary_code_norm_product_firstrepresentation)) * S ((ge_representation_real_code_norm_product_firstrepresentation) + (ge_representation_imaginary_code_norm_product_firstrepresentation)) + ((ge_representation_imaginary_code_norm_product_firstrepresentation) + (ge_representation_imaginary_code_norm_product_firstrepresentation))) /\ ((exists ge_balance_positive_norm_product_firstrepresentationreal ge_balance_negative_norm_product_firstrepresentationreal. (((((ge_representation_real_code_norm_product_firstrepresentation) = 2 * (ge_balance_positive_norm_product_firstrepresentationreal) /\ (ge_balance_negative_norm_product_firstrepresentationreal) = 0) \/ exists ge_signed_half_norm_product_firstrepresentationrealdecode. (((ge_representation_real_code_norm_product_firstrepresentation) = 2 * ge_signed_half_norm_product_firstrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_product_firstrepresentationreal) = 0) /\ (ge_balance_negative_norm_product_firstrepresentationreal) = S ge_signed_half_norm_product_firstrepresentationrealdecode))) /\ ((ge_norm_rp_norm_product_first) + ge_balance_negative_norm_product_firstrepresentationreal = (ge_norm_rn_norm_product_first) + ge_balance_positive_norm_product_firstrepresentationreal))) /\ (exists ge_balance_positive_norm_product_firstrepresentationimaginary ge_balance_negative_norm_product_firstrepresentationimaginary. (((((ge_representation_imaginary_code_norm_product_firstrepresentation) = 2 * (ge_balance_positive_norm_product_firstrepresentationimaginary) /\ (ge_balance_negative_norm_product_firstrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_product_firstrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_product_firstrepresentation) = 2 * ge_signed_half_norm_product_firstrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_product_firstrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_product_firstrepresentationimaginary) = S ge_signed_half_norm_product_firstrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_product_first) + ge_balance_negative_norm_product_firstrepresentationimaginary = (ge_norm_in_norm_product_first) + ge_balance_positive_norm_product_firstrepresentationimaginary)))))) /\ (exists ge_real_square_norm_product_firstsquare ge_imaginary_square_norm_product_firstsquare. ((((((ge_norm_rp_norm_product_first) * (ge_norm_rp_norm_product_first))) + (((ge_norm_rn_norm_product_first) * (ge_norm_rn_norm_product_first)))) = ((ge_real_square_norm_product_firstsquare) + (((((ge_norm_rp_norm_product_first) * (ge_norm_rn_norm_product_first))) + (((ge_norm_rn_norm_product_first) * (ge_norm_rp_norm_product_first))))))) /\ ((((((ge_norm_ip_norm_product_first) * (ge_norm_ip_norm_product_first))) + (((ge_norm_in_norm_product_first) * (ge_norm_in_norm_product_first)))) = ((ge_imaginary_square_norm_product_firstsquare) + (((((ge_norm_ip_norm_product_first) * (ge_norm_in_norm_product_first))) + (((ge_norm_in_norm_product_first) * (ge_norm_ip_norm_product_first))))))) /\ ((N) = ge_real_square_norm_product_firstsquare + ge_imaginary_square_norm_product_firstsquare)))))) -> (exists ge_norm_rp_norm_product_second ge_norm_rn_norm_product_second ge_norm_ip_norm_product_second ge_norm_in_norm_product_second. ((exists ge_representation_real_code_norm_product_secondrepresentation ge_representation_imaginary_code_norm_product_secondrepresentation. (((bc) = ((ge_representation_real_code_norm_product_secondrepresentation) + (ge_representation_imaginary_code_norm_product_secondrepresentation)) * S ((ge_representation_real_code_norm_product_secondrepresentation) + (ge_representation_imaginary_code_norm_product_secondrepresentation)) + ((ge_representation_imaginary_code_norm_product_secondrepresentation) + (ge_representation_imaginary_code_norm_product_secondrepresentation))) /\ ((exists ge_balance_positive_norm_product_secondrepresentationreal ge_balance_negative_norm_product_secondrepresentationreal. (((((ge_representation_real_code_norm_product_secondrepresentation) = 2 * (ge_balance_positive_norm_product_secondrepresentationreal) /\ (ge_balance_negative_norm_product_secondrepresentationreal) = 0) \/ exists ge_signed_half_norm_product_secondrepresentationrealdecode. (((ge_representation_real_code_norm_product_secondrepresentation) = 2 * ge_signed_half_norm_product_secondrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_product_secondrepresentationreal) = 0) /\ (ge_balance_negative_norm_product_secondrepresentationreal) = S ge_signed_half_norm_product_secondrepresentationrealdecode))) /\ ((ge_norm_rp_norm_product_second) + ge_balance_negative_norm_product_secondrepresentationreal = (ge_norm_rn_norm_product_second) + ge_balance_positive_norm_product_secondrepresentationreal))) /\ (exists ge_balance_positive_norm_product_secondrepresentationimaginary ge_balance_negative_norm_product_secondrepresentationimaginary. (((((ge_representation_imaginary_code_norm_product_secondrepresentation) = 2 * (ge_balance_positive_norm_product_secondrepresentationimaginary) /\ (ge_balance_negative_norm_product_secondrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_product_secondrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_product_secondrepresentation) = 2 * ge_signed_half_norm_product_secondrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_product_secondrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_product_secondrepresentationimaginary) = S ge_signed_half_norm_product_secondrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_product_second) + ge_balance_negative_norm_product_secondrepresentationimaginary = (ge_norm_in_norm_product_second) + ge_balance_positive_norm_product_secondrepresentationimaginary)))))) /\ (exists ge_real_square_norm_product_secondsquare ge_imaginary_square_norm_product_secondsquare. ((((((ge_norm_rp_norm_product_second) * (ge_norm_rp_norm_product_second))) + (((ge_norm_rn_norm_product_second) * (ge_norm_rn_norm_product_second)))) = ((ge_real_square_norm_product_secondsquare) + (((((ge_norm_rp_norm_product_second) * (ge_norm_rn_norm_product_second))) + (((ge_norm_rn_norm_product_second) * (ge_norm_rp_norm_product_second))))))) /\ ((((((ge_norm_ip_norm_product_second) * (ge_norm_ip_norm_product_second))) + (((ge_norm_in_norm_product_second) * (ge_norm_in_norm_product_second)))) = ((ge_imaginary_square_norm_product_secondsquare) + (((((ge_norm_ip_norm_product_second) * (ge_norm_in_norm_product_second))) + (((ge_norm_in_norm_product_second) * (ge_norm_ip_norm_product_second))))))) /\ ((M) = ge_real_square_norm_product_secondsquare + ge_imaginary_square_norm_product_secondsquare)))))) -> (exists ge_first_rp_norm_product_operation ge_first_rn_norm_product_operation ge_first_ip_norm_product_operation ge_first_in_norm_product_operation ge_second_rp_norm_product_operation ge_second_rn_norm_product_operation ge_second_ip_norm_product_operation ge_second_in_norm_product_operation. ((exists ge_representation_real_code_norm_product_operationfirst ge_representation_imaginary_code_norm_product_operationfirst. (((ac) = ((ge_representation_real_code_norm_product_operationfirst) + (ge_representation_imaginary_code_norm_product_operationfirst)) * S ((ge_representation_real_code_norm_product_operationfirst) + (ge_representation_imaginary_code_norm_product_operationfirst)) + ((ge_representation_imaginary_code_norm_product_operationfirst) + (ge_representation_imaginary_code_norm_product_operationfirst))) /\ ((exists ge_balance_positive_norm_product_operationfirstreal ge_balance_negative_norm_product_operationfirstreal. (((((ge_representation_real_code_norm_product_operationfirst) = 2 * (ge_balance_positive_norm_product_operationfirstreal) /\ (ge_balance_negative_norm_product_operationfirstreal) = 0) \/ exists ge_signed_half_norm_product_operationfirstrealdecode. (((ge_representation_real_code_norm_product_operationfirst) = 2 * ge_signed_half_norm_product_operationfirstrealdecode + 1 /\ (ge_balance_positive_norm_product_operationfirstreal) = 0) /\ (ge_balance_negative_norm_product_operationfirstreal) = S ge_signed_half_norm_product_operationfirstrealdecode))) /\ ((ge_first_rp_norm_product_operation) + ge_balance_negative_norm_product_operationfirstreal = (ge_first_rn_norm_product_operation) + ge_balance_positive_norm_product_operationfirstreal))) /\ (exists ge_balance_positive_norm_product_operationfirstimaginary ge_balance_negative_norm_product_operationfirstimaginary. (((((ge_representation_imaginary_code_norm_product_operationfirst) = 2 * (ge_balance_positive_norm_product_operationfirstimaginary) /\ (ge_balance_negative_norm_product_operationfirstimaginary) = 0) \/ exists ge_signed_half_norm_product_operationfirstimaginarydecode. (((ge_representation_imaginary_code_norm_product_operationfirst) = 2 * ge_signed_half_norm_product_operationfirstimaginarydecode + 1 /\ (ge_balance_positive_norm_product_operationfirstimaginary) = 0) /\ (ge_balance_negative_norm_product_operationfirstimaginary) = S ge_signed_half_norm_product_operationfirstimaginarydecode))) /\ ((ge_first_ip_norm_product_operation) + ge_balance_negative_norm_product_operationfirstimaginary = (ge_first_in_norm_product_operation) + ge_balance_positive_norm_product_operationfirstimaginary)))))) /\ ((exists ge_representation_real_code_norm_product_operationsecond ge_representation_imaginary_code_norm_product_operationsecond. (((bc) = ((ge_representation_real_code_norm_product_operationsecond) + (ge_representation_imaginary_code_norm_product_operationsecond)) * S ((ge_representation_real_code_norm_product_operationsecond) + (ge_representation_imaginary_code_norm_product_operationsecond)) + ((ge_representation_imaginary_code_norm_product_operationsecond) + (ge_representation_imaginary_code_norm_product_operationsecond))) /\ ((exists ge_balance_positive_norm_product_operationsecondreal ge_balance_negative_norm_product_operationsecondreal. (((((ge_representation_real_code_norm_product_operationsecond) = 2 * (ge_balance_positive_norm_product_operationsecondreal) /\ (ge_balance_negative_norm_product_operationsecondreal) = 0) \/ exists ge_signed_half_norm_product_operationsecondrealdecode. (((ge_representation_real_code_norm_product_operationsecond) = 2 * ge_signed_half_norm_product_operationsecondrealdecode + 1 /\ (ge_balance_positive_norm_product_operationsecondreal) = 0) /\ (ge_balance_negative_norm_product_operationsecondreal) = S ge_signed_half_norm_product_operationsecondrealdecode))) /\ ((ge_second_rp_norm_product_operation) + ge_balance_negative_norm_product_operationsecondreal = (ge_second_rn_norm_product_operation) + ge_balance_positive_norm_product_operationsecondreal))) /\ (exists ge_balance_positive_norm_product_operationsecondimaginary ge_balance_negative_norm_product_operationsecondimaginary. (((((ge_representation_imaginary_code_norm_product_operationsecond) = 2 * (ge_balance_positive_norm_product_operationsecondimaginary) /\ (ge_balance_negative_norm_product_operationsecondimaginary) = 0) \/ exists ge_signed_half_norm_product_operationsecondimaginarydecode. (((ge_representation_imaginary_code_norm_product_operationsecond) = 2 * ge_signed_half_norm_product_operationsecondimaginarydecode + 1 /\ (ge_balance_positive_norm_product_operationsecondimaginary) = 0) /\ (ge_balance_negative_norm_product_operationsecondimaginary) = S ge_signed_half_norm_product_operationsecondimaginarydecode))) /\ ((ge_second_ip_norm_product_operation) + ge_balance_negative_norm_product_operationsecondimaginary = (ge_second_in_norm_product_operation) + ge_balance_positive_norm_product_operationsecondimaginary)))))) /\ (exists ge_representation_real_code_norm_product_operationoutput ge_representation_imaginary_code_norm_product_operationoutput. (((cc) = ((ge_representation_real_code_norm_product_operationoutput) + (ge_representation_imaginary_code_norm_product_operationoutput)) * S ((ge_representation_real_code_norm_product_operationoutput) + (ge_representation_imaginary_code_norm_product_operationoutput)) + ((ge_representation_imaginary_code_norm_product_operationoutput) + (ge_representation_imaginary_code_norm_product_operationoutput))) /\ ((exists ge_balance_positive_norm_product_operationoutputreal ge_balance_negative_norm_product_operationoutputreal. (((((ge_representation_real_code_norm_product_operationoutput) = 2 * (ge_balance_positive_norm_product_operationoutputreal) /\ (ge_balance_negative_norm_product_operationoutputreal) = 0) \/ exists ge_signed_half_norm_product_operationoutputrealdecode. (((ge_representation_real_code_norm_product_operationoutput) = 2 * ge_signed_half_norm_product_operationoutputrealdecode + 1 /\ (ge_balance_positive_norm_product_operationoutputreal) = 0) /\ (ge_balance_negative_norm_product_operationoutputreal) = S ge_signed_half_norm_product_operationoutputrealdecode))) /\ ((((((((ge_first_rp_norm_product_operation) * (ge_second_rp_norm_product_operation))) + (((ge_first_rn_norm_product_operation) * (ge_second_rn_norm_product_operation))))) + (((((ge_first_ip_norm_product_operation) * (ge_second_in_norm_product_operation))) + (((ge_first_in_norm_product_operation) * (ge_second_ip_norm_product_operation))))))) + ge_balance_negative_norm_product_operationoutputreal = (((((((ge_first_rp_norm_product_operation) * (ge_second_rn_norm_product_operation))) + (((ge_first_rn_norm_product_operation) * (ge_second_rp_norm_product_operation))))) + (((((ge_first_ip_norm_product_operation) * (ge_second_ip_norm_product_operation))) + (((ge_first_in_norm_product_operation) * (ge_second_in_norm_product_operation))))))) + ge_balance_positive_norm_product_operationoutputreal))) /\ (exists ge_balance_positive_norm_product_operationoutputimaginary ge_balance_negative_norm_product_operationoutputimaginary. (((((ge_representation_imaginary_code_norm_product_operationoutput) = 2 * (ge_balance_positive_norm_product_operationoutputimaginary) /\ (ge_balance_negative_norm_product_operationoutputimaginary) = 0) \/ exists ge_signed_half_norm_product_operationoutputimaginarydecode. (((ge_representation_imaginary_code_norm_product_operationoutput) = 2 * ge_signed_half_norm_product_operationoutputimaginarydecode + 1 /\ (ge_balance_positive_norm_product_operationoutputimaginary) = 0) /\ (ge_balance_negative_norm_product_operationoutputimaginary) = S ge_signed_half_norm_product_operationoutputimaginarydecode))) /\ ((((((((ge_first_rp_norm_product_operation) * (ge_second_ip_norm_product_operation))) + (((ge_first_rn_norm_product_operation) * (ge_second_in_norm_product_operation))))) + (((((ge_first_ip_norm_product_operation) * (ge_second_rp_norm_product_operation))) + (((ge_first_in_norm_product_operation) * (ge_second_rn_norm_product_operation))))))) + ge_balance_negative_norm_product_operationoutputimaginary = (((((((ge_first_rp_norm_product_operation) * (ge_second_in_norm_product_operation))) + (((ge_first_rn_norm_product_operation) * (ge_second_ip_norm_product_operation))))) + (((((ge_first_ip_norm_product_operation) * (ge_second_rn_norm_product_operation))) + (((ge_first_in_norm_product_operation) * (ge_second_rp_norm_product_operation))))))) + ge_balance_positive_norm_product_operationoutputimaginary))))))))) -> (exists ge_norm_rp_norm_product_output ge_norm_rn_norm_product_output ge_norm_ip_norm_product_output ge_norm_in_norm_product_output. ((exists ge_representation_real_code_norm_product_outputrepresentation ge_representation_imaginary_code_norm_product_outputrepresentation. (((cc) = ((ge_representation_real_code_norm_product_outputrepresentation) + (ge_representation_imaginary_code_norm_product_outputrepresentation)) * S ((ge_representation_real_code_norm_product_outputrepresentation) + (ge_representation_imaginary_code_norm_product_outputrepresentation)) + ((ge_representation_imaginary_code_norm_product_outputrepresentation) + (ge_representation_imaginary_code_norm_product_outputrepresentation))) /\ ((exists ge_balance_positive_norm_product_outputrepresentationreal ge_balance_negative_norm_product_outputrepresentationreal. (((((ge_representation_real_code_norm_product_outputrepresentation) = 2 * (ge_balance_positive_norm_product_outputrepresentationreal) /\ (ge_balance_negative_norm_product_outputrepresentationreal) = 0) \/ exists ge_signed_half_norm_product_outputrepresentationrealdecode. (((ge_representation_real_code_norm_product_outputrepresentation) = 2 * ge_signed_half_norm_product_outputrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_product_outputrepresentationreal) = 0) /\ (ge_balance_negative_norm_product_outputrepresentationreal) = S ge_signed_half_norm_product_outputrepresentationrealdecode))) /\ ((ge_norm_rp_norm_product_output) + ge_balance_negative_norm_product_outputrepresentationreal = (ge_norm_rn_norm_product_output) + ge_balance_positive_norm_product_outputrepresentationreal))) /\ (exists ge_balance_positive_norm_product_outputrepresentationimaginary ge_balance_negative_norm_product_outputrepresentationimaginary. (((((ge_representation_imaginary_code_norm_product_outputrepresentation) = 2 * (ge_balance_positive_norm_product_outputrepresentationimaginary) /\ (ge_balance_negative_norm_product_outputrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_product_outputrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_product_outputrepresentation) = 2 * ge_signed_half_norm_product_outputrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_product_outputrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_product_outputrepresentationimaginary) = S ge_signed_half_norm_product_outputrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_product_output) + ge_balance_negative_norm_product_outputrepresentationimaginary = (ge_norm_in_norm_product_output) + ge_balance_positive_norm_product_outputrepresentationimaginary)))))) /\ (exists ge_real_square_norm_product_outputsquare ge_imaginary_square_norm_product_outputsquare. ((((((ge_norm_rp_norm_product_output) * (ge_norm_rp_norm_product_output))) + (((ge_norm_rn_norm_product_output) * (ge_norm_rn_norm_product_output)))) = ((ge_real_square_norm_product_outputsquare) + (((((ge_norm_rp_norm_product_output) * (ge_norm_rn_norm_product_output))) + (((ge_norm_rn_norm_product_output) * (ge_norm_rp_norm_product_output))))))) /\ ((((((ge_norm_ip_norm_product_output) * (ge_norm_ip_norm_product_output))) + (((ge_norm_in_norm_product_output) * (ge_norm_in_norm_product_output)))) = ((ge_imaginary_square_norm_product_outputsquare) + (((((ge_norm_ip_norm_product_output) * (ge_norm_in_norm_product_output))) + (((ge_norm_in_norm_product_output) * (ge_norm_ip_norm_product_output))))))) /\ ((N * M) = ge_real_square_norm_product_outputsquare + ge_imaginary_square_norm_product_outputsquare))))))