EDivRem(a,b,q,r)

exists ee_division_product_lowerlayer. ((exists ee_first_rp_lowerlayerproduct ee_first_rn_lowerlayerproduct ee_first_ip_lowerlayerproduct ee_first_in_lowerlayerproduct ee_second_rp_lowerlayerproduct ee_second_rn_lowerlayerproduct ee_second_ip_lowerlayerproduct ee_second_in_lowerlayerproduct. ((exists ge_representation_real_code_lowerlayerproductfirst ge_representation_imaginary_code_lowerlayerproductfirst. (((b) = ((ge_representation_real_code_lowerlayerproductfirst) + (ge_representation_imaginary_code_lowerlayerproductfirst)) * S ((ge_representation_real_code_lowerlayerproductfirst) + (ge_representation_imaginary_code_lowerlayerproductfirst)) + ((ge_representation_imaginary_code_lowerlayerproductfirst) + (ge_representation_imaginary_code_lowerlayerproductfirst))) /\ ((exists ge_balance_positive_lowerlayerproductfirstreal ge_balance_negative_lowerlayerproductfirstreal. (((((ge_representation_real_code_lowerlayerproductfirst) = 2 * (ge_balance_positive_lowerlayerproductfirstreal) /\ (ge_balance_negative_lowerlayerproductfirstreal) = 0) \/ exists ge_signed_half_lowerlayerproductfirstrealdecode. (((ge_representation_real_code_lowerlayerproductfirst) = 2 * ge_signed_half_lowerlayerproductfirstrealdecode + 1 /\ (ge_balance_positive_lowerlayerproductfirstreal) = 0) /\ (ge_balance_negative_lowerlayerproductfirstreal) = S ge_signed_half_lowerlayerproductfirstrealdecode))) /\ ((ee_first_rp_lowerlayerproduct) + ge_balance_negative_lowerlayerproductfirstreal = (ee_first_rn_lowerlayerproduct) + ge_balance_positive_lowerlayerproductfirstreal))) /\ (exists ge_balance_positive_lowerlayerproductfirstimaginary ge_balance_negative_lowerlayerproductfirstimaginary. (((((ge_representation_imaginary_code_lowerlayerproductfirst) = 2 * (ge_balance_positive_lowerlayerproductfirstimaginary) /\ (ge_balance_negative_lowerlayerproductfirstimaginary) = 0) \/ exists ge_signed_half_lowerlayerproductfirstimaginarydecode. (((ge_representation_imaginary_code_lowerlayerproductfirst) = 2 * ge_signed_half_lowerlayerproductfirstimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerproductfirstimaginary) = 0) /\ (ge_balance_negative_lowerlayerproductfirstimaginary) = S ge_signed_half_lowerlayerproductfirstimaginarydecode))) /\ ((ee_first_ip_lowerlayerproduct) + ge_balance_negative_lowerlayerproductfirstimaginary = (ee_first_in_lowerlayerproduct) + ge_balance_positive_lowerlayerproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_lowerlayerproductsecond ge_representation_imaginary_code_lowerlayerproductsecond. (((q) = ((ge_representation_real_code_lowerlayerproductsecond) + (ge_representation_imaginary_code_lowerlayerproductsecond)) * S ((ge_representation_real_code_lowerlayerproductsecond) + (ge_representation_imaginary_code_lowerlayerproductsecond)) + ((ge_representation_imaginary_code_lowerlayerproductsecond) + (ge_representation_imaginary_code_lowerlayerproductsecond))) /\ ((exists ge_balance_positive_lowerlayerproductsecondreal ge_balance_negative_lowerlayerproductsecondreal. (((((ge_representation_real_code_lowerlayerproductsecond) = 2 * (ge_balance_positive_lowerlayerproductsecondreal) /\ (ge_balance_negative_lowerlayerproductsecondreal) = 0) \/ exists ge_signed_half_lowerlayerproductsecondrealdecode. (((ge_representation_real_code_lowerlayerproductsecond) = 2 * ge_signed_half_lowerlayerproductsecondrealdecode + 1 /\ (ge_balance_positive_lowerlayerproductsecondreal) = 0) /\ (ge_balance_negative_lowerlayerproductsecondreal) = S ge_signed_half_lowerlayerproductsecondrealdecode))) /\ ((ee_second_rp_lowerlayerproduct) + ge_balance_negative_lowerlayerproductsecondreal = (ee_second_rn_lowerlayerproduct) + ge_balance_positive_lowerlayerproductsecondreal))) /\ (exists ge_balance_positive_lowerlayerproductsecondimaginary ge_balance_negative_lowerlayerproductsecondimaginary. (((((ge_representation_imaginary_code_lowerlayerproductsecond) = 2 * (ge_balance_positive_lowerlayerproductsecondimaginary) /\ (ge_balance_negative_lowerlayerproductsecondimaginary) = 0) \/ exists ge_signed_half_lowerlayerproductsecondimaginarydecode. (((ge_representation_imaginary_code_lowerlayerproductsecond) = 2 * ge_signed_half_lowerlayerproductsecondimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerproductsecondimaginary) = 0) /\ (ge_balance_negative_lowerlayerproductsecondimaginary) = S ge_signed_half_lowerlayerproductsecondimaginarydecode))) /\ ((ee_second_ip_lowerlayerproduct) + ge_balance_negative_lowerlayerproductsecondimaginary = (ee_second_in_lowerlayerproduct) + ge_balance_positive_lowerlayerproductsecondimaginary)))))) /\ (exists ge_representation_real_code_lowerlayerproductoutput ge_representation_imaginary_code_lowerlayerproductoutput. (((ee_division_product_lowerlayer) = ((ge_representation_real_code_lowerlayerproductoutput) + (ge_representation_imaginary_code_lowerlayerproductoutput)) * S ((ge_representation_real_code_lowerlayerproductoutput) + (ge_representation_imaginary_code_lowerlayerproductoutput)) + ((ge_representation_imaginary_code_lowerlayerproductoutput) + (ge_representation_imaginary_code_lowerlayerproductoutput))) /\ ((exists ge_balance_positive_lowerlayerproductoutputreal ge_balance_negative_lowerlayerproductoutputreal. (((((ge_representation_real_code_lowerlayerproductoutput) = 2 * (ge_balance_positive_lowerlayerproductoutputreal) /\ (ge_balance_negative_lowerlayerproductoutputreal) = 0) \/ exists ge_signed_half_lowerlayerproductoutputrealdecode. (((ge_representation_real_code_lowerlayerproductoutput) = 2 * ge_signed_half_lowerlayerproductoutputrealdecode + 1 /\ (ge_balance_positive_lowerlayerproductoutputreal) = 0) /\ (ge_balance_negative_lowerlayerproductoutputreal) = S ge_signed_half_lowerlayerproductoutputrealdecode))) /\ ((((((((ee_first_rp_lowerlayerproduct) * (ee_second_rp_lowerlayerproduct))) + (((ee_first_rn_lowerlayerproduct) * (ee_second_rn_lowerlayerproduct))))) + (((((ee_first_ip_lowerlayerproduct) * (ee_second_in_lowerlayerproduct))) + (((ee_first_in_lowerlayerproduct) * (ee_second_ip_lowerlayerproduct))))))) + ge_balance_negative_lowerlayerproductoutputreal = (((((((ee_first_rp_lowerlayerproduct) * (ee_second_rn_lowerlayerproduct))) + (((ee_first_rn_lowerlayerproduct) * (ee_second_rp_lowerlayerproduct))))) + (((((ee_first_ip_lowerlayerproduct) * (ee_second_ip_lowerlayerproduct))) + (((ee_first_in_lowerlayerproduct) * (ee_second_in_lowerlayerproduct))))))) + ge_balance_positive_lowerlayerproductoutputreal))) /\ (exists ge_balance_positive_lowerlayerproductoutputimaginary ge_balance_negative_lowerlayerproductoutputimaginary. (((((ge_representation_imaginary_code_lowerlayerproductoutput) = 2 * (ge_balance_positive_lowerlayerproductoutputimaginary) /\ (ge_balance_negative_lowerlayerproductoutputimaginary) = 0) \/ exists ge_signed_half_lowerlayerproductoutputimaginarydecode. (((ge_representation_imaginary_code_lowerlayerproductoutput) = 2 * ge_signed_half_lowerlayerproductoutputimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerproductoutputimaginary) = 0) /\ (ge_balance_negative_lowerlayerproductoutputimaginary) = S ge_signed_half_lowerlayerproductoutputimaginarydecode))) /\ ((((((((((ee_first_rp_lowerlayerproduct) * (ee_second_ip_lowerlayerproduct))) + (((ee_first_rn_lowerlayerproduct) * (ee_second_in_lowerlayerproduct))))) + (((((ee_first_ip_lowerlayerproduct) * (ee_second_rp_lowerlayerproduct))) + (((ee_first_in_lowerlayerproduct) * (ee_second_rn_lowerlayerproduct))))))) + (((((ee_first_ip_lowerlayerproduct) * (ee_second_in_lowerlayerproduct))) + (((ee_first_in_lowerlayerproduct) * (ee_second_ip_lowerlayerproduct))))))) + ge_balance_negative_lowerlayerproductoutputimaginary = (((((((((ee_first_rp_lowerlayerproduct) * (ee_second_in_lowerlayerproduct))) + (((ee_first_rn_lowerlayerproduct) * (ee_second_ip_lowerlayerproduct))))) + (((((ee_first_ip_lowerlayerproduct) * (ee_second_rn_lowerlayerproduct))) + (((ee_first_in_lowerlayerproduct) * (ee_second_rp_lowerlayerproduct))))))) + (((((ee_first_ip_lowerlayerproduct) * (ee_second_ip_lowerlayerproduct))) + (((ee_first_in_lowerlayerproduct) * (ee_second_in_lowerlayerproduct))))))) + ge_balance_positive_lowerlayerproductoutputimaginary))))))))) /\ (exists ge_first_rp_lowerlayersum ge_first_rn_lowerlayersum ge_first_ip_lowerlayersum ge_first_in_lowerlayersum ge_second_rp_lowerlayersum ge_second_rn_lowerlayersum ge_second_ip_lowerlayersum ge_second_in_lowerlayersum. ((exists ge_representation_real_code_lowerlayersumfirst ge_representation_imaginary_code_lowerlayersumfirst. (((ee_division_product_lowerlayer) = ((ge_representation_real_code_lowerlayersumfirst) + (ge_representation_imaginary_code_lowerlayersumfirst)) * S ((ge_representation_real_code_lowerlayersumfirst) + (ge_representation_imaginary_code_lowerlayersumfirst)) + ((ge_representation_imaginary_code_lowerlayersumfirst) + (ge_representation_imaginary_code_lowerlayersumfirst))) /\ ((exists ge_balance_positive_lowerlayersumfirstreal ge_balance_negative_lowerlayersumfirstreal. (((((ge_representation_real_code_lowerlayersumfirst) = 2 * (ge_balance_positive_lowerlayersumfirstreal) /\ (ge_balance_negative_lowerlayersumfirstreal) = 0) \/ exists ge_signed_half_lowerlayersumfirstrealdecode. (((ge_representation_real_code_lowerlayersumfirst) = 2 * ge_signed_half_lowerlayersumfirstrealdecode + 1 /\ (ge_balance_positive_lowerlayersumfirstreal) = 0) /\ (ge_balance_negative_lowerlayersumfirstreal) = S ge_signed_half_lowerlayersumfirstrealdecode))) /\ ((ge_first_rp_lowerlayersum) + ge_balance_negative_lowerlayersumfirstreal = (ge_first_rn_lowerlayersum) + ge_balance_positive_lowerlayersumfirstreal))) /\ (exists ge_balance_positive_lowerlayersumfirstimaginary ge_balance_negative_lowerlayersumfirstimaginary. (((((ge_representation_imaginary_code_lowerlayersumfirst) = 2 * (ge_balance_positive_lowerlayersumfirstimaginary) /\ (ge_balance_negative_lowerlayersumfirstimaginary) = 0) \/ exists ge_signed_half_lowerlayersumfirstimaginarydecode. (((ge_representation_imaginary_code_lowerlayersumfirst) = 2 * ge_signed_half_lowerlayersumfirstimaginarydecode + 1 /\ (ge_balance_positive_lowerlayersumfirstimaginary) = 0) /\ (ge_balance_negative_lowerlayersumfirstimaginary) = S ge_signed_half_lowerlayersumfirstimaginarydecode))) /\ ((ge_first_ip_lowerlayersum) + ge_balance_negative_lowerlayersumfirstimaginary = (ge_first_in_lowerlayersum) + ge_balance_positive_lowerlayersumfirstimaginary)))))) /\ ((exists ge_representation_real_code_lowerlayersumsecond ge_representation_imaginary_code_lowerlayersumsecond. (((r) = ((ge_representation_real_code_lowerlayersumsecond) + (ge_representation_imaginary_code_lowerlayersumsecond)) * S ((ge_representation_real_code_lowerlayersumsecond) + (ge_representation_imaginary_code_lowerlayersumsecond)) + ((ge_representation_imaginary_code_lowerlayersumsecond) + (ge_representation_imaginary_code_lowerlayersumsecond))) /\ ((exists ge_balance_positive_lowerlayersumsecondreal ge_balance_negative_lowerlayersumsecondreal. (((((ge_representation_real_code_lowerlayersumsecond) = 2 * (ge_balance_positive_lowerlayersumsecondreal) /\ (ge_balance_negative_lowerlayersumsecondreal) = 0) \/ exists ge_signed_half_lowerlayersumsecondrealdecode. (((ge_representation_real_code_lowerlayersumsecond) = 2 * ge_signed_half_lowerlayersumsecondrealdecode + 1 /\ (ge_balance_positive_lowerlayersumsecondreal) = 0) /\ (ge_balance_negative_lowerlayersumsecondreal) = S ge_signed_half_lowerlayersumsecondrealdecode))) /\ ((ge_second_rp_lowerlayersum) + ge_balance_negative_lowerlayersumsecondreal = (ge_second_rn_lowerlayersum) + ge_balance_positive_lowerlayersumsecondreal))) /\ (exists ge_balance_positive_lowerlayersumsecondimaginary ge_balance_negative_lowerlayersumsecondimaginary. (((((ge_representation_imaginary_code_lowerlayersumsecond) = 2 * (ge_balance_positive_lowerlayersumsecondimaginary) /\ (ge_balance_negative_lowerlayersumsecondimaginary) = 0) \/ exists ge_signed_half_lowerlayersumsecondimaginarydecode. (((ge_representation_imaginary_code_lowerlayersumsecond) = 2 * ge_signed_half_lowerlayersumsecondimaginarydecode + 1 /\ (ge_balance_positive_lowerlayersumsecondimaginary) = 0) /\ (ge_balance_negative_lowerlayersumsecondimaginary) = S ge_signed_half_lowerlayersumsecondimaginarydecode))) /\ ((ge_second_ip_lowerlayersum) + ge_balance_negative_lowerlayersumsecondimaginary = (ge_second_in_lowerlayersum) + ge_balance_positive_lowerlayersumsecondimaginary)))))) /\ (exists ge_representation_real_code_lowerlayersumoutput ge_representation_imaginary_code_lowerlayersumoutput. (((a) = ((ge_representation_real_code_lowerlayersumoutput) + (ge_representation_imaginary_code_lowerlayersumoutput)) * S ((ge_representation_real_code_lowerlayersumoutput) + (ge_representation_imaginary_code_lowerlayersumoutput)) + ((ge_representation_imaginary_code_lowerlayersumoutput) + (ge_representation_imaginary_code_lowerlayersumoutput))) /\ ((exists ge_balance_positive_lowerlayersumoutputreal ge_balance_negative_lowerlayersumoutputreal. (((((ge_representation_real_code_lowerlayersumoutput) = 2 * (ge_balance_positive_lowerlayersumoutputreal) /\ (ge_balance_negative_lowerlayersumoutputreal) = 0) \/ exists ge_signed_half_lowerlayersumoutputrealdecode. (((ge_representation_real_code_lowerlayersumoutput) = 2 * ge_signed_half_lowerlayersumoutputrealdecode + 1 /\ (ge_balance_positive_lowerlayersumoutputreal) = 0) /\ (ge_balance_negative_lowerlayersumoutputreal) = S ge_signed_half_lowerlayersumoutputrealdecode))) /\ ((((ge_first_rp_lowerlayersum) + (ge_second_rp_lowerlayersum))) + ge_balance_negative_lowerlayersumoutputreal = (((ge_first_rn_lowerlayersum) + (ge_second_rn_lowerlayersum))) + ge_balance_positive_lowerlayersumoutputreal))) /\ (exists ge_balance_positive_lowerlayersumoutputimaginary ge_balance_negative_lowerlayersumoutputimaginary. (((((ge_representation_imaginary_code_lowerlayersumoutput) = 2 * (ge_balance_positive_lowerlayersumoutputimaginary) /\ (ge_balance_negative_lowerlayersumoutputimaginary) = 0) \/ exists ge_signed_half_lowerlayersumoutputimaginarydecode. (((ge_representation_imaginary_code_lowerlayersumoutput) = 2 * ge_signed_half_lowerlayersumoutputimaginarydecode + 1 /\ (ge_balance_positive_lowerlayersumoutputimaginary) = 0) /\ (ge_balance_negative_lowerlayersumoutputimaginary) = S ge_signed_half_lowerlayersumoutputimaginarydecode))) /\ ((((ge_first_ip_lowerlayersum) + (ge_second_ip_lowerlayersum))) + ge_balance_negative_lowerlayersumoutputimaginary = (((ge_first_in_lowerlayersum) + (ge_second_in_lowerlayersum))) + ge_balance_positive_lowerlayersumoutputimaginary))))))))))

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