GMul(a,b,c)

exists ge_first_rp_lowerlayer ge_first_rn_lowerlayer ge_first_ip_lowerlayer ge_first_in_lowerlayer ge_second_rp_lowerlayer ge_second_rn_lowerlayer ge_second_ip_lowerlayer ge_second_in_lowerlayer. ((exists ge_representation_real_code_lowerlayerfirst ge_representation_imaginary_code_lowerlayerfirst. (((a) = ((ge_representation_real_code_lowerlayerfirst) + (ge_representation_imaginary_code_lowerlayerfirst)) * S ((ge_representation_real_code_lowerlayerfirst) + (ge_representation_imaginary_code_lowerlayerfirst)) + ((ge_representation_imaginary_code_lowerlayerfirst) + (ge_representation_imaginary_code_lowerlayerfirst))) /\ ((exists ge_balance_positive_lowerlayerfirstreal ge_balance_negative_lowerlayerfirstreal. (((((ge_representation_real_code_lowerlayerfirst) = 2 * (ge_balance_positive_lowerlayerfirstreal) /\ (ge_balance_negative_lowerlayerfirstreal) = 0) \/ exists ge_signed_half_lowerlayerfirstrealdecode. (((ge_representation_real_code_lowerlayerfirst) = 2 * ge_signed_half_lowerlayerfirstrealdecode + 1 /\ (ge_balance_positive_lowerlayerfirstreal) = 0) /\ (ge_balance_negative_lowerlayerfirstreal) = S ge_signed_half_lowerlayerfirstrealdecode))) /\ ((ge_first_rp_lowerlayer) + ge_balance_negative_lowerlayerfirstreal = (ge_first_rn_lowerlayer) + ge_balance_positive_lowerlayerfirstreal))) /\ (exists ge_balance_positive_lowerlayerfirstimaginary ge_balance_negative_lowerlayerfirstimaginary. (((((ge_representation_imaginary_code_lowerlayerfirst) = 2 * (ge_balance_positive_lowerlayerfirstimaginary) /\ (ge_balance_negative_lowerlayerfirstimaginary) = 0) \/ exists ge_signed_half_lowerlayerfirstimaginarydecode. (((ge_representation_imaginary_code_lowerlayerfirst) = 2 * ge_signed_half_lowerlayerfirstimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerfirstimaginary) = 0) /\ (ge_balance_negative_lowerlayerfirstimaginary) = S ge_signed_half_lowerlayerfirstimaginarydecode))) /\ ((ge_first_ip_lowerlayer) + ge_balance_negative_lowerlayerfirstimaginary = (ge_first_in_lowerlayer) + ge_balance_positive_lowerlayerfirstimaginary)))))) /\ ((exists ge_representation_real_code_lowerlayersecond ge_representation_imaginary_code_lowerlayersecond. (((b) = ((ge_representation_real_code_lowerlayersecond) + (ge_representation_imaginary_code_lowerlayersecond)) * S ((ge_representation_real_code_lowerlayersecond) + (ge_representation_imaginary_code_lowerlayersecond)) + ((ge_representation_imaginary_code_lowerlayersecond) + (ge_representation_imaginary_code_lowerlayersecond))) /\ ((exists ge_balance_positive_lowerlayersecondreal ge_balance_negative_lowerlayersecondreal. (((((ge_representation_real_code_lowerlayersecond) = 2 * (ge_balance_positive_lowerlayersecondreal) /\ (ge_balance_negative_lowerlayersecondreal) = 0) \/ exists ge_signed_half_lowerlayersecondrealdecode. (((ge_representation_real_code_lowerlayersecond) = 2 * ge_signed_half_lowerlayersecondrealdecode + 1 /\ (ge_balance_positive_lowerlayersecondreal) = 0) /\ (ge_balance_negative_lowerlayersecondreal) = S ge_signed_half_lowerlayersecondrealdecode))) /\ ((ge_second_rp_lowerlayer) + ge_balance_negative_lowerlayersecondreal = (ge_second_rn_lowerlayer) + ge_balance_positive_lowerlayersecondreal))) /\ (exists ge_balance_positive_lowerlayersecondimaginary ge_balance_negative_lowerlayersecondimaginary. (((((ge_representation_imaginary_code_lowerlayersecond) = 2 * (ge_balance_positive_lowerlayersecondimaginary) /\ (ge_balance_negative_lowerlayersecondimaginary) = 0) \/ exists ge_signed_half_lowerlayersecondimaginarydecode. (((ge_representation_imaginary_code_lowerlayersecond) = 2 * ge_signed_half_lowerlayersecondimaginarydecode + 1 /\ (ge_balance_positive_lowerlayersecondimaginary) = 0) /\ (ge_balance_negative_lowerlayersecondimaginary) = S ge_signed_half_lowerlayersecondimaginarydecode))) /\ ((ge_second_ip_lowerlayer) + ge_balance_negative_lowerlayersecondimaginary = (ge_second_in_lowerlayer) + ge_balance_positive_lowerlayersecondimaginary)))))) /\ (exists ge_representation_real_code_lowerlayeroutput ge_representation_imaginary_code_lowerlayeroutput. (((c) = ((ge_representation_real_code_lowerlayeroutput) + (ge_representation_imaginary_code_lowerlayeroutput)) * S ((ge_representation_real_code_lowerlayeroutput) + (ge_representation_imaginary_code_lowerlayeroutput)) + ((ge_representation_imaginary_code_lowerlayeroutput) + (ge_representation_imaginary_code_lowerlayeroutput))) /\ ((exists ge_balance_positive_lowerlayeroutputreal ge_balance_negative_lowerlayeroutputreal. (((((ge_representation_real_code_lowerlayeroutput) = 2 * (ge_balance_positive_lowerlayeroutputreal) /\ (ge_balance_negative_lowerlayeroutputreal) = 0) \/ exists ge_signed_half_lowerlayeroutputrealdecode. (((ge_representation_real_code_lowerlayeroutput) = 2 * ge_signed_half_lowerlayeroutputrealdecode + 1 /\ (ge_balance_positive_lowerlayeroutputreal) = 0) /\ (ge_balance_negative_lowerlayeroutputreal) = S ge_signed_half_lowerlayeroutputrealdecode))) /\ ((((((((ge_first_rp_lowerlayer) * (ge_second_rp_lowerlayer))) + (((ge_first_rn_lowerlayer) * (ge_second_rn_lowerlayer))))) + (((((ge_first_ip_lowerlayer) * (ge_second_in_lowerlayer))) + (((ge_first_in_lowerlayer) * (ge_second_ip_lowerlayer))))))) + ge_balance_negative_lowerlayeroutputreal = (((((((ge_first_rp_lowerlayer) * (ge_second_rn_lowerlayer))) + (((ge_first_rn_lowerlayer) * (ge_second_rp_lowerlayer))))) + (((((ge_first_ip_lowerlayer) * (ge_second_ip_lowerlayer))) + (((ge_first_in_lowerlayer) * (ge_second_in_lowerlayer))))))) + ge_balance_positive_lowerlayeroutputreal))) /\ (exists ge_balance_positive_lowerlayeroutputimaginary ge_balance_negative_lowerlayeroutputimaginary. (((((ge_representation_imaginary_code_lowerlayeroutput) = 2 * (ge_balance_positive_lowerlayeroutputimaginary) /\ (ge_balance_negative_lowerlayeroutputimaginary) = 0) \/ exists ge_signed_half_lowerlayeroutputimaginarydecode. (((ge_representation_imaginary_code_lowerlayeroutput) = 2 * ge_signed_half_lowerlayeroutputimaginarydecode + 1 /\ (ge_balance_positive_lowerlayeroutputimaginary) = 0) /\ (ge_balance_negative_lowerlayeroutputimaginary) = S ge_signed_half_lowerlayeroutputimaginarydecode))) /\ ((((((((ge_first_rp_lowerlayer) * (ge_second_ip_lowerlayer))) + (((ge_first_rn_lowerlayer) * (ge_second_in_lowerlayer))))) + (((((ge_first_ip_lowerlayer) * (ge_second_rp_lowerlayer))) + (((ge_first_in_lowerlayer) * (ge_second_rn_lowerlayer))))))) + ge_balance_negative_lowerlayeroutputimaginary = (((((((ge_first_rp_lowerlayer) * (ge_second_in_lowerlayer))) + (((ge_first_rn_lowerlayer) * (ge_second_ip_lowerlayer))))) + (((((ge_first_ip_lowerlayer) * (ge_second_rn_lowerlayer))) + (((ge_first_in_lowerlayer) * (ge_second_rp_lowerlayer))))))) + ge_balance_positive_lowerlayeroutputimaginary))))))))

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