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

Hygienic expanded first-order definition

forall gcomp_left_index_breakthrough gcomp_right_index_breakthrough gcomp_left_residue_breakthrough gcomp_right_residue_breakthrough gcomp_left_modulus_breakthrough gcomp_right_modulus_breakthrough gcomp_pair_gcd_breakthrough. (exists ff_lt_gcrt_breakthrough_left_bound. ff_lt_gcrt_breakthrough_left_bound + S gcomp_left_index_breakthrough = l) -> (exists ff_lt_gcrt_breakthrough_right_bound. ff_lt_gcrt_breakthrough_right_bound + S gcomp_right_index_breakthrough = l) -> (((exists ff_h_gcrt_breakthrough_left_residue. ff_h_gcrt_breakthrough_left_residue + S (gcomp_left_residue_breakthrough) = S ((S (gcomp_left_index_breakthrough)) * s)) /\ exists ff_q_gcrt_breakthrough_left_residue. r = ff_q_gcrt_breakthrough_left_residue * S ((S (gcomp_left_index_breakthrough)) * s) + (gcomp_left_residue_breakthrough))) -> (((exists ff_h_gcrt_breakthrough_right_residue. ff_h_gcrt_breakthrough_right_residue + S (gcomp_right_residue_breakthrough) = S ((S (gcomp_right_index_breakthrough)) * s)) /\ exists ff_q_gcrt_breakthrough_right_residue. r = ff_q_gcrt_breakthrough_right_residue * S ((S (gcomp_right_index_breakthrough)) * s) + (gcomp_right_residue_breakthrough))) -> (((exists ff_h_gcrt_breakthrough_left_modulus. ff_h_gcrt_breakthrough_left_modulus + S (gcomp_left_modulus_breakthrough) = S ((S (gcomp_left_index_breakthrough)) * c)) /\ exists ff_q_gcrt_breakthrough_left_modulus. b = ff_q_gcrt_breakthrough_left_modulus * S ((S (gcomp_left_index_breakthrough)) * c) + (gcomp_left_modulus_breakthrough))) -> (((exists ff_h_gcrt_breakthrough_right_modulus. ff_h_gcrt_breakthrough_right_modulus + S (gcomp_right_modulus_breakthrough) = S ((S (gcomp_right_index_breakthrough)) * c)) /\ exists ff_q_gcrt_breakthrough_right_modulus. b = ff_q_gcrt_breakthrough_right_modulus * S ((S (gcomp_right_index_breakthrough)) * c) + (gcomp_right_modulus_breakthrough))) -> ((((exists hag_left_factor_gcomp_breakthrough_gcd. gcomp_left_modulus_breakthrough = gcomp_pair_gcd_breakthrough * hag_left_factor_gcomp_breakthrough_gcd) /\ (exists hag_right_factor_gcomp_breakthrough_gcd. gcomp_right_modulus_breakthrough = gcomp_pair_gcd_breakthrough * hag_right_factor_gcomp_breakthrough_gcd)) /\ forall hag_divisor_gcomp_breakthrough_gcd. (exists hag_common_left_gcomp_breakthrough_gcd. gcomp_left_modulus_breakthrough = hag_divisor_gcomp_breakthrough_gcd * hag_common_left_gcomp_breakthrough_gcd) -> (exists hag_common_right_gcomp_breakthrough_gcd. gcomp_right_modulus_breakthrough = hag_divisor_gcomp_breakthrough_gcd * hag_common_right_gcomp_breakthrough_gcd) -> exists hag_greatest_factor_gcomp_breakthrough_gcd. gcomp_pair_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_left_residue_breakthrough + gcomp_pair_gcd_breakthrough * hgcrt_mod_left_gcrt_breakthrough_result = gcomp_right_residue_breakthrough + gcomp_pair_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