gaussian_search_norm_factors_strict

Exact expanded first-order arithmetic statement

forall a b A B N. (exists ge_norm_rp_strict_first_norm ge_norm_rn_strict_first_norm ge_norm_ip_strict_first_norm ge_norm_in_strict_first_norm. ((exists ge_representation_real_code_strict_first_normrepresentation ge_representation_imaginary_code_strict_first_normrepresentation. (((a) = ((ge_representation_real_code_strict_first_normrepresentation) + (ge_representation_imaginary_code_strict_first_normrepresentation)) * S ((ge_representation_real_code_strict_first_normrepresentation) + (ge_representation_imaginary_code_strict_first_normrepresentation)) + ((ge_representation_imaginary_code_strict_first_normrepresentation) + (ge_representation_imaginary_code_strict_first_normrepresentation))) /\ ((exists ge_balance_positive_strict_first_normrepresentationreal ge_balance_negative_strict_first_normrepresentationreal. (((((ge_representation_real_code_strict_first_normrepresentation) = 2 * (ge_balance_positive_strict_first_normrepresentationreal) /\ (ge_balance_negative_strict_first_normrepresentationreal) = 0) \/ exists ge_signed_half_strict_first_normrepresentationrealdecode. (((ge_representation_real_code_strict_first_normrepresentation) = 2 * ge_signed_half_strict_first_normrepresentationrealdecode + 1 /\ (ge_balance_positive_strict_first_normrepresentationreal) = 0) /\ (ge_balance_negative_strict_first_normrepresentationreal) = S ge_signed_half_strict_first_normrepresentationrealdecode))) /\ ((ge_norm_rp_strict_first_norm) + ge_balance_negative_strict_first_normrepresentationreal = (ge_norm_rn_strict_first_norm) + ge_balance_positive_strict_first_normrepresentationreal))) /\ (exists ge_balance_positive_strict_first_normrepresentationimaginary ge_balance_negative_strict_first_normrepresentationimaginary. (((((ge_representation_imaginary_code_strict_first_normrepresentation) = 2 * (ge_balance_positive_strict_first_normrepresentationimaginary) /\ (ge_balance_negative_strict_first_normrepresentationimaginary) = 0) \/ exists ge_signed_half_strict_first_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_strict_first_normrepresentation) = 2 * ge_signed_half_strict_first_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_strict_first_normrepresentationimaginary) = 0) /\ (ge_balance_negative_strict_first_normrepresentationimaginary) = S ge_signed_half_strict_first_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_strict_first_norm) + ge_balance_negative_strict_first_normrepresentationimaginary = (ge_norm_in_strict_first_norm) + ge_balance_positive_strict_first_normrepresentationimaginary)))))) /\ (exists ge_real_square_strict_first_normsquare ge_imaginary_square_strict_first_normsquare. ((((((ge_norm_rp_strict_first_norm) * (ge_norm_rp_strict_first_norm))) + (((ge_norm_rn_strict_first_norm) * (ge_norm_rn_strict_first_norm)))) = ((ge_real_square_strict_first_normsquare) + (((((ge_norm_rp_strict_first_norm) * (ge_norm_rn_strict_first_norm))) + (((ge_norm_rn_strict_first_norm) * (ge_norm_rp_strict_first_norm))))))) /\ ((((((ge_norm_ip_strict_first_norm) * (ge_norm_ip_strict_first_norm))) + (((ge_norm_in_strict_first_norm) * (ge_norm_in_strict_first_norm)))) = ((ge_imaginary_square_strict_first_normsquare) + (((((ge_norm_ip_strict_first_norm) * (ge_norm_in_strict_first_norm))) + (((ge_norm_in_strict_first_norm) * (ge_norm_ip_strict_first_norm))))))) /\ ((A) = ge_real_square_strict_first_normsquare + ge_imaginary_square_strict_first_normsquare)))))) -> (exists ge_norm_rp_strict_second_norm ge_norm_rn_strict_second_norm ge_norm_ip_strict_second_norm ge_norm_in_strict_second_norm. ((exists ge_representation_real_code_strict_second_normrepresentation ge_representation_imaginary_code_strict_second_normrepresentation. (((b) = ((ge_representation_real_code_strict_second_normrepresentation) + (ge_representation_imaginary_code_strict_second_normrepresentation)) * S ((ge_representation_real_code_strict_second_normrepresentation) + (ge_representation_imaginary_code_strict_second_normrepresentation)) + ((ge_representation_imaginary_code_strict_second_normrepresentation) + (ge_representation_imaginary_code_strict_second_normrepresentation))) /\ ((exists ge_balance_positive_strict_second_normrepresentationreal ge_balance_negative_strict_second_normrepresentationreal. (((((ge_representation_real_code_strict_second_normrepresentation) = 2 * (ge_balance_positive_strict_second_normrepresentationreal) /\ (ge_balance_negative_strict_second_normrepresentationreal) = 0) \/ exists ge_signed_half_strict_second_normrepresentationrealdecode. (((ge_representation_real_code_strict_second_normrepresentation) = 2 * ge_signed_half_strict_second_normrepresentationrealdecode + 1 /\ (ge_balance_positive_strict_second_normrepresentationreal) = 0) /\ (ge_balance_negative_strict_second_normrepresentationreal) = S ge_signed_half_strict_second_normrepresentationrealdecode))) /\ ((ge_norm_rp_strict_second_norm) + ge_balance_negative_strict_second_normrepresentationreal = (ge_norm_rn_strict_second_norm) + ge_balance_positive_strict_second_normrepresentationreal))) /\ (exists ge_balance_positive_strict_second_normrepresentationimaginary ge_balance_negative_strict_second_normrepresentationimaginary. (((((ge_representation_imaginary_code_strict_second_normrepresentation) = 2 * (ge_balance_positive_strict_second_normrepresentationimaginary) /\ (ge_balance_negative_strict_second_normrepresentationimaginary) = 0) \/ exists ge_signed_half_strict_second_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_strict_second_normrepresentation) = 2 * ge_signed_half_strict_second_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_strict_second_normrepresentationimaginary) = 0) /\ (ge_balance_negative_strict_second_normrepresentationimaginary) = S ge_signed_half_strict_second_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_strict_second_norm) + ge_balance_negative_strict_second_normrepresentationimaginary = (ge_norm_in_strict_second_norm) + ge_balance_positive_strict_second_normrepresentationimaginary)))))) /\ (exists ge_real_square_strict_second_normsquare ge_imaginary_square_strict_second_normsquare. ((((((ge_norm_rp_strict_second_norm) * (ge_norm_rp_strict_second_norm))) + (((ge_norm_rn_strict_second_norm) * (ge_norm_rn_strict_second_norm)))) = ((ge_real_square_strict_second_normsquare) + (((((ge_norm_rp_strict_second_norm) * (ge_norm_rn_strict_second_norm))) + (((ge_norm_rn_strict_second_norm) * (ge_norm_rp_strict_second_norm))))))) /\ ((((((ge_norm_ip_strict_second_norm) * (ge_norm_ip_strict_second_norm))) + (((ge_norm_in_strict_second_norm) * (ge_norm_in_strict_second_norm)))) = ((ge_imaginary_square_strict_second_normsquare) + (((((ge_norm_ip_strict_second_norm) * (ge_norm_in_strict_second_norm))) + (((ge_norm_in_strict_second_norm) * (ge_norm_ip_strict_second_norm))))))) /\ ((B) = ge_real_square_strict_second_normsquare + ge_imaginary_square_strict_second_normsquare)))))) -> N=A*B -> ~(N=0) -> ~(exists gr_inverse_strict_first_nonunit. (exists ge_first_rp_strict_first_nonunitidentity ge_first_rn_strict_first_nonunitidentity ge_first_ip_strict_first_nonunitidentity ge_first_in_strict_first_nonunitidentity ge_second_rp_strict_first_nonunitidentity ge_second_rn_strict_first_nonunitidentity ge_second_ip_strict_first_nonunitidentity ge_second_in_strict_first_nonunitidentity. ((exists ge_representation_real_code_strict_first_nonunitidentityfirst ge_representation_imaginary_code_strict_first_nonunitidentityfirst. (((a) = ((ge_representation_real_code_strict_first_nonunitidentityfirst) + (ge_representation_imaginary_code_strict_first_nonunitidentityfirst)) * S ((ge_representation_real_code_strict_first_nonunitidentityfirst) + (ge_representation_imaginary_code_strict_first_nonunitidentityfirst)) + ((ge_representation_imaginary_code_strict_first_nonunitidentityfirst) + (ge_representation_imaginary_code_strict_first_nonunitidentityfirst))) /\ ((exists ge_balance_positive_strict_first_nonunitidentityfirstreal ge_balance_negative_strict_first_nonunitidentityfirstreal. (((((ge_representation_real_code_strict_first_nonunitidentityfirst) = 2 * (ge_balance_positive_strict_first_nonunitidentityfirstreal) /\ (ge_balance_negative_strict_first_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_strict_first_nonunitidentityfirstrealdecode. (((ge_representation_real_code_strict_first_nonunitidentityfirst) = 2 * ge_signed_half_strict_first_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_strict_first_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_strict_first_nonunitidentityfirstreal) = S ge_signed_half_strict_first_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_strict_first_nonunitidentity) + ge_balance_negative_strict_first_nonunitidentityfirstreal = (ge_first_rn_strict_first_nonunitidentity) + ge_balance_positive_strict_first_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_strict_first_nonunitidentityfirstimaginary ge_balance_negative_strict_first_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_strict_first_nonunitidentityfirst) = 2 * (ge_balance_positive_strict_first_nonunitidentityfirstimaginary) /\ (ge_balance_negative_strict_first_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_strict_first_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_strict_first_nonunitidentityfirst) = 2 * ge_signed_half_strict_first_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_strict_first_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_strict_first_nonunitidentityfirstimaginary) = S ge_signed_half_strict_first_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_strict_first_nonunitidentity) + ge_balance_negative_strict_first_nonunitidentityfirstimaginary = (ge_first_in_strict_first_nonunitidentity) + ge_balance_positive_strict_first_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_strict_first_nonunitidentitysecond ge_representation_imaginary_code_strict_first_nonunitidentitysecond. (((gr_inverse_strict_first_nonunit) = ((ge_representation_real_code_strict_first_nonunitidentitysecond) + (ge_representation_imaginary_code_strict_first_nonunitidentitysecond)) * S ((ge_representation_real_code_strict_first_nonunitidentitysecond) + (ge_representation_imaginary_code_strict_first_nonunitidentitysecond)) + ((ge_representation_imaginary_code_strict_first_nonunitidentitysecond) + (ge_representation_imaginary_code_strict_first_nonunitidentitysecond))) /\ ((exists ge_balance_positive_strict_first_nonunitidentitysecondreal ge_balance_negative_strict_first_nonunitidentitysecondreal. (((((ge_representation_real_code_strict_first_nonunitidentitysecond) = 2 * (ge_balance_positive_strict_first_nonunitidentitysecondreal) /\ (ge_balance_negative_strict_first_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_strict_first_nonunitidentitysecondrealdecode. (((ge_representation_real_code_strict_first_nonunitidentitysecond) = 2 * ge_signed_half_strict_first_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_strict_first_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_strict_first_nonunitidentitysecondreal) = S ge_signed_half_strict_first_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_strict_first_nonunitidentity) + ge_balance_negative_strict_first_nonunitidentitysecondreal = (ge_second_rn_strict_first_nonunitidentity) + ge_balance_positive_strict_first_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_strict_first_nonunitidentitysecondimaginary ge_balance_negative_strict_first_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_strict_first_nonunitidentitysecond) = 2 * (ge_balance_positive_strict_first_nonunitidentitysecondimaginary) /\ (ge_balance_negative_strict_first_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_strict_first_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_strict_first_nonunitidentitysecond) = 2 * ge_signed_half_strict_first_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_strict_first_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_strict_first_nonunitidentitysecondimaginary) = S ge_signed_half_strict_first_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_strict_first_nonunitidentity) + ge_balance_negative_strict_first_nonunitidentitysecondimaginary = (ge_second_in_strict_first_nonunitidentity) + ge_balance_positive_strict_first_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_strict_first_nonunitidentityoutput ge_representation_imaginary_code_strict_first_nonunitidentityoutput. (((6) = ((ge_representation_real_code_strict_first_nonunitidentityoutput) + (ge_representation_imaginary_code_strict_first_nonunitidentityoutput)) * S ((ge_representation_real_code_strict_first_nonunitidentityoutput) + (ge_representation_imaginary_code_strict_first_nonunitidentityoutput)) + ((ge_representation_imaginary_code_strict_first_nonunitidentityoutput) + (ge_representation_imaginary_code_strict_first_nonunitidentityoutput))) /\ ((exists ge_balance_positive_strict_first_nonunitidentityoutputreal ge_balance_negative_strict_first_nonunitidentityoutputreal. (((((ge_representation_real_code_strict_first_nonunitidentityoutput) = 2 * (ge_balance_positive_strict_first_nonunitidentityoutputreal) /\ (ge_balance_negative_strict_first_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_strict_first_nonunitidentityoutputrealdecode. (((ge_representation_real_code_strict_first_nonunitidentityoutput) = 2 * ge_signed_half_strict_first_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_strict_first_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_strict_first_nonunitidentityoutputreal) = S ge_signed_half_strict_first_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_strict_first_nonunitidentity) * (ge_second_rp_strict_first_nonunitidentity))) + (((ge_first_rn_strict_first_nonunitidentity) * (ge_second_rn_strict_first_nonunitidentity))))) + (((((ge_first_ip_strict_first_nonunitidentity) * (ge_second_in_strict_first_nonunitidentity))) + (((ge_first_in_strict_first_nonunitidentity) * (ge_second_ip_strict_first_nonunitidentity))))))) + ge_balance_negative_strict_first_nonunitidentityoutputreal = (((((((ge_first_rp_strict_first_nonunitidentity) * (ge_second_rn_strict_first_nonunitidentity))) + (((ge_first_rn_strict_first_nonunitidentity) * (ge_second_rp_strict_first_nonunitidentity))))) + (((((ge_first_ip_strict_first_nonunitidentity) * (ge_second_ip_strict_first_nonunitidentity))) + (((ge_first_in_strict_first_nonunitidentity) * (ge_second_in_strict_first_nonunitidentity))))))) + ge_balance_positive_strict_first_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_strict_first_nonunitidentityoutputimaginary ge_balance_negative_strict_first_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_strict_first_nonunitidentityoutput) = 2 * (ge_balance_positive_strict_first_nonunitidentityoutputimaginary) /\ (ge_balance_negative_strict_first_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_strict_first_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_strict_first_nonunitidentityoutput) = 2 * ge_signed_half_strict_first_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_strict_first_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_strict_first_nonunitidentityoutputimaginary) = S ge_signed_half_strict_first_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_strict_first_nonunitidentity) * (ge_second_ip_strict_first_nonunitidentity))) + (((ge_first_rn_strict_first_nonunitidentity) * (ge_second_in_strict_first_nonunitidentity))))) + (((((ge_first_ip_strict_first_nonunitidentity) * (ge_second_rp_strict_first_nonunitidentity))) + (((ge_first_in_strict_first_nonunitidentity) * (ge_second_rn_strict_first_nonunitidentity))))))) + ge_balance_negative_strict_first_nonunitidentityoutputimaginary = (((((((ge_first_rp_strict_first_nonunitidentity) * (ge_second_in_strict_first_nonunitidentity))) + (((ge_first_rn_strict_first_nonunitidentity) * (ge_second_ip_strict_first_nonunitidentity))))) + (((((ge_first_ip_strict_first_nonunitidentity) * (ge_second_rn_strict_first_nonunitidentity))) + (((ge_first_in_strict_first_nonunitidentity) * (ge_second_rp_strict_first_nonunitidentity))))))) + ge_balance_positive_strict_first_nonunitidentityoutputimaginary)))))))))) -> ~(exists gr_inverse_strict_second_nonunit. (exists ge_first_rp_strict_second_nonunitidentity ge_first_rn_strict_second_nonunitidentity ge_first_ip_strict_second_nonunitidentity ge_first_in_strict_second_nonunitidentity ge_second_rp_strict_second_nonunitidentity ge_second_rn_strict_second_nonunitidentity ge_second_ip_strict_second_nonunitidentity ge_second_in_strict_second_nonunitidentity. ((exists ge_representation_real_code_strict_second_nonunitidentityfirst ge_representation_imaginary_code_strict_second_nonunitidentityfirst. (((b) = ((ge_representation_real_code_strict_second_nonunitidentityfirst) + (ge_representation_imaginary_code_strict_second_nonunitidentityfirst)) * S ((ge_representation_real_code_strict_second_nonunitidentityfirst) + (ge_representation_imaginary_code_strict_second_nonunitidentityfirst)) + ((ge_representation_imaginary_code_strict_second_nonunitidentityfirst) + (ge_representation_imaginary_code_strict_second_nonunitidentityfirst))) /\ ((exists ge_balance_positive_strict_second_nonunitidentityfirstreal ge_balance_negative_strict_second_nonunitidentityfirstreal. (((((ge_representation_real_code_strict_second_nonunitidentityfirst) = 2 * (ge_balance_positive_strict_second_nonunitidentityfirstreal) /\ (ge_balance_negative_strict_second_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_strict_second_nonunitidentityfirstrealdecode. (((ge_representation_real_code_strict_second_nonunitidentityfirst) = 2 * ge_signed_half_strict_second_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_strict_second_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_strict_second_nonunitidentityfirstreal) = S ge_signed_half_strict_second_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_strict_second_nonunitidentity) + ge_balance_negative_strict_second_nonunitidentityfirstreal = (ge_first_rn_strict_second_nonunitidentity) + ge_balance_positive_strict_second_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_strict_second_nonunitidentityfirstimaginary ge_balance_negative_strict_second_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_strict_second_nonunitidentityfirst) = 2 * (ge_balance_positive_strict_second_nonunitidentityfirstimaginary) /\ (ge_balance_negative_strict_second_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_strict_second_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_strict_second_nonunitidentityfirst) = 2 * ge_signed_half_strict_second_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_strict_second_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_strict_second_nonunitidentityfirstimaginary) = S ge_signed_half_strict_second_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_strict_second_nonunitidentity) + ge_balance_negative_strict_second_nonunitidentityfirstimaginary = (ge_first_in_strict_second_nonunitidentity) + ge_balance_positive_strict_second_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_strict_second_nonunitidentitysecond ge_representation_imaginary_code_strict_second_nonunitidentitysecond. (((gr_inverse_strict_second_nonunit) = ((ge_representation_real_code_strict_second_nonunitidentitysecond) + (ge_representation_imaginary_code_strict_second_nonunitidentitysecond)) * S ((ge_representation_real_code_strict_second_nonunitidentitysecond) + (ge_representation_imaginary_code_strict_second_nonunitidentitysecond)) + ((ge_representation_imaginary_code_strict_second_nonunitidentitysecond) + (ge_representation_imaginary_code_strict_second_nonunitidentitysecond))) /\ ((exists ge_balance_positive_strict_second_nonunitidentitysecondreal ge_balance_negative_strict_second_nonunitidentitysecondreal. (((((ge_representation_real_code_strict_second_nonunitidentitysecond) = 2 * (ge_balance_positive_strict_second_nonunitidentitysecondreal) /\ (ge_balance_negative_strict_second_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_strict_second_nonunitidentitysecondrealdecode. (((ge_representation_real_code_strict_second_nonunitidentitysecond) = 2 * ge_signed_half_strict_second_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_strict_second_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_strict_second_nonunitidentitysecondreal) = S ge_signed_half_strict_second_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_strict_second_nonunitidentity) + ge_balance_negative_strict_second_nonunitidentitysecondreal = (ge_second_rn_strict_second_nonunitidentity) + ge_balance_positive_strict_second_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_strict_second_nonunitidentitysecondimaginary ge_balance_negative_strict_second_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_strict_second_nonunitidentitysecond) = 2 * (ge_balance_positive_strict_second_nonunitidentitysecondimaginary) /\ (ge_balance_negative_strict_second_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_strict_second_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_strict_second_nonunitidentitysecond) = 2 * ge_signed_half_strict_second_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_strict_second_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_strict_second_nonunitidentitysecondimaginary) = S ge_signed_half_strict_second_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_strict_second_nonunitidentity) + ge_balance_negative_strict_second_nonunitidentitysecondimaginary = (ge_second_in_strict_second_nonunitidentity) + ge_balance_positive_strict_second_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_strict_second_nonunitidentityoutput ge_representation_imaginary_code_strict_second_nonunitidentityoutput. (((6) = ((ge_representation_real_code_strict_second_nonunitidentityoutput) + (ge_representation_imaginary_code_strict_second_nonunitidentityoutput)) * S ((ge_representation_real_code_strict_second_nonunitidentityoutput) + (ge_representation_imaginary_code_strict_second_nonunitidentityoutput)) + ((ge_representation_imaginary_code_strict_second_nonunitidentityoutput) + (ge_representation_imaginary_code_strict_second_nonunitidentityoutput))) /\ ((exists ge_balance_positive_strict_second_nonunitidentityoutputreal ge_balance_negative_strict_second_nonunitidentityoutputreal. (((((ge_representation_real_code_strict_second_nonunitidentityoutput) = 2 * (ge_balance_positive_strict_second_nonunitidentityoutputreal) /\ (ge_balance_negative_strict_second_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_strict_second_nonunitidentityoutputrealdecode. (((ge_representation_real_code_strict_second_nonunitidentityoutput) = 2 * ge_signed_half_strict_second_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_strict_second_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_strict_second_nonunitidentityoutputreal) = S ge_signed_half_strict_second_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_strict_second_nonunitidentity) * (ge_second_rp_strict_second_nonunitidentity))) + (((ge_first_rn_strict_second_nonunitidentity) * (ge_second_rn_strict_second_nonunitidentity))))) + (((((ge_first_ip_strict_second_nonunitidentity) * (ge_second_in_strict_second_nonunitidentity))) + (((ge_first_in_strict_second_nonunitidentity) * (ge_second_ip_strict_second_nonunitidentity))))))) + ge_balance_negative_strict_second_nonunitidentityoutputreal = (((((((ge_first_rp_strict_second_nonunitidentity) * (ge_second_rn_strict_second_nonunitidentity))) + (((ge_first_rn_strict_second_nonunitidentity) * (ge_second_rp_strict_second_nonunitidentity))))) + (((((ge_first_ip_strict_second_nonunitidentity) * (ge_second_ip_strict_second_nonunitidentity))) + (((ge_first_in_strict_second_nonunitidentity) * (ge_second_in_strict_second_nonunitidentity))))))) + ge_balance_positive_strict_second_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_strict_second_nonunitidentityoutputimaginary ge_balance_negative_strict_second_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_strict_second_nonunitidentityoutput) = 2 * (ge_balance_positive_strict_second_nonunitidentityoutputimaginary) /\ (ge_balance_negative_strict_second_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_strict_second_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_strict_second_nonunitidentityoutput) = 2 * ge_signed_half_strict_second_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_strict_second_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_strict_second_nonunitidentityoutputimaginary) = S ge_signed_half_strict_second_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_strict_second_nonunitidentity) * (ge_second_ip_strict_second_nonunitidentity))) + (((ge_first_rn_strict_second_nonunitidentity) * (ge_second_in_strict_second_nonunitidentity))))) + (((((ge_first_ip_strict_second_nonunitidentity) * (ge_second_rp_strict_second_nonunitidentity))) + (((ge_first_in_strict_second_nonunitidentity) * (ge_second_rn_strict_second_nonunitidentity))))))) + ge_balance_negative_strict_second_nonunitidentityoutputimaginary = (((((((ge_first_rp_strict_second_nonunitidentity) * (ge_second_in_strict_second_nonunitidentity))) + (((ge_first_rn_strict_second_nonunitidentity) * (ge_second_ip_strict_second_nonunitidentity))))) + (((((ge_first_ip_strict_second_nonunitidentity) * (ge_second_rn_strict_second_nonunitidentity))) + (((ge_first_in_strict_second_nonunitidentity) * (ge_second_rp_strict_second_nonunitidentity))))))) + ge_balance_positive_strict_second_nonunitidentityoutputimaginary)))))))))) -> ((exists ge_gap_strict_first_result. ge_gap_strict_first_result + S (A) = (N)) /\ (exists ge_gap_strict_second_result. ge_gap_strict_second_result + S (B) = (N)))