EEuclideanDivision(a,b,q,r,U,V)

((exists ee_division_product_lowerlayerequation. ((exists ee_first_rp_lowerlayerequationproduct ee_first_rn_lowerlayerequationproduct ee_first_ip_lowerlayerequationproduct ee_first_in_lowerlayerequationproduct ee_second_rp_lowerlayerequationproduct ee_second_rn_lowerlayerequationproduct ee_second_ip_lowerlayerequationproduct ee_second_in_lowerlayerequationproduct. ((exists ge_representation_real_code_lowerlayerequationproductfirst ge_representation_imaginary_code_lowerlayerequationproductfirst. (((b) = ((ge_representation_real_code_lowerlayerequationproductfirst) + (ge_representation_imaginary_code_lowerlayerequationproductfirst)) * S ((ge_representation_real_code_lowerlayerequationproductfirst) + (ge_representation_imaginary_code_lowerlayerequationproductfirst)) + ((ge_representation_imaginary_code_lowerlayerequationproductfirst) + (ge_representation_imaginary_code_lowerlayerequationproductfirst))) /\ ((exists ge_balance_positive_lowerlayerequationproductfirstreal ge_balance_negative_lowerlayerequationproductfirstreal. (((((ge_representation_real_code_lowerlayerequationproductfirst) = 2 * (ge_balance_positive_lowerlayerequationproductfirstreal) /\ (ge_balance_negative_lowerlayerequationproductfirstreal) = 0) \/ exists ge_signed_half_lowerlayerequationproductfirstrealdecode. (((ge_representation_real_code_lowerlayerequationproductfirst) = 2 * ge_signed_half_lowerlayerequationproductfirstrealdecode + 1 /\ (ge_balance_positive_lowerlayerequationproductfirstreal) = 0) /\ (ge_balance_negative_lowerlayerequationproductfirstreal) = S ge_signed_half_lowerlayerequationproductfirstrealdecode))) /\ ((ee_first_rp_lowerlayerequationproduct) + ge_balance_negative_lowerlayerequationproductfirstreal = (ee_first_rn_lowerlayerequationproduct) + ge_balance_positive_lowerlayerequationproductfirstreal))) /\ (exists ge_balance_positive_lowerlayerequationproductfirstimaginary ge_balance_negative_lowerlayerequationproductfirstimaginary. (((((ge_representation_imaginary_code_lowerlayerequationproductfirst) = 2 * (ge_balance_positive_lowerlayerequationproductfirstimaginary) /\ (ge_balance_negative_lowerlayerequationproductfirstimaginary) = 0) \/ exists ge_signed_half_lowerlayerequationproductfirstimaginarydecode. (((ge_representation_imaginary_code_lowerlayerequationproductfirst) = 2 * ge_signed_half_lowerlayerequationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerequationproductfirstimaginary) = 0) /\ (ge_balance_negative_lowerlayerequationproductfirstimaginary) = S ge_signed_half_lowerlayerequationproductfirstimaginarydecode))) /\ ((ee_first_ip_lowerlayerequationproduct) + ge_balance_negative_lowerlayerequationproductfirstimaginary = (ee_first_in_lowerlayerequationproduct) + ge_balance_positive_lowerlayerequationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_lowerlayerequationproductsecond ge_representation_imaginary_code_lowerlayerequationproductsecond. (((q) = ((ge_representation_real_code_lowerlayerequationproductsecond) + (ge_representation_imaginary_code_lowerlayerequationproductsecond)) * S ((ge_representation_real_code_lowerlayerequationproductsecond) + (ge_representation_imaginary_code_lowerlayerequationproductsecond)) + ((ge_representation_imaginary_code_lowerlayerequationproductsecond) + (ge_representation_imaginary_code_lowerlayerequationproductsecond))) /\ ((exists ge_balance_positive_lowerlayerequationproductsecondreal ge_balance_negative_lowerlayerequationproductsecondreal. (((((ge_representation_real_code_lowerlayerequationproductsecond) = 2 * (ge_balance_positive_lowerlayerequationproductsecondreal) /\ (ge_balance_negative_lowerlayerequationproductsecondreal) = 0) \/ exists ge_signed_half_lowerlayerequationproductsecondrealdecode. (((ge_representation_real_code_lowerlayerequationproductsecond) = 2 * ge_signed_half_lowerlayerequationproductsecondrealdecode + 1 /\ (ge_balance_positive_lowerlayerequationproductsecondreal) = 0) /\ (ge_balance_negative_lowerlayerequationproductsecondreal) = S ge_signed_half_lowerlayerequationproductsecondrealdecode))) /\ ((ee_second_rp_lowerlayerequationproduct) + ge_balance_negative_lowerlayerequationproductsecondreal = (ee_second_rn_lowerlayerequationproduct) + ge_balance_positive_lowerlayerequationproductsecondreal))) /\ (exists ge_balance_positive_lowerlayerequationproductsecondimaginary ge_balance_negative_lowerlayerequationproductsecondimaginary. (((((ge_representation_imaginary_code_lowerlayerequationproductsecond) = 2 * (ge_balance_positive_lowerlayerequationproductsecondimaginary) /\ (ge_balance_negative_lowerlayerequationproductsecondimaginary) = 0) \/ exists ge_signed_half_lowerlayerequationproductsecondimaginarydecode. (((ge_representation_imaginary_code_lowerlayerequationproductsecond) = 2 * ge_signed_half_lowerlayerequationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerequationproductsecondimaginary) = 0) /\ (ge_balance_negative_lowerlayerequationproductsecondimaginary) = S ge_signed_half_lowerlayerequationproductsecondimaginarydecode))) /\ ((ee_second_ip_lowerlayerequationproduct) + ge_balance_negative_lowerlayerequationproductsecondimaginary = (ee_second_in_lowerlayerequationproduct) + ge_balance_positive_lowerlayerequationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_lowerlayerequationproductoutput ge_representation_imaginary_code_lowerlayerequationproductoutput. (((ee_division_product_lowerlayerequation) = ((ge_representation_real_code_lowerlayerequationproductoutput) + (ge_representation_imaginary_code_lowerlayerequationproductoutput)) * S ((ge_representation_real_code_lowerlayerequationproductoutput) + (ge_representation_imaginary_code_lowerlayerequationproductoutput)) + ((ge_representation_imaginary_code_lowerlayerequationproductoutput) + (ge_representation_imaginary_code_lowerlayerequationproductoutput))) /\ ((exists ge_balance_positive_lowerlayerequationproductoutputreal ge_balance_negative_lowerlayerequationproductoutputreal. (((((ge_representation_real_code_lowerlayerequationproductoutput) = 2 * (ge_balance_positive_lowerlayerequationproductoutputreal) /\ (ge_balance_negative_lowerlayerequationproductoutputreal) = 0) \/ exists ge_signed_half_lowerlayerequationproductoutputrealdecode. (((ge_representation_real_code_lowerlayerequationproductoutput) = 2 * ge_signed_half_lowerlayerequationproductoutputrealdecode + 1 /\ (ge_balance_positive_lowerlayerequationproductoutputreal) = 0) /\ (ge_balance_negative_lowerlayerequationproductoutputreal) = S ge_signed_half_lowerlayerequationproductoutputrealdecode))) /\ ((((((((ee_first_rp_lowerlayerequationproduct) * (ee_second_rp_lowerlayerequationproduct))) + (((ee_first_rn_lowerlayerequationproduct) * (ee_second_rn_lowerlayerequationproduct))))) + (((((ee_first_ip_lowerlayerequationproduct) * (ee_second_in_lowerlayerequationproduct))) + (((ee_first_in_lowerlayerequationproduct) * (ee_second_ip_lowerlayerequationproduct))))))) + ge_balance_negative_lowerlayerequationproductoutputreal = (((((((ee_first_rp_lowerlayerequationproduct) * (ee_second_rn_lowerlayerequationproduct))) + (((ee_first_rn_lowerlayerequationproduct) * (ee_second_rp_lowerlayerequationproduct))))) + (((((ee_first_ip_lowerlayerequationproduct) * (ee_second_ip_lowerlayerequationproduct))) + (((ee_first_in_lowerlayerequationproduct) * (ee_second_in_lowerlayerequationproduct))))))) + ge_balance_positive_lowerlayerequationproductoutputreal))) /\ (exists ge_balance_positive_lowerlayerequationproductoutputimaginary ge_balance_negative_lowerlayerequationproductoutputimaginary. (((((ge_representation_imaginary_code_lowerlayerequationproductoutput) = 2 * (ge_balance_positive_lowerlayerequationproductoutputimaginary) /\ (ge_balance_negative_lowerlayerequationproductoutputimaginary) = 0) \/ exists ge_signed_half_lowerlayerequationproductoutputimaginarydecode. (((ge_representation_imaginary_code_lowerlayerequationproductoutput) = 2 * ge_signed_half_lowerlayerequationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerequationproductoutputimaginary) = 0) /\ (ge_balance_negative_lowerlayerequationproductoutputimaginary) = S ge_signed_half_lowerlayerequationproductoutputimaginarydecode))) /\ ((((((((((ee_first_rp_lowerlayerequationproduct) * (ee_second_ip_lowerlayerequationproduct))) + (((ee_first_rn_lowerlayerequationproduct) * (ee_second_in_lowerlayerequationproduct))))) + (((((ee_first_ip_lowerlayerequationproduct) * (ee_second_rp_lowerlayerequationproduct))) + (((ee_first_in_lowerlayerequationproduct) * (ee_second_rn_lowerlayerequationproduct))))))) + (((((ee_first_ip_lowerlayerequationproduct) * (ee_second_in_lowerlayerequationproduct))) + (((ee_first_in_lowerlayerequationproduct) * (ee_second_ip_lowerlayerequationproduct))))))) + ge_balance_negative_lowerlayerequationproductoutputimaginary = (((((((((ee_first_rp_lowerlayerequationproduct) * (ee_second_in_lowerlayerequationproduct))) + (((ee_first_rn_lowerlayerequationproduct) * (ee_second_ip_lowerlayerequationproduct))))) + (((((ee_first_ip_lowerlayerequationproduct) * (ee_second_rn_lowerlayerequationproduct))) + (((ee_first_in_lowerlayerequationproduct) * (ee_second_rp_lowerlayerequationproduct))))))) + (((((ee_first_ip_lowerlayerequationproduct) * (ee_second_ip_lowerlayerequationproduct))) + (((ee_first_in_lowerlayerequationproduct) * (ee_second_in_lowerlayerequationproduct))))))) + ge_balance_positive_lowerlayerequationproductoutputimaginary))))))))) /\ (exists ge_first_rp_lowerlayerequationsum ge_first_rn_lowerlayerequationsum ge_first_ip_lowerlayerequationsum ge_first_in_lowerlayerequationsum ge_second_rp_lowerlayerequationsum ge_second_rn_lowerlayerequationsum ge_second_ip_lowerlayerequationsum ge_second_in_lowerlayerequationsum. ((exists ge_representation_real_code_lowerlayerequationsumfirst ge_representation_imaginary_code_lowerlayerequationsumfirst. (((ee_division_product_lowerlayerequation) = ((ge_representation_real_code_lowerlayerequationsumfirst) + (ge_representation_imaginary_code_lowerlayerequationsumfirst)) * S ((ge_representation_real_code_lowerlayerequationsumfirst) + (ge_representation_imaginary_code_lowerlayerequationsumfirst)) + ((ge_representation_imaginary_code_lowerlayerequationsumfirst) + (ge_representation_imaginary_code_lowerlayerequationsumfirst))) /\ ((exists ge_balance_positive_lowerlayerequationsumfirstreal ge_balance_negative_lowerlayerequationsumfirstreal. (((((ge_representation_real_code_lowerlayerequationsumfirst) = 2 * (ge_balance_positive_lowerlayerequationsumfirstreal) /\ (ge_balance_negative_lowerlayerequationsumfirstreal) = 0) \/ exists ge_signed_half_lowerlayerequationsumfirstrealdecode. (((ge_representation_real_code_lowerlayerequationsumfirst) = 2 * ge_signed_half_lowerlayerequationsumfirstrealdecode + 1 /\ (ge_balance_positive_lowerlayerequationsumfirstreal) = 0) /\ (ge_balance_negative_lowerlayerequationsumfirstreal) = S ge_signed_half_lowerlayerequationsumfirstrealdecode))) /\ ((ge_first_rp_lowerlayerequationsum) + ge_balance_negative_lowerlayerequationsumfirstreal = (ge_first_rn_lowerlayerequationsum) + ge_balance_positive_lowerlayerequationsumfirstreal))) /\ (exists ge_balance_positive_lowerlayerequationsumfirstimaginary ge_balance_negative_lowerlayerequationsumfirstimaginary. (((((ge_representation_imaginary_code_lowerlayerequationsumfirst) = 2 * (ge_balance_positive_lowerlayerequationsumfirstimaginary) /\ (ge_balance_negative_lowerlayerequationsumfirstimaginary) = 0) \/ exists ge_signed_half_lowerlayerequationsumfirstimaginarydecode. (((ge_representation_imaginary_code_lowerlayerequationsumfirst) = 2 * ge_signed_half_lowerlayerequationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerequationsumfirstimaginary) = 0) /\ (ge_balance_negative_lowerlayerequationsumfirstimaginary) = S ge_signed_half_lowerlayerequationsumfirstimaginarydecode))) /\ ((ge_first_ip_lowerlayerequationsum) + ge_balance_negative_lowerlayerequationsumfirstimaginary = (ge_first_in_lowerlayerequationsum) + ge_balance_positive_lowerlayerequationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_lowerlayerequationsumsecond ge_representation_imaginary_code_lowerlayerequationsumsecond. (((r) = ((ge_representation_real_code_lowerlayerequationsumsecond) + (ge_representation_imaginary_code_lowerlayerequationsumsecond)) * S ((ge_representation_real_code_lowerlayerequationsumsecond) + (ge_representation_imaginary_code_lowerlayerequationsumsecond)) + ((ge_representation_imaginary_code_lowerlayerequationsumsecond) + (ge_representation_imaginary_code_lowerlayerequationsumsecond))) /\ ((exists ge_balance_positive_lowerlayerequationsumsecondreal ge_balance_negative_lowerlayerequationsumsecondreal. (((((ge_representation_real_code_lowerlayerequationsumsecond) = 2 * (ge_balance_positive_lowerlayerequationsumsecondreal) /\ (ge_balance_negative_lowerlayerequationsumsecondreal) = 0) \/ exists ge_signed_half_lowerlayerequationsumsecondrealdecode. (((ge_representation_real_code_lowerlayerequationsumsecond) = 2 * ge_signed_half_lowerlayerequationsumsecondrealdecode + 1 /\ (ge_balance_positive_lowerlayerequationsumsecondreal) = 0) /\ (ge_balance_negative_lowerlayerequationsumsecondreal) = S ge_signed_half_lowerlayerequationsumsecondrealdecode))) /\ ((ge_second_rp_lowerlayerequationsum) + ge_balance_negative_lowerlayerequationsumsecondreal = (ge_second_rn_lowerlayerequationsum) + ge_balance_positive_lowerlayerequationsumsecondreal))) /\ (exists ge_balance_positive_lowerlayerequationsumsecondimaginary ge_balance_negative_lowerlayerequationsumsecondimaginary. (((((ge_representation_imaginary_code_lowerlayerequationsumsecond) = 2 * (ge_balance_positive_lowerlayerequationsumsecondimaginary) /\ (ge_balance_negative_lowerlayerequationsumsecondimaginary) = 0) \/ exists ge_signed_half_lowerlayerequationsumsecondimaginarydecode. (((ge_representation_imaginary_code_lowerlayerequationsumsecond) = 2 * ge_signed_half_lowerlayerequationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerequationsumsecondimaginary) = 0) /\ (ge_balance_negative_lowerlayerequationsumsecondimaginary) = S ge_signed_half_lowerlayerequationsumsecondimaginarydecode))) /\ ((ge_second_ip_lowerlayerequationsum) + ge_balance_negative_lowerlayerequationsumsecondimaginary = (ge_second_in_lowerlayerequationsum) + ge_balance_positive_lowerlayerequationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_lowerlayerequationsumoutput ge_representation_imaginary_code_lowerlayerequationsumoutput. (((a) = ((ge_representation_real_code_lowerlayerequationsumoutput) + (ge_representation_imaginary_code_lowerlayerequationsumoutput)) * S ((ge_representation_real_code_lowerlayerequationsumoutput) + (ge_representation_imaginary_code_lowerlayerequationsumoutput)) + ((ge_representation_imaginary_code_lowerlayerequationsumoutput) + (ge_representation_imaginary_code_lowerlayerequationsumoutput))) /\ ((exists ge_balance_positive_lowerlayerequationsumoutputreal ge_balance_negative_lowerlayerequationsumoutputreal. (((((ge_representation_real_code_lowerlayerequationsumoutput) = 2 * (ge_balance_positive_lowerlayerequationsumoutputreal) /\ (ge_balance_negative_lowerlayerequationsumoutputreal) = 0) \/ exists ge_signed_half_lowerlayerequationsumoutputrealdecode. (((ge_representation_real_code_lowerlayerequationsumoutput) = 2 * ge_signed_half_lowerlayerequationsumoutputrealdecode + 1 /\ (ge_balance_positive_lowerlayerequationsumoutputreal) = 0) /\ (ge_balance_negative_lowerlayerequationsumoutputreal) = S ge_signed_half_lowerlayerequationsumoutputrealdecode))) /\ ((((ge_first_rp_lowerlayerequationsum) + (ge_second_rp_lowerlayerequationsum))) + ge_balance_negative_lowerlayerequationsumoutputreal = (((ge_first_rn_lowerlayerequationsum) + (ge_second_rn_lowerlayerequationsum))) + ge_balance_positive_lowerlayerequationsumoutputreal))) /\ (exists ge_balance_positive_lowerlayerequationsumoutputimaginary ge_balance_negative_lowerlayerequationsumoutputimaginary. (((((ge_representation_imaginary_code_lowerlayerequationsumoutput) = 2 * (ge_balance_positive_lowerlayerequationsumoutputimaginary) /\ (ge_balance_negative_lowerlayerequationsumoutputimaginary) = 0) \/ exists ge_signed_half_lowerlayerequationsumoutputimaginarydecode. (((ge_representation_imaginary_code_lowerlayerequationsumoutput) = 2 * ge_signed_half_lowerlayerequationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerequationsumoutputimaginary) = 0) /\ (ge_balance_negative_lowerlayerequationsumoutputimaginary) = S ge_signed_half_lowerlayerequationsumoutputimaginarydecode))) /\ ((((ge_first_ip_lowerlayerequationsum) + (ge_second_ip_lowerlayerequationsum))) + ge_balance_negative_lowerlayerequationsumoutputimaginary = (((ge_first_in_lowerlayerequationsum) + (ge_second_in_lowerlayerequationsum))) + ge_balance_positive_lowerlayerequationsumoutputimaginary))))))))))) /\ ((exists ee_norm_rp_lowerlayersmallnorm ee_norm_rn_lowerlayersmallnorm ee_norm_ip_lowerlayersmallnorm ee_norm_in_lowerlayersmallnorm. ((exists ge_representation_real_code_lowerlayersmallnormrepresentation ge_representation_imaginary_code_lowerlayersmallnormrepresentation. (((r) = ((ge_representation_real_code_lowerlayersmallnormrepresentation) + (ge_representation_imaginary_code_lowerlayersmallnormrepresentation)) * S ((ge_representation_real_code_lowerlayersmallnormrepresentation) + (ge_representation_imaginary_code_lowerlayersmallnormrepresentation)) + ((ge_representation_imaginary_code_lowerlayersmallnormrepresentation) + (ge_representation_imaginary_code_lowerlayersmallnormrepresentation))) /\ ((exists ge_balance_positive_lowerlayersmallnormrepresentationreal ge_balance_negative_lowerlayersmallnormrepresentationreal. (((((ge_representation_real_code_lowerlayersmallnormrepresentation) = 2 * (ge_balance_positive_lowerlayersmallnormrepresentationreal) /\ (ge_balance_negative_lowerlayersmallnormrepresentationreal) = 0) \/ exists ge_signed_half_lowerlayersmallnormrepresentationrealdecode. (((ge_representation_real_code_lowerlayersmallnormrepresentation) = 2 * ge_signed_half_lowerlayersmallnormrepresentationrealdecode + 1 /\ (ge_balance_positive_lowerlayersmallnormrepresentationreal) = 0) /\ (ge_balance_negative_lowerlayersmallnormrepresentationreal) = S ge_signed_half_lowerlayersmallnormrepresentationrealdecode))) /\ ((ee_norm_rp_lowerlayersmallnorm) + ge_balance_negative_lowerlayersmallnormrepresentationreal = (ee_norm_rn_lowerlayersmallnorm) + ge_balance_positive_lowerlayersmallnormrepresentationreal))) /\ (exists ge_balance_positive_lowerlayersmallnormrepresentationimaginary ge_balance_negative_lowerlayersmallnormrepresentationimaginary. (((((ge_representation_imaginary_code_lowerlayersmallnormrepresentation) = 2 * (ge_balance_positive_lowerlayersmallnormrepresentationimaginary) /\ (ge_balance_negative_lowerlayersmallnormrepresentationimaginary) = 0) \/ exists ge_signed_half_lowerlayersmallnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_lowerlayersmallnormrepresentation) = 2 * ge_signed_half_lowerlayersmallnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_lowerlayersmallnormrepresentationimaginary) = 0) /\ (ge_balance_negative_lowerlayersmallnormrepresentationimaginary) = S ge_signed_half_lowerlayersmallnormrepresentationimaginarydecode))) /\ ((ee_norm_ip_lowerlayersmallnorm) + ge_balance_negative_lowerlayersmallnormrepresentationimaginary = (ee_norm_in_lowerlayersmallnorm) + ge_balance_positive_lowerlayersmallnormrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_lowerlayersmallnorm) * (ee_norm_rp_lowerlayersmallnorm))) + (((ee_norm_rn_lowerlayersmallnorm) * (ee_norm_rn_lowerlayersmallnorm))))) + (((((ee_norm_ip_lowerlayersmallnorm) * (ee_norm_ip_lowerlayersmallnorm))) + (((ee_norm_in_lowerlayersmallnorm) * (ee_norm_in_lowerlayersmallnorm))))))) + (((((ee_norm_rp_lowerlayersmallnorm) * (ee_norm_in_lowerlayersmallnorm))) + (((ee_norm_rn_lowerlayersmallnorm) * (ee_norm_ip_lowerlayersmallnorm)))))) = ((((((((((ee_norm_rp_lowerlayersmallnorm) * (ee_norm_rn_lowerlayersmallnorm))) + (((ee_norm_rn_lowerlayersmallnorm) * (ee_norm_rp_lowerlayersmallnorm))))) + (((((ee_norm_ip_lowerlayersmallnorm) * (ee_norm_in_lowerlayersmallnorm))) + (((ee_norm_in_lowerlayersmallnorm) * (ee_norm_ip_lowerlayersmallnorm))))))) + (((((ee_norm_rp_lowerlayersmallnorm) * (ee_norm_ip_lowerlayersmallnorm))) + (((ee_norm_rn_lowerlayersmallnorm) * (ee_norm_in_lowerlayersmallnorm))))))) + (U))))) /\ ((exists ee_norm_rp_lowerlayerlargenorm ee_norm_rn_lowerlayerlargenorm ee_norm_ip_lowerlayerlargenorm ee_norm_in_lowerlayerlargenorm. ((exists ge_representation_real_code_lowerlayerlargenormrepresentation ge_representation_imaginary_code_lowerlayerlargenormrepresentation. (((b) = ((ge_representation_real_code_lowerlayerlargenormrepresentation) + (ge_representation_imaginary_code_lowerlayerlargenormrepresentation)) * S ((ge_representation_real_code_lowerlayerlargenormrepresentation) + (ge_representation_imaginary_code_lowerlayerlargenormrepresentation)) + ((ge_representation_imaginary_code_lowerlayerlargenormrepresentation) + (ge_representation_imaginary_code_lowerlayerlargenormrepresentation))) /\ ((exists ge_balance_positive_lowerlayerlargenormrepresentationreal ge_balance_negative_lowerlayerlargenormrepresentationreal. (((((ge_representation_real_code_lowerlayerlargenormrepresentation) = 2 * (ge_balance_positive_lowerlayerlargenormrepresentationreal) /\ (ge_balance_negative_lowerlayerlargenormrepresentationreal) = 0) \/ exists ge_signed_half_lowerlayerlargenormrepresentationrealdecode. (((ge_representation_real_code_lowerlayerlargenormrepresentation) = 2 * ge_signed_half_lowerlayerlargenormrepresentationrealdecode + 1 /\ (ge_balance_positive_lowerlayerlargenormrepresentationreal) = 0) /\ (ge_balance_negative_lowerlayerlargenormrepresentationreal) = S ge_signed_half_lowerlayerlargenormrepresentationrealdecode))) /\ ((ee_norm_rp_lowerlayerlargenorm) + ge_balance_negative_lowerlayerlargenormrepresentationreal = (ee_norm_rn_lowerlayerlargenorm) + ge_balance_positive_lowerlayerlargenormrepresentationreal))) /\ (exists ge_balance_positive_lowerlayerlargenormrepresentationimaginary ge_balance_negative_lowerlayerlargenormrepresentationimaginary. (((((ge_representation_imaginary_code_lowerlayerlargenormrepresentation) = 2 * (ge_balance_positive_lowerlayerlargenormrepresentationimaginary) /\ (ge_balance_negative_lowerlayerlargenormrepresentationimaginary) = 0) \/ exists ge_signed_half_lowerlayerlargenormrepresentationimaginarydecode. (((ge_representation_imaginary_code_lowerlayerlargenormrepresentation) = 2 * ge_signed_half_lowerlayerlargenormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerlargenormrepresentationimaginary) = 0) /\ (ge_balance_negative_lowerlayerlargenormrepresentationimaginary) = S ge_signed_half_lowerlayerlargenormrepresentationimaginarydecode))) /\ ((ee_norm_ip_lowerlayerlargenorm) + ge_balance_negative_lowerlayerlargenormrepresentationimaginary = (ee_norm_in_lowerlayerlargenorm) + ge_balance_positive_lowerlayerlargenormrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_lowerlayerlargenorm) * (ee_norm_rp_lowerlayerlargenorm))) + (((ee_norm_rn_lowerlayerlargenorm) * (ee_norm_rn_lowerlayerlargenorm))))) + (((((ee_norm_ip_lowerlayerlargenorm) * (ee_norm_ip_lowerlayerlargenorm))) + (((ee_norm_in_lowerlayerlargenorm) * (ee_norm_in_lowerlayerlargenorm))))))) + (((((ee_norm_rp_lowerlayerlargenorm) * (ee_norm_in_lowerlayerlargenorm))) + (((ee_norm_rn_lowerlayerlargenorm) * (ee_norm_ip_lowerlayerlargenorm)))))) = ((((((((((ee_norm_rp_lowerlayerlargenorm) * (ee_norm_rn_lowerlayerlargenorm))) + (((ee_norm_rn_lowerlayerlargenorm) * (ee_norm_rp_lowerlayerlargenorm))))) + (((((ee_norm_ip_lowerlayerlargenorm) * (ee_norm_in_lowerlayerlargenorm))) + (((ee_norm_in_lowerlayerlargenorm) * (ee_norm_ip_lowerlayerlargenorm))))))) + (((((ee_norm_rp_lowerlayerlargenorm) * (ee_norm_ip_lowerlayerlargenorm))) + (((ee_norm_rn_lowerlayerlargenorm) * (ee_norm_in_lowerlayerlargenorm))))))) + (V))))) /\ (exists ee_gap_lowerlayerstrict. ee_gap_lowerlayerstrict + S (U) = (V)))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.