CRTNormalizedPrefixSolution(r,s,b,c,l,x,M)

((((forall gcrt_common_index_gfull_secondwave_lcm_own gcrt_common_modulus_gfull_secondwave_lcm_own. (exists ff_lt_gcrt_gfull_secondwave_lcm_own_bound. ff_lt_gcrt_gfull_secondwave_lcm_own_bound + S gcrt_common_index_gfull_secondwave_lcm_own = l) -> (((exists ff_h_gcrt_gfull_secondwave_lcm_own_entry. ff_h_gcrt_gfull_secondwave_lcm_own_entry + S (gcrt_common_modulus_gfull_secondwave_lcm_own) = S ((S (gcrt_common_index_gfull_secondwave_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_secondwave_lcm_own_entry. b = ff_q_gcrt_gfull_secondwave_lcm_own_entry * S ((S (gcrt_common_index_gfull_secondwave_lcm_own)) * c) + (gcrt_common_modulus_gfull_secondwave_lcm_own))) -> exists gcrt_common_quotient_gfull_secondwave_lcm_own. M = gcrt_common_modulus_gfull_secondwave_lcm_own * gcrt_common_quotient_gfull_secondwave_lcm_own) /\ forall gcrt_lcm_common_gfull_secondwave_lcm. (forall gcrt_common_index_gfull_secondwave_lcm_other gcrt_common_modulus_gfull_secondwave_lcm_other. (exists ff_lt_gcrt_gfull_secondwave_lcm_other_bound. ff_lt_gcrt_gfull_secondwave_lcm_other_bound + S gcrt_common_index_gfull_secondwave_lcm_other = l) -> (((exists ff_h_gcrt_gfull_secondwave_lcm_other_entry. ff_h_gcrt_gfull_secondwave_lcm_other_entry + S (gcrt_common_modulus_gfull_secondwave_lcm_other) = S ((S (gcrt_common_index_gfull_secondwave_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_secondwave_lcm_other_entry. b = ff_q_gcrt_gfull_secondwave_lcm_other_entry * S ((S (gcrt_common_index_gfull_secondwave_lcm_other)) * c) + (gcrt_common_modulus_gfull_secondwave_lcm_other))) -> exists gcrt_common_quotient_gfull_secondwave_lcm_other. gcrt_lcm_common_gfull_secondwave_lcm = gcrt_common_modulus_gfull_secondwave_lcm_other * gcrt_common_quotient_gfull_secondwave_lcm_other) -> exists gcrt_lcm_quotient_gfull_secondwave_lcm. gcrt_lcm_common_gfull_secondwave_lcm = M * gcrt_lcm_quotient_gfull_secondwave_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_secondwave_bound. ff_lt_gcrt_gfull_secondwave_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_secondwave_solution gcrt_solution_residue_gfull_secondwave_solution gcrt_solution_modulus_gfull_secondwave_solution. (exists ff_lt_gcrt_gfull_secondwave_solution_bound. ff_lt_gcrt_gfull_secondwave_solution_bound + S gcrt_solution_index_gfull_secondwave_solution = l) -> (((exists ff_h_gcrt_gfull_secondwave_solution_residue. ff_h_gcrt_gfull_secondwave_solution_residue + S (gcrt_solution_residue_gfull_secondwave_solution) = S ((S (gcrt_solution_index_gfull_secondwave_solution)) * s)) /\ exists ff_q_gcrt_gfull_secondwave_solution_residue. r = ff_q_gcrt_gfull_secondwave_solution_residue * S ((S (gcrt_solution_index_gfull_secondwave_solution)) * s) + (gcrt_solution_residue_gfull_secondwave_solution))) -> (((exists ff_h_gcrt_gfull_secondwave_solution_modulus. ff_h_gcrt_gfull_secondwave_solution_modulus + S (gcrt_solution_modulus_gfull_secondwave_solution) = S ((S (gcrt_solution_index_gfull_secondwave_solution)) * c)) /\ exists ff_q_gcrt_gfull_secondwave_solution_modulus. b = ff_q_gcrt_gfull_secondwave_solution_modulus * S ((S (gcrt_solution_index_gfull_secondwave_solution)) * c) + (gcrt_solution_modulus_gfull_secondwave_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_secondwave_solution_congruence hgcrt_mod_right_gcrt_gfull_secondwave_solution_congruence. x + gcrt_solution_modulus_gfull_secondwave_solution * hgcrt_mod_left_gcrt_gfull_secondwave_solution_congruence = gcrt_solution_residue_gfull_secondwave_solution + gcrt_solution_modulus_gfull_secondwave_solution * hgcrt_mod_right_gcrt_gfull_secondwave_solution_congruence))))

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