gaussian_proper_norm_divisor_split

Exact expanded first-order arithmetic statement

forall d z N. (((~(exists gr_inverse_proper_split_inputnonunit. (exists ge_first_rp_proper_split_inputnonunitidentity ge_first_rn_proper_split_inputnonunitidentity ge_first_ip_proper_split_inputnonunitidentity ge_first_in_proper_split_inputnonunitidentity ge_second_rp_proper_split_inputnonunitidentity ge_second_rn_proper_split_inputnonunitidentity ge_second_ip_proper_split_inputnonunitidentity ge_second_in_proper_split_inputnonunitidentity. ((exists ge_representation_real_code_proper_split_inputnonunitidentityfirst ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst. (((d) = ((ge_representation_real_code_proper_split_inputnonunitidentityfirst) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst)) * S ((ge_representation_real_code_proper_split_inputnonunitidentityfirst) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_split_inputnonunitidentityfirstreal ge_balance_negative_proper_split_inputnonunitidentityfirstreal. (((((ge_representation_real_code_proper_split_inputnonunitidentityfirst) = 2 * (ge_balance_positive_proper_split_inputnonunitidentityfirstreal) /\ (ge_balance_negative_proper_split_inputnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_split_inputnonunitidentityfirst) = 2 * ge_signed_half_proper_split_inputnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentityfirstreal) = S ge_signed_half_proper_split_inputnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_split_inputnonunitidentity) + ge_balance_negative_proper_split_inputnonunitidentityfirstreal = (ge_first_rn_proper_split_inputnonunitidentity) + ge_balance_positive_proper_split_inputnonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_split_inputnonunitidentityfirstimaginary ge_balance_negative_proper_split_inputnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst) = 2 * (ge_balance_positive_proper_split_inputnonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_split_inputnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst) = 2 * ge_signed_half_proper_split_inputnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentityfirstimaginary) = S ge_signed_half_proper_split_inputnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_split_inputnonunitidentity) + ge_balance_negative_proper_split_inputnonunitidentityfirstimaginary = (ge_first_in_proper_split_inputnonunitidentity) + ge_balance_positive_proper_split_inputnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_split_inputnonunitidentitysecond ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond. (((gr_inverse_proper_split_inputnonunit) = ((ge_representation_real_code_proper_split_inputnonunitidentitysecond) + (ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond)) * S ((ge_representation_real_code_proper_split_inputnonunitidentitysecond) + (ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond) + (ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_split_inputnonunitidentitysecondreal ge_balance_negative_proper_split_inputnonunitidentitysecondreal. (((((ge_representation_real_code_proper_split_inputnonunitidentitysecond) = 2 * (ge_balance_positive_proper_split_inputnonunitidentitysecondreal) /\ (ge_balance_negative_proper_split_inputnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_split_inputnonunitidentitysecond) = 2 * ge_signed_half_proper_split_inputnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentitysecondreal) = S ge_signed_half_proper_split_inputnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_split_inputnonunitidentity) + ge_balance_negative_proper_split_inputnonunitidentitysecondreal = (ge_second_rn_proper_split_inputnonunitidentity) + ge_balance_positive_proper_split_inputnonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_split_inputnonunitidentitysecondimaginary ge_balance_negative_proper_split_inputnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond) = 2 * (ge_balance_positive_proper_split_inputnonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_split_inputnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond) = 2 * ge_signed_half_proper_split_inputnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentitysecondimaginary) = S ge_signed_half_proper_split_inputnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_split_inputnonunitidentity) + ge_balance_negative_proper_split_inputnonunitidentitysecondimaginary = (ge_second_in_proper_split_inputnonunitidentity) + ge_balance_positive_proper_split_inputnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_split_inputnonunitidentityoutput ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_split_inputnonunitidentityoutput) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput)) * S ((ge_representation_real_code_proper_split_inputnonunitidentityoutput) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_split_inputnonunitidentityoutputreal ge_balance_negative_proper_split_inputnonunitidentityoutputreal. (((((ge_representation_real_code_proper_split_inputnonunitidentityoutput) = 2 * (ge_balance_positive_proper_split_inputnonunitidentityoutputreal) /\ (ge_balance_negative_proper_split_inputnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_split_inputnonunitidentityoutput) = 2 * ge_signed_half_proper_split_inputnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentityoutputreal) = S ge_signed_half_proper_split_inputnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_split_inputnonunitidentity) * (ge_second_rp_proper_split_inputnonunitidentity))) + (((ge_first_rn_proper_split_inputnonunitidentity) * (ge_second_rn_proper_split_inputnonunitidentity))))) + (((((ge_first_ip_proper_split_inputnonunitidentity) * (ge_second_in_proper_split_inputnonunitidentity))) + (((ge_first_in_proper_split_inputnonunitidentity) * (ge_second_ip_proper_split_inputnonunitidentity))))))) + ge_balance_negative_proper_split_inputnonunitidentityoutputreal = (((((((ge_first_rp_proper_split_inputnonunitidentity) * (ge_second_rn_proper_split_inputnonunitidentity))) + (((ge_first_rn_proper_split_inputnonunitidentity) * (ge_second_rp_proper_split_inputnonunitidentity))))) + (((((ge_first_ip_proper_split_inputnonunitidentity) * (ge_second_ip_proper_split_inputnonunitidentity))) + (((ge_first_in_proper_split_inputnonunitidentity) * (ge_second_in_proper_split_inputnonunitidentity))))))) + ge_balance_positive_proper_split_inputnonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_split_inputnonunitidentityoutputimaginary ge_balance_negative_proper_split_inputnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput) = 2 * (ge_balance_positive_proper_split_inputnonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_split_inputnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput) = 2 * ge_signed_half_proper_split_inputnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentityoutputimaginary) = S ge_signed_half_proper_split_inputnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_split_inputnonunitidentity) * (ge_second_ip_proper_split_inputnonunitidentity))) + (((ge_first_rn_proper_split_inputnonunitidentity) * (ge_second_in_proper_split_inputnonunitidentity))))) + (((((ge_first_ip_proper_split_inputnonunitidentity) * (ge_second_rp_proper_split_inputnonunitidentity))) + (((ge_first_in_proper_split_inputnonunitidentity) * (ge_second_rn_proper_split_inputnonunitidentity))))))) + ge_balance_negative_proper_split_inputnonunitidentityoutputimaginary = (((((((ge_first_rp_proper_split_inputnonunitidentity) * (ge_second_in_proper_split_inputnonunitidentity))) + (((ge_first_rn_proper_split_inputnonunitidentity) * (ge_second_ip_proper_split_inputnonunitidentity))))) + (((((ge_first_ip_proper_split_inputnonunitidentity) * (ge_second_rn_proper_split_inputnonunitidentity))) + (((ge_first_in_proper_split_inputnonunitidentity) * (ge_second_rp_proper_split_inputnonunitidentity))))))) + ge_balance_positive_proper_split_inputnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_proper_split_inputquotient. (exists ge_first_rp_proper_split_inputquotientproduct ge_first_rn_proper_split_inputquotientproduct ge_first_ip_proper_split_inputquotientproduct ge_first_in_proper_split_inputquotientproduct ge_second_rp_proper_split_inputquotientproduct ge_second_rn_proper_split_inputquotientproduct ge_second_ip_proper_split_inputquotientproduct ge_second_in_proper_split_inputquotientproduct. ((exists ge_representation_real_code_proper_split_inputquotientproductfirst ge_representation_imaginary_code_proper_split_inputquotientproductfirst. (((d) = ((ge_representation_real_code_proper_split_inputquotientproductfirst) + (ge_representation_imaginary_code_proper_split_inputquotientproductfirst)) * S ((ge_representation_real_code_proper_split_inputquotientproductfirst) + (ge_representation_imaginary_code_proper_split_inputquotientproductfirst)) + ((ge_representation_imaginary_code_proper_split_inputquotientproductfirst) + (ge_representation_imaginary_code_proper_split_inputquotientproductfirst))) /\ ((exists ge_balance_positive_proper_split_inputquotientproductfirstreal ge_balance_negative_proper_split_inputquotientproductfirstreal. (((((ge_representation_real_code_proper_split_inputquotientproductfirst) = 2 * (ge_balance_positive_proper_split_inputquotientproductfirstreal) /\ (ge_balance_negative_proper_split_inputquotientproductfirstreal) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductfirstrealdecode. (((ge_representation_real_code_proper_split_inputquotientproductfirst) = 2 * ge_signed_half_proper_split_inputquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductfirstreal) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductfirstreal) = S ge_signed_half_proper_split_inputquotientproductfirstrealdecode))) /\ ((ge_first_rp_proper_split_inputquotientproduct) + ge_balance_negative_proper_split_inputquotientproductfirstreal = (ge_first_rn_proper_split_inputquotientproduct) + ge_balance_positive_proper_split_inputquotientproductfirstreal))) /\ (exists ge_balance_positive_proper_split_inputquotientproductfirstimaginary ge_balance_negative_proper_split_inputquotientproductfirstimaginary. (((((ge_representation_imaginary_code_proper_split_inputquotientproductfirst) = 2 * (ge_balance_positive_proper_split_inputquotientproductfirstimaginary) /\ (ge_balance_negative_proper_split_inputquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputquotientproductfirst) = 2 * ge_signed_half_proper_split_inputquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductfirstimaginary) = S ge_signed_half_proper_split_inputquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_split_inputquotientproduct) + ge_balance_negative_proper_split_inputquotientproductfirstimaginary = (ge_first_in_proper_split_inputquotientproduct) + ge_balance_positive_proper_split_inputquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_split_inputquotientproductsecond ge_representation_imaginary_code_proper_split_inputquotientproductsecond. (((gr_quotient_proper_split_inputquotient) = ((ge_representation_real_code_proper_split_inputquotientproductsecond) + (ge_representation_imaginary_code_proper_split_inputquotientproductsecond)) * S ((ge_representation_real_code_proper_split_inputquotientproductsecond) + (ge_representation_imaginary_code_proper_split_inputquotientproductsecond)) + ((ge_representation_imaginary_code_proper_split_inputquotientproductsecond) + (ge_representation_imaginary_code_proper_split_inputquotientproductsecond))) /\ ((exists ge_balance_positive_proper_split_inputquotientproductsecondreal ge_balance_negative_proper_split_inputquotientproductsecondreal. (((((ge_representation_real_code_proper_split_inputquotientproductsecond) = 2 * (ge_balance_positive_proper_split_inputquotientproductsecondreal) /\ (ge_balance_negative_proper_split_inputquotientproductsecondreal) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductsecondrealdecode. (((ge_representation_real_code_proper_split_inputquotientproductsecond) = 2 * ge_signed_half_proper_split_inputquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductsecondreal) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductsecondreal) = S ge_signed_half_proper_split_inputquotientproductsecondrealdecode))) /\ ((ge_second_rp_proper_split_inputquotientproduct) + ge_balance_negative_proper_split_inputquotientproductsecondreal = (ge_second_rn_proper_split_inputquotientproduct) + ge_balance_positive_proper_split_inputquotientproductsecondreal))) /\ (exists ge_balance_positive_proper_split_inputquotientproductsecondimaginary ge_balance_negative_proper_split_inputquotientproductsecondimaginary. (((((ge_representation_imaginary_code_proper_split_inputquotientproductsecond) = 2 * (ge_balance_positive_proper_split_inputquotientproductsecondimaginary) /\ (ge_balance_negative_proper_split_inputquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputquotientproductsecond) = 2 * ge_signed_half_proper_split_inputquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductsecondimaginary) = S ge_signed_half_proper_split_inputquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_split_inputquotientproduct) + ge_balance_negative_proper_split_inputquotientproductsecondimaginary = (ge_second_in_proper_split_inputquotientproduct) + ge_balance_positive_proper_split_inputquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_split_inputquotientproductoutput ge_representation_imaginary_code_proper_split_inputquotientproductoutput. (((z) = ((ge_representation_real_code_proper_split_inputquotientproductoutput) + (ge_representation_imaginary_code_proper_split_inputquotientproductoutput)) * S ((ge_representation_real_code_proper_split_inputquotientproductoutput) + (ge_representation_imaginary_code_proper_split_inputquotientproductoutput)) + ((ge_representation_imaginary_code_proper_split_inputquotientproductoutput) + (ge_representation_imaginary_code_proper_split_inputquotientproductoutput))) /\ ((exists ge_balance_positive_proper_split_inputquotientproductoutputreal ge_balance_negative_proper_split_inputquotientproductoutputreal. (((((ge_representation_real_code_proper_split_inputquotientproductoutput) = 2 * (ge_balance_positive_proper_split_inputquotientproductoutputreal) /\ (ge_balance_negative_proper_split_inputquotientproductoutputreal) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductoutputrealdecode. (((ge_representation_real_code_proper_split_inputquotientproductoutput) = 2 * ge_signed_half_proper_split_inputquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductoutputreal) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductoutputreal) = S ge_signed_half_proper_split_inputquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_split_inputquotientproduct) * (ge_second_rp_proper_split_inputquotientproduct))) + (((ge_first_rn_proper_split_inputquotientproduct) * (ge_second_rn_proper_split_inputquotientproduct))))) + (((((ge_first_ip_proper_split_inputquotientproduct) * (ge_second_in_proper_split_inputquotientproduct))) + (((ge_first_in_proper_split_inputquotientproduct) * (ge_second_ip_proper_split_inputquotientproduct))))))) + ge_balance_negative_proper_split_inputquotientproductoutputreal = (((((((ge_first_rp_proper_split_inputquotientproduct) * (ge_second_rn_proper_split_inputquotientproduct))) + (((ge_first_rn_proper_split_inputquotientproduct) * (ge_second_rp_proper_split_inputquotientproduct))))) + (((((ge_first_ip_proper_split_inputquotientproduct) * (ge_second_ip_proper_split_inputquotientproduct))) + (((ge_first_in_proper_split_inputquotientproduct) * (ge_second_in_proper_split_inputquotientproduct))))))) + ge_balance_positive_proper_split_inputquotientproductoutputreal))) /\ (exists ge_balance_positive_proper_split_inputquotientproductoutputimaginary ge_balance_negative_proper_split_inputquotientproductoutputimaginary. (((((ge_representation_imaginary_code_proper_split_inputquotientproductoutput) = 2 * (ge_balance_positive_proper_split_inputquotientproductoutputimaginary) /\ (ge_balance_negative_proper_split_inputquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputquotientproductoutput) = 2 * ge_signed_half_proper_split_inputquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductoutputimaginary) = S ge_signed_half_proper_split_inputquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_split_inputquotientproduct) * (ge_second_ip_proper_split_inputquotientproduct))) + (((ge_first_rn_proper_split_inputquotientproduct) * (ge_second_in_proper_split_inputquotientproduct))))) + (((((ge_first_ip_proper_split_inputquotientproduct) * (ge_second_rp_proper_split_inputquotientproduct))) + (((ge_first_in_proper_split_inputquotientproduct) * (ge_second_rn_proper_split_inputquotientproduct))))))) + ge_balance_negative_proper_split_inputquotientproductoutputimaginary = (((((((ge_first_rp_proper_split_inputquotientproduct) * (ge_second_in_proper_split_inputquotientproduct))) + (((ge_first_rn_proper_split_inputquotientproduct) * (ge_second_ip_proper_split_inputquotientproduct))))) + (((((ge_first_ip_proper_split_inputquotientproduct) * (ge_second_rn_proper_split_inputquotientproduct))) + (((ge_first_in_proper_split_inputquotientproduct) * (ge_second_rp_proper_split_inputquotientproduct))))))) + ge_balance_positive_proper_split_inputquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_proper_split_input. ((exists ge_norm_rp_proper_split_inputnorm ge_norm_rn_proper_split_inputnorm ge_norm_ip_proper_split_inputnorm ge_norm_in_proper_split_inputnorm. ((exists ge_representation_real_code_proper_split_inputnormrepresentation ge_representation_imaginary_code_proper_split_inputnormrepresentation. (((d) = ((ge_representation_real_code_proper_split_inputnormrepresentation) + (ge_representation_imaginary_code_proper_split_inputnormrepresentation)) * S ((ge_representation_real_code_proper_split_inputnormrepresentation) + (ge_representation_imaginary_code_proper_split_inputnormrepresentation)) + ((ge_representation_imaginary_code_proper_split_inputnormrepresentation) + (ge_representation_imaginary_code_proper_split_inputnormrepresentation))) /\ ((exists ge_balance_positive_proper_split_inputnormrepresentationreal ge_balance_negative_proper_split_inputnormrepresentationreal. (((((ge_representation_real_code_proper_split_inputnormrepresentation) = 2 * (ge_balance_positive_proper_split_inputnormrepresentationreal) /\ (ge_balance_negative_proper_split_inputnormrepresentationreal) = 0) \/ exists ge_signed_half_proper_split_inputnormrepresentationrealdecode. (((ge_representation_real_code_proper_split_inputnormrepresentation) = 2 * ge_signed_half_proper_split_inputnormrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_split_inputnormrepresentationreal) = 0) /\ (ge_balance_negative_proper_split_inputnormrepresentationreal) = S ge_signed_half_proper_split_inputnormrepresentationrealdecode))) /\ ((ge_norm_rp_proper_split_inputnorm) + ge_balance_negative_proper_split_inputnormrepresentationreal = (ge_norm_rn_proper_split_inputnorm) + ge_balance_positive_proper_split_inputnormrepresentationreal))) /\ (exists ge_balance_positive_proper_split_inputnormrepresentationimaginary ge_balance_negative_proper_split_inputnormrepresentationimaginary. (((((ge_representation_imaginary_code_proper_split_inputnormrepresentation) = 2 * (ge_balance_positive_proper_split_inputnormrepresentationimaginary) /\ (ge_balance_negative_proper_split_inputnormrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_split_inputnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputnormrepresentation) = 2 * ge_signed_half_proper_split_inputnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputnormrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_split_inputnormrepresentationimaginary) = S ge_signed_half_proper_split_inputnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_split_inputnorm) + ge_balance_negative_proper_split_inputnormrepresentationimaginary = (ge_norm_in_proper_split_inputnorm) + ge_balance_positive_proper_split_inputnormrepresentationimaginary)))))) /\ (exists ge_real_square_proper_split_inputnormsquare ge_imaginary_square_proper_split_inputnormsquare. ((((((ge_norm_rp_proper_split_inputnorm) * (ge_norm_rp_proper_split_inputnorm))) + (((ge_norm_rn_proper_split_inputnorm) * (ge_norm_rn_proper_split_inputnorm)))) = ((ge_real_square_proper_split_inputnormsquare) + (((((ge_norm_rp_proper_split_inputnorm) * (ge_norm_rn_proper_split_inputnorm))) + (((ge_norm_rn_proper_split_inputnorm) * (ge_norm_rp_proper_split_inputnorm))))))) /\ ((((((ge_norm_ip_proper_split_inputnorm) * (ge_norm_ip_proper_split_inputnorm))) + (((ge_norm_in_proper_split_inputnorm) * (ge_norm_in_proper_split_inputnorm)))) = ((ge_imaginary_square_proper_split_inputnormsquare) + (((((ge_norm_ip_proper_split_inputnorm) * (ge_norm_in_proper_split_inputnorm))) + (((ge_norm_in_proper_split_inputnorm) * (ge_norm_ip_proper_split_inputnorm))))))) /\ ((gr_proper_divisor_norm_proper_split_input) = ge_real_square_proper_split_inputnormsquare + ge_imaginary_square_proper_split_inputnormsquare)))))) /\ (exists ge_gap_proper_split_inputstrict. ge_gap_proper_split_inputstrict + S (gr_proper_divisor_norm_proper_split_input) = (N))))))) -> (exists ge_norm_rp_proper_split_norm ge_norm_rn_proper_split_norm ge_norm_ip_proper_split_norm ge_norm_in_proper_split_norm. ((exists ge_representation_real_code_proper_split_normrepresentation ge_representation_imaginary_code_proper_split_normrepresentation. (((z) = ((ge_representation_real_code_proper_split_normrepresentation) + (ge_representation_imaginary_code_proper_split_normrepresentation)) * S ((ge_representation_real_code_proper_split_normrepresentation) + (ge_representation_imaginary_code_proper_split_normrepresentation)) + ((ge_representation_imaginary_code_proper_split_normrepresentation) + (ge_representation_imaginary_code_proper_split_normrepresentation))) /\ ((exists ge_balance_positive_proper_split_normrepresentationreal ge_balance_negative_proper_split_normrepresentationreal. (((((ge_representation_real_code_proper_split_normrepresentation) = 2 * (ge_balance_positive_proper_split_normrepresentationreal) /\ (ge_balance_negative_proper_split_normrepresentationreal) = 0) \/ exists ge_signed_half_proper_split_normrepresentationrealdecode. (((ge_representation_real_code_proper_split_normrepresentation) = 2 * ge_signed_half_proper_split_normrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_split_normrepresentationreal) = 0) /\ (ge_balance_negative_proper_split_normrepresentationreal) = S ge_signed_half_proper_split_normrepresentationrealdecode))) /\ ((ge_norm_rp_proper_split_norm) + ge_balance_negative_proper_split_normrepresentationreal = (ge_norm_rn_proper_split_norm) + ge_balance_positive_proper_split_normrepresentationreal))) /\ (exists ge_balance_positive_proper_split_normrepresentationimaginary ge_balance_negative_proper_split_normrepresentationimaginary. (((((ge_representation_imaginary_code_proper_split_normrepresentation) = 2 * (ge_balance_positive_proper_split_normrepresentationimaginary) /\ (ge_balance_negative_proper_split_normrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_split_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_split_normrepresentation) = 2 * ge_signed_half_proper_split_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_split_normrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_split_normrepresentationimaginary) = S ge_signed_half_proper_split_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_split_norm) + ge_balance_negative_proper_split_normrepresentationimaginary = (ge_norm_in_proper_split_norm) + ge_balance_positive_proper_split_normrepresentationimaginary)))))) /\ (exists ge_real_square_proper_split_normsquare ge_imaginary_square_proper_split_normsquare. ((((((ge_norm_rp_proper_split_norm) * (ge_norm_rp_proper_split_norm))) + (((ge_norm_rn_proper_split_norm) * (ge_norm_rn_proper_split_norm)))) = ((ge_real_square_proper_split_normsquare) + (((((ge_norm_rp_proper_split_norm) * (ge_norm_rn_proper_split_norm))) + (((ge_norm_rn_proper_split_norm) * (ge_norm_rp_proper_split_norm))))))) /\ ((((((ge_norm_ip_proper_split_norm) * (ge_norm_ip_proper_split_norm))) + (((ge_norm_in_proper_split_norm) * (ge_norm_in_proper_split_norm)))) = ((ge_imaginary_square_proper_split_normsquare) + (((((ge_norm_ip_proper_split_norm) * (ge_norm_in_proper_split_norm))) + (((ge_norm_in_proper_split_norm) * (ge_norm_ip_proper_split_norm))))))) /\ ((N) = ge_real_square_proper_split_normsquare + ge_imaginary_square_proper_split_normsquare)))))) -> ~(z=0) -> (exists q D Q. (((exists ge_first_rp_proper_constructed_splitproduct ge_first_rn_proper_constructed_splitproduct ge_first_ip_proper_constructed_splitproduct ge_first_in_proper_constructed_splitproduct ge_second_rp_proper_constructed_splitproduct ge_second_rn_proper_constructed_splitproduct ge_second_ip_proper_constructed_splitproduct ge_second_in_proper_constructed_splitproduct. ((exists ge_representation_real_code_proper_constructed_splitproductfirst ge_representation_imaginary_code_proper_constructed_splitproductfirst. (((d) = ((ge_representation_real_code_proper_constructed_splitproductfirst) + (ge_representation_imaginary_code_proper_constructed_splitproductfirst)) * S ((ge_representation_real_code_proper_constructed_splitproductfirst) + (ge_representation_imaginary_code_proper_constructed_splitproductfirst)) + ((ge_representation_imaginary_code_proper_constructed_splitproductfirst) + (ge_representation_imaginary_code_proper_constructed_splitproductfirst))) /\ ((exists ge_balance_positive_proper_constructed_splitproductfirstreal ge_balance_negative_proper_constructed_splitproductfirstreal. (((((ge_representation_real_code_proper_constructed_splitproductfirst) = 2 * (ge_balance_positive_proper_constructed_splitproductfirstreal) /\ (ge_balance_negative_proper_constructed_splitproductfirstreal) = 0) \/ exists ge_signed_half_proper_constructed_splitproductfirstrealdecode. (((ge_representation_real_code_proper_constructed_splitproductfirst) = 2 * ge_signed_half_proper_constructed_splitproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductfirstreal) = 0) /\ (ge_balance_negative_proper_constructed_splitproductfirstreal) = S ge_signed_half_proper_constructed_splitproductfirstrealdecode))) /\ ((ge_first_rp_proper_constructed_splitproduct) + ge_balance_negative_proper_constructed_splitproductfirstreal = (ge_first_rn_proper_constructed_splitproduct) + ge_balance_positive_proper_constructed_splitproductfirstreal))) /\ (exists ge_balance_positive_proper_constructed_splitproductfirstimaginary ge_balance_negative_proper_constructed_splitproductfirstimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitproductfirst) = 2 * (ge_balance_positive_proper_constructed_splitproductfirstimaginary) /\ (ge_balance_negative_proper_constructed_splitproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitproductfirst) = 2 * ge_signed_half_proper_constructed_splitproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitproductfirstimaginary) = S ge_signed_half_proper_constructed_splitproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_constructed_splitproduct) + ge_balance_negative_proper_constructed_splitproductfirstimaginary = (ge_first_in_proper_constructed_splitproduct) + ge_balance_positive_proper_constructed_splitproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_constructed_splitproductsecond ge_representation_imaginary_code_proper_constructed_splitproductsecond. (((q) = ((ge_representation_real_code_proper_constructed_splitproductsecond) + (ge_representation_imaginary_code_proper_constructed_splitproductsecond)) * S ((ge_representation_real_code_proper_constructed_splitproductsecond) + (ge_representation_imaginary_code_proper_constructed_splitproductsecond)) + ((ge_representation_imaginary_code_proper_constructed_splitproductsecond) + (ge_representation_imaginary_code_proper_constructed_splitproductsecond))) /\ ((exists ge_balance_positive_proper_constructed_splitproductsecondreal ge_balance_negative_proper_constructed_splitproductsecondreal. (((((ge_representation_real_code_proper_constructed_splitproductsecond) = 2 * (ge_balance_positive_proper_constructed_splitproductsecondreal) /\ (ge_balance_negative_proper_constructed_splitproductsecondreal) = 0) \/ exists ge_signed_half_proper_constructed_splitproductsecondrealdecode. (((ge_representation_real_code_proper_constructed_splitproductsecond) = 2 * ge_signed_half_proper_constructed_splitproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductsecondreal) = 0) /\ (ge_balance_negative_proper_constructed_splitproductsecondreal) = S ge_signed_half_proper_constructed_splitproductsecondrealdecode))) /\ ((ge_second_rp_proper_constructed_splitproduct) + ge_balance_negative_proper_constructed_splitproductsecondreal = (ge_second_rn_proper_constructed_splitproduct) + ge_balance_positive_proper_constructed_splitproductsecondreal))) /\ (exists ge_balance_positive_proper_constructed_splitproductsecondimaginary ge_balance_negative_proper_constructed_splitproductsecondimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitproductsecond) = 2 * (ge_balance_positive_proper_constructed_splitproductsecondimaginary) /\ (ge_balance_negative_proper_constructed_splitproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitproductsecond) = 2 * ge_signed_half_proper_constructed_splitproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitproductsecondimaginary) = S ge_signed_half_proper_constructed_splitproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_constructed_splitproduct) + ge_balance_negative_proper_constructed_splitproductsecondimaginary = (ge_second_in_proper_constructed_splitproduct) + ge_balance_positive_proper_constructed_splitproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_constructed_splitproductoutput ge_representation_imaginary_code_proper_constructed_splitproductoutput. (((z) = ((ge_representation_real_code_proper_constructed_splitproductoutput) + (ge_representation_imaginary_code_proper_constructed_splitproductoutput)) * S ((ge_representation_real_code_proper_constructed_splitproductoutput) + (ge_representation_imaginary_code_proper_constructed_splitproductoutput)) + ((ge_representation_imaginary_code_proper_constructed_splitproductoutput) + (ge_representation_imaginary_code_proper_constructed_splitproductoutput))) /\ ((exists ge_balance_positive_proper_constructed_splitproductoutputreal ge_balance_negative_proper_constructed_splitproductoutputreal. (((((ge_representation_real_code_proper_constructed_splitproductoutput) = 2 * (ge_balance_positive_proper_constructed_splitproductoutputreal) /\ (ge_balance_negative_proper_constructed_splitproductoutputreal) = 0) \/ exists ge_signed_half_proper_constructed_splitproductoutputrealdecode. (((ge_representation_real_code_proper_constructed_splitproductoutput) = 2 * ge_signed_half_proper_constructed_splitproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductoutputreal) = 0) /\ (ge_balance_negative_proper_constructed_splitproductoutputreal) = S ge_signed_half_proper_constructed_splitproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_constructed_splitproduct) * (ge_second_rp_proper_constructed_splitproduct))) + (((ge_first_rn_proper_constructed_splitproduct) * (ge_second_rn_proper_constructed_splitproduct))))) + (((((ge_first_ip_proper_constructed_splitproduct) * (ge_second_in_proper_constructed_splitproduct))) + (((ge_first_in_proper_constructed_splitproduct) * (ge_second_ip_proper_constructed_splitproduct))))))) + ge_balance_negative_proper_constructed_splitproductoutputreal = (((((((ge_first_rp_proper_constructed_splitproduct) * (ge_second_rn_proper_constructed_splitproduct))) + (((ge_first_rn_proper_constructed_splitproduct) * (ge_second_rp_proper_constructed_splitproduct))))) + (((((ge_first_ip_proper_constructed_splitproduct) * (ge_second_ip_proper_constructed_splitproduct))) + (((ge_first_in_proper_constructed_splitproduct) * (ge_second_in_proper_constructed_splitproduct))))))) + ge_balance_positive_proper_constructed_splitproductoutputreal))) /\ (exists ge_balance_positive_proper_constructed_splitproductoutputimaginary ge_balance_negative_proper_constructed_splitproductoutputimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitproductoutput) = 2 * (ge_balance_positive_proper_constructed_splitproductoutputimaginary) /\ (ge_balance_negative_proper_constructed_splitproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitproductoutput) = 2 * ge_signed_half_proper_constructed_splitproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitproductoutputimaginary) = S ge_signed_half_proper_constructed_splitproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_constructed_splitproduct) * (ge_second_ip_proper_constructed_splitproduct))) + (((ge_first_rn_proper_constructed_splitproduct) * (ge_second_in_proper_constructed_splitproduct))))) + (((((ge_first_ip_proper_constructed_splitproduct) * (ge_second_rp_proper_constructed_splitproduct))) + (((ge_first_in_proper_constructed_splitproduct) * (ge_second_rn_proper_constructed_splitproduct))))))) + ge_balance_negative_proper_constructed_splitproductoutputimaginary = (((((((ge_first_rp_proper_constructed_splitproduct) * (ge_second_in_proper_constructed_splitproduct))) + (((ge_first_rn_proper_constructed_splitproduct) * (ge_second_ip_proper_constructed_splitproduct))))) + (((((ge_first_ip_proper_constructed_splitproduct) * (ge_second_rn_proper_constructed_splitproduct))) + (((ge_first_in_proper_constructed_splitproduct) * (ge_second_rp_proper_constructed_splitproduct))))))) + ge_balance_positive_proper_constructed_splitproductoutputimaginary))))))))) /\ ((exists ge_norm_rp_proper_constructed_splitfirst_norm ge_norm_rn_proper_constructed_splitfirst_norm ge_norm_ip_proper_constructed_splitfirst_norm ge_norm_in_proper_constructed_splitfirst_norm. ((exists ge_representation_real_code_proper_constructed_splitfirst_normrepresentation ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation. (((d) = ((ge_representation_real_code_proper_constructed_splitfirst_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation)) * S ((ge_representation_real_code_proper_constructed_splitfirst_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation)) + ((ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation))) /\ ((exists ge_balance_positive_proper_constructed_splitfirst_normrepresentationreal ge_balance_negative_proper_constructed_splitfirst_normrepresentationreal. (((((ge_representation_real_code_proper_constructed_splitfirst_normrepresentation) = 2 * (ge_balance_positive_proper_constructed_splitfirst_normrepresentationreal) /\ (ge_balance_negative_proper_constructed_splitfirst_normrepresentationreal) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_normrepresentationrealdecode. (((ge_representation_real_code_proper_constructed_splitfirst_normrepresentation) = 2 * ge_signed_half_proper_constructed_splitfirst_normrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_normrepresentationreal) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_normrepresentationreal) = S ge_signed_half_proper_constructed_splitfirst_normrepresentationrealdecode))) /\ ((ge_norm_rp_proper_constructed_splitfirst_norm) + ge_balance_negative_proper_constructed_splitfirst_normrepresentationreal = (ge_norm_rn_proper_constructed_splitfirst_norm) + ge_balance_positive_proper_constructed_splitfirst_normrepresentationreal))) /\ (exists ge_balance_positive_proper_constructed_splitfirst_normrepresentationimaginary ge_balance_negative_proper_constructed_splitfirst_normrepresentationimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation) = 2 * (ge_balance_positive_proper_constructed_splitfirst_normrepresentationimaginary) /\ (ge_balance_negative_proper_constructed_splitfirst_normrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation) = 2 * ge_signed_half_proper_constructed_splitfirst_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_normrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_normrepresentationimaginary) = S ge_signed_half_proper_constructed_splitfirst_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_constructed_splitfirst_norm) + ge_balance_negative_proper_constructed_splitfirst_normrepresentationimaginary = (ge_norm_in_proper_constructed_splitfirst_norm) + ge_balance_positive_proper_constructed_splitfirst_normrepresentationimaginary)))))) /\ (exists ge_real_square_proper_constructed_splitfirst_normsquare ge_imaginary_square_proper_constructed_splitfirst_normsquare. ((((((ge_norm_rp_proper_constructed_splitfirst_norm) * (ge_norm_rp_proper_constructed_splitfirst_norm))) + (((ge_norm_rn_proper_constructed_splitfirst_norm) * (ge_norm_rn_proper_constructed_splitfirst_norm)))) = ((ge_real_square_proper_constructed_splitfirst_normsquare) + (((((ge_norm_rp_proper_constructed_splitfirst_norm) * (ge_norm_rn_proper_constructed_splitfirst_norm))) + (((ge_norm_rn_proper_constructed_splitfirst_norm) * (ge_norm_rp_proper_constructed_splitfirst_norm))))))) /\ ((((((ge_norm_ip_proper_constructed_splitfirst_norm) * (ge_norm_ip_proper_constructed_splitfirst_norm))) + (((ge_norm_in_proper_constructed_splitfirst_norm) * (ge_norm_in_proper_constructed_splitfirst_norm)))) = ((ge_imaginary_square_proper_constructed_splitfirst_normsquare) + (((((ge_norm_ip_proper_constructed_splitfirst_norm) * (ge_norm_in_proper_constructed_splitfirst_norm))) + (((ge_norm_in_proper_constructed_splitfirst_norm) * (ge_norm_ip_proper_constructed_splitfirst_norm))))))) /\ ((D) = ge_real_square_proper_constructed_splitfirst_normsquare + ge_imaginary_square_proper_constructed_splitfirst_normsquare)))))) /\ ((exists ge_norm_rp_proper_constructed_splitsecond_norm ge_norm_rn_proper_constructed_splitsecond_norm ge_norm_ip_proper_constructed_splitsecond_norm ge_norm_in_proper_constructed_splitsecond_norm. ((exists ge_representation_real_code_proper_constructed_splitsecond_normrepresentation ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation. (((q) = ((ge_representation_real_code_proper_constructed_splitsecond_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation)) * S ((ge_representation_real_code_proper_constructed_splitsecond_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation)) + ((ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation))) /\ ((exists ge_balance_positive_proper_constructed_splitsecond_normrepresentationreal ge_balance_negative_proper_constructed_splitsecond_normrepresentationreal. (((((ge_representation_real_code_proper_constructed_splitsecond_normrepresentation) = 2 * (ge_balance_positive_proper_constructed_splitsecond_normrepresentationreal) /\ (ge_balance_negative_proper_constructed_splitsecond_normrepresentationreal) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_normrepresentationrealdecode. (((ge_representation_real_code_proper_constructed_splitsecond_normrepresentation) = 2 * ge_signed_half_proper_constructed_splitsecond_normrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_normrepresentationreal) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_normrepresentationreal) = S ge_signed_half_proper_constructed_splitsecond_normrepresentationrealdecode))) /\ ((ge_norm_rp_proper_constructed_splitsecond_norm) + ge_balance_negative_proper_constructed_splitsecond_normrepresentationreal = (ge_norm_rn_proper_constructed_splitsecond_norm) + ge_balance_positive_proper_constructed_splitsecond_normrepresentationreal))) /\ (exists ge_balance_positive_proper_constructed_splitsecond_normrepresentationimaginary ge_balance_negative_proper_constructed_splitsecond_normrepresentationimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation) = 2 * (ge_balance_positive_proper_constructed_splitsecond_normrepresentationimaginary) /\ (ge_balance_negative_proper_constructed_splitsecond_normrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation) = 2 * ge_signed_half_proper_constructed_splitsecond_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_normrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_normrepresentationimaginary) = S ge_signed_half_proper_constructed_splitsecond_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_constructed_splitsecond_norm) + ge_balance_negative_proper_constructed_splitsecond_normrepresentationimaginary = (ge_norm_in_proper_constructed_splitsecond_norm) + ge_balance_positive_proper_constructed_splitsecond_normrepresentationimaginary)))))) /\ (exists ge_real_square_proper_constructed_splitsecond_normsquare ge_imaginary_square_proper_constructed_splitsecond_normsquare. ((((((ge_norm_rp_proper_constructed_splitsecond_norm) * (ge_norm_rp_proper_constructed_splitsecond_norm))) + (((ge_norm_rn_proper_constructed_splitsecond_norm) * (ge_norm_rn_proper_constructed_splitsecond_norm)))) = ((ge_real_square_proper_constructed_splitsecond_normsquare) + (((((ge_norm_rp_proper_constructed_splitsecond_norm) * (ge_norm_rn_proper_constructed_splitsecond_norm))) + (((ge_norm_rn_proper_constructed_splitsecond_norm) * (ge_norm_rp_proper_constructed_splitsecond_norm))))))) /\ ((((((ge_norm_ip_proper_constructed_splitsecond_norm) * (ge_norm_ip_proper_constructed_splitsecond_norm))) + (((ge_norm_in_proper_constructed_splitsecond_norm) * (ge_norm_in_proper_constructed_splitsecond_norm)))) = ((ge_imaginary_square_proper_constructed_splitsecond_normsquare) + (((((ge_norm_ip_proper_constructed_splitsecond_norm) * (ge_norm_in_proper_constructed_splitsecond_norm))) + (((ge_norm_in_proper_constructed_splitsecond_norm) * (ge_norm_ip_proper_constructed_splitsecond_norm))))))) /\ ((Q) = ge_real_square_proper_constructed_splitsecond_normsquare + ge_imaginary_square_proper_constructed_splitsecond_normsquare)))))) /\ ((~(exists gr_inverse_proper_constructed_splitfirst_nonunit. (exists ge_first_rp_proper_constructed_splitfirst_nonunitidentity ge_first_rn_proper_constructed_splitfirst_nonunitidentity ge_first_ip_proper_constructed_splitfirst_nonunitidentity ge_first_in_proper_constructed_splitfirst_nonunitidentity ge_second_rp_proper_constructed_splitfirst_nonunitidentity ge_second_rn_proper_constructed_splitfirst_nonunitidentity ge_second_ip_proper_constructed_splitfirst_nonunitidentity ge_second_in_proper_constructed_splitfirst_nonunitidentity. ((exists ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst. (((d) = ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst)) * S ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstreal ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstreal. (((((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstreal) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstreal) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstreal = (ge_first_rn_proper_constructed_splitfirst_nonunitidentity) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstimaginary ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstimaginary) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstimaginary = (ge_first_in_proper_constructed_splitfirst_nonunitidentity) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond. (((gr_inverse_proper_constructed_splitfirst_nonunit) = ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond)) * S ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondreal ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondreal. (((((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondreal) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondreal) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_constructed_splitfirst_nonunitidentity) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondreal = (ge_second_rn_proper_constructed_splitfirst_nonunitidentity) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondimaginary ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondimaginary) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_constructed_splitfirst_nonunitidentity) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondimaginary = (ge_second_in_proper_constructed_splitfirst_nonunitidentity) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput)) * S ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputreal ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputreal. (((((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputreal) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputreal) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rp_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rn_proper_constructed_splitfirst_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) * (ge_second_in_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_in_proper_constructed_splitfirst_nonunitidentity) * (ge_second_ip_proper_constructed_splitfirst_nonunitidentity))))))) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputreal = (((((((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rn_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rp_proper_constructed_splitfirst_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) * (ge_second_ip_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_in_proper_constructed_splitfirst_nonunitidentity) * (ge_second_in_proper_constructed_splitfirst_nonunitidentity))))))) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputimaginary ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputimaginary) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) * (ge_second_ip_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitfirst_nonunitidentity) * (ge_second_in_proper_constructed_splitfirst_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rp_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_in_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rn_proper_constructed_splitfirst_nonunitidentity))))))) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputimaginary = (((((((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) * (ge_second_in_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitfirst_nonunitidentity) * (ge_second_ip_proper_constructed_splitfirst_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rn_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_in_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rp_proper_constructed_splitfirst_nonunitidentity))))))) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputimaginary))))))))))) /\ ((~(exists gr_inverse_proper_constructed_splitsecond_nonunit. (exists ge_first_rp_proper_constructed_splitsecond_nonunitidentity ge_first_rn_proper_constructed_splitsecond_nonunitidentity ge_first_ip_proper_constructed_splitsecond_nonunitidentity ge_first_in_proper_constructed_splitsecond_nonunitidentity ge_second_rp_proper_constructed_splitsecond_nonunitidentity ge_second_rn_proper_constructed_splitsecond_nonunitidentity ge_second_ip_proper_constructed_splitsecond_nonunitidentity ge_second_in_proper_constructed_splitsecond_nonunitidentity. ((exists ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst. (((q) = ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst)) * S ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstreal ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstreal. (((((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstreal) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstreal) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstreal = (ge_first_rn_proper_constructed_splitsecond_nonunitidentity) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstimaginary ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstimaginary) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstimaginary = (ge_first_in_proper_constructed_splitsecond_nonunitidentity) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond. (((gr_inverse_proper_constructed_splitsecond_nonunit) = ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond)) * S ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondreal ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondreal. (((((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondreal) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondreal) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_constructed_splitsecond_nonunitidentity) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondreal = (ge_second_rn_proper_constructed_splitsecond_nonunitidentity) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondimaginary ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondimaginary) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_constructed_splitsecond_nonunitidentity) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondimaginary = (ge_second_in_proper_constructed_splitsecond_nonunitidentity) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput)) * S ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputreal ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputreal. (((((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputreal) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputreal) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rp_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rn_proper_constructed_splitsecond_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) * (ge_second_in_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_in_proper_constructed_splitsecond_nonunitidentity) * (ge_second_ip_proper_constructed_splitsecond_nonunitidentity))))))) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputreal = (((((((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rn_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rp_proper_constructed_splitsecond_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) * (ge_second_ip_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_in_proper_constructed_splitsecond_nonunitidentity) * (ge_second_in_proper_constructed_splitsecond_nonunitidentity))))))) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputimaginary ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputimaginary) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) * (ge_second_ip_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitsecond_nonunitidentity) * (ge_second_in_proper_constructed_splitsecond_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rp_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_in_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rn_proper_constructed_splitsecond_nonunitidentity))))))) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputimaginary = (((((((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) * (ge_second_in_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitsecond_nonunitidentity) * (ge_second_ip_proper_constructed_splitsecond_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rn_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_in_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rp_proper_constructed_splitsecond_nonunitidentity))))))) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputimaginary))))))))))) /\ ((exists ge_gap_proper_constructed_splitfirst_strict. ge_gap_proper_constructed_splitfirst_strict + S (D) = (N)) /\ (exists ge_gap_proper_constructed_splitsecond_strict. ge_gap_proper_constructed_splitsecond_strict + S (Q) = (N))))))))))