gaussian_search_nonunit_norm_two

Exact expanded first-order arithmetic statement

forall z N. (exists ge_norm_rp_nonunit_actual_norm ge_norm_rn_nonunit_actual_norm ge_norm_ip_nonunit_actual_norm ge_norm_in_nonunit_actual_norm. ((exists ge_representation_real_code_nonunit_actual_normrepresentation ge_representation_imaginary_code_nonunit_actual_normrepresentation. (((z) = ((ge_representation_real_code_nonunit_actual_normrepresentation) + (ge_representation_imaginary_code_nonunit_actual_normrepresentation)) * S ((ge_representation_real_code_nonunit_actual_normrepresentation) + (ge_representation_imaginary_code_nonunit_actual_normrepresentation)) + ((ge_representation_imaginary_code_nonunit_actual_normrepresentation) + (ge_representation_imaginary_code_nonunit_actual_normrepresentation))) /\ ((exists ge_balance_positive_nonunit_actual_normrepresentationreal ge_balance_negative_nonunit_actual_normrepresentationreal. (((((ge_representation_real_code_nonunit_actual_normrepresentation) = 2 * (ge_balance_positive_nonunit_actual_normrepresentationreal) /\ (ge_balance_negative_nonunit_actual_normrepresentationreal) = 0) \/ exists ge_signed_half_nonunit_actual_normrepresentationrealdecode. (((ge_representation_real_code_nonunit_actual_normrepresentation) = 2 * ge_signed_half_nonunit_actual_normrepresentationrealdecode + 1 /\ (ge_balance_positive_nonunit_actual_normrepresentationreal) = 0) /\ (ge_balance_negative_nonunit_actual_normrepresentationreal) = S ge_signed_half_nonunit_actual_normrepresentationrealdecode))) /\ ((ge_norm_rp_nonunit_actual_norm) + ge_balance_negative_nonunit_actual_normrepresentationreal = (ge_norm_rn_nonunit_actual_norm) + ge_balance_positive_nonunit_actual_normrepresentationreal))) /\ (exists ge_balance_positive_nonunit_actual_normrepresentationimaginary ge_balance_negative_nonunit_actual_normrepresentationimaginary. (((((ge_representation_imaginary_code_nonunit_actual_normrepresentation) = 2 * (ge_balance_positive_nonunit_actual_normrepresentationimaginary) /\ (ge_balance_negative_nonunit_actual_normrepresentationimaginary) = 0) \/ exists ge_signed_half_nonunit_actual_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_nonunit_actual_normrepresentation) = 2 * ge_signed_half_nonunit_actual_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_nonunit_actual_normrepresentationimaginary) = 0) /\ (ge_balance_negative_nonunit_actual_normrepresentationimaginary) = S ge_signed_half_nonunit_actual_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_nonunit_actual_norm) + ge_balance_negative_nonunit_actual_normrepresentationimaginary = (ge_norm_in_nonunit_actual_norm) + ge_balance_positive_nonunit_actual_normrepresentationimaginary)))))) /\ (exists ge_real_square_nonunit_actual_normsquare ge_imaginary_square_nonunit_actual_normsquare. ((((((ge_norm_rp_nonunit_actual_norm) * (ge_norm_rp_nonunit_actual_norm))) + (((ge_norm_rn_nonunit_actual_norm) * (ge_norm_rn_nonunit_actual_norm)))) = ((ge_real_square_nonunit_actual_normsquare) + (((((ge_norm_rp_nonunit_actual_norm) * (ge_norm_rn_nonunit_actual_norm))) + (((ge_norm_rn_nonunit_actual_norm) * (ge_norm_rp_nonunit_actual_norm))))))) /\ ((((((ge_norm_ip_nonunit_actual_norm) * (ge_norm_ip_nonunit_actual_norm))) + (((ge_norm_in_nonunit_actual_norm) * (ge_norm_in_nonunit_actual_norm)))) = ((ge_imaginary_square_nonunit_actual_normsquare) + (((((ge_norm_ip_nonunit_actual_norm) * (ge_norm_in_nonunit_actual_norm))) + (((ge_norm_in_nonunit_actual_norm) * (ge_norm_ip_nonunit_actual_norm))))))) /\ ((N) = ge_real_square_nonunit_actual_normsquare + ge_imaginary_square_nonunit_actual_normsquare)))))) -> ~(N=0) -> ~(exists gr_inverse_nonunit_given. (exists ge_first_rp_nonunit_givenidentity ge_first_rn_nonunit_givenidentity ge_first_ip_nonunit_givenidentity ge_first_in_nonunit_givenidentity ge_second_rp_nonunit_givenidentity ge_second_rn_nonunit_givenidentity ge_second_ip_nonunit_givenidentity ge_second_in_nonunit_givenidentity. ((exists ge_representation_real_code_nonunit_givenidentityfirst ge_representation_imaginary_code_nonunit_givenidentityfirst. (((z) = ((ge_representation_real_code_nonunit_givenidentityfirst) + (ge_representation_imaginary_code_nonunit_givenidentityfirst)) * S ((ge_representation_real_code_nonunit_givenidentityfirst) + (ge_representation_imaginary_code_nonunit_givenidentityfirst)) + ((ge_representation_imaginary_code_nonunit_givenidentityfirst) + (ge_representation_imaginary_code_nonunit_givenidentityfirst))) /\ ((exists ge_balance_positive_nonunit_givenidentityfirstreal ge_balance_negative_nonunit_givenidentityfirstreal. (((((ge_representation_real_code_nonunit_givenidentityfirst) = 2 * (ge_balance_positive_nonunit_givenidentityfirstreal) /\ (ge_balance_negative_nonunit_givenidentityfirstreal) = 0) \/ exists ge_signed_half_nonunit_givenidentityfirstrealdecode. (((ge_representation_real_code_nonunit_givenidentityfirst) = 2 * ge_signed_half_nonunit_givenidentityfirstrealdecode + 1 /\ (ge_balance_positive_nonunit_givenidentityfirstreal) = 0) /\ (ge_balance_negative_nonunit_givenidentityfirstreal) = S ge_signed_half_nonunit_givenidentityfirstrealdecode))) /\ ((ge_first_rp_nonunit_givenidentity) + ge_balance_negative_nonunit_givenidentityfirstreal = (ge_first_rn_nonunit_givenidentity) + ge_balance_positive_nonunit_givenidentityfirstreal))) /\ (exists ge_balance_positive_nonunit_givenidentityfirstimaginary ge_balance_negative_nonunit_givenidentityfirstimaginary. (((((ge_representation_imaginary_code_nonunit_givenidentityfirst) = 2 * (ge_balance_positive_nonunit_givenidentityfirstimaginary) /\ (ge_balance_negative_nonunit_givenidentityfirstimaginary) = 0) \/ exists ge_signed_half_nonunit_givenidentityfirstimaginarydecode. (((ge_representation_imaginary_code_nonunit_givenidentityfirst) = 2 * ge_signed_half_nonunit_givenidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_nonunit_givenidentityfirstimaginary) = 0) /\ (ge_balance_negative_nonunit_givenidentityfirstimaginary) = S ge_signed_half_nonunit_givenidentityfirstimaginarydecode))) /\ ((ge_first_ip_nonunit_givenidentity) + ge_balance_negative_nonunit_givenidentityfirstimaginary = (ge_first_in_nonunit_givenidentity) + ge_balance_positive_nonunit_givenidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_nonunit_givenidentitysecond ge_representation_imaginary_code_nonunit_givenidentitysecond. (((gr_inverse_nonunit_given) = ((ge_representation_real_code_nonunit_givenidentitysecond) + (ge_representation_imaginary_code_nonunit_givenidentitysecond)) * S ((ge_representation_real_code_nonunit_givenidentitysecond) + (ge_representation_imaginary_code_nonunit_givenidentitysecond)) + ((ge_representation_imaginary_code_nonunit_givenidentitysecond) + (ge_representation_imaginary_code_nonunit_givenidentitysecond))) /\ ((exists ge_balance_positive_nonunit_givenidentitysecondreal ge_balance_negative_nonunit_givenidentitysecondreal. (((((ge_representation_real_code_nonunit_givenidentitysecond) = 2 * (ge_balance_positive_nonunit_givenidentitysecondreal) /\ (ge_balance_negative_nonunit_givenidentitysecondreal) = 0) \/ exists ge_signed_half_nonunit_givenidentitysecondrealdecode. (((ge_representation_real_code_nonunit_givenidentitysecond) = 2 * ge_signed_half_nonunit_givenidentitysecondrealdecode + 1 /\ (ge_balance_positive_nonunit_givenidentitysecondreal) = 0) /\ (ge_balance_negative_nonunit_givenidentitysecondreal) = S ge_signed_half_nonunit_givenidentitysecondrealdecode))) /\ ((ge_second_rp_nonunit_givenidentity) + ge_balance_negative_nonunit_givenidentitysecondreal = (ge_second_rn_nonunit_givenidentity) + ge_balance_positive_nonunit_givenidentitysecondreal))) /\ (exists ge_balance_positive_nonunit_givenidentitysecondimaginary ge_balance_negative_nonunit_givenidentitysecondimaginary. (((((ge_representation_imaginary_code_nonunit_givenidentitysecond) = 2 * (ge_balance_positive_nonunit_givenidentitysecondimaginary) /\ (ge_balance_negative_nonunit_givenidentitysecondimaginary) = 0) \/ exists ge_signed_half_nonunit_givenidentitysecondimaginarydecode. (((ge_representation_imaginary_code_nonunit_givenidentitysecond) = 2 * ge_signed_half_nonunit_givenidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_nonunit_givenidentitysecondimaginary) = 0) /\ (ge_balance_negative_nonunit_givenidentitysecondimaginary) = S ge_signed_half_nonunit_givenidentitysecondimaginarydecode))) /\ ((ge_second_ip_nonunit_givenidentity) + ge_balance_negative_nonunit_givenidentitysecondimaginary = (ge_second_in_nonunit_givenidentity) + ge_balance_positive_nonunit_givenidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_nonunit_givenidentityoutput ge_representation_imaginary_code_nonunit_givenidentityoutput. (((6) = ((ge_representation_real_code_nonunit_givenidentityoutput) + (ge_representation_imaginary_code_nonunit_givenidentityoutput)) * S ((ge_representation_real_code_nonunit_givenidentityoutput) + (ge_representation_imaginary_code_nonunit_givenidentityoutput)) + ((ge_representation_imaginary_code_nonunit_givenidentityoutput) + (ge_representation_imaginary_code_nonunit_givenidentityoutput))) /\ ((exists ge_balance_positive_nonunit_givenidentityoutputreal ge_balance_negative_nonunit_givenidentityoutputreal. (((((ge_representation_real_code_nonunit_givenidentityoutput) = 2 * (ge_balance_positive_nonunit_givenidentityoutputreal) /\ (ge_balance_negative_nonunit_givenidentityoutputreal) = 0) \/ exists ge_signed_half_nonunit_givenidentityoutputrealdecode. (((ge_representation_real_code_nonunit_givenidentityoutput) = 2 * ge_signed_half_nonunit_givenidentityoutputrealdecode + 1 /\ (ge_balance_positive_nonunit_givenidentityoutputreal) = 0) /\ (ge_balance_negative_nonunit_givenidentityoutputreal) = S ge_signed_half_nonunit_givenidentityoutputrealdecode))) /\ ((((((((ge_first_rp_nonunit_givenidentity) * (ge_second_rp_nonunit_givenidentity))) + (((ge_first_rn_nonunit_givenidentity) * (ge_second_rn_nonunit_givenidentity))))) + (((((ge_first_ip_nonunit_givenidentity) * (ge_second_in_nonunit_givenidentity))) + (((ge_first_in_nonunit_givenidentity) * (ge_second_ip_nonunit_givenidentity))))))) + ge_balance_negative_nonunit_givenidentityoutputreal = (((((((ge_first_rp_nonunit_givenidentity) * (ge_second_rn_nonunit_givenidentity))) + (((ge_first_rn_nonunit_givenidentity) * (ge_second_rp_nonunit_givenidentity))))) + (((((ge_first_ip_nonunit_givenidentity) * (ge_second_ip_nonunit_givenidentity))) + (((ge_first_in_nonunit_givenidentity) * (ge_second_in_nonunit_givenidentity))))))) + ge_balance_positive_nonunit_givenidentityoutputreal))) /\ (exists ge_balance_positive_nonunit_givenidentityoutputimaginary ge_balance_negative_nonunit_givenidentityoutputimaginary. (((((ge_representation_imaginary_code_nonunit_givenidentityoutput) = 2 * (ge_balance_positive_nonunit_givenidentityoutputimaginary) /\ (ge_balance_negative_nonunit_givenidentityoutputimaginary) = 0) \/ exists ge_signed_half_nonunit_givenidentityoutputimaginarydecode. (((ge_representation_imaginary_code_nonunit_givenidentityoutput) = 2 * ge_signed_half_nonunit_givenidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_nonunit_givenidentityoutputimaginary) = 0) /\ (ge_balance_negative_nonunit_givenidentityoutputimaginary) = S ge_signed_half_nonunit_givenidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_nonunit_givenidentity) * (ge_second_ip_nonunit_givenidentity))) + (((ge_first_rn_nonunit_givenidentity) * (ge_second_in_nonunit_givenidentity))))) + (((((ge_first_ip_nonunit_givenidentity) * (ge_second_rp_nonunit_givenidentity))) + (((ge_first_in_nonunit_givenidentity) * (ge_second_rn_nonunit_givenidentity))))))) + ge_balance_negative_nonunit_givenidentityoutputimaginary = (((((((ge_first_rp_nonunit_givenidentity) * (ge_second_in_nonunit_givenidentity))) + (((ge_first_rn_nonunit_givenidentity) * (ge_second_ip_nonunit_givenidentity))))) + (((((ge_first_ip_nonunit_givenidentity) * (ge_second_rn_nonunit_givenidentity))) + (((ge_first_in_nonunit_givenidentity) * (ge_second_rp_nonunit_givenidentity))))))) + ge_balance_positive_nonunit_givenidentityoutputimaginary)))))))))) -> (exists ge_gap_nonunit_norm_lower. ge_gap_nonunit_norm_lower + (2) = (N))