CRTPrefixSolution(r,s,b,c,l,x)

Hygienic expanded first-order definition

forall gcrt_solution_index_research gcrt_solution_residue_research gcrt_solution_modulus_research. (exists ff_lt_gcrt_research_bound. ff_lt_gcrt_research_bound + S gcrt_solution_index_research = l) -> (((exists ff_h_gcrt_research_residue. ff_h_gcrt_research_residue + S (gcrt_solution_residue_research) = S ((S (gcrt_solution_index_research)) * s)) /\ exists ff_q_gcrt_research_residue. r = ff_q_gcrt_research_residue * S ((S (gcrt_solution_index_research)) * s) + (gcrt_solution_residue_research))) -> (((exists ff_h_gcrt_research_modulus. ff_h_gcrt_research_modulus + S (gcrt_solution_modulus_research) = S ((S (gcrt_solution_index_research)) * c)) /\ exists ff_q_gcrt_research_modulus. b = ff_q_gcrt_research_modulus * S ((S (gcrt_solution_index_research)) * c) + (gcrt_solution_modulus_research))) -> (exists hgcrt_mod_left_gcrt_research_congruence hgcrt_mod_right_gcrt_research_congruence. x + gcrt_solution_modulus_research * hgcrt_mod_left_gcrt_research_congruence = gcrt_solution_residue_research + gcrt_solution_modulus_research * hgcrt_mod_right_gcrt_research_congruence)

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

Direct definition dependencies

Definitions depending on this notation

Checked theorems using this definition