gaussian_search_proper_divisor_code_transport

Exact expanded first-order arithmetic statement

forall d e z N. d=e -> (((~(exists gr_inverse_proper_sourcenonunit. (exists ge_first_rp_proper_sourcenonunitidentity ge_first_rn_proper_sourcenonunitidentity ge_first_ip_proper_sourcenonunitidentity ge_first_in_proper_sourcenonunitidentity ge_second_rp_proper_sourcenonunitidentity ge_second_rn_proper_sourcenonunitidentity ge_second_ip_proper_sourcenonunitidentity ge_second_in_proper_sourcenonunitidentity. ((exists ge_representation_real_code_proper_sourcenonunitidentityfirst ge_representation_imaginary_code_proper_sourcenonunitidentityfirst. (((d) = ((ge_representation_real_code_proper_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_proper_sourcenonunitidentityfirst)) * S ((ge_representation_real_code_proper_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_proper_sourcenonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_proper_sourcenonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_sourcenonunitidentityfirstreal ge_balance_negative_proper_sourcenonunitidentityfirstreal. (((((ge_representation_real_code_proper_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_proper_sourcenonunitidentityfirstreal) /\ (ge_balance_negative_proper_sourcenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_sourcenonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_sourcenonunitidentityfirst) = 2 * ge_signed_half_proper_sourcenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_sourcenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_sourcenonunitidentityfirstreal) = S ge_signed_half_proper_sourcenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_sourcenonunitidentity) + ge_balance_negative_proper_sourcenonunitidentityfirstreal = (ge_first_rn_proper_sourcenonunitidentity) + ge_balance_positive_proper_sourcenonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_sourcenonunitidentityfirstimaginary ge_balance_negative_proper_sourcenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_proper_sourcenonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_sourcenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_sourcenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_sourcenonunitidentityfirst) = 2 * ge_signed_half_proper_sourcenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_sourcenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_sourcenonunitidentityfirstimaginary) = S ge_signed_half_proper_sourcenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_sourcenonunitidentity) + ge_balance_negative_proper_sourcenonunitidentityfirstimaginary = (ge_first_in_proper_sourcenonunitidentity) + ge_balance_positive_proper_sourcenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_sourcenonunitidentitysecond ge_representation_imaginary_code_proper_sourcenonunitidentitysecond. (((gr_inverse_proper_sourcenonunit) = ((ge_representation_real_code_proper_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_proper_sourcenonunitidentitysecond)) * S ((ge_representation_real_code_proper_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_proper_sourcenonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_proper_sourcenonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_sourcenonunitidentitysecondreal ge_balance_negative_proper_sourcenonunitidentitysecondreal. (((((ge_representation_real_code_proper_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_proper_sourcenonunitidentitysecondreal) /\ (ge_balance_negative_proper_sourcenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_sourcenonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_sourcenonunitidentitysecond) = 2 * ge_signed_half_proper_sourcenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_sourcenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_sourcenonunitidentitysecondreal) = S ge_signed_half_proper_sourcenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_sourcenonunitidentity) + ge_balance_negative_proper_sourcenonunitidentitysecondreal = (ge_second_rn_proper_sourcenonunitidentity) + ge_balance_positive_proper_sourcenonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_sourcenonunitidentitysecondimaginary ge_balance_negative_proper_sourcenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_proper_sourcenonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_sourcenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_sourcenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_sourcenonunitidentitysecond) = 2 * ge_signed_half_proper_sourcenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_sourcenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_sourcenonunitidentitysecondimaginary) = S ge_signed_half_proper_sourcenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_sourcenonunitidentity) + ge_balance_negative_proper_sourcenonunitidentitysecondimaginary = (ge_second_in_proper_sourcenonunitidentity) + ge_balance_positive_proper_sourcenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_sourcenonunitidentityoutput ge_representation_imaginary_code_proper_sourcenonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_proper_sourcenonunitidentityoutput)) * S ((ge_representation_real_code_proper_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_proper_sourcenonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_proper_sourcenonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_sourcenonunitidentityoutputreal ge_balance_negative_proper_sourcenonunitidentityoutputreal. (((((ge_representation_real_code_proper_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_proper_sourcenonunitidentityoutputreal) /\ (ge_balance_negative_proper_sourcenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_sourcenonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_sourcenonunitidentityoutput) = 2 * ge_signed_half_proper_sourcenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_sourcenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_sourcenonunitidentityoutputreal) = S ge_signed_half_proper_sourcenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_sourcenonunitidentity) * (ge_second_rp_proper_sourcenonunitidentity))) + (((ge_first_rn_proper_sourcenonunitidentity) * (ge_second_rn_proper_sourcenonunitidentity))))) + (((((ge_first_ip_proper_sourcenonunitidentity) * (ge_second_in_proper_sourcenonunitidentity))) + (((ge_first_in_proper_sourcenonunitidentity) * (ge_second_ip_proper_sourcenonunitidentity))))))) + ge_balance_negative_proper_sourcenonunitidentityoutputreal = (((((((ge_first_rp_proper_sourcenonunitidentity) * (ge_second_rn_proper_sourcenonunitidentity))) + (((ge_first_rn_proper_sourcenonunitidentity) * (ge_second_rp_proper_sourcenonunitidentity))))) + (((((ge_first_ip_proper_sourcenonunitidentity) * (ge_second_ip_proper_sourcenonunitidentity))) + (((ge_first_in_proper_sourcenonunitidentity) * (ge_second_in_proper_sourcenonunitidentity))))))) + ge_balance_positive_proper_sourcenonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_sourcenonunitidentityoutputimaginary ge_balance_negative_proper_sourcenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_proper_sourcenonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_sourcenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_sourcenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_sourcenonunitidentityoutput) = 2 * ge_signed_half_proper_sourcenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_sourcenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_sourcenonunitidentityoutputimaginary) = S ge_signed_half_proper_sourcenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_sourcenonunitidentity) * (ge_second_ip_proper_sourcenonunitidentity))) + (((ge_first_rn_proper_sourcenonunitidentity) * (ge_second_in_proper_sourcenonunitidentity))))) + (((((ge_first_ip_proper_sourcenonunitidentity) * (ge_second_rp_proper_sourcenonunitidentity))) + (((ge_first_in_proper_sourcenonunitidentity) * (ge_second_rn_proper_sourcenonunitidentity))))))) + ge_balance_negative_proper_sourcenonunitidentityoutputimaginary = (((((((ge_first_rp_proper_sourcenonunitidentity) * (ge_second_in_proper_sourcenonunitidentity))) + (((ge_first_rn_proper_sourcenonunitidentity) * (ge_second_ip_proper_sourcenonunitidentity))))) + (((((ge_first_ip_proper_sourcenonunitidentity) * (ge_second_rn_proper_sourcenonunitidentity))) + (((ge_first_in_proper_sourcenonunitidentity) * (ge_second_rp_proper_sourcenonunitidentity))))))) + ge_balance_positive_proper_sourcenonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_proper_sourcequotient. (exists ge_first_rp_proper_sourcequotientproduct ge_first_rn_proper_sourcequotientproduct ge_first_ip_proper_sourcequotientproduct ge_first_in_proper_sourcequotientproduct ge_second_rp_proper_sourcequotientproduct ge_second_rn_proper_sourcequotientproduct ge_second_ip_proper_sourcequotientproduct ge_second_in_proper_sourcequotientproduct. ((exists ge_representation_real_code_proper_sourcequotientproductfirst ge_representation_imaginary_code_proper_sourcequotientproductfirst. (((d) = ((ge_representation_real_code_proper_sourcequotientproductfirst) + (ge_representation_imaginary_code_proper_sourcequotientproductfirst)) * S ((ge_representation_real_code_proper_sourcequotientproductfirst) + (ge_representation_imaginary_code_proper_sourcequotientproductfirst)) + ((ge_representation_imaginary_code_proper_sourcequotientproductfirst) + (ge_representation_imaginary_code_proper_sourcequotientproductfirst))) /\ ((exists ge_balance_positive_proper_sourcequotientproductfirstreal ge_balance_negative_proper_sourcequotientproductfirstreal. (((((ge_representation_real_code_proper_sourcequotientproductfirst) = 2 * (ge_balance_positive_proper_sourcequotientproductfirstreal) /\ (ge_balance_negative_proper_sourcequotientproductfirstreal) = 0) \/ exists ge_signed_half_proper_sourcequotientproductfirstrealdecode. (((ge_representation_real_code_proper_sourcequotientproductfirst) = 2 * ge_signed_half_proper_sourcequotientproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_sourcequotientproductfirstreal) = 0) /\ (ge_balance_negative_proper_sourcequotientproductfirstreal) = S ge_signed_half_proper_sourcequotientproductfirstrealdecode))) /\ ((ge_first_rp_proper_sourcequotientproduct) + ge_balance_negative_proper_sourcequotientproductfirstreal = (ge_first_rn_proper_sourcequotientproduct) + ge_balance_positive_proper_sourcequotientproductfirstreal))) /\ (exists ge_balance_positive_proper_sourcequotientproductfirstimaginary ge_balance_negative_proper_sourcequotientproductfirstimaginary. (((((ge_representation_imaginary_code_proper_sourcequotientproductfirst) = 2 * (ge_balance_positive_proper_sourcequotientproductfirstimaginary) /\ (ge_balance_negative_proper_sourcequotientproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_sourcequotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_sourcequotientproductfirst) = 2 * ge_signed_half_proper_sourcequotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_sourcequotientproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_sourcequotientproductfirstimaginary) = S ge_signed_half_proper_sourcequotientproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_sourcequotientproduct) + ge_balance_negative_proper_sourcequotientproductfirstimaginary = (ge_first_in_proper_sourcequotientproduct) + ge_balance_positive_proper_sourcequotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_sourcequotientproductsecond ge_representation_imaginary_code_proper_sourcequotientproductsecond. (((gr_quotient_proper_sourcequotient) = ((ge_representation_real_code_proper_sourcequotientproductsecond) + (ge_representation_imaginary_code_proper_sourcequotientproductsecond)) * S ((ge_representation_real_code_proper_sourcequotientproductsecond) + (ge_representation_imaginary_code_proper_sourcequotientproductsecond)) + ((ge_representation_imaginary_code_proper_sourcequotientproductsecond) + (ge_representation_imaginary_code_proper_sourcequotientproductsecond))) /\ ((exists ge_balance_positive_proper_sourcequotientproductsecondreal ge_balance_negative_proper_sourcequotientproductsecondreal. (((((ge_representation_real_code_proper_sourcequotientproductsecond) = 2 * (ge_balance_positive_proper_sourcequotientproductsecondreal) /\ (ge_balance_negative_proper_sourcequotientproductsecondreal) = 0) \/ exists ge_signed_half_proper_sourcequotientproductsecondrealdecode. (((ge_representation_real_code_proper_sourcequotientproductsecond) = 2 * ge_signed_half_proper_sourcequotientproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_sourcequotientproductsecondreal) = 0) /\ (ge_balance_negative_proper_sourcequotientproductsecondreal) = S ge_signed_half_proper_sourcequotientproductsecondrealdecode))) /\ ((ge_second_rp_proper_sourcequotientproduct) + ge_balance_negative_proper_sourcequotientproductsecondreal = (ge_second_rn_proper_sourcequotientproduct) + ge_balance_positive_proper_sourcequotientproductsecondreal))) /\ (exists ge_balance_positive_proper_sourcequotientproductsecondimaginary ge_balance_negative_proper_sourcequotientproductsecondimaginary. (((((ge_representation_imaginary_code_proper_sourcequotientproductsecond) = 2 * (ge_balance_positive_proper_sourcequotientproductsecondimaginary) /\ (ge_balance_negative_proper_sourcequotientproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_sourcequotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_sourcequotientproductsecond) = 2 * ge_signed_half_proper_sourcequotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_sourcequotientproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_sourcequotientproductsecondimaginary) = S ge_signed_half_proper_sourcequotientproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_sourcequotientproduct) + ge_balance_negative_proper_sourcequotientproductsecondimaginary = (ge_second_in_proper_sourcequotientproduct) + ge_balance_positive_proper_sourcequotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_sourcequotientproductoutput ge_representation_imaginary_code_proper_sourcequotientproductoutput. (((z) = ((ge_representation_real_code_proper_sourcequotientproductoutput) + (ge_representation_imaginary_code_proper_sourcequotientproductoutput)) * S ((ge_representation_real_code_proper_sourcequotientproductoutput) + (ge_representation_imaginary_code_proper_sourcequotientproductoutput)) + ((ge_representation_imaginary_code_proper_sourcequotientproductoutput) + (ge_representation_imaginary_code_proper_sourcequotientproductoutput))) /\ ((exists ge_balance_positive_proper_sourcequotientproductoutputreal ge_balance_negative_proper_sourcequotientproductoutputreal. (((((ge_representation_real_code_proper_sourcequotientproductoutput) = 2 * (ge_balance_positive_proper_sourcequotientproductoutputreal) /\ (ge_balance_negative_proper_sourcequotientproductoutputreal) = 0) \/ exists ge_signed_half_proper_sourcequotientproductoutputrealdecode. (((ge_representation_real_code_proper_sourcequotientproductoutput) = 2 * ge_signed_half_proper_sourcequotientproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_sourcequotientproductoutputreal) = 0) /\ (ge_balance_negative_proper_sourcequotientproductoutputreal) = S ge_signed_half_proper_sourcequotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_sourcequotientproduct) * (ge_second_rp_proper_sourcequotientproduct))) + (((ge_first_rn_proper_sourcequotientproduct) * (ge_second_rn_proper_sourcequotientproduct))))) + (((((ge_first_ip_proper_sourcequotientproduct) * (ge_second_in_proper_sourcequotientproduct))) + (((ge_first_in_proper_sourcequotientproduct) * (ge_second_ip_proper_sourcequotientproduct))))))) + ge_balance_negative_proper_sourcequotientproductoutputreal = (((((((ge_first_rp_proper_sourcequotientproduct) * (ge_second_rn_proper_sourcequotientproduct))) + (((ge_first_rn_proper_sourcequotientproduct) * (ge_second_rp_proper_sourcequotientproduct))))) + (((((ge_first_ip_proper_sourcequotientproduct) * (ge_second_ip_proper_sourcequotientproduct))) + (((ge_first_in_proper_sourcequotientproduct) * (ge_second_in_proper_sourcequotientproduct))))))) + ge_balance_positive_proper_sourcequotientproductoutputreal))) /\ (exists ge_balance_positive_proper_sourcequotientproductoutputimaginary ge_balance_negative_proper_sourcequotientproductoutputimaginary. (((((ge_representation_imaginary_code_proper_sourcequotientproductoutput) = 2 * (ge_balance_positive_proper_sourcequotientproductoutputimaginary) /\ (ge_balance_negative_proper_sourcequotientproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_sourcequotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_sourcequotientproductoutput) = 2 * ge_signed_half_proper_sourcequotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_sourcequotientproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_sourcequotientproductoutputimaginary) = S ge_signed_half_proper_sourcequotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_sourcequotientproduct) * (ge_second_ip_proper_sourcequotientproduct))) + (((ge_first_rn_proper_sourcequotientproduct) * (ge_second_in_proper_sourcequotientproduct))))) + (((((ge_first_ip_proper_sourcequotientproduct) * (ge_second_rp_proper_sourcequotientproduct))) + (((ge_first_in_proper_sourcequotientproduct) * (ge_second_rn_proper_sourcequotientproduct))))))) + ge_balance_negative_proper_sourcequotientproductoutputimaginary = (((((((ge_first_rp_proper_sourcequotientproduct) * (ge_second_in_proper_sourcequotientproduct))) + (((ge_first_rn_proper_sourcequotientproduct) * (ge_second_ip_proper_sourcequotientproduct))))) + (((((ge_first_ip_proper_sourcequotientproduct) * (ge_second_rn_proper_sourcequotientproduct))) + (((ge_first_in_proper_sourcequotientproduct) * (ge_second_rp_proper_sourcequotientproduct))))))) + ge_balance_positive_proper_sourcequotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_proper_source. ((exists ge_norm_rp_proper_sourcenorm ge_norm_rn_proper_sourcenorm ge_norm_ip_proper_sourcenorm ge_norm_in_proper_sourcenorm. ((exists ge_representation_real_code_proper_sourcenormrepresentation ge_representation_imaginary_code_proper_sourcenormrepresentation. (((d) = ((ge_representation_real_code_proper_sourcenormrepresentation) + (ge_representation_imaginary_code_proper_sourcenormrepresentation)) * S ((ge_representation_real_code_proper_sourcenormrepresentation) + (ge_representation_imaginary_code_proper_sourcenormrepresentation)) + ((ge_representation_imaginary_code_proper_sourcenormrepresentation) + (ge_representation_imaginary_code_proper_sourcenormrepresentation))) /\ ((exists ge_balance_positive_proper_sourcenormrepresentationreal ge_balance_negative_proper_sourcenormrepresentationreal. (((((ge_representation_real_code_proper_sourcenormrepresentation) = 2 * (ge_balance_positive_proper_sourcenormrepresentationreal) /\ (ge_balance_negative_proper_sourcenormrepresentationreal) = 0) \/ exists ge_signed_half_proper_sourcenormrepresentationrealdecode. (((ge_representation_real_code_proper_sourcenormrepresentation) = 2 * ge_signed_half_proper_sourcenormrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_sourcenormrepresentationreal) = 0) /\ (ge_balance_negative_proper_sourcenormrepresentationreal) = S ge_signed_half_proper_sourcenormrepresentationrealdecode))) /\ ((ge_norm_rp_proper_sourcenorm) + ge_balance_negative_proper_sourcenormrepresentationreal = (ge_norm_rn_proper_sourcenorm) + ge_balance_positive_proper_sourcenormrepresentationreal))) /\ (exists ge_balance_positive_proper_sourcenormrepresentationimaginary ge_balance_negative_proper_sourcenormrepresentationimaginary. (((((ge_representation_imaginary_code_proper_sourcenormrepresentation) = 2 * (ge_balance_positive_proper_sourcenormrepresentationimaginary) /\ (ge_balance_negative_proper_sourcenormrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_sourcenormrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_sourcenormrepresentation) = 2 * ge_signed_half_proper_sourcenormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_sourcenormrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_sourcenormrepresentationimaginary) = S ge_signed_half_proper_sourcenormrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_sourcenorm) + ge_balance_negative_proper_sourcenormrepresentationimaginary = (ge_norm_in_proper_sourcenorm) + ge_balance_positive_proper_sourcenormrepresentationimaginary)))))) /\ (exists ge_real_square_proper_sourcenormsquare ge_imaginary_square_proper_sourcenormsquare. ((((((ge_norm_rp_proper_sourcenorm) * (ge_norm_rp_proper_sourcenorm))) + (((ge_norm_rn_proper_sourcenorm) * (ge_norm_rn_proper_sourcenorm)))) = ((ge_real_square_proper_sourcenormsquare) + (((((ge_norm_rp_proper_sourcenorm) * (ge_norm_rn_proper_sourcenorm))) + (((ge_norm_rn_proper_sourcenorm) * (ge_norm_rp_proper_sourcenorm))))))) /\ ((((((ge_norm_ip_proper_sourcenorm) * (ge_norm_ip_proper_sourcenorm))) + (((ge_norm_in_proper_sourcenorm) * (ge_norm_in_proper_sourcenorm)))) = ((ge_imaginary_square_proper_sourcenormsquare) + (((((ge_norm_ip_proper_sourcenorm) * (ge_norm_in_proper_sourcenorm))) + (((ge_norm_in_proper_sourcenorm) * (ge_norm_ip_proper_sourcenorm))))))) /\ ((gr_proper_divisor_norm_proper_source) = ge_real_square_proper_sourcenormsquare + ge_imaginary_square_proper_sourcenormsquare)))))) /\ (exists ge_gap_proper_sourcestrict. ge_gap_proper_sourcestrict + S (gr_proper_divisor_norm_proper_source) = (N))))))) -> (((~(exists gr_inverse_proper_targetnonunit. (exists ge_first_rp_proper_targetnonunitidentity ge_first_rn_proper_targetnonunitidentity ge_first_ip_proper_targetnonunitidentity ge_first_in_proper_targetnonunitidentity ge_second_rp_proper_targetnonunitidentity ge_second_rn_proper_targetnonunitidentity ge_second_ip_proper_targetnonunitidentity ge_second_in_proper_targetnonunitidentity. ((exists ge_representation_real_code_proper_targetnonunitidentityfirst ge_representation_imaginary_code_proper_targetnonunitidentityfirst. (((e) = ((ge_representation_real_code_proper_targetnonunitidentityfirst) + (ge_representation_imaginary_code_proper_targetnonunitidentityfirst)) * S ((ge_representation_real_code_proper_targetnonunitidentityfirst) + (ge_representation_imaginary_code_proper_targetnonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_targetnonunitidentityfirst) + (ge_representation_imaginary_code_proper_targetnonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_targetnonunitidentityfirstreal ge_balance_negative_proper_targetnonunitidentityfirstreal. (((((ge_representation_real_code_proper_targetnonunitidentityfirst) = 2 * (ge_balance_positive_proper_targetnonunitidentityfirstreal) /\ (ge_balance_negative_proper_targetnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_targetnonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_targetnonunitidentityfirst) = 2 * ge_signed_half_proper_targetnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_targetnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_targetnonunitidentityfirstreal) = S ge_signed_half_proper_targetnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_targetnonunitidentity) + ge_balance_negative_proper_targetnonunitidentityfirstreal = (ge_first_rn_proper_targetnonunitidentity) + ge_balance_positive_proper_targetnonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_targetnonunitidentityfirstimaginary ge_balance_negative_proper_targetnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_targetnonunitidentityfirst) = 2 * (ge_balance_positive_proper_targetnonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_targetnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_targetnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_targetnonunitidentityfirst) = 2 * ge_signed_half_proper_targetnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_targetnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_targetnonunitidentityfirstimaginary) = S ge_signed_half_proper_targetnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_targetnonunitidentity) + ge_balance_negative_proper_targetnonunitidentityfirstimaginary = (ge_first_in_proper_targetnonunitidentity) + ge_balance_positive_proper_targetnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_targetnonunitidentitysecond ge_representation_imaginary_code_proper_targetnonunitidentitysecond. (((gr_inverse_proper_targetnonunit) = ((ge_representation_real_code_proper_targetnonunitidentitysecond) + (ge_representation_imaginary_code_proper_targetnonunitidentitysecond)) * S ((ge_representation_real_code_proper_targetnonunitidentitysecond) + (ge_representation_imaginary_code_proper_targetnonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_targetnonunitidentitysecond) + (ge_representation_imaginary_code_proper_targetnonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_targetnonunitidentitysecondreal ge_balance_negative_proper_targetnonunitidentitysecondreal. (((((ge_representation_real_code_proper_targetnonunitidentitysecond) = 2 * (ge_balance_positive_proper_targetnonunitidentitysecondreal) /\ (ge_balance_negative_proper_targetnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_targetnonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_targetnonunitidentitysecond) = 2 * ge_signed_half_proper_targetnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_targetnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_targetnonunitidentitysecondreal) = S ge_signed_half_proper_targetnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_targetnonunitidentity) + ge_balance_negative_proper_targetnonunitidentitysecondreal = (ge_second_rn_proper_targetnonunitidentity) + ge_balance_positive_proper_targetnonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_targetnonunitidentitysecondimaginary ge_balance_negative_proper_targetnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_targetnonunitidentitysecond) = 2 * (ge_balance_positive_proper_targetnonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_targetnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_targetnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_targetnonunitidentitysecond) = 2 * ge_signed_half_proper_targetnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_targetnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_targetnonunitidentitysecondimaginary) = S ge_signed_half_proper_targetnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_targetnonunitidentity) + ge_balance_negative_proper_targetnonunitidentitysecondimaginary = (ge_second_in_proper_targetnonunitidentity) + ge_balance_positive_proper_targetnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_targetnonunitidentityoutput ge_representation_imaginary_code_proper_targetnonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_targetnonunitidentityoutput) + (ge_representation_imaginary_code_proper_targetnonunitidentityoutput)) * S ((ge_representation_real_code_proper_targetnonunitidentityoutput) + (ge_representation_imaginary_code_proper_targetnonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_targetnonunitidentityoutput) + (ge_representation_imaginary_code_proper_targetnonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_targetnonunitidentityoutputreal ge_balance_negative_proper_targetnonunitidentityoutputreal. (((((ge_representation_real_code_proper_targetnonunitidentityoutput) = 2 * (ge_balance_positive_proper_targetnonunitidentityoutputreal) /\ (ge_balance_negative_proper_targetnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_targetnonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_targetnonunitidentityoutput) = 2 * ge_signed_half_proper_targetnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_targetnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_targetnonunitidentityoutputreal) = S ge_signed_half_proper_targetnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_targetnonunitidentity) * (ge_second_rp_proper_targetnonunitidentity))) + (((ge_first_rn_proper_targetnonunitidentity) * (ge_second_rn_proper_targetnonunitidentity))))) + (((((ge_first_ip_proper_targetnonunitidentity) * (ge_second_in_proper_targetnonunitidentity))) + (((ge_first_in_proper_targetnonunitidentity) * (ge_second_ip_proper_targetnonunitidentity))))))) + ge_balance_negative_proper_targetnonunitidentityoutputreal = (((((((ge_first_rp_proper_targetnonunitidentity) * (ge_second_rn_proper_targetnonunitidentity))) + (((ge_first_rn_proper_targetnonunitidentity) * (ge_second_rp_proper_targetnonunitidentity))))) + (((((ge_first_ip_proper_targetnonunitidentity) * (ge_second_ip_proper_targetnonunitidentity))) + (((ge_first_in_proper_targetnonunitidentity) * (ge_second_in_proper_targetnonunitidentity))))))) + ge_balance_positive_proper_targetnonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_targetnonunitidentityoutputimaginary ge_balance_negative_proper_targetnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_targetnonunitidentityoutput) = 2 * (ge_balance_positive_proper_targetnonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_targetnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_targetnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_targetnonunitidentityoutput) = 2 * ge_signed_half_proper_targetnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_targetnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_targetnonunitidentityoutputimaginary) = S ge_signed_half_proper_targetnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_targetnonunitidentity) * (ge_second_ip_proper_targetnonunitidentity))) + (((ge_first_rn_proper_targetnonunitidentity) * (ge_second_in_proper_targetnonunitidentity))))) + (((((ge_first_ip_proper_targetnonunitidentity) * (ge_second_rp_proper_targetnonunitidentity))) + (((ge_first_in_proper_targetnonunitidentity) * (ge_second_rn_proper_targetnonunitidentity))))))) + ge_balance_negative_proper_targetnonunitidentityoutputimaginary = (((((((ge_first_rp_proper_targetnonunitidentity) * (ge_second_in_proper_targetnonunitidentity))) + (((ge_first_rn_proper_targetnonunitidentity) * (ge_second_ip_proper_targetnonunitidentity))))) + (((((ge_first_ip_proper_targetnonunitidentity) * (ge_second_rn_proper_targetnonunitidentity))) + (((ge_first_in_proper_targetnonunitidentity) * (ge_second_rp_proper_targetnonunitidentity))))))) + ge_balance_positive_proper_targetnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_proper_targetquotient. (exists ge_first_rp_proper_targetquotientproduct ge_first_rn_proper_targetquotientproduct ge_first_ip_proper_targetquotientproduct ge_first_in_proper_targetquotientproduct ge_second_rp_proper_targetquotientproduct ge_second_rn_proper_targetquotientproduct ge_second_ip_proper_targetquotientproduct ge_second_in_proper_targetquotientproduct. ((exists ge_representation_real_code_proper_targetquotientproductfirst ge_representation_imaginary_code_proper_targetquotientproductfirst. (((e) = ((ge_representation_real_code_proper_targetquotientproductfirst) + (ge_representation_imaginary_code_proper_targetquotientproductfirst)) * S ((ge_representation_real_code_proper_targetquotientproductfirst) + (ge_representation_imaginary_code_proper_targetquotientproductfirst)) + ((ge_representation_imaginary_code_proper_targetquotientproductfirst) + (ge_representation_imaginary_code_proper_targetquotientproductfirst))) /\ ((exists ge_balance_positive_proper_targetquotientproductfirstreal ge_balance_negative_proper_targetquotientproductfirstreal. (((((ge_representation_real_code_proper_targetquotientproductfirst) = 2 * (ge_balance_positive_proper_targetquotientproductfirstreal) /\ (ge_balance_negative_proper_targetquotientproductfirstreal) = 0) \/ exists ge_signed_half_proper_targetquotientproductfirstrealdecode. (((ge_representation_real_code_proper_targetquotientproductfirst) = 2 * ge_signed_half_proper_targetquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_targetquotientproductfirstreal) = 0) /\ (ge_balance_negative_proper_targetquotientproductfirstreal) = S ge_signed_half_proper_targetquotientproductfirstrealdecode))) /\ ((ge_first_rp_proper_targetquotientproduct) + ge_balance_negative_proper_targetquotientproductfirstreal = (ge_first_rn_proper_targetquotientproduct) + ge_balance_positive_proper_targetquotientproductfirstreal))) /\ (exists ge_balance_positive_proper_targetquotientproductfirstimaginary ge_balance_negative_proper_targetquotientproductfirstimaginary. (((((ge_representation_imaginary_code_proper_targetquotientproductfirst) = 2 * (ge_balance_positive_proper_targetquotientproductfirstimaginary) /\ (ge_balance_negative_proper_targetquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_targetquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_targetquotientproductfirst) = 2 * ge_signed_half_proper_targetquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_targetquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_targetquotientproductfirstimaginary) = S ge_signed_half_proper_targetquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_targetquotientproduct) + ge_balance_negative_proper_targetquotientproductfirstimaginary = (ge_first_in_proper_targetquotientproduct) + ge_balance_positive_proper_targetquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_targetquotientproductsecond ge_representation_imaginary_code_proper_targetquotientproductsecond. (((gr_quotient_proper_targetquotient) = ((ge_representation_real_code_proper_targetquotientproductsecond) + (ge_representation_imaginary_code_proper_targetquotientproductsecond)) * S ((ge_representation_real_code_proper_targetquotientproductsecond) + (ge_representation_imaginary_code_proper_targetquotientproductsecond)) + ((ge_representation_imaginary_code_proper_targetquotientproductsecond) + (ge_representation_imaginary_code_proper_targetquotientproductsecond))) /\ ((exists ge_balance_positive_proper_targetquotientproductsecondreal ge_balance_negative_proper_targetquotientproductsecondreal. (((((ge_representation_real_code_proper_targetquotientproductsecond) = 2 * (ge_balance_positive_proper_targetquotientproductsecondreal) /\ (ge_balance_negative_proper_targetquotientproductsecondreal) = 0) \/ exists ge_signed_half_proper_targetquotientproductsecondrealdecode. (((ge_representation_real_code_proper_targetquotientproductsecond) = 2 * ge_signed_half_proper_targetquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_targetquotientproductsecondreal) = 0) /\ (ge_balance_negative_proper_targetquotientproductsecondreal) = S ge_signed_half_proper_targetquotientproductsecondrealdecode))) /\ ((ge_second_rp_proper_targetquotientproduct) + ge_balance_negative_proper_targetquotientproductsecondreal = (ge_second_rn_proper_targetquotientproduct) + ge_balance_positive_proper_targetquotientproductsecondreal))) /\ (exists ge_balance_positive_proper_targetquotientproductsecondimaginary ge_balance_negative_proper_targetquotientproductsecondimaginary. (((((ge_representation_imaginary_code_proper_targetquotientproductsecond) = 2 * (ge_balance_positive_proper_targetquotientproductsecondimaginary) /\ (ge_balance_negative_proper_targetquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_targetquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_targetquotientproductsecond) = 2 * ge_signed_half_proper_targetquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_targetquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_targetquotientproductsecondimaginary) = S ge_signed_half_proper_targetquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_targetquotientproduct) + ge_balance_negative_proper_targetquotientproductsecondimaginary = (ge_second_in_proper_targetquotientproduct) + ge_balance_positive_proper_targetquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_targetquotientproductoutput ge_representation_imaginary_code_proper_targetquotientproductoutput. (((z) = ((ge_representation_real_code_proper_targetquotientproductoutput) + (ge_representation_imaginary_code_proper_targetquotientproductoutput)) * S ((ge_representation_real_code_proper_targetquotientproductoutput) + (ge_representation_imaginary_code_proper_targetquotientproductoutput)) + ((ge_representation_imaginary_code_proper_targetquotientproductoutput) + (ge_representation_imaginary_code_proper_targetquotientproductoutput))) /\ ((exists ge_balance_positive_proper_targetquotientproductoutputreal ge_balance_negative_proper_targetquotientproductoutputreal. (((((ge_representation_real_code_proper_targetquotientproductoutput) = 2 * (ge_balance_positive_proper_targetquotientproductoutputreal) /\ (ge_balance_negative_proper_targetquotientproductoutputreal) = 0) \/ exists ge_signed_half_proper_targetquotientproductoutputrealdecode. (((ge_representation_real_code_proper_targetquotientproductoutput) = 2 * ge_signed_half_proper_targetquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_targetquotientproductoutputreal) = 0) /\ (ge_balance_negative_proper_targetquotientproductoutputreal) = S ge_signed_half_proper_targetquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_targetquotientproduct) * (ge_second_rp_proper_targetquotientproduct))) + (((ge_first_rn_proper_targetquotientproduct) * (ge_second_rn_proper_targetquotientproduct))))) + (((((ge_first_ip_proper_targetquotientproduct) * (ge_second_in_proper_targetquotientproduct))) + (((ge_first_in_proper_targetquotientproduct) * (ge_second_ip_proper_targetquotientproduct))))))) + ge_balance_negative_proper_targetquotientproductoutputreal = (((((((ge_first_rp_proper_targetquotientproduct) * (ge_second_rn_proper_targetquotientproduct))) + (((ge_first_rn_proper_targetquotientproduct) * (ge_second_rp_proper_targetquotientproduct))))) + (((((ge_first_ip_proper_targetquotientproduct) * (ge_second_ip_proper_targetquotientproduct))) + (((ge_first_in_proper_targetquotientproduct) * (ge_second_in_proper_targetquotientproduct))))))) + ge_balance_positive_proper_targetquotientproductoutputreal))) /\ (exists ge_balance_positive_proper_targetquotientproductoutputimaginary ge_balance_negative_proper_targetquotientproductoutputimaginary. (((((ge_representation_imaginary_code_proper_targetquotientproductoutput) = 2 * (ge_balance_positive_proper_targetquotientproductoutputimaginary) /\ (ge_balance_negative_proper_targetquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_targetquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_targetquotientproductoutput) = 2 * ge_signed_half_proper_targetquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_targetquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_targetquotientproductoutputimaginary) = S ge_signed_half_proper_targetquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_targetquotientproduct) * (ge_second_ip_proper_targetquotientproduct))) + (((ge_first_rn_proper_targetquotientproduct) * (ge_second_in_proper_targetquotientproduct))))) + (((((ge_first_ip_proper_targetquotientproduct) * (ge_second_rp_proper_targetquotientproduct))) + (((ge_first_in_proper_targetquotientproduct) * (ge_second_rn_proper_targetquotientproduct))))))) + ge_balance_negative_proper_targetquotientproductoutputimaginary = (((((((ge_first_rp_proper_targetquotientproduct) * (ge_second_in_proper_targetquotientproduct))) + (((ge_first_rn_proper_targetquotientproduct) * (ge_second_ip_proper_targetquotientproduct))))) + (((((ge_first_ip_proper_targetquotientproduct) * (ge_second_rn_proper_targetquotientproduct))) + (((ge_first_in_proper_targetquotientproduct) * (ge_second_rp_proper_targetquotientproduct))))))) + ge_balance_positive_proper_targetquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_proper_target. ((exists ge_norm_rp_proper_targetnorm ge_norm_rn_proper_targetnorm ge_norm_ip_proper_targetnorm ge_norm_in_proper_targetnorm. ((exists ge_representation_real_code_proper_targetnormrepresentation ge_representation_imaginary_code_proper_targetnormrepresentation. (((e) = ((ge_representation_real_code_proper_targetnormrepresentation) + (ge_representation_imaginary_code_proper_targetnormrepresentation)) * S ((ge_representation_real_code_proper_targetnormrepresentation) + (ge_representation_imaginary_code_proper_targetnormrepresentation)) + ((ge_representation_imaginary_code_proper_targetnormrepresentation) + (ge_representation_imaginary_code_proper_targetnormrepresentation))) /\ ((exists ge_balance_positive_proper_targetnormrepresentationreal ge_balance_negative_proper_targetnormrepresentationreal. (((((ge_representation_real_code_proper_targetnormrepresentation) = 2 * (ge_balance_positive_proper_targetnormrepresentationreal) /\ (ge_balance_negative_proper_targetnormrepresentationreal) = 0) \/ exists ge_signed_half_proper_targetnormrepresentationrealdecode. (((ge_representation_real_code_proper_targetnormrepresentation) = 2 * ge_signed_half_proper_targetnormrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_targetnormrepresentationreal) = 0) /\ (ge_balance_negative_proper_targetnormrepresentationreal) = S ge_signed_half_proper_targetnormrepresentationrealdecode))) /\ ((ge_norm_rp_proper_targetnorm) + ge_balance_negative_proper_targetnormrepresentationreal = (ge_norm_rn_proper_targetnorm) + ge_balance_positive_proper_targetnormrepresentationreal))) /\ (exists ge_balance_positive_proper_targetnormrepresentationimaginary ge_balance_negative_proper_targetnormrepresentationimaginary. (((((ge_representation_imaginary_code_proper_targetnormrepresentation) = 2 * (ge_balance_positive_proper_targetnormrepresentationimaginary) /\ (ge_balance_negative_proper_targetnormrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_targetnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_targetnormrepresentation) = 2 * ge_signed_half_proper_targetnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_targetnormrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_targetnormrepresentationimaginary) = S ge_signed_half_proper_targetnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_targetnorm) + ge_balance_negative_proper_targetnormrepresentationimaginary = (ge_norm_in_proper_targetnorm) + ge_balance_positive_proper_targetnormrepresentationimaginary)))))) /\ (exists ge_real_square_proper_targetnormsquare ge_imaginary_square_proper_targetnormsquare. ((((((ge_norm_rp_proper_targetnorm) * (ge_norm_rp_proper_targetnorm))) + (((ge_norm_rn_proper_targetnorm) * (ge_norm_rn_proper_targetnorm)))) = ((ge_real_square_proper_targetnormsquare) + (((((ge_norm_rp_proper_targetnorm) * (ge_norm_rn_proper_targetnorm))) + (((ge_norm_rn_proper_targetnorm) * (ge_norm_rp_proper_targetnorm))))))) /\ ((((((ge_norm_ip_proper_targetnorm) * (ge_norm_ip_proper_targetnorm))) + (((ge_norm_in_proper_targetnorm) * (ge_norm_in_proper_targetnorm)))) = ((ge_imaginary_square_proper_targetnormsquare) + (((((ge_norm_ip_proper_targetnorm) * (ge_norm_in_proper_targetnorm))) + (((ge_norm_in_proper_targetnorm) * (ge_norm_ip_proper_targetnorm))))))) /\ ((gr_proper_divisor_norm_proper_target) = ge_real_square_proper_targetnormsquare + ge_imaginary_square_proper_targetnormsquare)))))) /\ (exists ge_gap_proper_targetstrict. ge_gap_proper_targetstrict + S (gr_proper_divisor_norm_proper_target) = (N)))))))