eisenstein_norm_multiply

Exact expanded first-order arithmetic statement

forall ac bc cc N M. (exists ee_norm_rp_norm_product_first ee_norm_rn_norm_product_first ee_norm_ip_norm_product_first ee_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))) /\ ((ee_norm_rp_norm_product_first) + ge_balance_negative_norm_product_firstrepresentationreal = (ee_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))) /\ ((ee_norm_ip_norm_product_first) + ge_balance_negative_norm_product_firstrepresentationimaginary = (ee_norm_in_norm_product_first) + ge_balance_positive_norm_product_firstrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_norm_product_first) * (ee_norm_rp_norm_product_first))) + (((ee_norm_rn_norm_product_first) * (ee_norm_rn_norm_product_first))))) + (((((ee_norm_ip_norm_product_first) * (ee_norm_ip_norm_product_first))) + (((ee_norm_in_norm_product_first) * (ee_norm_in_norm_product_first))))))) + (((((ee_norm_rp_norm_product_first) * (ee_norm_in_norm_product_first))) + (((ee_norm_rn_norm_product_first) * (ee_norm_ip_norm_product_first)))))) = ((((((((((ee_norm_rp_norm_product_first) * (ee_norm_rn_norm_product_first))) + (((ee_norm_rn_norm_product_first) * (ee_norm_rp_norm_product_first))))) + (((((ee_norm_ip_norm_product_first) * (ee_norm_in_norm_product_first))) + (((ee_norm_in_norm_product_first) * (ee_norm_ip_norm_product_first))))))) + (((((ee_norm_rp_norm_product_first) * (ee_norm_ip_norm_product_first))) + (((ee_norm_rn_norm_product_first) * (ee_norm_in_norm_product_first))))))) + (N))))) -> (exists ee_norm_rp_norm_product_second ee_norm_rn_norm_product_second ee_norm_ip_norm_product_second ee_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))) /\ ((ee_norm_rp_norm_product_second) + ge_balance_negative_norm_product_secondrepresentationreal = (ee_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))) /\ ((ee_norm_ip_norm_product_second) + ge_balance_negative_norm_product_secondrepresentationimaginary = (ee_norm_in_norm_product_second) + ge_balance_positive_norm_product_secondrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_norm_product_second) * (ee_norm_rp_norm_product_second))) + (((ee_norm_rn_norm_product_second) * (ee_norm_rn_norm_product_second))))) + (((((ee_norm_ip_norm_product_second) * (ee_norm_ip_norm_product_second))) + (((ee_norm_in_norm_product_second) * (ee_norm_in_norm_product_second))))))) + (((((ee_norm_rp_norm_product_second) * (ee_norm_in_norm_product_second))) + (((ee_norm_rn_norm_product_second) * (ee_norm_ip_norm_product_second)))))) = ((((((((((ee_norm_rp_norm_product_second) * (ee_norm_rn_norm_product_second))) + (((ee_norm_rn_norm_product_second) * (ee_norm_rp_norm_product_second))))) + (((((ee_norm_ip_norm_product_second) * (ee_norm_in_norm_product_second))) + (((ee_norm_in_norm_product_second) * (ee_norm_ip_norm_product_second))))))) + (((((ee_norm_rp_norm_product_second) * (ee_norm_ip_norm_product_second))) + (((ee_norm_rn_norm_product_second) * (ee_norm_in_norm_product_second))))))) + (M))))) -> (exists ee_first_rp_norm_product_operation ee_first_rn_norm_product_operation ee_first_ip_norm_product_operation ee_first_in_norm_product_operation ee_second_rp_norm_product_operation ee_second_rn_norm_product_operation ee_second_ip_norm_product_operation ee_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))) /\ ((ee_first_rp_norm_product_operation) + ge_balance_negative_norm_product_operationfirstreal = (ee_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))) /\ ((ee_first_ip_norm_product_operation) + ge_balance_negative_norm_product_operationfirstimaginary = (ee_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))) /\ ((ee_second_rp_norm_product_operation) + ge_balance_negative_norm_product_operationsecondreal = (ee_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))) /\ ((ee_second_ip_norm_product_operation) + ge_balance_negative_norm_product_operationsecondimaginary = (ee_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))) /\ ((((((((ee_first_rp_norm_product_operation) * (ee_second_rp_norm_product_operation))) + (((ee_first_rn_norm_product_operation) * (ee_second_rn_norm_product_operation))))) + (((((ee_first_ip_norm_product_operation) * (ee_second_in_norm_product_operation))) + (((ee_first_in_norm_product_operation) * (ee_second_ip_norm_product_operation))))))) + ge_balance_negative_norm_product_operationoutputreal = (((((((ee_first_rp_norm_product_operation) * (ee_second_rn_norm_product_operation))) + (((ee_first_rn_norm_product_operation) * (ee_second_rp_norm_product_operation))))) + (((((ee_first_ip_norm_product_operation) * (ee_second_ip_norm_product_operation))) + (((ee_first_in_norm_product_operation) * (ee_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))) /\ ((((((((((ee_first_rp_norm_product_operation) * (ee_second_ip_norm_product_operation))) + (((ee_first_rn_norm_product_operation) * (ee_second_in_norm_product_operation))))) + (((((ee_first_ip_norm_product_operation) * (ee_second_rp_norm_product_operation))) + (((ee_first_in_norm_product_operation) * (ee_second_rn_norm_product_operation))))))) + (((((ee_first_ip_norm_product_operation) * (ee_second_in_norm_product_operation))) + (((ee_first_in_norm_product_operation) * (ee_second_ip_norm_product_operation))))))) + ge_balance_negative_norm_product_operationoutputimaginary = (((((((((ee_first_rp_norm_product_operation) * (ee_second_in_norm_product_operation))) + (((ee_first_rn_norm_product_operation) * (ee_second_ip_norm_product_operation))))) + (((((ee_first_ip_norm_product_operation) * (ee_second_rn_norm_product_operation))) + (((ee_first_in_norm_product_operation) * (ee_second_rp_norm_product_operation))))))) + (((((ee_first_ip_norm_product_operation) * (ee_second_ip_norm_product_operation))) + (((ee_first_in_norm_product_operation) * (ee_second_in_norm_product_operation))))))) + ge_balance_positive_norm_product_operationoutputimaginary))))))))) -> (exists ee_norm_rp_norm_product_output ee_norm_rn_norm_product_output ee_norm_ip_norm_product_output ee_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))) /\ ((ee_norm_rp_norm_product_output) + ge_balance_negative_norm_product_outputrepresentationreal = (ee_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))) /\ ((ee_norm_ip_norm_product_output) + ge_balance_negative_norm_product_outputrepresentationimaginary = (ee_norm_in_norm_product_output) + ge_balance_positive_norm_product_outputrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_norm_product_output) * (ee_norm_rp_norm_product_output))) + (((ee_norm_rn_norm_product_output) * (ee_norm_rn_norm_product_output))))) + (((((ee_norm_ip_norm_product_output) * (ee_norm_ip_norm_product_output))) + (((ee_norm_in_norm_product_output) * (ee_norm_in_norm_product_output))))))) + (((((ee_norm_rp_norm_product_output) * (ee_norm_in_norm_product_output))) + (((ee_norm_rn_norm_product_output) * (ee_norm_ip_norm_product_output)))))) = ((((((((((ee_norm_rp_norm_product_output) * (ee_norm_rn_norm_product_output))) + (((ee_norm_rn_norm_product_output) * (ee_norm_rp_norm_product_output))))) + (((((ee_norm_ip_norm_product_output) * (ee_norm_in_norm_product_output))) + (((ee_norm_in_norm_product_output) * (ee_norm_ip_norm_product_output))))))) + (((((ee_norm_rp_norm_product_output) * (ee_norm_ip_norm_product_output))) + (((ee_norm_rn_norm_product_output) * (ee_norm_in_norm_product_output))))))) + (N * M)))))