CRTMergeCompatiblePrefix(r,s,b,c,l)

Hygienic expanded first-order definition

forall gcomp_merge_index_breakthrough gcomp_merge_solution_breakthrough gcomp_merge_lcm_breakthrough gcomp_merge_residue_breakthrough gcomp_merge_modulus_breakthrough gcomp_merge_gcd_breakthrough. (exists ff_lt_gcrt_breakthrough_bound. ff_lt_gcrt_breakthrough_bound + S gcomp_merge_index_breakthrough = l) -> (((forall gcrt_common_index_breakthrough_lcm_own gcrt_common_modulus_breakthrough_lcm_own. (exists ff_lt_gcrt_breakthrough_lcm_own_bound. ff_lt_gcrt_breakthrough_lcm_own_bound + S gcrt_common_index_breakthrough_lcm_own = gcomp_merge_index_breakthrough) -> (((exists ff_h_gcrt_breakthrough_lcm_own_entry. ff_h_gcrt_breakthrough_lcm_own_entry + S (gcrt_common_modulus_breakthrough_lcm_own) = S ((S (gcrt_common_index_breakthrough_lcm_own)) * c)) /\ exists ff_q_gcrt_breakthrough_lcm_own_entry. b = ff_q_gcrt_breakthrough_lcm_own_entry * S ((S (gcrt_common_index_breakthrough_lcm_own)) * c) + (gcrt_common_modulus_breakthrough_lcm_own))) -> exists gcrt_common_quotient_breakthrough_lcm_own. gcomp_merge_lcm_breakthrough = gcrt_common_modulus_breakthrough_lcm_own * gcrt_common_quotient_breakthrough_lcm_own) /\ forall gcrt_lcm_common_breakthrough_lcm. (forall gcrt_common_index_breakthrough_lcm_other gcrt_common_modulus_breakthrough_lcm_other. (exists ff_lt_gcrt_breakthrough_lcm_other_bound. ff_lt_gcrt_breakthrough_lcm_other_bound + S gcrt_common_index_breakthrough_lcm_other = gcomp_merge_index_breakthrough) -> (((exists ff_h_gcrt_breakthrough_lcm_other_entry. ff_h_gcrt_breakthrough_lcm_other_entry + S (gcrt_common_modulus_breakthrough_lcm_other) = S ((S (gcrt_common_index_breakthrough_lcm_other)) * c)) /\ exists ff_q_gcrt_breakthrough_lcm_other_entry. b = ff_q_gcrt_breakthrough_lcm_other_entry * S ((S (gcrt_common_index_breakthrough_lcm_other)) * c) + (gcrt_common_modulus_breakthrough_lcm_other))) -> exists gcrt_common_quotient_breakthrough_lcm_other. gcrt_lcm_common_breakthrough_lcm = gcrt_common_modulus_breakthrough_lcm_other * gcrt_common_quotient_breakthrough_lcm_other) -> exists gcrt_lcm_quotient_breakthrough_lcm. gcrt_lcm_common_breakthrough_lcm = gcomp_merge_lcm_breakthrough * gcrt_lcm_quotient_breakthrough_lcm)) -> (forall gcrt_solution_index_breakthrough_solution gcrt_solution_residue_breakthrough_solution gcrt_solution_modulus_breakthrough_solution. (exists ff_lt_gcrt_breakthrough_solution_bound. ff_lt_gcrt_breakthrough_solution_bound + S gcrt_solution_index_breakthrough_solution = gcomp_merge_index_breakthrough) -> (((exists ff_h_gcrt_breakthrough_solution_residue. ff_h_gcrt_breakthrough_solution_residue + S (gcrt_solution_residue_breakthrough_solution) = S ((S (gcrt_solution_index_breakthrough_solution)) * s)) /\ exists ff_q_gcrt_breakthrough_solution_residue. r = ff_q_gcrt_breakthrough_solution_residue * S ((S (gcrt_solution_index_breakthrough_solution)) * s) + (gcrt_solution_residue_breakthrough_solution))) -> (((exists ff_h_gcrt_breakthrough_solution_modulus. ff_h_gcrt_breakthrough_solution_modulus + S (gcrt_solution_modulus_breakthrough_solution) = S ((S (gcrt_solution_index_breakthrough_solution)) * c)) /\ exists ff_q_gcrt_breakthrough_solution_modulus. b = ff_q_gcrt_breakthrough_solution_modulus * S ((S (gcrt_solution_index_breakthrough_solution)) * c) + (gcrt_solution_modulus_breakthrough_solution))) -> (exists hgcrt_mod_left_gcrt_breakthrough_solution_congruence hgcrt_mod_right_gcrt_breakthrough_solution_congruence. gcomp_merge_solution_breakthrough + gcrt_solution_modulus_breakthrough_solution * hgcrt_mod_left_gcrt_breakthrough_solution_congruence = gcrt_solution_residue_breakthrough_solution + gcrt_solution_modulus_breakthrough_solution * hgcrt_mod_right_gcrt_breakthrough_solution_congruence)) -> (((exists ff_h_gcrt_breakthrough_residue. ff_h_gcrt_breakthrough_residue + S (gcomp_merge_residue_breakthrough) = S ((S (gcomp_merge_index_breakthrough)) * s)) /\ exists ff_q_gcrt_breakthrough_residue. r = ff_q_gcrt_breakthrough_residue * S ((S (gcomp_merge_index_breakthrough)) * s) + (gcomp_merge_residue_breakthrough))) -> (((exists ff_h_gcrt_breakthrough_modulus. ff_h_gcrt_breakthrough_modulus + S (gcomp_merge_modulus_breakthrough) = S ((S (gcomp_merge_index_breakthrough)) * c)) /\ exists ff_q_gcrt_breakthrough_modulus. b = ff_q_gcrt_breakthrough_modulus * S ((S (gcomp_merge_index_breakthrough)) * c) + (gcomp_merge_modulus_breakthrough))) -> ((((exists hag_left_factor_gcomp_breakthrough_gcd. gcomp_merge_lcm_breakthrough = gcomp_merge_gcd_breakthrough * hag_left_factor_gcomp_breakthrough_gcd) /\ (exists hag_right_factor_gcomp_breakthrough_gcd. gcomp_merge_modulus_breakthrough = gcomp_merge_gcd_breakthrough * hag_right_factor_gcomp_breakthrough_gcd)) /\ forall hag_divisor_gcomp_breakthrough_gcd. (exists hag_common_left_gcomp_breakthrough_gcd. gcomp_merge_lcm_breakthrough = hag_divisor_gcomp_breakthrough_gcd * hag_common_left_gcomp_breakthrough_gcd) -> (exists hag_common_right_gcomp_breakthrough_gcd. gcomp_merge_modulus_breakthrough = hag_divisor_gcomp_breakthrough_gcd * hag_common_right_gcomp_breakthrough_gcd) -> exists hag_greatest_factor_gcomp_breakthrough_gcd. gcomp_merge_gcd_breakthrough = hag_divisor_gcomp_breakthrough_gcd * hag_greatest_factor_gcomp_breakthrough_gcd)) -> (exists hgcrt_mod_left_gcrt_breakthrough_result hgcrt_mod_right_gcrt_breakthrough_result. gcomp_merge_solution_breakthrough + gcomp_merge_gcd_breakthrough * hgcrt_mod_left_gcrt_breakthrough_result = gcomp_merge_residue_breakthrough + gcomp_merge_gcd_breakthrough * hgcrt_mod_right_gcrt_breakthrough_result)

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