gaussian_factor_search_coordinate_row

Exact expanded first-order arithmetic statement

forall k z N rc. (exists ge_real_positive_row_target ge_real_negative_row_target ge_imaginary_positive_row_target ge_imaginary_negative_row_target. (exists ge_real_code_row_targetdecode ge_imaginary_code_row_targetdecode. (((z) = ((ge_real_code_row_targetdecode) + (ge_imaginary_code_row_targetdecode)) * S ((ge_real_code_row_targetdecode) + (ge_imaginary_code_row_targetdecode)) + ((ge_imaginary_code_row_targetdecode) + (ge_imaginary_code_row_targetdecode))) /\ (((((ge_real_code_row_targetdecode) = 2 * (ge_real_positive_row_target) /\ (ge_real_negative_row_target) = 0) \/ exists ge_signed_half_ge_row_targetdecode_real. (((ge_real_code_row_targetdecode) = 2 * ge_signed_half_ge_row_targetdecode_real + 1 /\ (ge_real_positive_row_target) = 0) /\ (ge_real_negative_row_target) = S ge_signed_half_ge_row_targetdecode_real))) /\ ((((ge_imaginary_code_row_targetdecode) = 2 * (ge_imaginary_positive_row_target) /\ (ge_imaginary_negative_row_target) = 0) \/ exists ge_signed_half_ge_row_targetdecode_imaginary. (((ge_imaginary_code_row_targetdecode) = 2 * ge_signed_half_ge_row_targetdecode_imaginary + 1 /\ (ge_imaginary_positive_row_target) = 0) /\ (ge_imaginary_negative_row_target) = S ge_signed_half_ge_row_targetdecode_imaginary))))))) -> ((exists gr_row_coordinate_row_scan. ((exists ge_gap_row_scanfound_index. ge_gap_row_scanfound_index + S (gr_row_coordinate_row_scan) = (k)) /\ (((~(exists gr_inverse_row_scanfoundnonunit. (exists ge_first_rp_row_scanfoundnonunitidentity ge_first_rn_row_scanfoundnonunitidentity ge_first_ip_row_scanfoundnonunitidentity ge_first_in_row_scanfoundnonunitidentity ge_second_rp_row_scanfoundnonunitidentity ge_second_rn_row_scanfoundnonunitidentity ge_second_ip_row_scanfoundnonunitidentity ge_second_in_row_scanfoundnonunitidentity. ((exists ge_representation_real_code_row_scanfoundnonunitidentityfirst ge_representation_imaginary_code_row_scanfoundnonunitidentityfirst. (((((rc) + (gr_row_coordinate_row_scan)) * S ((rc) + (gr_row_coordinate_row_scan)) + ((gr_row_coordinate_row_scan) + (gr_row_coordinate_row_scan))) = ((ge_representation_real_code_row_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_row_scanfoundnonunitidentityfirst)) * S ((ge_representation_real_code_row_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_row_scanfoundnonunitidentityfirst)) + ((ge_representation_imaginary_code_row_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_row_scanfoundnonunitidentityfirst))) /\ ((exists ge_balance_positive_row_scanfoundnonunitidentityfirstreal ge_balance_negative_row_scanfoundnonunitidentityfirstreal. (((((ge_representation_real_code_row_scanfoundnonunitidentityfirst) = 2 * (ge_balance_positive_row_scanfoundnonunitidentityfirstreal) /\ (ge_balance_negative_row_scanfoundnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_row_scanfoundnonunitidentityfirstrealdecode. (((ge_representation_real_code_row_scanfoundnonunitidentityfirst) = 2 * ge_signed_half_row_scanfoundnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_row_scanfoundnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_row_scanfoundnonunitidentityfirstreal) = S ge_signed_half_row_scanfoundnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_row_scanfoundnonunitidentity) + ge_balance_negative_row_scanfoundnonunitidentityfirstreal = (ge_first_rn_row_scanfoundnonunitidentity) + ge_balance_positive_row_scanfoundnonunitidentityfirstreal))) /\ (exists ge_balance_positive_row_scanfoundnonunitidentityfirstimaginary ge_balance_negative_row_scanfoundnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_row_scanfoundnonunitidentityfirst) = 2 * (ge_balance_positive_row_scanfoundnonunitidentityfirstimaginary) /\ (ge_balance_negative_row_scanfoundnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_row_scanfoundnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_row_scanfoundnonunitidentityfirst) = 2 * ge_signed_half_row_scanfoundnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_row_scanfoundnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_row_scanfoundnonunitidentityfirstimaginary) = S ge_signed_half_row_scanfoundnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_row_scanfoundnonunitidentity) + ge_balance_negative_row_scanfoundnonunitidentityfirstimaginary = (ge_first_in_row_scanfoundnonunitidentity) + ge_balance_positive_row_scanfoundnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_row_scanfoundnonunitidentitysecond ge_representation_imaginary_code_row_scanfoundnonunitidentitysecond. (((gr_inverse_row_scanfoundnonunit) = ((ge_representation_real_code_row_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_row_scanfoundnonunitidentitysecond)) * S ((ge_representation_real_code_row_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_row_scanfoundnonunitidentitysecond)) + ((ge_representation_imaginary_code_row_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_row_scanfoundnonunitidentitysecond))) /\ ((exists ge_balance_positive_row_scanfoundnonunitidentitysecondreal ge_balance_negative_row_scanfoundnonunitidentitysecondreal. (((((ge_representation_real_code_row_scanfoundnonunitidentitysecond) = 2 * (ge_balance_positive_row_scanfoundnonunitidentitysecondreal) /\ (ge_balance_negative_row_scanfoundnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_row_scanfoundnonunitidentitysecondrealdecode. (((ge_representation_real_code_row_scanfoundnonunitidentitysecond) = 2 * ge_signed_half_row_scanfoundnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_row_scanfoundnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_row_scanfoundnonunitidentitysecondreal) = S ge_signed_half_row_scanfoundnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_row_scanfoundnonunitidentity) + ge_balance_negative_row_scanfoundnonunitidentitysecondreal = (ge_second_rn_row_scanfoundnonunitidentity) + ge_balance_positive_row_scanfoundnonunitidentitysecondreal))) /\ (exists ge_balance_positive_row_scanfoundnonunitidentitysecondimaginary ge_balance_negative_row_scanfoundnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_row_scanfoundnonunitidentitysecond) = 2 * (ge_balance_positive_row_scanfoundnonunitidentitysecondimaginary) /\ (ge_balance_negative_row_scanfoundnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_row_scanfoundnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_row_scanfoundnonunitidentitysecond) = 2 * ge_signed_half_row_scanfoundnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_row_scanfoundnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_row_scanfoundnonunitidentitysecondimaginary) = S ge_signed_half_row_scanfoundnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_row_scanfoundnonunitidentity) + ge_balance_negative_row_scanfoundnonunitidentitysecondimaginary = (ge_second_in_row_scanfoundnonunitidentity) + ge_balance_positive_row_scanfoundnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_row_scanfoundnonunitidentityoutput ge_representation_imaginary_code_row_scanfoundnonunitidentityoutput. (((6) = ((ge_representation_real_code_row_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_row_scanfoundnonunitidentityoutput)) * S ((ge_representation_real_code_row_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_row_scanfoundnonunitidentityoutput)) + ((ge_representation_imaginary_code_row_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_row_scanfoundnonunitidentityoutput))) /\ ((exists ge_balance_positive_row_scanfoundnonunitidentityoutputreal ge_balance_negative_row_scanfoundnonunitidentityoutputreal. (((((ge_representation_real_code_row_scanfoundnonunitidentityoutput) = 2 * (ge_balance_positive_row_scanfoundnonunitidentityoutputreal) /\ (ge_balance_negative_row_scanfoundnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_row_scanfoundnonunitidentityoutputrealdecode. (((ge_representation_real_code_row_scanfoundnonunitidentityoutput) = 2 * ge_signed_half_row_scanfoundnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_row_scanfoundnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_row_scanfoundnonunitidentityoutputreal) = S ge_signed_half_row_scanfoundnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_row_scanfoundnonunitidentity) * (ge_second_rp_row_scanfoundnonunitidentity))) + (((ge_first_rn_row_scanfoundnonunitidentity) * (ge_second_rn_row_scanfoundnonunitidentity))))) + (((((ge_first_ip_row_scanfoundnonunitidentity) * (ge_second_in_row_scanfoundnonunitidentity))) + (((ge_first_in_row_scanfoundnonunitidentity) * (ge_second_ip_row_scanfoundnonunitidentity))))))) + ge_balance_negative_row_scanfoundnonunitidentityoutputreal = (((((((ge_first_rp_row_scanfoundnonunitidentity) * (ge_second_rn_row_scanfoundnonunitidentity))) + (((ge_first_rn_row_scanfoundnonunitidentity) * (ge_second_rp_row_scanfoundnonunitidentity))))) + (((((ge_first_ip_row_scanfoundnonunitidentity) * (ge_second_ip_row_scanfoundnonunitidentity))) + (((ge_first_in_row_scanfoundnonunitidentity) * (ge_second_in_row_scanfoundnonunitidentity))))))) + ge_balance_positive_row_scanfoundnonunitidentityoutputreal))) /\ (exists ge_balance_positive_row_scanfoundnonunitidentityoutputimaginary ge_balance_negative_row_scanfoundnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_row_scanfoundnonunitidentityoutput) = 2 * (ge_balance_positive_row_scanfoundnonunitidentityoutputimaginary) /\ (ge_balance_negative_row_scanfoundnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_row_scanfoundnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_row_scanfoundnonunitidentityoutput) = 2 * ge_signed_half_row_scanfoundnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_row_scanfoundnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_row_scanfoundnonunitidentityoutputimaginary) = S ge_signed_half_row_scanfoundnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_row_scanfoundnonunitidentity) * (ge_second_ip_row_scanfoundnonunitidentity))) + (((ge_first_rn_row_scanfoundnonunitidentity) * (ge_second_in_row_scanfoundnonunitidentity))))) + (((((ge_first_ip_row_scanfoundnonunitidentity) * (ge_second_rp_row_scanfoundnonunitidentity))) + (((ge_first_in_row_scanfoundnonunitidentity) * (ge_second_rn_row_scanfoundnonunitidentity))))))) + ge_balance_negative_row_scanfoundnonunitidentityoutputimaginary = (((((((ge_first_rp_row_scanfoundnonunitidentity) * (ge_second_in_row_scanfoundnonunitidentity))) + (((ge_first_rn_row_scanfoundnonunitidentity) * (ge_second_ip_row_scanfoundnonunitidentity))))) + (((((ge_first_ip_row_scanfoundnonunitidentity) * (ge_second_rn_row_scanfoundnonunitidentity))) + (((ge_first_in_row_scanfoundnonunitidentity) * (ge_second_rp_row_scanfoundnonunitidentity))))))) + ge_balance_positive_row_scanfoundnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_row_scanfoundquotient. (exists ge_first_rp_row_scanfoundquotientproduct ge_first_rn_row_scanfoundquotientproduct ge_first_ip_row_scanfoundquotientproduct ge_first_in_row_scanfoundquotientproduct ge_second_rp_row_scanfoundquotientproduct ge_second_rn_row_scanfoundquotientproduct ge_second_ip_row_scanfoundquotientproduct ge_second_in_row_scanfoundquotientproduct. ((exists ge_representation_real_code_row_scanfoundquotientproductfirst ge_representation_imaginary_code_row_scanfoundquotientproductfirst. (((((rc) + (gr_row_coordinate_row_scan)) * S ((rc) + (gr_row_coordinate_row_scan)) + ((gr_row_coordinate_row_scan) + (gr_row_coordinate_row_scan))) = ((ge_representation_real_code_row_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_row_scanfoundquotientproductfirst)) * S ((ge_representation_real_code_row_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_row_scanfoundquotientproductfirst)) + ((ge_representation_imaginary_code_row_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_row_scanfoundquotientproductfirst))) /\ ((exists ge_balance_positive_row_scanfoundquotientproductfirstreal ge_balance_negative_row_scanfoundquotientproductfirstreal. (((((ge_representation_real_code_row_scanfoundquotientproductfirst) = 2 * (ge_balance_positive_row_scanfoundquotientproductfirstreal) /\ (ge_balance_negative_row_scanfoundquotientproductfirstreal) = 0) \/ exists ge_signed_half_row_scanfoundquotientproductfirstrealdecode. (((ge_representation_real_code_row_scanfoundquotientproductfirst) = 2 * ge_signed_half_row_scanfoundquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_row_scanfoundquotientproductfirstreal) = 0) /\ (ge_balance_negative_row_scanfoundquotientproductfirstreal) = S ge_signed_half_row_scanfoundquotientproductfirstrealdecode))) /\ ((ge_first_rp_row_scanfoundquotientproduct) + ge_balance_negative_row_scanfoundquotientproductfirstreal = (ge_first_rn_row_scanfoundquotientproduct) + ge_balance_positive_row_scanfoundquotientproductfirstreal))) /\ (exists ge_balance_positive_row_scanfoundquotientproductfirstimaginary ge_balance_negative_row_scanfoundquotientproductfirstimaginary. (((((ge_representation_imaginary_code_row_scanfoundquotientproductfirst) = 2 * (ge_balance_positive_row_scanfoundquotientproductfirstimaginary) /\ (ge_balance_negative_row_scanfoundquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_row_scanfoundquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_row_scanfoundquotientproductfirst) = 2 * ge_signed_half_row_scanfoundquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_row_scanfoundquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_row_scanfoundquotientproductfirstimaginary) = S ge_signed_half_row_scanfoundquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_row_scanfoundquotientproduct) + ge_balance_negative_row_scanfoundquotientproductfirstimaginary = (ge_first_in_row_scanfoundquotientproduct) + ge_balance_positive_row_scanfoundquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_row_scanfoundquotientproductsecond ge_representation_imaginary_code_row_scanfoundquotientproductsecond. (((gr_quotient_row_scanfoundquotient) = ((ge_representation_real_code_row_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_row_scanfoundquotientproductsecond)) * S ((ge_representation_real_code_row_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_row_scanfoundquotientproductsecond)) + ((ge_representation_imaginary_code_row_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_row_scanfoundquotientproductsecond))) /\ ((exists ge_balance_positive_row_scanfoundquotientproductsecondreal ge_balance_negative_row_scanfoundquotientproductsecondreal. (((((ge_representation_real_code_row_scanfoundquotientproductsecond) = 2 * (ge_balance_positive_row_scanfoundquotientproductsecondreal) /\ (ge_balance_negative_row_scanfoundquotientproductsecondreal) = 0) \/ exists ge_signed_half_row_scanfoundquotientproductsecondrealdecode. (((ge_representation_real_code_row_scanfoundquotientproductsecond) = 2 * ge_signed_half_row_scanfoundquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_row_scanfoundquotientproductsecondreal) = 0) /\ (ge_balance_negative_row_scanfoundquotientproductsecondreal) = S ge_signed_half_row_scanfoundquotientproductsecondrealdecode))) /\ ((ge_second_rp_row_scanfoundquotientproduct) + ge_balance_negative_row_scanfoundquotientproductsecondreal = (ge_second_rn_row_scanfoundquotientproduct) + ge_balance_positive_row_scanfoundquotientproductsecondreal))) /\ (exists ge_balance_positive_row_scanfoundquotientproductsecondimaginary ge_balance_negative_row_scanfoundquotientproductsecondimaginary. (((((ge_representation_imaginary_code_row_scanfoundquotientproductsecond) = 2 * (ge_balance_positive_row_scanfoundquotientproductsecondimaginary) /\ (ge_balance_negative_row_scanfoundquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_row_scanfoundquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_row_scanfoundquotientproductsecond) = 2 * ge_signed_half_row_scanfoundquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_row_scanfoundquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_row_scanfoundquotientproductsecondimaginary) = S ge_signed_half_row_scanfoundquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_row_scanfoundquotientproduct) + ge_balance_negative_row_scanfoundquotientproductsecondimaginary = (ge_second_in_row_scanfoundquotientproduct) + ge_balance_positive_row_scanfoundquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_row_scanfoundquotientproductoutput ge_representation_imaginary_code_row_scanfoundquotientproductoutput. (((z) = ((ge_representation_real_code_row_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_row_scanfoundquotientproductoutput)) * S ((ge_representation_real_code_row_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_row_scanfoundquotientproductoutput)) + ((ge_representation_imaginary_code_row_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_row_scanfoundquotientproductoutput))) /\ ((exists ge_balance_positive_row_scanfoundquotientproductoutputreal ge_balance_negative_row_scanfoundquotientproductoutputreal. (((((ge_representation_real_code_row_scanfoundquotientproductoutput) = 2 * (ge_balance_positive_row_scanfoundquotientproductoutputreal) /\ (ge_balance_negative_row_scanfoundquotientproductoutputreal) = 0) \/ exists ge_signed_half_row_scanfoundquotientproductoutputrealdecode. (((ge_representation_real_code_row_scanfoundquotientproductoutput) = 2 * ge_signed_half_row_scanfoundquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_row_scanfoundquotientproductoutputreal) = 0) /\ (ge_balance_negative_row_scanfoundquotientproductoutputreal) = S ge_signed_half_row_scanfoundquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_row_scanfoundquotientproduct) * (ge_second_rp_row_scanfoundquotientproduct))) + (((ge_first_rn_row_scanfoundquotientproduct) * (ge_second_rn_row_scanfoundquotientproduct))))) + (((((ge_first_ip_row_scanfoundquotientproduct) * (ge_second_in_row_scanfoundquotientproduct))) + (((ge_first_in_row_scanfoundquotientproduct) * (ge_second_ip_row_scanfoundquotientproduct))))))) + ge_balance_negative_row_scanfoundquotientproductoutputreal = (((((((ge_first_rp_row_scanfoundquotientproduct) * (ge_second_rn_row_scanfoundquotientproduct))) + (((ge_first_rn_row_scanfoundquotientproduct) * (ge_second_rp_row_scanfoundquotientproduct))))) + (((((ge_first_ip_row_scanfoundquotientproduct) * (ge_second_ip_row_scanfoundquotientproduct))) + (((ge_first_in_row_scanfoundquotientproduct) * (ge_second_in_row_scanfoundquotientproduct))))))) + ge_balance_positive_row_scanfoundquotientproductoutputreal))) /\ (exists ge_balance_positive_row_scanfoundquotientproductoutputimaginary ge_balance_negative_row_scanfoundquotientproductoutputimaginary. (((((ge_representation_imaginary_code_row_scanfoundquotientproductoutput) = 2 * (ge_balance_positive_row_scanfoundquotientproductoutputimaginary) /\ (ge_balance_negative_row_scanfoundquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_row_scanfoundquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_row_scanfoundquotientproductoutput) = 2 * ge_signed_half_row_scanfoundquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_row_scanfoundquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_row_scanfoundquotientproductoutputimaginary) = S ge_signed_half_row_scanfoundquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_row_scanfoundquotientproduct) * (ge_second_ip_row_scanfoundquotientproduct))) + (((ge_first_rn_row_scanfoundquotientproduct) * (ge_second_in_row_scanfoundquotientproduct))))) + (((((ge_first_ip_row_scanfoundquotientproduct) * (ge_second_rp_row_scanfoundquotientproduct))) + (((ge_first_in_row_scanfoundquotientproduct) * (ge_second_rn_row_scanfoundquotientproduct))))))) + ge_balance_negative_row_scanfoundquotientproductoutputimaginary = (((((((ge_first_rp_row_scanfoundquotientproduct) * (ge_second_in_row_scanfoundquotientproduct))) + (((ge_first_rn_row_scanfoundquotientproduct) * (ge_second_ip_row_scanfoundquotientproduct))))) + (((((ge_first_ip_row_scanfoundquotientproduct) * (ge_second_rn_row_scanfoundquotientproduct))) + (((ge_first_in_row_scanfoundquotientproduct) * (ge_second_rp_row_scanfoundquotientproduct))))))) + ge_balance_positive_row_scanfoundquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_row_scanfound. ((exists ge_norm_rp_row_scanfoundnorm ge_norm_rn_row_scanfoundnorm ge_norm_ip_row_scanfoundnorm ge_norm_in_row_scanfoundnorm. ((exists ge_representation_real_code_row_scanfoundnormrepresentation ge_representation_imaginary_code_row_scanfoundnormrepresentation. (((((rc) + (gr_row_coordinate_row_scan)) * S ((rc) + (gr_row_coordinate_row_scan)) + ((gr_row_coordinate_row_scan) + (gr_row_coordinate_row_scan))) = ((ge_representation_real_code_row_scanfoundnormrepresentation) + (ge_representation_imaginary_code_row_scanfoundnormrepresentation)) * S ((ge_representation_real_code_row_scanfoundnormrepresentation) + (ge_representation_imaginary_code_row_scanfoundnormrepresentation)) + ((ge_representation_imaginary_code_row_scanfoundnormrepresentation) + (ge_representation_imaginary_code_row_scanfoundnormrepresentation))) /\ ((exists ge_balance_positive_row_scanfoundnormrepresentationreal ge_balance_negative_row_scanfoundnormrepresentationreal. (((((ge_representation_real_code_row_scanfoundnormrepresentation) = 2 * (ge_balance_positive_row_scanfoundnormrepresentationreal) /\ (ge_balance_negative_row_scanfoundnormrepresentationreal) = 0) \/ exists ge_signed_half_row_scanfoundnormrepresentationrealdecode. (((ge_representation_real_code_row_scanfoundnormrepresentation) = 2 * ge_signed_half_row_scanfoundnormrepresentationrealdecode + 1 /\ (ge_balance_positive_row_scanfoundnormrepresentationreal) = 0) /\ (ge_balance_negative_row_scanfoundnormrepresentationreal) = S ge_signed_half_row_scanfoundnormrepresentationrealdecode))) /\ ((ge_norm_rp_row_scanfoundnorm) + ge_balance_negative_row_scanfoundnormrepresentationreal = (ge_norm_rn_row_scanfoundnorm) + ge_balance_positive_row_scanfoundnormrepresentationreal))) /\ (exists ge_balance_positive_row_scanfoundnormrepresentationimaginary ge_balance_negative_row_scanfoundnormrepresentationimaginary. (((((ge_representation_imaginary_code_row_scanfoundnormrepresentation) = 2 * (ge_balance_positive_row_scanfoundnormrepresentationimaginary) /\ (ge_balance_negative_row_scanfoundnormrepresentationimaginary) = 0) \/ exists ge_signed_half_row_scanfoundnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_row_scanfoundnormrepresentation) = 2 * ge_signed_half_row_scanfoundnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_row_scanfoundnormrepresentationimaginary) = 0) /\ (ge_balance_negative_row_scanfoundnormrepresentationimaginary) = S ge_signed_half_row_scanfoundnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_row_scanfoundnorm) + ge_balance_negative_row_scanfoundnormrepresentationimaginary = (ge_norm_in_row_scanfoundnorm) + ge_balance_positive_row_scanfoundnormrepresentationimaginary)))))) /\ (exists ge_real_square_row_scanfoundnormsquare ge_imaginary_square_row_scanfoundnormsquare. ((((((ge_norm_rp_row_scanfoundnorm) * (ge_norm_rp_row_scanfoundnorm))) + (((ge_norm_rn_row_scanfoundnorm) * (ge_norm_rn_row_scanfoundnorm)))) = ((ge_real_square_row_scanfoundnormsquare) + (((((ge_norm_rp_row_scanfoundnorm) * (ge_norm_rn_row_scanfoundnorm))) + (((ge_norm_rn_row_scanfoundnorm) * (ge_norm_rp_row_scanfoundnorm))))))) /\ ((((((ge_norm_ip_row_scanfoundnorm) * (ge_norm_ip_row_scanfoundnorm))) + (((ge_norm_in_row_scanfoundnorm) * (ge_norm_in_row_scanfoundnorm)))) = ((ge_imaginary_square_row_scanfoundnormsquare) + (((((ge_norm_ip_row_scanfoundnorm) * (ge_norm_in_row_scanfoundnorm))) + (((ge_norm_in_row_scanfoundnorm) * (ge_norm_ip_row_scanfoundnorm))))))) /\ ((gr_proper_divisor_norm_row_scanfound) = ge_real_square_row_scanfoundnormsquare + ge_imaginary_square_row_scanfoundnormsquare)))))) /\ (exists ge_gap_row_scanfoundstrict. ge_gap_row_scanfoundstrict + S (gr_proper_divisor_norm_row_scanfound) = (N))))))))) \/ (forall gr_row_coordinate_row_scan. (exists ge_gap_row_scanabsent_index. ge_gap_row_scanabsent_index + S (gr_row_coordinate_row_scan) = (k)) -> ~(((~(exists gr_inverse_row_scanabsentnonunit. (exists ge_first_rp_row_scanabsentnonunitidentity ge_first_rn_row_scanabsentnonunitidentity ge_first_ip_row_scanabsentnonunitidentity ge_first_in_row_scanabsentnonunitidentity ge_second_rp_row_scanabsentnonunitidentity ge_second_rn_row_scanabsentnonunitidentity ge_second_ip_row_scanabsentnonunitidentity ge_second_in_row_scanabsentnonunitidentity. ((exists ge_representation_real_code_row_scanabsentnonunitidentityfirst ge_representation_imaginary_code_row_scanabsentnonunitidentityfirst. (((((rc) + (gr_row_coordinate_row_scan)) * S ((rc) + (gr_row_coordinate_row_scan)) + ((gr_row_coordinate_row_scan) + (gr_row_coordinate_row_scan))) = ((ge_representation_real_code_row_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_row_scanabsentnonunitidentityfirst)) * S ((ge_representation_real_code_row_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_row_scanabsentnonunitidentityfirst)) + ((ge_representation_imaginary_code_row_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_row_scanabsentnonunitidentityfirst))) /\ ((exists ge_balance_positive_row_scanabsentnonunitidentityfirstreal ge_balance_negative_row_scanabsentnonunitidentityfirstreal. (((((ge_representation_real_code_row_scanabsentnonunitidentityfirst) = 2 * (ge_balance_positive_row_scanabsentnonunitidentityfirstreal) /\ (ge_balance_negative_row_scanabsentnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_row_scanabsentnonunitidentityfirstrealdecode. (((ge_representation_real_code_row_scanabsentnonunitidentityfirst) = 2 * ge_signed_half_row_scanabsentnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_row_scanabsentnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_row_scanabsentnonunitidentityfirstreal) = S ge_signed_half_row_scanabsentnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_row_scanabsentnonunitidentity) + ge_balance_negative_row_scanabsentnonunitidentityfirstreal = (ge_first_rn_row_scanabsentnonunitidentity) + ge_balance_positive_row_scanabsentnonunitidentityfirstreal))) /\ (exists ge_balance_positive_row_scanabsentnonunitidentityfirstimaginary ge_balance_negative_row_scanabsentnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_row_scanabsentnonunitidentityfirst) = 2 * (ge_balance_positive_row_scanabsentnonunitidentityfirstimaginary) /\ (ge_balance_negative_row_scanabsentnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_row_scanabsentnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_row_scanabsentnonunitidentityfirst) = 2 * ge_signed_half_row_scanabsentnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_row_scanabsentnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_row_scanabsentnonunitidentityfirstimaginary) = S ge_signed_half_row_scanabsentnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_row_scanabsentnonunitidentity) + ge_balance_negative_row_scanabsentnonunitidentityfirstimaginary = (ge_first_in_row_scanabsentnonunitidentity) + ge_balance_positive_row_scanabsentnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_row_scanabsentnonunitidentitysecond ge_representation_imaginary_code_row_scanabsentnonunitidentitysecond. (((gr_inverse_row_scanabsentnonunit) = ((ge_representation_real_code_row_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_row_scanabsentnonunitidentitysecond)) * S ((ge_representation_real_code_row_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_row_scanabsentnonunitidentitysecond)) + ((ge_representation_imaginary_code_row_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_row_scanabsentnonunitidentitysecond))) /\ ((exists ge_balance_positive_row_scanabsentnonunitidentitysecondreal ge_balance_negative_row_scanabsentnonunitidentitysecondreal. (((((ge_representation_real_code_row_scanabsentnonunitidentitysecond) = 2 * (ge_balance_positive_row_scanabsentnonunitidentitysecondreal) /\ (ge_balance_negative_row_scanabsentnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_row_scanabsentnonunitidentitysecondrealdecode. (((ge_representation_real_code_row_scanabsentnonunitidentitysecond) = 2 * ge_signed_half_row_scanabsentnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_row_scanabsentnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_row_scanabsentnonunitidentitysecondreal) = S ge_signed_half_row_scanabsentnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_row_scanabsentnonunitidentity) + ge_balance_negative_row_scanabsentnonunitidentitysecondreal = (ge_second_rn_row_scanabsentnonunitidentity) + ge_balance_positive_row_scanabsentnonunitidentitysecondreal))) /\ (exists ge_balance_positive_row_scanabsentnonunitidentitysecondimaginary ge_balance_negative_row_scanabsentnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_row_scanabsentnonunitidentitysecond) = 2 * (ge_balance_positive_row_scanabsentnonunitidentitysecondimaginary) /\ (ge_balance_negative_row_scanabsentnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_row_scanabsentnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_row_scanabsentnonunitidentitysecond) = 2 * ge_signed_half_row_scanabsentnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_row_scanabsentnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_row_scanabsentnonunitidentitysecondimaginary) = S ge_signed_half_row_scanabsentnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_row_scanabsentnonunitidentity) + ge_balance_negative_row_scanabsentnonunitidentitysecondimaginary = (ge_second_in_row_scanabsentnonunitidentity) + ge_balance_positive_row_scanabsentnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_row_scanabsentnonunitidentityoutput ge_representation_imaginary_code_row_scanabsentnonunitidentityoutput. (((6) = ((ge_representation_real_code_row_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_row_scanabsentnonunitidentityoutput)) * S ((ge_representation_real_code_row_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_row_scanabsentnonunitidentityoutput)) + ((ge_representation_imaginary_code_row_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_row_scanabsentnonunitidentityoutput))) /\ ((exists ge_balance_positive_row_scanabsentnonunitidentityoutputreal ge_balance_negative_row_scanabsentnonunitidentityoutputreal. (((((ge_representation_real_code_row_scanabsentnonunitidentityoutput) = 2 * (ge_balance_positive_row_scanabsentnonunitidentityoutputreal) /\ (ge_balance_negative_row_scanabsentnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_row_scanabsentnonunitidentityoutputrealdecode. (((ge_representation_real_code_row_scanabsentnonunitidentityoutput) = 2 * ge_signed_half_row_scanabsentnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_row_scanabsentnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_row_scanabsentnonunitidentityoutputreal) = S ge_signed_half_row_scanabsentnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_row_scanabsentnonunitidentity) * (ge_second_rp_row_scanabsentnonunitidentity))) + (((ge_first_rn_row_scanabsentnonunitidentity) * (ge_second_rn_row_scanabsentnonunitidentity))))) + (((((ge_first_ip_row_scanabsentnonunitidentity) * (ge_second_in_row_scanabsentnonunitidentity))) + (((ge_first_in_row_scanabsentnonunitidentity) * (ge_second_ip_row_scanabsentnonunitidentity))))))) + ge_balance_negative_row_scanabsentnonunitidentityoutputreal = (((((((ge_first_rp_row_scanabsentnonunitidentity) * (ge_second_rn_row_scanabsentnonunitidentity))) + (((ge_first_rn_row_scanabsentnonunitidentity) * (ge_second_rp_row_scanabsentnonunitidentity))))) + (((((ge_first_ip_row_scanabsentnonunitidentity) * (ge_second_ip_row_scanabsentnonunitidentity))) + (((ge_first_in_row_scanabsentnonunitidentity) * (ge_second_in_row_scanabsentnonunitidentity))))))) + ge_balance_positive_row_scanabsentnonunitidentityoutputreal))) /\ (exists ge_balance_positive_row_scanabsentnonunitidentityoutputimaginary ge_balance_negative_row_scanabsentnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_row_scanabsentnonunitidentityoutput) = 2 * (ge_balance_positive_row_scanabsentnonunitidentityoutputimaginary) /\ (ge_balance_negative_row_scanabsentnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_row_scanabsentnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_row_scanabsentnonunitidentityoutput) = 2 * ge_signed_half_row_scanabsentnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_row_scanabsentnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_row_scanabsentnonunitidentityoutputimaginary) = S ge_signed_half_row_scanabsentnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_row_scanabsentnonunitidentity) * (ge_second_ip_row_scanabsentnonunitidentity))) + (((ge_first_rn_row_scanabsentnonunitidentity) * (ge_second_in_row_scanabsentnonunitidentity))))) + (((((ge_first_ip_row_scanabsentnonunitidentity) * (ge_second_rp_row_scanabsentnonunitidentity))) + (((ge_first_in_row_scanabsentnonunitidentity) * (ge_second_rn_row_scanabsentnonunitidentity))))))) + ge_balance_negative_row_scanabsentnonunitidentityoutputimaginary = (((((((ge_first_rp_row_scanabsentnonunitidentity) * (ge_second_in_row_scanabsentnonunitidentity))) + (((ge_first_rn_row_scanabsentnonunitidentity) * (ge_second_ip_row_scanabsentnonunitidentity))))) + (((((ge_first_ip_row_scanabsentnonunitidentity) * (ge_second_rn_row_scanabsentnonunitidentity))) + (((ge_first_in_row_scanabsentnonunitidentity) * (ge_second_rp_row_scanabsentnonunitidentity))))))) + ge_balance_positive_row_scanabsentnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_row_scanabsentquotient. (exists ge_first_rp_row_scanabsentquotientproduct ge_first_rn_row_scanabsentquotientproduct ge_first_ip_row_scanabsentquotientproduct ge_first_in_row_scanabsentquotientproduct ge_second_rp_row_scanabsentquotientproduct ge_second_rn_row_scanabsentquotientproduct ge_second_ip_row_scanabsentquotientproduct ge_second_in_row_scanabsentquotientproduct. ((exists ge_representation_real_code_row_scanabsentquotientproductfirst ge_representation_imaginary_code_row_scanabsentquotientproductfirst. (((((rc) + (gr_row_coordinate_row_scan)) * S ((rc) + (gr_row_coordinate_row_scan)) + ((gr_row_coordinate_row_scan) + (gr_row_coordinate_row_scan))) = ((ge_representation_real_code_row_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_row_scanabsentquotientproductfirst)) * S ((ge_representation_real_code_row_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_row_scanabsentquotientproductfirst)) + ((ge_representation_imaginary_code_row_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_row_scanabsentquotientproductfirst))) /\ ((exists ge_balance_positive_row_scanabsentquotientproductfirstreal ge_balance_negative_row_scanabsentquotientproductfirstreal. (((((ge_representation_real_code_row_scanabsentquotientproductfirst) = 2 * (ge_balance_positive_row_scanabsentquotientproductfirstreal) /\ (ge_balance_negative_row_scanabsentquotientproductfirstreal) = 0) \/ exists ge_signed_half_row_scanabsentquotientproductfirstrealdecode. (((ge_representation_real_code_row_scanabsentquotientproductfirst) = 2 * ge_signed_half_row_scanabsentquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_row_scanabsentquotientproductfirstreal) = 0) /\ (ge_balance_negative_row_scanabsentquotientproductfirstreal) = S ge_signed_half_row_scanabsentquotientproductfirstrealdecode))) /\ ((ge_first_rp_row_scanabsentquotientproduct) + ge_balance_negative_row_scanabsentquotientproductfirstreal = (ge_first_rn_row_scanabsentquotientproduct) + ge_balance_positive_row_scanabsentquotientproductfirstreal))) /\ (exists ge_balance_positive_row_scanabsentquotientproductfirstimaginary ge_balance_negative_row_scanabsentquotientproductfirstimaginary. (((((ge_representation_imaginary_code_row_scanabsentquotientproductfirst) = 2 * (ge_balance_positive_row_scanabsentquotientproductfirstimaginary) /\ (ge_balance_negative_row_scanabsentquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_row_scanabsentquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_row_scanabsentquotientproductfirst) = 2 * ge_signed_half_row_scanabsentquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_row_scanabsentquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_row_scanabsentquotientproductfirstimaginary) = S ge_signed_half_row_scanabsentquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_row_scanabsentquotientproduct) + ge_balance_negative_row_scanabsentquotientproductfirstimaginary = (ge_first_in_row_scanabsentquotientproduct) + ge_balance_positive_row_scanabsentquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_row_scanabsentquotientproductsecond ge_representation_imaginary_code_row_scanabsentquotientproductsecond. (((gr_quotient_row_scanabsentquotient) = ((ge_representation_real_code_row_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_row_scanabsentquotientproductsecond)) * S ((ge_representation_real_code_row_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_row_scanabsentquotientproductsecond)) + ((ge_representation_imaginary_code_row_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_row_scanabsentquotientproductsecond))) /\ ((exists ge_balance_positive_row_scanabsentquotientproductsecondreal ge_balance_negative_row_scanabsentquotientproductsecondreal. (((((ge_representation_real_code_row_scanabsentquotientproductsecond) = 2 * (ge_balance_positive_row_scanabsentquotientproductsecondreal) /\ (ge_balance_negative_row_scanabsentquotientproductsecondreal) = 0) \/ exists ge_signed_half_row_scanabsentquotientproductsecondrealdecode. (((ge_representation_real_code_row_scanabsentquotientproductsecond) = 2 * ge_signed_half_row_scanabsentquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_row_scanabsentquotientproductsecondreal) = 0) /\ (ge_balance_negative_row_scanabsentquotientproductsecondreal) = S ge_signed_half_row_scanabsentquotientproductsecondrealdecode))) /\ ((ge_second_rp_row_scanabsentquotientproduct) + ge_balance_negative_row_scanabsentquotientproductsecondreal = (ge_second_rn_row_scanabsentquotientproduct) + ge_balance_positive_row_scanabsentquotientproductsecondreal))) /\ (exists ge_balance_positive_row_scanabsentquotientproductsecondimaginary ge_balance_negative_row_scanabsentquotientproductsecondimaginary. (((((ge_representation_imaginary_code_row_scanabsentquotientproductsecond) = 2 * (ge_balance_positive_row_scanabsentquotientproductsecondimaginary) /\ (ge_balance_negative_row_scanabsentquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_row_scanabsentquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_row_scanabsentquotientproductsecond) = 2 * ge_signed_half_row_scanabsentquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_row_scanabsentquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_row_scanabsentquotientproductsecondimaginary) = S ge_signed_half_row_scanabsentquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_row_scanabsentquotientproduct) + ge_balance_negative_row_scanabsentquotientproductsecondimaginary = (ge_second_in_row_scanabsentquotientproduct) + ge_balance_positive_row_scanabsentquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_row_scanabsentquotientproductoutput ge_representation_imaginary_code_row_scanabsentquotientproductoutput. (((z) = ((ge_representation_real_code_row_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_row_scanabsentquotientproductoutput)) * S ((ge_representation_real_code_row_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_row_scanabsentquotientproductoutput)) + ((ge_representation_imaginary_code_row_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_row_scanabsentquotientproductoutput))) /\ ((exists ge_balance_positive_row_scanabsentquotientproductoutputreal ge_balance_negative_row_scanabsentquotientproductoutputreal. (((((ge_representation_real_code_row_scanabsentquotientproductoutput) = 2 * (ge_balance_positive_row_scanabsentquotientproductoutputreal) /\ (ge_balance_negative_row_scanabsentquotientproductoutputreal) = 0) \/ exists ge_signed_half_row_scanabsentquotientproductoutputrealdecode. (((ge_representation_real_code_row_scanabsentquotientproductoutput) = 2 * ge_signed_half_row_scanabsentquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_row_scanabsentquotientproductoutputreal) = 0) /\ (ge_balance_negative_row_scanabsentquotientproductoutputreal) = S ge_signed_half_row_scanabsentquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_row_scanabsentquotientproduct) * (ge_second_rp_row_scanabsentquotientproduct))) + (((ge_first_rn_row_scanabsentquotientproduct) * (ge_second_rn_row_scanabsentquotientproduct))))) + (((((ge_first_ip_row_scanabsentquotientproduct) * (ge_second_in_row_scanabsentquotientproduct))) + (((ge_first_in_row_scanabsentquotientproduct) * (ge_second_ip_row_scanabsentquotientproduct))))))) + ge_balance_negative_row_scanabsentquotientproductoutputreal = (((((((ge_first_rp_row_scanabsentquotientproduct) * (ge_second_rn_row_scanabsentquotientproduct))) + (((ge_first_rn_row_scanabsentquotientproduct) * (ge_second_rp_row_scanabsentquotientproduct))))) + (((((ge_first_ip_row_scanabsentquotientproduct) * (ge_second_ip_row_scanabsentquotientproduct))) + (((ge_first_in_row_scanabsentquotientproduct) * (ge_second_in_row_scanabsentquotientproduct))))))) + ge_balance_positive_row_scanabsentquotientproductoutputreal))) /\ (exists ge_balance_positive_row_scanabsentquotientproductoutputimaginary ge_balance_negative_row_scanabsentquotientproductoutputimaginary. (((((ge_representation_imaginary_code_row_scanabsentquotientproductoutput) = 2 * (ge_balance_positive_row_scanabsentquotientproductoutputimaginary) /\ (ge_balance_negative_row_scanabsentquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_row_scanabsentquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_row_scanabsentquotientproductoutput) = 2 * ge_signed_half_row_scanabsentquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_row_scanabsentquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_row_scanabsentquotientproductoutputimaginary) = S ge_signed_half_row_scanabsentquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_row_scanabsentquotientproduct) * (ge_second_ip_row_scanabsentquotientproduct))) + (((ge_first_rn_row_scanabsentquotientproduct) * (ge_second_in_row_scanabsentquotientproduct))))) + (((((ge_first_ip_row_scanabsentquotientproduct) * (ge_second_rp_row_scanabsentquotientproduct))) + (((ge_first_in_row_scanabsentquotientproduct) * (ge_second_rn_row_scanabsentquotientproduct))))))) + ge_balance_negative_row_scanabsentquotientproductoutputimaginary = (((((((ge_first_rp_row_scanabsentquotientproduct) * (ge_second_in_row_scanabsentquotientproduct))) + (((ge_first_rn_row_scanabsentquotientproduct) * (ge_second_ip_row_scanabsentquotientproduct))))) + (((((ge_first_ip_row_scanabsentquotientproduct) * (ge_second_rn_row_scanabsentquotientproduct))) + (((ge_first_in_row_scanabsentquotientproduct) * (ge_second_rp_row_scanabsentquotientproduct))))))) + ge_balance_positive_row_scanabsentquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_row_scanabsent. ((exists ge_norm_rp_row_scanabsentnorm ge_norm_rn_row_scanabsentnorm ge_norm_ip_row_scanabsentnorm ge_norm_in_row_scanabsentnorm. ((exists ge_representation_real_code_row_scanabsentnormrepresentation ge_representation_imaginary_code_row_scanabsentnormrepresentation. (((((rc) + (gr_row_coordinate_row_scan)) * S ((rc) + (gr_row_coordinate_row_scan)) + ((gr_row_coordinate_row_scan) + (gr_row_coordinate_row_scan))) = ((ge_representation_real_code_row_scanabsentnormrepresentation) + (ge_representation_imaginary_code_row_scanabsentnormrepresentation)) * S ((ge_representation_real_code_row_scanabsentnormrepresentation) + (ge_representation_imaginary_code_row_scanabsentnormrepresentation)) + ((ge_representation_imaginary_code_row_scanabsentnormrepresentation) + (ge_representation_imaginary_code_row_scanabsentnormrepresentation))) /\ ((exists ge_balance_positive_row_scanabsentnormrepresentationreal ge_balance_negative_row_scanabsentnormrepresentationreal. (((((ge_representation_real_code_row_scanabsentnormrepresentation) = 2 * (ge_balance_positive_row_scanabsentnormrepresentationreal) /\ (ge_balance_negative_row_scanabsentnormrepresentationreal) = 0) \/ exists ge_signed_half_row_scanabsentnormrepresentationrealdecode. (((ge_representation_real_code_row_scanabsentnormrepresentation) = 2 * ge_signed_half_row_scanabsentnormrepresentationrealdecode + 1 /\ (ge_balance_positive_row_scanabsentnormrepresentationreal) = 0) /\ (ge_balance_negative_row_scanabsentnormrepresentationreal) = S ge_signed_half_row_scanabsentnormrepresentationrealdecode))) /\ ((ge_norm_rp_row_scanabsentnorm) + ge_balance_negative_row_scanabsentnormrepresentationreal = (ge_norm_rn_row_scanabsentnorm) + ge_balance_positive_row_scanabsentnormrepresentationreal))) /\ (exists ge_balance_positive_row_scanabsentnormrepresentationimaginary ge_balance_negative_row_scanabsentnormrepresentationimaginary. (((((ge_representation_imaginary_code_row_scanabsentnormrepresentation) = 2 * (ge_balance_positive_row_scanabsentnormrepresentationimaginary) /\ (ge_balance_negative_row_scanabsentnormrepresentationimaginary) = 0) \/ exists ge_signed_half_row_scanabsentnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_row_scanabsentnormrepresentation) = 2 * ge_signed_half_row_scanabsentnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_row_scanabsentnormrepresentationimaginary) = 0) /\ (ge_balance_negative_row_scanabsentnormrepresentationimaginary) = S ge_signed_half_row_scanabsentnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_row_scanabsentnorm) + ge_balance_negative_row_scanabsentnormrepresentationimaginary = (ge_norm_in_row_scanabsentnorm) + ge_balance_positive_row_scanabsentnormrepresentationimaginary)))))) /\ (exists ge_real_square_row_scanabsentnormsquare ge_imaginary_square_row_scanabsentnormsquare. ((((((ge_norm_rp_row_scanabsentnorm) * (ge_norm_rp_row_scanabsentnorm))) + (((ge_norm_rn_row_scanabsentnorm) * (ge_norm_rn_row_scanabsentnorm)))) = ((ge_real_square_row_scanabsentnormsquare) + (((((ge_norm_rp_row_scanabsentnorm) * (ge_norm_rn_row_scanabsentnorm))) + (((ge_norm_rn_row_scanabsentnorm) * (ge_norm_rp_row_scanabsentnorm))))))) /\ ((((((ge_norm_ip_row_scanabsentnorm) * (ge_norm_ip_row_scanabsentnorm))) + (((ge_norm_in_row_scanabsentnorm) * (ge_norm_in_row_scanabsentnorm)))) = ((ge_imaginary_square_row_scanabsentnormsquare) + (((((ge_norm_ip_row_scanabsentnorm) * (ge_norm_in_row_scanabsentnorm))) + (((ge_norm_in_row_scanabsentnorm) * (ge_norm_ip_row_scanabsentnorm))))))) /\ ((gr_proper_divisor_norm_row_scanabsent) = ge_real_square_row_scanabsentnormsquare + ge_imaginary_square_row_scanabsentnormsquare)))))) /\ (exists ge_gap_row_scanabsentstrict. ge_gap_row_scanabsentstrict + S (gr_proper_divisor_norm_row_scanabsent) = (N)))))))))