GProduct(b,c,l,P)

exists gr_product_trace_gaussianfactorization gr_product_scale_gaussianfactorization. ((((exists ff_h_gprod_gaussianfactorizationstart. ff_h_gprod_gaussianfactorizationstart + S (6) = S ((S (0)) * gr_product_scale_gaussianfactorization)) /\ exists ff_q_gprod_gaussianfactorizationstart. gr_product_trace_gaussianfactorization = ff_q_gprod_gaussianfactorizationstart * S ((S (0)) * gr_product_scale_gaussianfactorization) + (6))) /\ ((((exists ff_h_gprod_gaussianfactorizationend. ff_h_gprod_gaussianfactorizationend + S ((P)) = S ((S ((l))) * gr_product_scale_gaussianfactorization)) /\ exists ff_q_gprod_gaussianfactorizationend. gr_product_trace_gaussianfactorization = ff_q_gprod_gaussianfactorizationend * S ((S ((l))) * gr_product_scale_gaussianfactorization) + ((P)))) /\ (forall gr_product_index_gaussianfactorizationsteps. (exists ge_gap_gaussianfactorizationstepsindex_bound. ge_gap_gaussianfactorizationstepsindex_bound + S (gr_product_index_gaussianfactorizationsteps) = ((l))) -> exists gr_product_factor_gaussianfactorizationsteps gr_product_before_gaussianfactorizationsteps gr_product_after_gaussianfactorizationsteps. ((((exists ff_h_gprod_gaussianfactorizationstepsfactor. ff_h_gprod_gaussianfactorizationstepsfactor + S (gr_product_factor_gaussianfactorizationsteps) = S ((S (gr_product_index_gaussianfactorizationsteps)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationstepsfactor. (b) = ff_q_gprod_gaussianfactorizationstepsfactor * S ((S (gr_product_index_gaussianfactorizationsteps)) * (c)) + (gr_product_factor_gaussianfactorizationsteps))) /\ ((((exists ff_h_gprod_gaussianfactorizationstepsbefore. ff_h_gprod_gaussianfactorizationstepsbefore + S (gr_product_before_gaussianfactorizationsteps) = S ((S (gr_product_index_gaussianfactorizationsteps)) * gr_product_scale_gaussianfactorization)) /\ exists ff_q_gprod_gaussianfactorizationstepsbefore. gr_product_trace_gaussianfactorization = ff_q_gprod_gaussianfactorizationstepsbefore * S ((S (gr_product_index_gaussianfactorizationsteps)) * gr_product_scale_gaussianfactorization) + (gr_product_before_gaussianfactorizationsteps))) /\ ((((exists ff_h_gprod_gaussianfactorizationstepsafter. ff_h_gprod_gaussianfactorizationstepsafter + S (gr_product_after_gaussianfactorizationsteps) = S ((S (S (gr_product_index_gaussianfactorizationsteps))) * gr_product_scale_gaussianfactorization)) /\ exists ff_q_gprod_gaussianfactorizationstepsafter. gr_product_trace_gaussianfactorization = ff_q_gprod_gaussianfactorizationstepsafter * S ((S (S (gr_product_index_gaussianfactorizationsteps))) * gr_product_scale_gaussianfactorization) + (gr_product_after_gaussianfactorizationsteps))) /\ (exists ge_first_rp_gaussianfactorizationstepsmultiply ge_first_rn_gaussianfactorizationstepsmultiply ge_first_ip_gaussianfactorizationstepsmultiply ge_first_in_gaussianfactorizationstepsmultiply ge_second_rp_gaussianfactorizationstepsmultiply ge_second_rn_gaussianfactorizationstepsmultiply ge_second_ip_gaussianfactorizationstepsmultiply ge_second_in_gaussianfactorizationstepsmultiply. ((exists ge_representation_real_code_gaussianfactorizationstepsmultiplyfirst ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyfirst. (((gr_product_before_gaussianfactorizationsteps) = ((ge_representation_real_code_gaussianfactorizationstepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyfirst)) * S ((ge_representation_real_code_gaussianfactorizationstepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationstepsmultiplyfirstreal ge_balance_negative_gaussianfactorizationstepsmultiplyfirstreal. (((((ge_representation_real_code_gaussianfactorizationstepsmultiplyfirst) = 2 * (ge_balance_positive_gaussianfactorizationstepsmultiplyfirstreal) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationstepsmultiplyfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationstepsmultiplyfirst) = 2 * ge_signed_half_gaussianfactorizationstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplyfirstreal) = S ge_signed_half_gaussianfactorizationstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationstepsmultiply) + ge_balance_negative_gaussianfactorizationstepsmultiplyfirstreal = (ge_first_rn_gaussianfactorizationstepsmultiply) + ge_balance_positive_gaussianfactorizationstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationstepsmultiplyfirstimaginary ge_balance_negative_gaussianfactorizationstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyfirst) = 2 * (ge_balance_positive_gaussianfactorizationstepsmultiplyfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyfirst) = 2 * ge_signed_half_gaussianfactorizationstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplyfirstimaginary) = S ge_signed_half_gaussianfactorizationstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationstepsmultiply) + ge_balance_negative_gaussianfactorizationstepsmultiplyfirstimaginary = (ge_first_in_gaussianfactorizationstepsmultiply) + ge_balance_positive_gaussianfactorizationstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationstepsmultiplysecond ge_representation_imaginary_code_gaussianfactorizationstepsmultiplysecond. (((gr_product_factor_gaussianfactorizationsteps) = ((ge_representation_real_code_gaussianfactorizationstepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplysecond)) * S ((ge_representation_real_code_gaussianfactorizationstepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationstepsmultiplysecondreal ge_balance_negative_gaussianfactorizationstepsmultiplysecondreal. (((((ge_representation_real_code_gaussianfactorizationstepsmultiplysecond) = 2 * (ge_balance_positive_gaussianfactorizationstepsmultiplysecondreal) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationstepsmultiplysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationstepsmultiplysecond) = 2 * ge_signed_half_gaussianfactorizationstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplysecondreal) = S ge_signed_half_gaussianfactorizationstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationstepsmultiply) + ge_balance_negative_gaussianfactorizationstepsmultiplysecondreal = (ge_second_rn_gaussianfactorizationstepsmultiply) + ge_balance_positive_gaussianfactorizationstepsmultiplysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationstepsmultiplysecondimaginary ge_balance_negative_gaussianfactorizationstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplysecond) = 2 * (ge_balance_positive_gaussianfactorizationstepsmultiplysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplysecond) = 2 * ge_signed_half_gaussianfactorizationstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplysecondimaginary) = S ge_signed_half_gaussianfactorizationstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationstepsmultiply) + ge_balance_negative_gaussianfactorizationstepsmultiplysecondimaginary = (ge_second_in_gaussianfactorizationstepsmultiply) + ge_balance_positive_gaussianfactorizationstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationstepsmultiplyoutput ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyoutput. (((gr_product_after_gaussianfactorizationsteps) = ((ge_representation_real_code_gaussianfactorizationstepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyoutput)) * S ((ge_representation_real_code_gaussianfactorizationstepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationstepsmultiplyoutputreal ge_balance_negative_gaussianfactorizationstepsmultiplyoutputreal. (((((ge_representation_real_code_gaussianfactorizationstepsmultiplyoutput) = 2 * (ge_balance_positive_gaussianfactorizationstepsmultiplyoutputreal) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationstepsmultiplyoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationstepsmultiplyoutput) = 2 * ge_signed_half_gaussianfactorizationstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplyoutputreal) = S ge_signed_half_gaussianfactorizationstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationstepsmultiply) * (ge_second_rp_gaussianfactorizationstepsmultiply))) + (((ge_first_rn_gaussianfactorizationstepsmultiply) * (ge_second_rn_gaussianfactorizationstepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationstepsmultiply) * (ge_second_in_gaussianfactorizationstepsmultiply))) + (((ge_first_in_gaussianfactorizationstepsmultiply) * (ge_second_ip_gaussianfactorizationstepsmultiply))))))) + ge_balance_negative_gaussianfactorizationstepsmultiplyoutputreal = (((((((ge_first_rp_gaussianfactorizationstepsmultiply) * (ge_second_rn_gaussianfactorizationstepsmultiply))) + (((ge_first_rn_gaussianfactorizationstepsmultiply) * (ge_second_rp_gaussianfactorizationstepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationstepsmultiply) * (ge_second_ip_gaussianfactorizationstepsmultiply))) + (((ge_first_in_gaussianfactorizationstepsmultiply) * (ge_second_in_gaussianfactorizationstepsmultiply))))))) + ge_balance_positive_gaussianfactorizationstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationstepsmultiplyoutputimaginary ge_balance_negative_gaussianfactorizationstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyoutput) = 2 * (ge_balance_positive_gaussianfactorizationstepsmultiplyoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationstepsmultiplyoutput) = 2 * ge_signed_half_gaussianfactorizationstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationstepsmultiplyoutputimaginary) = S ge_signed_half_gaussianfactorizationstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationstepsmultiply) * (ge_second_ip_gaussianfactorizationstepsmultiply))) + (((ge_first_rn_gaussianfactorizationstepsmultiply) * (ge_second_in_gaussianfactorizationstepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationstepsmultiply) * (ge_second_rp_gaussianfactorizationstepsmultiply))) + (((ge_first_in_gaussianfactorizationstepsmultiply) * (ge_second_rn_gaussianfactorizationstepsmultiply))))))) + ge_balance_negative_gaussianfactorizationstepsmultiplyoutputimaginary = (((((((ge_first_rp_gaussianfactorizationstepsmultiply) * (ge_second_in_gaussianfactorizationstepsmultiply))) + (((ge_first_rn_gaussianfactorizationstepsmultiply) * (ge_second_ip_gaussianfactorizationstepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationstepsmultiply) * (ge_second_rn_gaussianfactorizationstepsmultiply))) + (((ge_first_in_gaussianfactorizationstepsmultiply) * (ge_second_rp_gaussianfactorizationstepsmultiply))))))) + ge_balance_positive_gaussianfactorizationstepsmultiplyoutputimaginary)))))))))))))))

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