gaussian_divisor_norm_factor

Exact expanded first-order arithmetic statement

forall d z D N. (exists gr_quotient_norm_factor_divisor. (exists ge_first_rp_norm_factor_divisorproduct ge_first_rn_norm_factor_divisorproduct ge_first_ip_norm_factor_divisorproduct ge_first_in_norm_factor_divisorproduct ge_second_rp_norm_factor_divisorproduct ge_second_rn_norm_factor_divisorproduct ge_second_ip_norm_factor_divisorproduct ge_second_in_norm_factor_divisorproduct. ((exists ge_representation_real_code_norm_factor_divisorproductfirst ge_representation_imaginary_code_norm_factor_divisorproductfirst. (((d) = ((ge_representation_real_code_norm_factor_divisorproductfirst) + (ge_representation_imaginary_code_norm_factor_divisorproductfirst)) * S ((ge_representation_real_code_norm_factor_divisorproductfirst) + (ge_representation_imaginary_code_norm_factor_divisorproductfirst)) + ((ge_representation_imaginary_code_norm_factor_divisorproductfirst) + (ge_representation_imaginary_code_norm_factor_divisorproductfirst))) /\ ((exists ge_balance_positive_norm_factor_divisorproductfirstreal ge_balance_negative_norm_factor_divisorproductfirstreal. (((((ge_representation_real_code_norm_factor_divisorproductfirst) = 2 * (ge_balance_positive_norm_factor_divisorproductfirstreal) /\ (ge_balance_negative_norm_factor_divisorproductfirstreal) = 0) \/ exists ge_signed_half_norm_factor_divisorproductfirstrealdecode. (((ge_representation_real_code_norm_factor_divisorproductfirst) = 2 * ge_signed_half_norm_factor_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductfirstreal) = 0) /\ (ge_balance_negative_norm_factor_divisorproductfirstreal) = S ge_signed_half_norm_factor_divisorproductfirstrealdecode))) /\ ((ge_first_rp_norm_factor_divisorproduct) + ge_balance_negative_norm_factor_divisorproductfirstreal = (ge_first_rn_norm_factor_divisorproduct) + ge_balance_positive_norm_factor_divisorproductfirstreal))) /\ (exists ge_balance_positive_norm_factor_divisorproductfirstimaginary ge_balance_negative_norm_factor_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_norm_factor_divisorproductfirst) = 2 * (ge_balance_positive_norm_factor_divisorproductfirstimaginary) /\ (ge_balance_negative_norm_factor_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_norm_factor_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_norm_factor_divisorproductfirst) = 2 * ge_signed_half_norm_factor_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_norm_factor_divisorproductfirstimaginary) = S ge_signed_half_norm_factor_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_norm_factor_divisorproduct) + ge_balance_negative_norm_factor_divisorproductfirstimaginary = (ge_first_in_norm_factor_divisorproduct) + ge_balance_positive_norm_factor_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_norm_factor_divisorproductsecond ge_representation_imaginary_code_norm_factor_divisorproductsecond. (((gr_quotient_norm_factor_divisor) = ((ge_representation_real_code_norm_factor_divisorproductsecond) + (ge_representation_imaginary_code_norm_factor_divisorproductsecond)) * S ((ge_representation_real_code_norm_factor_divisorproductsecond) + (ge_representation_imaginary_code_norm_factor_divisorproductsecond)) + ((ge_representation_imaginary_code_norm_factor_divisorproductsecond) + (ge_representation_imaginary_code_norm_factor_divisorproductsecond))) /\ ((exists ge_balance_positive_norm_factor_divisorproductsecondreal ge_balance_negative_norm_factor_divisorproductsecondreal. (((((ge_representation_real_code_norm_factor_divisorproductsecond) = 2 * (ge_balance_positive_norm_factor_divisorproductsecondreal) /\ (ge_balance_negative_norm_factor_divisorproductsecondreal) = 0) \/ exists ge_signed_half_norm_factor_divisorproductsecondrealdecode. (((ge_representation_real_code_norm_factor_divisorproductsecond) = 2 * ge_signed_half_norm_factor_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductsecondreal) = 0) /\ (ge_balance_negative_norm_factor_divisorproductsecondreal) = S ge_signed_half_norm_factor_divisorproductsecondrealdecode))) /\ ((ge_second_rp_norm_factor_divisorproduct) + ge_balance_negative_norm_factor_divisorproductsecondreal = (ge_second_rn_norm_factor_divisorproduct) + ge_balance_positive_norm_factor_divisorproductsecondreal))) /\ (exists ge_balance_positive_norm_factor_divisorproductsecondimaginary ge_balance_negative_norm_factor_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_norm_factor_divisorproductsecond) = 2 * (ge_balance_positive_norm_factor_divisorproductsecondimaginary) /\ (ge_balance_negative_norm_factor_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_norm_factor_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_norm_factor_divisorproductsecond) = 2 * ge_signed_half_norm_factor_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_norm_factor_divisorproductsecondimaginary) = S ge_signed_half_norm_factor_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_norm_factor_divisorproduct) + ge_balance_negative_norm_factor_divisorproductsecondimaginary = (ge_second_in_norm_factor_divisorproduct) + ge_balance_positive_norm_factor_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_norm_factor_divisorproductoutput ge_representation_imaginary_code_norm_factor_divisorproductoutput. (((z) = ((ge_representation_real_code_norm_factor_divisorproductoutput) + (ge_representation_imaginary_code_norm_factor_divisorproductoutput)) * S ((ge_representation_real_code_norm_factor_divisorproductoutput) + (ge_representation_imaginary_code_norm_factor_divisorproductoutput)) + ((ge_representation_imaginary_code_norm_factor_divisorproductoutput) + (ge_representation_imaginary_code_norm_factor_divisorproductoutput))) /\ ((exists ge_balance_positive_norm_factor_divisorproductoutputreal ge_balance_negative_norm_factor_divisorproductoutputreal. (((((ge_representation_real_code_norm_factor_divisorproductoutput) = 2 * (ge_balance_positive_norm_factor_divisorproductoutputreal) /\ (ge_balance_negative_norm_factor_divisorproductoutputreal) = 0) \/ exists ge_signed_half_norm_factor_divisorproductoutputrealdecode. (((ge_representation_real_code_norm_factor_divisorproductoutput) = 2 * ge_signed_half_norm_factor_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductoutputreal) = 0) /\ (ge_balance_negative_norm_factor_divisorproductoutputreal) = S ge_signed_half_norm_factor_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_norm_factor_divisorproduct) * (ge_second_rp_norm_factor_divisorproduct))) + (((ge_first_rn_norm_factor_divisorproduct) * (ge_second_rn_norm_factor_divisorproduct))))) + (((((ge_first_ip_norm_factor_divisorproduct) * (ge_second_in_norm_factor_divisorproduct))) + (((ge_first_in_norm_factor_divisorproduct) * (ge_second_ip_norm_factor_divisorproduct))))))) + ge_balance_negative_norm_factor_divisorproductoutputreal = (((((((ge_first_rp_norm_factor_divisorproduct) * (ge_second_rn_norm_factor_divisorproduct))) + (((ge_first_rn_norm_factor_divisorproduct) * (ge_second_rp_norm_factor_divisorproduct))))) + (((((ge_first_ip_norm_factor_divisorproduct) * (ge_second_ip_norm_factor_divisorproduct))) + (((ge_first_in_norm_factor_divisorproduct) * (ge_second_in_norm_factor_divisorproduct))))))) + ge_balance_positive_norm_factor_divisorproductoutputreal))) /\ (exists ge_balance_positive_norm_factor_divisorproductoutputimaginary ge_balance_negative_norm_factor_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_norm_factor_divisorproductoutput) = 2 * (ge_balance_positive_norm_factor_divisorproductoutputimaginary) /\ (ge_balance_negative_norm_factor_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_norm_factor_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_norm_factor_divisorproductoutput) = 2 * ge_signed_half_norm_factor_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_norm_factor_divisorproductoutputimaginary) = S ge_signed_half_norm_factor_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_norm_factor_divisorproduct) * (ge_second_ip_norm_factor_divisorproduct))) + (((ge_first_rn_norm_factor_divisorproduct) * (ge_second_in_norm_factor_divisorproduct))))) + (((((ge_first_ip_norm_factor_divisorproduct) * (ge_second_rp_norm_factor_divisorproduct))) + (((ge_first_in_norm_factor_divisorproduct) * (ge_second_rn_norm_factor_divisorproduct))))))) + ge_balance_negative_norm_factor_divisorproductoutputimaginary = (((((((ge_first_rp_norm_factor_divisorproduct) * (ge_second_in_norm_factor_divisorproduct))) + (((ge_first_rn_norm_factor_divisorproduct) * (ge_second_ip_norm_factor_divisorproduct))))) + (((((ge_first_ip_norm_factor_divisorproduct) * (ge_second_rn_norm_factor_divisorproduct))) + (((ge_first_in_norm_factor_divisorproduct) * (ge_second_rp_norm_factor_divisorproduct))))))) + ge_balance_positive_norm_factor_divisorproductoutputimaginary)))))))))) -> (exists ge_norm_rp_norm_factor_first ge_norm_rn_norm_factor_first ge_norm_ip_norm_factor_first ge_norm_in_norm_factor_first. ((exists ge_representation_real_code_norm_factor_firstrepresentation ge_representation_imaginary_code_norm_factor_firstrepresentation. (((d) = ((ge_representation_real_code_norm_factor_firstrepresentation) + (ge_representation_imaginary_code_norm_factor_firstrepresentation)) * S ((ge_representation_real_code_norm_factor_firstrepresentation) + (ge_representation_imaginary_code_norm_factor_firstrepresentation)) + ((ge_representation_imaginary_code_norm_factor_firstrepresentation) + (ge_representation_imaginary_code_norm_factor_firstrepresentation))) /\ ((exists ge_balance_positive_norm_factor_firstrepresentationreal ge_balance_negative_norm_factor_firstrepresentationreal. (((((ge_representation_real_code_norm_factor_firstrepresentation) = 2 * (ge_balance_positive_norm_factor_firstrepresentationreal) /\ (ge_balance_negative_norm_factor_firstrepresentationreal) = 0) \/ exists ge_signed_half_norm_factor_firstrepresentationrealdecode. (((ge_representation_real_code_norm_factor_firstrepresentation) = 2 * ge_signed_half_norm_factor_firstrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_factor_firstrepresentationreal) = 0) /\ (ge_balance_negative_norm_factor_firstrepresentationreal) = S ge_signed_half_norm_factor_firstrepresentationrealdecode))) /\ ((ge_norm_rp_norm_factor_first) + ge_balance_negative_norm_factor_firstrepresentationreal = (ge_norm_rn_norm_factor_first) + ge_balance_positive_norm_factor_firstrepresentationreal))) /\ (exists ge_balance_positive_norm_factor_firstrepresentationimaginary ge_balance_negative_norm_factor_firstrepresentationimaginary. (((((ge_representation_imaginary_code_norm_factor_firstrepresentation) = 2 * (ge_balance_positive_norm_factor_firstrepresentationimaginary) /\ (ge_balance_negative_norm_factor_firstrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_factor_firstrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_factor_firstrepresentation) = 2 * ge_signed_half_norm_factor_firstrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_firstrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_factor_firstrepresentationimaginary) = S ge_signed_half_norm_factor_firstrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_factor_first) + ge_balance_negative_norm_factor_firstrepresentationimaginary = (ge_norm_in_norm_factor_first) + ge_balance_positive_norm_factor_firstrepresentationimaginary)))))) /\ (exists ge_real_square_norm_factor_firstsquare ge_imaginary_square_norm_factor_firstsquare. ((((((ge_norm_rp_norm_factor_first) * (ge_norm_rp_norm_factor_first))) + (((ge_norm_rn_norm_factor_first) * (ge_norm_rn_norm_factor_first)))) = ((ge_real_square_norm_factor_firstsquare) + (((((ge_norm_rp_norm_factor_first) * (ge_norm_rn_norm_factor_first))) + (((ge_norm_rn_norm_factor_first) * (ge_norm_rp_norm_factor_first))))))) /\ ((((((ge_norm_ip_norm_factor_first) * (ge_norm_ip_norm_factor_first))) + (((ge_norm_in_norm_factor_first) * (ge_norm_in_norm_factor_first)))) = ((ge_imaginary_square_norm_factor_firstsquare) + (((((ge_norm_ip_norm_factor_first) * (ge_norm_in_norm_factor_first))) + (((ge_norm_in_norm_factor_first) * (ge_norm_ip_norm_factor_first))))))) /\ ((D) = ge_real_square_norm_factor_firstsquare + ge_imaginary_square_norm_factor_firstsquare)))))) -> (exists ge_norm_rp_norm_factor_total ge_norm_rn_norm_factor_total ge_norm_ip_norm_factor_total ge_norm_in_norm_factor_total. ((exists ge_representation_real_code_norm_factor_totalrepresentation ge_representation_imaginary_code_norm_factor_totalrepresentation. (((z) = ((ge_representation_real_code_norm_factor_totalrepresentation) + (ge_representation_imaginary_code_norm_factor_totalrepresentation)) * S ((ge_representation_real_code_norm_factor_totalrepresentation) + (ge_representation_imaginary_code_norm_factor_totalrepresentation)) + ((ge_representation_imaginary_code_norm_factor_totalrepresentation) + (ge_representation_imaginary_code_norm_factor_totalrepresentation))) /\ ((exists ge_balance_positive_norm_factor_totalrepresentationreal ge_balance_negative_norm_factor_totalrepresentationreal. (((((ge_representation_real_code_norm_factor_totalrepresentation) = 2 * (ge_balance_positive_norm_factor_totalrepresentationreal) /\ (ge_balance_negative_norm_factor_totalrepresentationreal) = 0) \/ exists ge_signed_half_norm_factor_totalrepresentationrealdecode. (((ge_representation_real_code_norm_factor_totalrepresentation) = 2 * ge_signed_half_norm_factor_totalrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_factor_totalrepresentationreal) = 0) /\ (ge_balance_negative_norm_factor_totalrepresentationreal) = S ge_signed_half_norm_factor_totalrepresentationrealdecode))) /\ ((ge_norm_rp_norm_factor_total) + ge_balance_negative_norm_factor_totalrepresentationreal = (ge_norm_rn_norm_factor_total) + ge_balance_positive_norm_factor_totalrepresentationreal))) /\ (exists ge_balance_positive_norm_factor_totalrepresentationimaginary ge_balance_negative_norm_factor_totalrepresentationimaginary. (((((ge_representation_imaginary_code_norm_factor_totalrepresentation) = 2 * (ge_balance_positive_norm_factor_totalrepresentationimaginary) /\ (ge_balance_negative_norm_factor_totalrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_factor_totalrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_factor_totalrepresentation) = 2 * ge_signed_half_norm_factor_totalrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_totalrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_factor_totalrepresentationimaginary) = S ge_signed_half_norm_factor_totalrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_factor_total) + ge_balance_negative_norm_factor_totalrepresentationimaginary = (ge_norm_in_norm_factor_total) + ge_balance_positive_norm_factor_totalrepresentationimaginary)))))) /\ (exists ge_real_square_norm_factor_totalsquare ge_imaginary_square_norm_factor_totalsquare. ((((((ge_norm_rp_norm_factor_total) * (ge_norm_rp_norm_factor_total))) + (((ge_norm_rn_norm_factor_total) * (ge_norm_rn_norm_factor_total)))) = ((ge_real_square_norm_factor_totalsquare) + (((((ge_norm_rp_norm_factor_total) * (ge_norm_rn_norm_factor_total))) + (((ge_norm_rn_norm_factor_total) * (ge_norm_rp_norm_factor_total))))))) /\ ((((((ge_norm_ip_norm_factor_total) * (ge_norm_ip_norm_factor_total))) + (((ge_norm_in_norm_factor_total) * (ge_norm_in_norm_factor_total)))) = ((ge_imaginary_square_norm_factor_totalsquare) + (((((ge_norm_ip_norm_factor_total) * (ge_norm_in_norm_factor_total))) + (((ge_norm_in_norm_factor_total) * (ge_norm_ip_norm_factor_total))))))) /\ ((N) = ge_real_square_norm_factor_totalsquare + ge_imaginary_square_norm_factor_totalsquare)))))) -> exists q Q. ((exists ge_first_rp_norm_factor_product ge_first_rn_norm_factor_product ge_first_ip_norm_factor_product ge_first_in_norm_factor_product ge_second_rp_norm_factor_product ge_second_rn_norm_factor_product ge_second_ip_norm_factor_product ge_second_in_norm_factor_product. ((exists ge_representation_real_code_norm_factor_productfirst ge_representation_imaginary_code_norm_factor_productfirst. (((d) = ((ge_representation_real_code_norm_factor_productfirst) + (ge_representation_imaginary_code_norm_factor_productfirst)) * S ((ge_representation_real_code_norm_factor_productfirst) + (ge_representation_imaginary_code_norm_factor_productfirst)) + ((ge_representation_imaginary_code_norm_factor_productfirst) + (ge_representation_imaginary_code_norm_factor_productfirst))) /\ ((exists ge_balance_positive_norm_factor_productfirstreal ge_balance_negative_norm_factor_productfirstreal. (((((ge_representation_real_code_norm_factor_productfirst) = 2 * (ge_balance_positive_norm_factor_productfirstreal) /\ (ge_balance_negative_norm_factor_productfirstreal) = 0) \/ exists ge_signed_half_norm_factor_productfirstrealdecode. (((ge_representation_real_code_norm_factor_productfirst) = 2 * ge_signed_half_norm_factor_productfirstrealdecode + 1 /\ (ge_balance_positive_norm_factor_productfirstreal) = 0) /\ (ge_balance_negative_norm_factor_productfirstreal) = S ge_signed_half_norm_factor_productfirstrealdecode))) /\ ((ge_first_rp_norm_factor_product) + ge_balance_negative_norm_factor_productfirstreal = (ge_first_rn_norm_factor_product) + ge_balance_positive_norm_factor_productfirstreal))) /\ (exists ge_balance_positive_norm_factor_productfirstimaginary ge_balance_negative_norm_factor_productfirstimaginary. (((((ge_representation_imaginary_code_norm_factor_productfirst) = 2 * (ge_balance_positive_norm_factor_productfirstimaginary) /\ (ge_balance_negative_norm_factor_productfirstimaginary) = 0) \/ exists ge_signed_half_norm_factor_productfirstimaginarydecode. (((ge_representation_imaginary_code_norm_factor_productfirst) = 2 * ge_signed_half_norm_factor_productfirstimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_productfirstimaginary) = 0) /\ (ge_balance_negative_norm_factor_productfirstimaginary) = S ge_signed_half_norm_factor_productfirstimaginarydecode))) /\ ((ge_first_ip_norm_factor_product) + ge_balance_negative_norm_factor_productfirstimaginary = (ge_first_in_norm_factor_product) + ge_balance_positive_norm_factor_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_norm_factor_productsecond ge_representation_imaginary_code_norm_factor_productsecond. (((q) = ((ge_representation_real_code_norm_factor_productsecond) + (ge_representation_imaginary_code_norm_factor_productsecond)) * S ((ge_representation_real_code_norm_factor_productsecond) + (ge_representation_imaginary_code_norm_factor_productsecond)) + ((ge_representation_imaginary_code_norm_factor_productsecond) + (ge_representation_imaginary_code_norm_factor_productsecond))) /\ ((exists ge_balance_positive_norm_factor_productsecondreal ge_balance_negative_norm_factor_productsecondreal. (((((ge_representation_real_code_norm_factor_productsecond) = 2 * (ge_balance_positive_norm_factor_productsecondreal) /\ (ge_balance_negative_norm_factor_productsecondreal) = 0) \/ exists ge_signed_half_norm_factor_productsecondrealdecode. (((ge_representation_real_code_norm_factor_productsecond) = 2 * ge_signed_half_norm_factor_productsecondrealdecode + 1 /\ (ge_balance_positive_norm_factor_productsecondreal) = 0) /\ (ge_balance_negative_norm_factor_productsecondreal) = S ge_signed_half_norm_factor_productsecondrealdecode))) /\ ((ge_second_rp_norm_factor_product) + ge_balance_negative_norm_factor_productsecondreal = (ge_second_rn_norm_factor_product) + ge_balance_positive_norm_factor_productsecondreal))) /\ (exists ge_balance_positive_norm_factor_productsecondimaginary ge_balance_negative_norm_factor_productsecondimaginary. (((((ge_representation_imaginary_code_norm_factor_productsecond) = 2 * (ge_balance_positive_norm_factor_productsecondimaginary) /\ (ge_balance_negative_norm_factor_productsecondimaginary) = 0) \/ exists ge_signed_half_norm_factor_productsecondimaginarydecode. (((ge_representation_imaginary_code_norm_factor_productsecond) = 2 * ge_signed_half_norm_factor_productsecondimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_productsecondimaginary) = 0) /\ (ge_balance_negative_norm_factor_productsecondimaginary) = S ge_signed_half_norm_factor_productsecondimaginarydecode))) /\ ((ge_second_ip_norm_factor_product) + ge_balance_negative_norm_factor_productsecondimaginary = (ge_second_in_norm_factor_product) + ge_balance_positive_norm_factor_productsecondimaginary)))))) /\ (exists ge_representation_real_code_norm_factor_productoutput ge_representation_imaginary_code_norm_factor_productoutput. (((z) = ((ge_representation_real_code_norm_factor_productoutput) + (ge_representation_imaginary_code_norm_factor_productoutput)) * S ((ge_representation_real_code_norm_factor_productoutput) + (ge_representation_imaginary_code_norm_factor_productoutput)) + ((ge_representation_imaginary_code_norm_factor_productoutput) + (ge_representation_imaginary_code_norm_factor_productoutput))) /\ ((exists ge_balance_positive_norm_factor_productoutputreal ge_balance_negative_norm_factor_productoutputreal. (((((ge_representation_real_code_norm_factor_productoutput) = 2 * (ge_balance_positive_norm_factor_productoutputreal) /\ (ge_balance_negative_norm_factor_productoutputreal) = 0) \/ exists ge_signed_half_norm_factor_productoutputrealdecode. (((ge_representation_real_code_norm_factor_productoutput) = 2 * ge_signed_half_norm_factor_productoutputrealdecode + 1 /\ (ge_balance_positive_norm_factor_productoutputreal) = 0) /\ (ge_balance_negative_norm_factor_productoutputreal) = S ge_signed_half_norm_factor_productoutputrealdecode))) /\ ((((((((ge_first_rp_norm_factor_product) * (ge_second_rp_norm_factor_product))) + (((ge_first_rn_norm_factor_product) * (ge_second_rn_norm_factor_product))))) + (((((ge_first_ip_norm_factor_product) * (ge_second_in_norm_factor_product))) + (((ge_first_in_norm_factor_product) * (ge_second_ip_norm_factor_product))))))) + ge_balance_negative_norm_factor_productoutputreal = (((((((ge_first_rp_norm_factor_product) * (ge_second_rn_norm_factor_product))) + (((ge_first_rn_norm_factor_product) * (ge_second_rp_norm_factor_product))))) + (((((ge_first_ip_norm_factor_product) * (ge_second_ip_norm_factor_product))) + (((ge_first_in_norm_factor_product) * (ge_second_in_norm_factor_product))))))) + ge_balance_positive_norm_factor_productoutputreal))) /\ (exists ge_balance_positive_norm_factor_productoutputimaginary ge_balance_negative_norm_factor_productoutputimaginary. (((((ge_representation_imaginary_code_norm_factor_productoutput) = 2 * (ge_balance_positive_norm_factor_productoutputimaginary) /\ (ge_balance_negative_norm_factor_productoutputimaginary) = 0) \/ exists ge_signed_half_norm_factor_productoutputimaginarydecode. (((ge_representation_imaginary_code_norm_factor_productoutput) = 2 * ge_signed_half_norm_factor_productoutputimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_productoutputimaginary) = 0) /\ (ge_balance_negative_norm_factor_productoutputimaginary) = S ge_signed_half_norm_factor_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_norm_factor_product) * (ge_second_ip_norm_factor_product))) + (((ge_first_rn_norm_factor_product) * (ge_second_in_norm_factor_product))))) + (((((ge_first_ip_norm_factor_product) * (ge_second_rp_norm_factor_product))) + (((ge_first_in_norm_factor_product) * (ge_second_rn_norm_factor_product))))))) + ge_balance_negative_norm_factor_productoutputimaginary = (((((((ge_first_rp_norm_factor_product) * (ge_second_in_norm_factor_product))) + (((ge_first_rn_norm_factor_product) * (ge_second_ip_norm_factor_product))))) + (((((ge_first_ip_norm_factor_product) * (ge_second_rn_norm_factor_product))) + (((ge_first_in_norm_factor_product) * (ge_second_rp_norm_factor_product))))))) + ge_balance_positive_norm_factor_productoutputimaginary))))))))) /\ ((exists ge_norm_rp_norm_factor_quotient ge_norm_rn_norm_factor_quotient ge_norm_ip_norm_factor_quotient ge_norm_in_norm_factor_quotient. ((exists ge_representation_real_code_norm_factor_quotientrepresentation ge_representation_imaginary_code_norm_factor_quotientrepresentation. (((q) = ((ge_representation_real_code_norm_factor_quotientrepresentation) + (ge_representation_imaginary_code_norm_factor_quotientrepresentation)) * S ((ge_representation_real_code_norm_factor_quotientrepresentation) + (ge_representation_imaginary_code_norm_factor_quotientrepresentation)) + ((ge_representation_imaginary_code_norm_factor_quotientrepresentation) + (ge_representation_imaginary_code_norm_factor_quotientrepresentation))) /\ ((exists ge_balance_positive_norm_factor_quotientrepresentationreal ge_balance_negative_norm_factor_quotientrepresentationreal. (((((ge_representation_real_code_norm_factor_quotientrepresentation) = 2 * (ge_balance_positive_norm_factor_quotientrepresentationreal) /\ (ge_balance_negative_norm_factor_quotientrepresentationreal) = 0) \/ exists ge_signed_half_norm_factor_quotientrepresentationrealdecode. (((ge_representation_real_code_norm_factor_quotientrepresentation) = 2 * ge_signed_half_norm_factor_quotientrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_factor_quotientrepresentationreal) = 0) /\ (ge_balance_negative_norm_factor_quotientrepresentationreal) = S ge_signed_half_norm_factor_quotientrepresentationrealdecode))) /\ ((ge_norm_rp_norm_factor_quotient) + ge_balance_negative_norm_factor_quotientrepresentationreal = (ge_norm_rn_norm_factor_quotient) + ge_balance_positive_norm_factor_quotientrepresentationreal))) /\ (exists ge_balance_positive_norm_factor_quotientrepresentationimaginary ge_balance_negative_norm_factor_quotientrepresentationimaginary. (((((ge_representation_imaginary_code_norm_factor_quotientrepresentation) = 2 * (ge_balance_positive_norm_factor_quotientrepresentationimaginary) /\ (ge_balance_negative_norm_factor_quotientrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_factor_quotientrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_factor_quotientrepresentation) = 2 * ge_signed_half_norm_factor_quotientrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_quotientrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_factor_quotientrepresentationimaginary) = S ge_signed_half_norm_factor_quotientrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_factor_quotient) + ge_balance_negative_norm_factor_quotientrepresentationimaginary = (ge_norm_in_norm_factor_quotient) + ge_balance_positive_norm_factor_quotientrepresentationimaginary)))))) /\ (exists ge_real_square_norm_factor_quotientsquare ge_imaginary_square_norm_factor_quotientsquare. ((((((ge_norm_rp_norm_factor_quotient) * (ge_norm_rp_norm_factor_quotient))) + (((ge_norm_rn_norm_factor_quotient) * (ge_norm_rn_norm_factor_quotient)))) = ((ge_real_square_norm_factor_quotientsquare) + (((((ge_norm_rp_norm_factor_quotient) * (ge_norm_rn_norm_factor_quotient))) + (((ge_norm_rn_norm_factor_quotient) * (ge_norm_rp_norm_factor_quotient))))))) /\ ((((((ge_norm_ip_norm_factor_quotient) * (ge_norm_ip_norm_factor_quotient))) + (((ge_norm_in_norm_factor_quotient) * (ge_norm_in_norm_factor_quotient)))) = ((ge_imaginary_square_norm_factor_quotientsquare) + (((((ge_norm_ip_norm_factor_quotient) * (ge_norm_in_norm_factor_quotient))) + (((ge_norm_in_norm_factor_quotient) * (ge_norm_ip_norm_factor_quotient))))))) /\ ((Q) = ge_real_square_norm_factor_quotientsquare + ge_imaginary_square_norm_factor_quotientsquare)))))) /\ (N=D*Q)))