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

Hygienic expanded first-order definition

((((forall gcrt_common_index_research_lcm_own gcrt_common_modulus_research_lcm_own. (exists ff_lt_gcrt_research_lcm_own_bound. ff_lt_gcrt_research_lcm_own_bound + S gcrt_common_index_research_lcm_own = l) -> (((exists ff_h_gcrt_research_lcm_own_entry. ff_h_gcrt_research_lcm_own_entry + S (gcrt_common_modulus_research_lcm_own) = S ((S (gcrt_common_index_research_lcm_own)) * c)) /\ exists ff_q_gcrt_research_lcm_own_entry. b = ff_q_gcrt_research_lcm_own_entry * S ((S (gcrt_common_index_research_lcm_own)) * c) + (gcrt_common_modulus_research_lcm_own))) -> exists gcrt_common_quotient_research_lcm_own. M = gcrt_common_modulus_research_lcm_own * gcrt_common_quotient_research_lcm_own) /\ forall gcrt_lcm_common_research_lcm. (forall gcrt_common_index_research_lcm_other gcrt_common_modulus_research_lcm_other. (exists ff_lt_gcrt_research_lcm_other_bound. ff_lt_gcrt_research_lcm_other_bound + S gcrt_common_index_research_lcm_other = l) -> (((exists ff_h_gcrt_research_lcm_other_entry. ff_h_gcrt_research_lcm_other_entry + S (gcrt_common_modulus_research_lcm_other) = S ((S (gcrt_common_index_research_lcm_other)) * c)) /\ exists ff_q_gcrt_research_lcm_other_entry. b = ff_q_gcrt_research_lcm_other_entry * S ((S (gcrt_common_index_research_lcm_other)) * c) + (gcrt_common_modulus_research_lcm_other))) -> exists gcrt_common_quotient_research_lcm_other. gcrt_lcm_common_research_lcm = gcrt_common_modulus_research_lcm_other * gcrt_common_quotient_research_lcm_other) -> exists gcrt_lcm_quotient_research_lcm. gcrt_lcm_common_research_lcm = M * gcrt_lcm_quotient_research_lcm)) /\ ((exists ff_lt_gcrt_research_bounded. ff_lt_gcrt_research_bounded + S x = M) /\ (forall gcrt_solution_index_research_solution gcrt_solution_residue_research_solution gcrt_solution_modulus_research_solution. (exists ff_lt_gcrt_research_solution_bound. ff_lt_gcrt_research_solution_bound + S gcrt_solution_index_research_solution = l) -> (((exists ff_h_gcrt_research_solution_residue. ff_h_gcrt_research_solution_residue + S (gcrt_solution_residue_research_solution) = S ((S (gcrt_solution_index_research_solution)) * s)) /\ exists ff_q_gcrt_research_solution_residue. r = ff_q_gcrt_research_solution_residue * S ((S (gcrt_solution_index_research_solution)) * s) + (gcrt_solution_residue_research_solution))) -> (((exists ff_h_gcrt_research_solution_modulus. ff_h_gcrt_research_solution_modulus + S (gcrt_solution_modulus_research_solution) = S ((S (gcrt_solution_index_research_solution)) * c)) /\ exists ff_q_gcrt_research_solution_modulus. b = ff_q_gcrt_research_solution_modulus * S ((S (gcrt_solution_index_research_solution)) * c) + (gcrt_solution_modulus_research_solution))) -> (exists hgcrt_mod_left_gcrt_research_solution_congruence hgcrt_mod_right_gcrt_research_solution_congruence. x + gcrt_solution_modulus_research_solution * hgcrt_mod_left_gcrt_research_solution_congruence = gcrt_solution_residue_research_solution + gcrt_solution_modulus_research_solution * hgcrt_mod_right_gcrt_research_solution_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