gaussian_proper_norm_divisor_decidable

Exact expanded first-order arithmetic statement

forall d z N. (exists ge_real_positive_proper_candidate_valid ge_real_negative_proper_candidate_valid ge_imaginary_positive_proper_candidate_valid ge_imaginary_negative_proper_candidate_valid. (exists ge_real_code_proper_candidate_validdecode ge_imaginary_code_proper_candidate_validdecode. (((d) = ((ge_real_code_proper_candidate_validdecode) + (ge_imaginary_code_proper_candidate_validdecode)) * S ((ge_real_code_proper_candidate_validdecode) + (ge_imaginary_code_proper_candidate_validdecode)) + ((ge_imaginary_code_proper_candidate_validdecode) + (ge_imaginary_code_proper_candidate_validdecode))) /\ (((((ge_real_code_proper_candidate_validdecode) = 2 * (ge_real_positive_proper_candidate_valid) /\ (ge_real_negative_proper_candidate_valid) = 0) \/ exists ge_signed_half_ge_proper_candidate_validdecode_real. (((ge_real_code_proper_candidate_validdecode) = 2 * ge_signed_half_ge_proper_candidate_validdecode_real + 1 /\ (ge_real_positive_proper_candidate_valid) = 0) /\ (ge_real_negative_proper_candidate_valid) = S ge_signed_half_ge_proper_candidate_validdecode_real))) /\ ((((ge_imaginary_code_proper_candidate_validdecode) = 2 * (ge_imaginary_positive_proper_candidate_valid) /\ (ge_imaginary_negative_proper_candidate_valid) = 0) \/ exists ge_signed_half_ge_proper_candidate_validdecode_imaginary. (((ge_imaginary_code_proper_candidate_validdecode) = 2 * ge_signed_half_ge_proper_candidate_validdecode_imaginary + 1 /\ (ge_imaginary_positive_proper_candidate_valid) = 0) /\ (ge_imaginary_negative_proper_candidate_valid) = S ge_signed_half_ge_proper_candidate_validdecode_imaginary))))))) -> (exists ge_real_positive_proper_target_valid ge_real_negative_proper_target_valid ge_imaginary_positive_proper_target_valid ge_imaginary_negative_proper_target_valid. (exists ge_real_code_proper_target_validdecode ge_imaginary_code_proper_target_validdecode. (((z) = ((ge_real_code_proper_target_validdecode) + (ge_imaginary_code_proper_target_validdecode)) * S ((ge_real_code_proper_target_validdecode) + (ge_imaginary_code_proper_target_validdecode)) + ((ge_imaginary_code_proper_target_validdecode) + (ge_imaginary_code_proper_target_validdecode))) /\ (((((ge_real_code_proper_target_validdecode) = 2 * (ge_real_positive_proper_target_valid) /\ (ge_real_negative_proper_target_valid) = 0) \/ exists ge_signed_half_ge_proper_target_validdecode_real. (((ge_real_code_proper_target_validdecode) = 2 * ge_signed_half_ge_proper_target_validdecode_real + 1 /\ (ge_real_positive_proper_target_valid) = 0) /\ (ge_real_negative_proper_target_valid) = S ge_signed_half_ge_proper_target_validdecode_real))) /\ ((((ge_imaginary_code_proper_target_validdecode) = 2 * (ge_imaginary_positive_proper_target_valid) /\ (ge_imaginary_negative_proper_target_valid) = 0) \/ exists ge_signed_half_ge_proper_target_validdecode_imaginary. (((ge_imaginary_code_proper_target_validdecode) = 2 * ge_signed_half_ge_proper_target_validdecode_imaginary + 1 /\ (ge_imaginary_positive_proper_target_valid) = 0) /\ (ge_imaginary_negative_proper_target_valid) = S ge_signed_half_ge_proper_target_validdecode_imaginary))))))) -> (((~(exists gr_inverse_proper_decision_yesnonunit. (exists ge_first_rp_proper_decision_yesnonunitidentity ge_first_rn_proper_decision_yesnonunitidentity ge_first_ip_proper_decision_yesnonunitidentity ge_first_in_proper_decision_yesnonunitidentity ge_second_rp_proper_decision_yesnonunitidentity ge_second_rn_proper_decision_yesnonunitidentity ge_second_ip_proper_decision_yesnonunitidentity ge_second_in_proper_decision_yesnonunitidentity. ((exists ge_representation_real_code_proper_decision_yesnonunitidentityfirst ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst. (((d) = ((ge_representation_real_code_proper_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst)) * S ((ge_representation_real_code_proper_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_decision_yesnonunitidentityfirstreal ge_balance_negative_proper_decision_yesnonunitidentityfirstreal. (((((ge_representation_real_code_proper_decision_yesnonunitidentityfirst) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentityfirstreal) /\ (ge_balance_negative_proper_decision_yesnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_decision_yesnonunitidentityfirst) = 2 * ge_signed_half_proper_decision_yesnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentityfirstreal) = S ge_signed_half_proper_decision_yesnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_decision_yesnonunitidentity) + ge_balance_negative_proper_decision_yesnonunitidentityfirstreal = (ge_first_rn_proper_decision_yesnonunitidentity) + ge_balance_positive_proper_decision_yesnonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_decision_yesnonunitidentityfirstimaginary ge_balance_negative_proper_decision_yesnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_decision_yesnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst) = 2 * ge_signed_half_proper_decision_yesnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentityfirstimaginary) = S ge_signed_half_proper_decision_yesnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_decision_yesnonunitidentity) + ge_balance_negative_proper_decision_yesnonunitidentityfirstimaginary = (ge_first_in_proper_decision_yesnonunitidentity) + ge_balance_positive_proper_decision_yesnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_decision_yesnonunitidentitysecond ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond. (((gr_inverse_proper_decision_yesnonunit) = ((ge_representation_real_code_proper_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond)) * S ((ge_representation_real_code_proper_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_decision_yesnonunitidentitysecondreal ge_balance_negative_proper_decision_yesnonunitidentitysecondreal. (((((ge_representation_real_code_proper_decision_yesnonunitidentitysecond) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentitysecondreal) /\ (ge_balance_negative_proper_decision_yesnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_decision_yesnonunitidentitysecond) = 2 * ge_signed_half_proper_decision_yesnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentitysecondreal) = S ge_signed_half_proper_decision_yesnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_decision_yesnonunitidentity) + ge_balance_negative_proper_decision_yesnonunitidentitysecondreal = (ge_second_rn_proper_decision_yesnonunitidentity) + ge_balance_positive_proper_decision_yesnonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_decision_yesnonunitidentitysecondimaginary ge_balance_negative_proper_decision_yesnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_decision_yesnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond) = 2 * ge_signed_half_proper_decision_yesnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentitysecondimaginary) = S ge_signed_half_proper_decision_yesnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_decision_yesnonunitidentity) + ge_balance_negative_proper_decision_yesnonunitidentitysecondimaginary = (ge_second_in_proper_decision_yesnonunitidentity) + ge_balance_positive_proper_decision_yesnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_decision_yesnonunitidentityoutput ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput)) * S ((ge_representation_real_code_proper_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_decision_yesnonunitidentityoutputreal ge_balance_negative_proper_decision_yesnonunitidentityoutputreal. (((((ge_representation_real_code_proper_decision_yesnonunitidentityoutput) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentityoutputreal) /\ (ge_balance_negative_proper_decision_yesnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_decision_yesnonunitidentityoutput) = 2 * ge_signed_half_proper_decision_yesnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentityoutputreal) = S ge_signed_half_proper_decision_yesnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_decision_yesnonunitidentity) * (ge_second_rp_proper_decision_yesnonunitidentity))) + (((ge_first_rn_proper_decision_yesnonunitidentity) * (ge_second_rn_proper_decision_yesnonunitidentity))))) + (((((ge_first_ip_proper_decision_yesnonunitidentity) * (ge_second_in_proper_decision_yesnonunitidentity))) + (((ge_first_in_proper_decision_yesnonunitidentity) * (ge_second_ip_proper_decision_yesnonunitidentity))))))) + ge_balance_negative_proper_decision_yesnonunitidentityoutputreal = (((((((ge_first_rp_proper_decision_yesnonunitidentity) * (ge_second_rn_proper_decision_yesnonunitidentity))) + (((ge_first_rn_proper_decision_yesnonunitidentity) * (ge_second_rp_proper_decision_yesnonunitidentity))))) + (((((ge_first_ip_proper_decision_yesnonunitidentity) * (ge_second_ip_proper_decision_yesnonunitidentity))) + (((ge_first_in_proper_decision_yesnonunitidentity) * (ge_second_in_proper_decision_yesnonunitidentity))))))) + ge_balance_positive_proper_decision_yesnonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_decision_yesnonunitidentityoutputimaginary ge_balance_negative_proper_decision_yesnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_decision_yesnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput) = 2 * ge_signed_half_proper_decision_yesnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentityoutputimaginary) = S ge_signed_half_proper_decision_yesnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_decision_yesnonunitidentity) * (ge_second_ip_proper_decision_yesnonunitidentity))) + (((ge_first_rn_proper_decision_yesnonunitidentity) * (ge_second_in_proper_decision_yesnonunitidentity))))) + (((((ge_first_ip_proper_decision_yesnonunitidentity) * (ge_second_rp_proper_decision_yesnonunitidentity))) + (((ge_first_in_proper_decision_yesnonunitidentity) * (ge_second_rn_proper_decision_yesnonunitidentity))))))) + ge_balance_negative_proper_decision_yesnonunitidentityoutputimaginary = (((((((ge_first_rp_proper_decision_yesnonunitidentity) * (ge_second_in_proper_decision_yesnonunitidentity))) + (((ge_first_rn_proper_decision_yesnonunitidentity) * (ge_second_ip_proper_decision_yesnonunitidentity))))) + (((((ge_first_ip_proper_decision_yesnonunitidentity) * (ge_second_rn_proper_decision_yesnonunitidentity))) + (((ge_first_in_proper_decision_yesnonunitidentity) * (ge_second_rp_proper_decision_yesnonunitidentity))))))) + ge_balance_positive_proper_decision_yesnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_proper_decision_yesquotient. (exists ge_first_rp_proper_decision_yesquotientproduct ge_first_rn_proper_decision_yesquotientproduct ge_first_ip_proper_decision_yesquotientproduct ge_first_in_proper_decision_yesquotientproduct ge_second_rp_proper_decision_yesquotientproduct ge_second_rn_proper_decision_yesquotientproduct ge_second_ip_proper_decision_yesquotientproduct ge_second_in_proper_decision_yesquotientproduct. ((exists ge_representation_real_code_proper_decision_yesquotientproductfirst ge_representation_imaginary_code_proper_decision_yesquotientproductfirst. (((d) = ((ge_representation_real_code_proper_decision_yesquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_yesquotientproductfirst)) * S ((ge_representation_real_code_proper_decision_yesquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_yesquotientproductfirst)) + ((ge_representation_imaginary_code_proper_decision_yesquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_yesquotientproductfirst))) /\ ((exists ge_balance_positive_proper_decision_yesquotientproductfirstreal ge_balance_negative_proper_decision_yesquotientproductfirstreal. (((((ge_representation_real_code_proper_decision_yesquotientproductfirst) = 2 * (ge_balance_positive_proper_decision_yesquotientproductfirstreal) /\ (ge_balance_negative_proper_decision_yesquotientproductfirstreal) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductfirstrealdecode. (((ge_representation_real_code_proper_decision_yesquotientproductfirst) = 2 * ge_signed_half_proper_decision_yesquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductfirstreal) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductfirstreal) = S ge_signed_half_proper_decision_yesquotientproductfirstrealdecode))) /\ ((ge_first_rp_proper_decision_yesquotientproduct) + ge_balance_negative_proper_decision_yesquotientproductfirstreal = (ge_first_rn_proper_decision_yesquotientproduct) + ge_balance_positive_proper_decision_yesquotientproductfirstreal))) /\ (exists ge_balance_positive_proper_decision_yesquotientproductfirstimaginary ge_balance_negative_proper_decision_yesquotientproductfirstimaginary. (((((ge_representation_imaginary_code_proper_decision_yesquotientproductfirst) = 2 * (ge_balance_positive_proper_decision_yesquotientproductfirstimaginary) /\ (ge_balance_negative_proper_decision_yesquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesquotientproductfirst) = 2 * ge_signed_half_proper_decision_yesquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductfirstimaginary) = S ge_signed_half_proper_decision_yesquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_decision_yesquotientproduct) + ge_balance_negative_proper_decision_yesquotientproductfirstimaginary = (ge_first_in_proper_decision_yesquotientproduct) + ge_balance_positive_proper_decision_yesquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_decision_yesquotientproductsecond ge_representation_imaginary_code_proper_decision_yesquotientproductsecond. (((gr_quotient_proper_decision_yesquotient) = ((ge_representation_real_code_proper_decision_yesquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_yesquotientproductsecond)) * S ((ge_representation_real_code_proper_decision_yesquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_yesquotientproductsecond)) + ((ge_representation_imaginary_code_proper_decision_yesquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_yesquotientproductsecond))) /\ ((exists ge_balance_positive_proper_decision_yesquotientproductsecondreal ge_balance_negative_proper_decision_yesquotientproductsecondreal. (((((ge_representation_real_code_proper_decision_yesquotientproductsecond) = 2 * (ge_balance_positive_proper_decision_yesquotientproductsecondreal) /\ (ge_balance_negative_proper_decision_yesquotientproductsecondreal) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductsecondrealdecode. (((ge_representation_real_code_proper_decision_yesquotientproductsecond) = 2 * ge_signed_half_proper_decision_yesquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductsecondreal) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductsecondreal) = S ge_signed_half_proper_decision_yesquotientproductsecondrealdecode))) /\ ((ge_second_rp_proper_decision_yesquotientproduct) + ge_balance_negative_proper_decision_yesquotientproductsecondreal = (ge_second_rn_proper_decision_yesquotientproduct) + ge_balance_positive_proper_decision_yesquotientproductsecondreal))) /\ (exists ge_balance_positive_proper_decision_yesquotientproductsecondimaginary ge_balance_negative_proper_decision_yesquotientproductsecondimaginary. (((((ge_representation_imaginary_code_proper_decision_yesquotientproductsecond) = 2 * (ge_balance_positive_proper_decision_yesquotientproductsecondimaginary) /\ (ge_balance_negative_proper_decision_yesquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesquotientproductsecond) = 2 * ge_signed_half_proper_decision_yesquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductsecondimaginary) = S ge_signed_half_proper_decision_yesquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_decision_yesquotientproduct) + ge_balance_negative_proper_decision_yesquotientproductsecondimaginary = (ge_second_in_proper_decision_yesquotientproduct) + ge_balance_positive_proper_decision_yesquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_decision_yesquotientproductoutput ge_representation_imaginary_code_proper_decision_yesquotientproductoutput. (((z) = ((ge_representation_real_code_proper_decision_yesquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_yesquotientproductoutput)) * S ((ge_representation_real_code_proper_decision_yesquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_yesquotientproductoutput)) + ((ge_representation_imaginary_code_proper_decision_yesquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_yesquotientproductoutput))) /\ ((exists ge_balance_positive_proper_decision_yesquotientproductoutputreal ge_balance_negative_proper_decision_yesquotientproductoutputreal. (((((ge_representation_real_code_proper_decision_yesquotientproductoutput) = 2 * (ge_balance_positive_proper_decision_yesquotientproductoutputreal) /\ (ge_balance_negative_proper_decision_yesquotientproductoutputreal) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductoutputrealdecode. (((ge_representation_real_code_proper_decision_yesquotientproductoutput) = 2 * ge_signed_half_proper_decision_yesquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductoutputreal) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductoutputreal) = S ge_signed_half_proper_decision_yesquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_decision_yesquotientproduct) * (ge_second_rp_proper_decision_yesquotientproduct))) + (((ge_first_rn_proper_decision_yesquotientproduct) * (ge_second_rn_proper_decision_yesquotientproduct))))) + (((((ge_first_ip_proper_decision_yesquotientproduct) * (ge_second_in_proper_decision_yesquotientproduct))) + (((ge_first_in_proper_decision_yesquotientproduct) * (ge_second_ip_proper_decision_yesquotientproduct))))))) + ge_balance_negative_proper_decision_yesquotientproductoutputreal = (((((((ge_first_rp_proper_decision_yesquotientproduct) * (ge_second_rn_proper_decision_yesquotientproduct))) + (((ge_first_rn_proper_decision_yesquotientproduct) * (ge_second_rp_proper_decision_yesquotientproduct))))) + (((((ge_first_ip_proper_decision_yesquotientproduct) * (ge_second_ip_proper_decision_yesquotientproduct))) + (((ge_first_in_proper_decision_yesquotientproduct) * (ge_second_in_proper_decision_yesquotientproduct))))))) + ge_balance_positive_proper_decision_yesquotientproductoutputreal))) /\ (exists ge_balance_positive_proper_decision_yesquotientproductoutputimaginary ge_balance_negative_proper_decision_yesquotientproductoutputimaginary. (((((ge_representation_imaginary_code_proper_decision_yesquotientproductoutput) = 2 * (ge_balance_positive_proper_decision_yesquotientproductoutputimaginary) /\ (ge_balance_negative_proper_decision_yesquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesquotientproductoutput) = 2 * ge_signed_half_proper_decision_yesquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductoutputimaginary) = S ge_signed_half_proper_decision_yesquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_decision_yesquotientproduct) * (ge_second_ip_proper_decision_yesquotientproduct))) + (((ge_first_rn_proper_decision_yesquotientproduct) * (ge_second_in_proper_decision_yesquotientproduct))))) + (((((ge_first_ip_proper_decision_yesquotientproduct) * (ge_second_rp_proper_decision_yesquotientproduct))) + (((ge_first_in_proper_decision_yesquotientproduct) * (ge_second_rn_proper_decision_yesquotientproduct))))))) + ge_balance_negative_proper_decision_yesquotientproductoutputimaginary = (((((((ge_first_rp_proper_decision_yesquotientproduct) * (ge_second_in_proper_decision_yesquotientproduct))) + (((ge_first_rn_proper_decision_yesquotientproduct) * (ge_second_ip_proper_decision_yesquotientproduct))))) + (((((ge_first_ip_proper_decision_yesquotientproduct) * (ge_second_rn_proper_decision_yesquotientproduct))) + (((ge_first_in_proper_decision_yesquotientproduct) * (ge_second_rp_proper_decision_yesquotientproduct))))))) + ge_balance_positive_proper_decision_yesquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_proper_decision_yes. ((exists ge_norm_rp_proper_decision_yesnorm ge_norm_rn_proper_decision_yesnorm ge_norm_ip_proper_decision_yesnorm ge_norm_in_proper_decision_yesnorm. ((exists ge_representation_real_code_proper_decision_yesnormrepresentation ge_representation_imaginary_code_proper_decision_yesnormrepresentation. (((d) = ((ge_representation_real_code_proper_decision_yesnormrepresentation) + (ge_representation_imaginary_code_proper_decision_yesnormrepresentation)) * S ((ge_representation_real_code_proper_decision_yesnormrepresentation) + (ge_representation_imaginary_code_proper_decision_yesnormrepresentation)) + ((ge_representation_imaginary_code_proper_decision_yesnormrepresentation) + (ge_representation_imaginary_code_proper_decision_yesnormrepresentation))) /\ ((exists ge_balance_positive_proper_decision_yesnormrepresentationreal ge_balance_negative_proper_decision_yesnormrepresentationreal. (((((ge_representation_real_code_proper_decision_yesnormrepresentation) = 2 * (ge_balance_positive_proper_decision_yesnormrepresentationreal) /\ (ge_balance_negative_proper_decision_yesnormrepresentationreal) = 0) \/ exists ge_signed_half_proper_decision_yesnormrepresentationrealdecode. (((ge_representation_real_code_proper_decision_yesnormrepresentation) = 2 * ge_signed_half_proper_decision_yesnormrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesnormrepresentationreal) = 0) /\ (ge_balance_negative_proper_decision_yesnormrepresentationreal) = S ge_signed_half_proper_decision_yesnormrepresentationrealdecode))) /\ ((ge_norm_rp_proper_decision_yesnorm) + ge_balance_negative_proper_decision_yesnormrepresentationreal = (ge_norm_rn_proper_decision_yesnorm) + ge_balance_positive_proper_decision_yesnormrepresentationreal))) /\ (exists ge_balance_positive_proper_decision_yesnormrepresentationimaginary ge_balance_negative_proper_decision_yesnormrepresentationimaginary. (((((ge_representation_imaginary_code_proper_decision_yesnormrepresentation) = 2 * (ge_balance_positive_proper_decision_yesnormrepresentationimaginary) /\ (ge_balance_negative_proper_decision_yesnormrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesnormrepresentation) = 2 * ge_signed_half_proper_decision_yesnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesnormrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesnormrepresentationimaginary) = S ge_signed_half_proper_decision_yesnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_decision_yesnorm) + ge_balance_negative_proper_decision_yesnormrepresentationimaginary = (ge_norm_in_proper_decision_yesnorm) + ge_balance_positive_proper_decision_yesnormrepresentationimaginary)))))) /\ (exists ge_real_square_proper_decision_yesnormsquare ge_imaginary_square_proper_decision_yesnormsquare. ((((((ge_norm_rp_proper_decision_yesnorm) * (ge_norm_rp_proper_decision_yesnorm))) + (((ge_norm_rn_proper_decision_yesnorm) * (ge_norm_rn_proper_decision_yesnorm)))) = ((ge_real_square_proper_decision_yesnormsquare) + (((((ge_norm_rp_proper_decision_yesnorm) * (ge_norm_rn_proper_decision_yesnorm))) + (((ge_norm_rn_proper_decision_yesnorm) * (ge_norm_rp_proper_decision_yesnorm))))))) /\ ((((((ge_norm_ip_proper_decision_yesnorm) * (ge_norm_ip_proper_decision_yesnorm))) + (((ge_norm_in_proper_decision_yesnorm) * (ge_norm_in_proper_decision_yesnorm)))) = ((ge_imaginary_square_proper_decision_yesnormsquare) + (((((ge_norm_ip_proper_decision_yesnorm) * (ge_norm_in_proper_decision_yesnorm))) + (((ge_norm_in_proper_decision_yesnorm) * (ge_norm_ip_proper_decision_yesnorm))))))) /\ ((gr_proper_divisor_norm_proper_decision_yes) = ge_real_square_proper_decision_yesnormsquare + ge_imaginary_square_proper_decision_yesnormsquare)))))) /\ (exists ge_gap_proper_decision_yesstrict. ge_gap_proper_decision_yesstrict + S (gr_proper_divisor_norm_proper_decision_yes) = (N))))))) \/ ~(((~(exists gr_inverse_proper_decision_nononunit. (exists ge_first_rp_proper_decision_nononunitidentity ge_first_rn_proper_decision_nononunitidentity ge_first_ip_proper_decision_nononunitidentity ge_first_in_proper_decision_nononunitidentity ge_second_rp_proper_decision_nononunitidentity ge_second_rn_proper_decision_nononunitidentity ge_second_ip_proper_decision_nononunitidentity ge_second_in_proper_decision_nononunitidentity. ((exists ge_representation_real_code_proper_decision_nononunitidentityfirst ge_representation_imaginary_code_proper_decision_nononunitidentityfirst. (((d) = ((ge_representation_real_code_proper_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_nononunitidentityfirst)) * S ((ge_representation_real_code_proper_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_nononunitidentityfirst)) + ((ge_representation_imaginary_code_proper_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_nononunitidentityfirst))) /\ ((exists ge_balance_positive_proper_decision_nononunitidentityfirstreal ge_balance_negative_proper_decision_nononunitidentityfirstreal. (((((ge_representation_real_code_proper_decision_nononunitidentityfirst) = 2 * (ge_balance_positive_proper_decision_nononunitidentityfirstreal) /\ (ge_balance_negative_proper_decision_nononunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentityfirstrealdecode. (((ge_representation_real_code_proper_decision_nononunitidentityfirst) = 2 * ge_signed_half_proper_decision_nononunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentityfirstreal) = S ge_signed_half_proper_decision_nononunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_decision_nononunitidentity) + ge_balance_negative_proper_decision_nononunitidentityfirstreal = (ge_first_rn_proper_decision_nononunitidentity) + ge_balance_positive_proper_decision_nononunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_decision_nononunitidentityfirstimaginary ge_balance_negative_proper_decision_nononunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_decision_nononunitidentityfirst) = 2 * (ge_balance_positive_proper_decision_nononunitidentityfirstimaginary) /\ (ge_balance_negative_proper_decision_nononunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_decision_nononunitidentityfirst) = 2 * ge_signed_half_proper_decision_nononunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentityfirstimaginary) = S ge_signed_half_proper_decision_nononunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_decision_nononunitidentity) + ge_balance_negative_proper_decision_nononunitidentityfirstimaginary = (ge_first_in_proper_decision_nononunitidentity) + ge_balance_positive_proper_decision_nononunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_decision_nononunitidentitysecond ge_representation_imaginary_code_proper_decision_nononunitidentitysecond. (((gr_inverse_proper_decision_nononunit) = ((ge_representation_real_code_proper_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_nononunitidentitysecond)) * S ((ge_representation_real_code_proper_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_nononunitidentitysecond)) + ((ge_representation_imaginary_code_proper_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_nononunitidentitysecond))) /\ ((exists ge_balance_positive_proper_decision_nononunitidentitysecondreal ge_balance_negative_proper_decision_nononunitidentitysecondreal. (((((ge_representation_real_code_proper_decision_nononunitidentitysecond) = 2 * (ge_balance_positive_proper_decision_nononunitidentitysecondreal) /\ (ge_balance_negative_proper_decision_nononunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentitysecondrealdecode. (((ge_representation_real_code_proper_decision_nononunitidentitysecond) = 2 * ge_signed_half_proper_decision_nononunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentitysecondreal) = S ge_signed_half_proper_decision_nononunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_decision_nononunitidentity) + ge_balance_negative_proper_decision_nononunitidentitysecondreal = (ge_second_rn_proper_decision_nononunitidentity) + ge_balance_positive_proper_decision_nononunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_decision_nononunitidentitysecondimaginary ge_balance_negative_proper_decision_nononunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_decision_nononunitidentitysecond) = 2 * (ge_balance_positive_proper_decision_nononunitidentitysecondimaginary) /\ (ge_balance_negative_proper_decision_nononunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_decision_nononunitidentitysecond) = 2 * ge_signed_half_proper_decision_nononunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentitysecondimaginary) = S ge_signed_half_proper_decision_nononunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_decision_nononunitidentity) + ge_balance_negative_proper_decision_nononunitidentitysecondimaginary = (ge_second_in_proper_decision_nononunitidentity) + ge_balance_positive_proper_decision_nononunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_decision_nononunitidentityoutput ge_representation_imaginary_code_proper_decision_nononunitidentityoutput. (((6) = ((ge_representation_real_code_proper_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_nononunitidentityoutput)) * S ((ge_representation_real_code_proper_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_nononunitidentityoutput)) + ((ge_representation_imaginary_code_proper_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_nononunitidentityoutput))) /\ ((exists ge_balance_positive_proper_decision_nononunitidentityoutputreal ge_balance_negative_proper_decision_nononunitidentityoutputreal. (((((ge_representation_real_code_proper_decision_nononunitidentityoutput) = 2 * (ge_balance_positive_proper_decision_nononunitidentityoutputreal) /\ (ge_balance_negative_proper_decision_nononunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentityoutputrealdecode. (((ge_representation_real_code_proper_decision_nononunitidentityoutput) = 2 * ge_signed_half_proper_decision_nononunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentityoutputreal) = S ge_signed_half_proper_decision_nononunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_decision_nononunitidentity) * (ge_second_rp_proper_decision_nononunitidentity))) + (((ge_first_rn_proper_decision_nononunitidentity) * (ge_second_rn_proper_decision_nononunitidentity))))) + (((((ge_first_ip_proper_decision_nononunitidentity) * (ge_second_in_proper_decision_nononunitidentity))) + (((ge_first_in_proper_decision_nononunitidentity) * (ge_second_ip_proper_decision_nononunitidentity))))))) + ge_balance_negative_proper_decision_nononunitidentityoutputreal = (((((((ge_first_rp_proper_decision_nononunitidentity) * (ge_second_rn_proper_decision_nononunitidentity))) + (((ge_first_rn_proper_decision_nononunitidentity) * (ge_second_rp_proper_decision_nononunitidentity))))) + (((((ge_first_ip_proper_decision_nononunitidentity) * (ge_second_ip_proper_decision_nononunitidentity))) + (((ge_first_in_proper_decision_nononunitidentity) * (ge_second_in_proper_decision_nononunitidentity))))))) + ge_balance_positive_proper_decision_nononunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_decision_nononunitidentityoutputimaginary ge_balance_negative_proper_decision_nononunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_decision_nononunitidentityoutput) = 2 * (ge_balance_positive_proper_decision_nononunitidentityoutputimaginary) /\ (ge_balance_negative_proper_decision_nononunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_decision_nononunitidentityoutput) = 2 * ge_signed_half_proper_decision_nononunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentityoutputimaginary) = S ge_signed_half_proper_decision_nononunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_decision_nononunitidentity) * (ge_second_ip_proper_decision_nononunitidentity))) + (((ge_first_rn_proper_decision_nononunitidentity) * (ge_second_in_proper_decision_nononunitidentity))))) + (((((ge_first_ip_proper_decision_nononunitidentity) * (ge_second_rp_proper_decision_nononunitidentity))) + (((ge_first_in_proper_decision_nononunitidentity) * (ge_second_rn_proper_decision_nononunitidentity))))))) + ge_balance_negative_proper_decision_nononunitidentityoutputimaginary = (((((((ge_first_rp_proper_decision_nononunitidentity) * (ge_second_in_proper_decision_nononunitidentity))) + (((ge_first_rn_proper_decision_nononunitidentity) * (ge_second_ip_proper_decision_nononunitidentity))))) + (((((ge_first_ip_proper_decision_nononunitidentity) * (ge_second_rn_proper_decision_nononunitidentity))) + (((ge_first_in_proper_decision_nononunitidentity) * (ge_second_rp_proper_decision_nononunitidentity))))))) + ge_balance_positive_proper_decision_nononunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_proper_decision_noquotient. (exists ge_first_rp_proper_decision_noquotientproduct ge_first_rn_proper_decision_noquotientproduct ge_first_ip_proper_decision_noquotientproduct ge_first_in_proper_decision_noquotientproduct ge_second_rp_proper_decision_noquotientproduct ge_second_rn_proper_decision_noquotientproduct ge_second_ip_proper_decision_noquotientproduct ge_second_in_proper_decision_noquotientproduct. ((exists ge_representation_real_code_proper_decision_noquotientproductfirst ge_representation_imaginary_code_proper_decision_noquotientproductfirst. (((d) = ((ge_representation_real_code_proper_decision_noquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_noquotientproductfirst)) * S ((ge_representation_real_code_proper_decision_noquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_noquotientproductfirst)) + ((ge_representation_imaginary_code_proper_decision_noquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_noquotientproductfirst))) /\ ((exists ge_balance_positive_proper_decision_noquotientproductfirstreal ge_balance_negative_proper_decision_noquotientproductfirstreal. (((((ge_representation_real_code_proper_decision_noquotientproductfirst) = 2 * (ge_balance_positive_proper_decision_noquotientproductfirstreal) /\ (ge_balance_negative_proper_decision_noquotientproductfirstreal) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductfirstrealdecode. (((ge_representation_real_code_proper_decision_noquotientproductfirst) = 2 * ge_signed_half_proper_decision_noquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductfirstreal) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductfirstreal) = S ge_signed_half_proper_decision_noquotientproductfirstrealdecode))) /\ ((ge_first_rp_proper_decision_noquotientproduct) + ge_balance_negative_proper_decision_noquotientproductfirstreal = (ge_first_rn_proper_decision_noquotientproduct) + ge_balance_positive_proper_decision_noquotientproductfirstreal))) /\ (exists ge_balance_positive_proper_decision_noquotientproductfirstimaginary ge_balance_negative_proper_decision_noquotientproductfirstimaginary. (((((ge_representation_imaginary_code_proper_decision_noquotientproductfirst) = 2 * (ge_balance_positive_proper_decision_noquotientproductfirstimaginary) /\ (ge_balance_negative_proper_decision_noquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_decision_noquotientproductfirst) = 2 * ge_signed_half_proper_decision_noquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductfirstimaginary) = S ge_signed_half_proper_decision_noquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_decision_noquotientproduct) + ge_balance_negative_proper_decision_noquotientproductfirstimaginary = (ge_first_in_proper_decision_noquotientproduct) + ge_balance_positive_proper_decision_noquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_decision_noquotientproductsecond ge_representation_imaginary_code_proper_decision_noquotientproductsecond. (((gr_quotient_proper_decision_noquotient) = ((ge_representation_real_code_proper_decision_noquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_noquotientproductsecond)) * S ((ge_representation_real_code_proper_decision_noquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_noquotientproductsecond)) + ((ge_representation_imaginary_code_proper_decision_noquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_noquotientproductsecond))) /\ ((exists ge_balance_positive_proper_decision_noquotientproductsecondreal ge_balance_negative_proper_decision_noquotientproductsecondreal. (((((ge_representation_real_code_proper_decision_noquotientproductsecond) = 2 * (ge_balance_positive_proper_decision_noquotientproductsecondreal) /\ (ge_balance_negative_proper_decision_noquotientproductsecondreal) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductsecondrealdecode. (((ge_representation_real_code_proper_decision_noquotientproductsecond) = 2 * ge_signed_half_proper_decision_noquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductsecondreal) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductsecondreal) = S ge_signed_half_proper_decision_noquotientproductsecondrealdecode))) /\ ((ge_second_rp_proper_decision_noquotientproduct) + ge_balance_negative_proper_decision_noquotientproductsecondreal = (ge_second_rn_proper_decision_noquotientproduct) + ge_balance_positive_proper_decision_noquotientproductsecondreal))) /\ (exists ge_balance_positive_proper_decision_noquotientproductsecondimaginary ge_balance_negative_proper_decision_noquotientproductsecondimaginary. (((((ge_representation_imaginary_code_proper_decision_noquotientproductsecond) = 2 * (ge_balance_positive_proper_decision_noquotientproductsecondimaginary) /\ (ge_balance_negative_proper_decision_noquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_decision_noquotientproductsecond) = 2 * ge_signed_half_proper_decision_noquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductsecondimaginary) = S ge_signed_half_proper_decision_noquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_decision_noquotientproduct) + ge_balance_negative_proper_decision_noquotientproductsecondimaginary = (ge_second_in_proper_decision_noquotientproduct) + ge_balance_positive_proper_decision_noquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_decision_noquotientproductoutput ge_representation_imaginary_code_proper_decision_noquotientproductoutput. (((z) = ((ge_representation_real_code_proper_decision_noquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_noquotientproductoutput)) * S ((ge_representation_real_code_proper_decision_noquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_noquotientproductoutput)) + ((ge_representation_imaginary_code_proper_decision_noquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_noquotientproductoutput))) /\ ((exists ge_balance_positive_proper_decision_noquotientproductoutputreal ge_balance_negative_proper_decision_noquotientproductoutputreal. (((((ge_representation_real_code_proper_decision_noquotientproductoutput) = 2 * (ge_balance_positive_proper_decision_noquotientproductoutputreal) /\ (ge_balance_negative_proper_decision_noquotientproductoutputreal) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductoutputrealdecode. (((ge_representation_real_code_proper_decision_noquotientproductoutput) = 2 * ge_signed_half_proper_decision_noquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductoutputreal) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductoutputreal) = S ge_signed_half_proper_decision_noquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_decision_noquotientproduct) * (ge_second_rp_proper_decision_noquotientproduct))) + (((ge_first_rn_proper_decision_noquotientproduct) * (ge_second_rn_proper_decision_noquotientproduct))))) + (((((ge_first_ip_proper_decision_noquotientproduct) * (ge_second_in_proper_decision_noquotientproduct))) + (((ge_first_in_proper_decision_noquotientproduct) * (ge_second_ip_proper_decision_noquotientproduct))))))) + ge_balance_negative_proper_decision_noquotientproductoutputreal = (((((((ge_first_rp_proper_decision_noquotientproduct) * (ge_second_rn_proper_decision_noquotientproduct))) + (((ge_first_rn_proper_decision_noquotientproduct) * (ge_second_rp_proper_decision_noquotientproduct))))) + (((((ge_first_ip_proper_decision_noquotientproduct) * (ge_second_ip_proper_decision_noquotientproduct))) + (((ge_first_in_proper_decision_noquotientproduct) * (ge_second_in_proper_decision_noquotientproduct))))))) + ge_balance_positive_proper_decision_noquotientproductoutputreal))) /\ (exists ge_balance_positive_proper_decision_noquotientproductoutputimaginary ge_balance_negative_proper_decision_noquotientproductoutputimaginary. (((((ge_representation_imaginary_code_proper_decision_noquotientproductoutput) = 2 * (ge_balance_positive_proper_decision_noquotientproductoutputimaginary) /\ (ge_balance_negative_proper_decision_noquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_decision_noquotientproductoutput) = 2 * ge_signed_half_proper_decision_noquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductoutputimaginary) = S ge_signed_half_proper_decision_noquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_decision_noquotientproduct) * (ge_second_ip_proper_decision_noquotientproduct))) + (((ge_first_rn_proper_decision_noquotientproduct) * (ge_second_in_proper_decision_noquotientproduct))))) + (((((ge_first_ip_proper_decision_noquotientproduct) * (ge_second_rp_proper_decision_noquotientproduct))) + (((ge_first_in_proper_decision_noquotientproduct) * (ge_second_rn_proper_decision_noquotientproduct))))))) + ge_balance_negative_proper_decision_noquotientproductoutputimaginary = (((((((ge_first_rp_proper_decision_noquotientproduct) * (ge_second_in_proper_decision_noquotientproduct))) + (((ge_first_rn_proper_decision_noquotientproduct) * (ge_second_ip_proper_decision_noquotientproduct))))) + (((((ge_first_ip_proper_decision_noquotientproduct) * (ge_second_rn_proper_decision_noquotientproduct))) + (((ge_first_in_proper_decision_noquotientproduct) * (ge_second_rp_proper_decision_noquotientproduct))))))) + ge_balance_positive_proper_decision_noquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_proper_decision_no. ((exists ge_norm_rp_proper_decision_nonorm ge_norm_rn_proper_decision_nonorm ge_norm_ip_proper_decision_nonorm ge_norm_in_proper_decision_nonorm. ((exists ge_representation_real_code_proper_decision_nonormrepresentation ge_representation_imaginary_code_proper_decision_nonormrepresentation. (((d) = ((ge_representation_real_code_proper_decision_nonormrepresentation) + (ge_representation_imaginary_code_proper_decision_nonormrepresentation)) * S ((ge_representation_real_code_proper_decision_nonormrepresentation) + (ge_representation_imaginary_code_proper_decision_nonormrepresentation)) + ((ge_representation_imaginary_code_proper_decision_nonormrepresentation) + (ge_representation_imaginary_code_proper_decision_nonormrepresentation))) /\ ((exists ge_balance_positive_proper_decision_nonormrepresentationreal ge_balance_negative_proper_decision_nonormrepresentationreal. (((((ge_representation_real_code_proper_decision_nonormrepresentation) = 2 * (ge_balance_positive_proper_decision_nonormrepresentationreal) /\ (ge_balance_negative_proper_decision_nonormrepresentationreal) = 0) \/ exists ge_signed_half_proper_decision_nonormrepresentationrealdecode. (((ge_representation_real_code_proper_decision_nonormrepresentation) = 2 * ge_signed_half_proper_decision_nonormrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_decision_nonormrepresentationreal) = 0) /\ (ge_balance_negative_proper_decision_nonormrepresentationreal) = S ge_signed_half_proper_decision_nonormrepresentationrealdecode))) /\ ((ge_norm_rp_proper_decision_nonorm) + ge_balance_negative_proper_decision_nonormrepresentationreal = (ge_norm_rn_proper_decision_nonorm) + ge_balance_positive_proper_decision_nonormrepresentationreal))) /\ (exists ge_balance_positive_proper_decision_nonormrepresentationimaginary ge_balance_negative_proper_decision_nonormrepresentationimaginary. (((((ge_representation_imaginary_code_proper_decision_nonormrepresentation) = 2 * (ge_balance_positive_proper_decision_nonormrepresentationimaginary) /\ (ge_balance_negative_proper_decision_nonormrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_decision_nonormrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_decision_nonormrepresentation) = 2 * ge_signed_half_proper_decision_nonormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_nonormrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_decision_nonormrepresentationimaginary) = S ge_signed_half_proper_decision_nonormrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_decision_nonorm) + ge_balance_negative_proper_decision_nonormrepresentationimaginary = (ge_norm_in_proper_decision_nonorm) + ge_balance_positive_proper_decision_nonormrepresentationimaginary)))))) /\ (exists ge_real_square_proper_decision_nonormsquare ge_imaginary_square_proper_decision_nonormsquare. ((((((ge_norm_rp_proper_decision_nonorm) * (ge_norm_rp_proper_decision_nonorm))) + (((ge_norm_rn_proper_decision_nonorm) * (ge_norm_rn_proper_decision_nonorm)))) = ((ge_real_square_proper_decision_nonormsquare) + (((((ge_norm_rp_proper_decision_nonorm) * (ge_norm_rn_proper_decision_nonorm))) + (((ge_norm_rn_proper_decision_nonorm) * (ge_norm_rp_proper_decision_nonorm))))))) /\ ((((((ge_norm_ip_proper_decision_nonorm) * (ge_norm_ip_proper_decision_nonorm))) + (((ge_norm_in_proper_decision_nonorm) * (ge_norm_in_proper_decision_nonorm)))) = ((ge_imaginary_square_proper_decision_nonormsquare) + (((((ge_norm_ip_proper_decision_nonorm) * (ge_norm_in_proper_decision_nonorm))) + (((ge_norm_in_proper_decision_nonorm) * (ge_norm_ip_proper_decision_nonorm))))))) /\ ((gr_proper_divisor_norm_proper_decision_no) = ge_real_square_proper_decision_nonormsquare + ge_imaginary_square_proper_decision_nonormsquare)))))) /\ (exists ge_gap_proper_decision_nostrict. ge_gap_proper_decision_nostrict + S (gr_proper_divisor_norm_proper_decision_no) = (N)))))))