GProductStep(b,c,h,e,i)

exists gr_step_factor_gaussianfactorization gr_step_before_gaussianfactorization gr_step_after_gaussianfactorization. ((((exists ff_h_gprod_gaussianfactorizationfactor. ff_h_gprod_gaussianfactorizationfactor + S (gr_step_factor_gaussianfactorization) = S ((S ((i))) * (c))) /\ exists ff_q_gprod_gaussianfactorizationfactor. (b) = ff_q_gprod_gaussianfactorizationfactor * S ((S ((i))) * (c)) + (gr_step_factor_gaussianfactorization))) /\ ((((exists ff_h_gprod_gaussianfactorizationbefore. ff_h_gprod_gaussianfactorizationbefore + S (gr_step_before_gaussianfactorization) = S ((S ((i))) * (e))) /\ exists ff_q_gprod_gaussianfactorizationbefore. (h) = ff_q_gprod_gaussianfactorizationbefore * S ((S ((i))) * (e)) + (gr_step_before_gaussianfactorization))) /\ ((((exists ff_h_gprod_gaussianfactorizationafter. ff_h_gprod_gaussianfactorizationafter + S (gr_step_after_gaussianfactorization) = S ((S (S ((i)))) * (e))) /\ exists ff_q_gprod_gaussianfactorizationafter. (h) = ff_q_gprod_gaussianfactorizationafter * S ((S (S ((i)))) * (e)) + (gr_step_after_gaussianfactorization))) /\ (exists ge_first_rp_gaussianfactorizationmultiply ge_first_rn_gaussianfactorizationmultiply ge_first_ip_gaussianfactorizationmultiply ge_first_in_gaussianfactorizationmultiply ge_second_rp_gaussianfactorizationmultiply ge_second_rn_gaussianfactorizationmultiply ge_second_ip_gaussianfactorizationmultiply ge_second_in_gaussianfactorizationmultiply. ((exists ge_representation_real_code_gaussianfactorizationmultiplyfirst ge_representation_imaginary_code_gaussianfactorizationmultiplyfirst. (((gr_step_before_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationmultiplyfirst)) * S ((ge_representation_real_code_gaussianfactorizationmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationmultiplyfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationmultiplyfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationmultiplyfirstreal ge_balance_negative_gaussianfactorizationmultiplyfirstreal. (((((ge_representation_real_code_gaussianfactorizationmultiplyfirst) = 2 * (ge_balance_positive_gaussianfactorizationmultiplyfirstreal) /\ (ge_balance_negative_gaussianfactorizationmultiplyfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmultiplyfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationmultiplyfirst) = 2 * ge_signed_half_gaussianfactorizationmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmultiplyfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmultiplyfirstreal) = S ge_signed_half_gaussianfactorizationmultiplyfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationmultiply) + ge_balance_negative_gaussianfactorizationmultiplyfirstreal = (ge_first_rn_gaussianfactorizationmultiply) + ge_balance_positive_gaussianfactorizationmultiplyfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationmultiplyfirstimaginary ge_balance_negative_gaussianfactorizationmultiplyfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmultiplyfirst) = 2 * (ge_balance_positive_gaussianfactorizationmultiplyfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmultiplyfirst) = 2 * ge_signed_half_gaussianfactorizationmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmultiplyfirstimaginary) = S ge_signed_half_gaussianfactorizationmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationmultiply) + ge_balance_negative_gaussianfactorizationmultiplyfirstimaginary = (ge_first_in_gaussianfactorizationmultiply) + ge_balance_positive_gaussianfactorizationmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationmultiplysecond ge_representation_imaginary_code_gaussianfactorizationmultiplysecond. (((gr_step_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationmultiplysecond)) * S ((ge_representation_real_code_gaussianfactorizationmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationmultiplysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationmultiplysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationmultiplysecondreal ge_balance_negative_gaussianfactorizationmultiplysecondreal. (((((ge_representation_real_code_gaussianfactorizationmultiplysecond) = 2 * (ge_balance_positive_gaussianfactorizationmultiplysecondreal) /\ (ge_balance_negative_gaussianfactorizationmultiplysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmultiplysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationmultiplysecond) = 2 * ge_signed_half_gaussianfactorizationmultiplysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmultiplysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmultiplysecondreal) = S ge_signed_half_gaussianfactorizationmultiplysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationmultiply) + ge_balance_negative_gaussianfactorizationmultiplysecondreal = (ge_second_rn_gaussianfactorizationmultiply) + ge_balance_positive_gaussianfactorizationmultiplysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationmultiplysecondimaginary ge_balance_negative_gaussianfactorizationmultiplysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmultiplysecond) = 2 * (ge_balance_positive_gaussianfactorizationmultiplysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationmultiplysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmultiplysecond) = 2 * ge_signed_half_gaussianfactorizationmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmultiplysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmultiplysecondimaginary) = S ge_signed_half_gaussianfactorizationmultiplysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationmultiply) + ge_balance_negative_gaussianfactorizationmultiplysecondimaginary = (ge_second_in_gaussianfactorizationmultiply) + ge_balance_positive_gaussianfactorizationmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationmultiplyoutput ge_representation_imaginary_code_gaussianfactorizationmultiplyoutput. (((gr_step_after_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationmultiplyoutput)) * S ((ge_representation_real_code_gaussianfactorizationmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationmultiplyoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationmultiplyoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationmultiplyoutputreal ge_balance_negative_gaussianfactorizationmultiplyoutputreal. (((((ge_representation_real_code_gaussianfactorizationmultiplyoutput) = 2 * (ge_balance_positive_gaussianfactorizationmultiplyoutputreal) /\ (ge_balance_negative_gaussianfactorizationmultiplyoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmultiplyoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationmultiplyoutput) = 2 * ge_signed_half_gaussianfactorizationmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmultiplyoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmultiplyoutputreal) = S ge_signed_half_gaussianfactorizationmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmultiply) * (ge_second_rp_gaussianfactorizationmultiply))) + (((ge_first_rn_gaussianfactorizationmultiply) * (ge_second_rn_gaussianfactorizationmultiply))))) + (((((ge_first_ip_gaussianfactorizationmultiply) * (ge_second_in_gaussianfactorizationmultiply))) + (((ge_first_in_gaussianfactorizationmultiply) * (ge_second_ip_gaussianfactorizationmultiply))))))) + ge_balance_negative_gaussianfactorizationmultiplyoutputreal = (((((((ge_first_rp_gaussianfactorizationmultiply) * (ge_second_rn_gaussianfactorizationmultiply))) + (((ge_first_rn_gaussianfactorizationmultiply) * (ge_second_rp_gaussianfactorizationmultiply))))) + (((((ge_first_ip_gaussianfactorizationmultiply) * (ge_second_ip_gaussianfactorizationmultiply))) + (((ge_first_in_gaussianfactorizationmultiply) * (ge_second_in_gaussianfactorizationmultiply))))))) + ge_balance_positive_gaussianfactorizationmultiplyoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationmultiplyoutputimaginary ge_balance_negative_gaussianfactorizationmultiplyoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmultiplyoutput) = 2 * (ge_balance_positive_gaussianfactorizationmultiplyoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmultiplyoutput) = 2 * ge_signed_half_gaussianfactorizationmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmultiplyoutputimaginary) = S ge_signed_half_gaussianfactorizationmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmultiply) * (ge_second_ip_gaussianfactorizationmultiply))) + (((ge_first_rn_gaussianfactorizationmultiply) * (ge_second_in_gaussianfactorizationmultiply))))) + (((((ge_first_ip_gaussianfactorizationmultiply) * (ge_second_rp_gaussianfactorizationmultiply))) + (((ge_first_in_gaussianfactorizationmultiply) * (ge_second_rn_gaussianfactorizationmultiply))))))) + ge_balance_negative_gaussianfactorizationmultiplyoutputimaginary = (((((((ge_first_rp_gaussianfactorizationmultiply) * (ge_second_in_gaussianfactorizationmultiply))) + (((ge_first_rn_gaussianfactorizationmultiply) * (ge_second_ip_gaussianfactorizationmultiply))))) + (((((ge_first_ip_gaussianfactorizationmultiply) * (ge_second_rn_gaussianfactorizationmultiply))) + (((ge_first_in_gaussianfactorizationmultiply) * (ge_second_rp_gaussianfactorizationmultiply))))))) + ge_balance_positive_gaussianfactorizationmultiplyoutputimaginary))))))))))))

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