crt_pairwise_compatible_prefix_last

Exact expanded first-order arithmetic statement

forall r s b c l i a d m n g. (forall gcomp_left_index_gcomp_last_source gcomp_right_index_gcomp_last_source gcomp_left_residue_gcomp_last_source gcomp_right_residue_gcomp_last_source gcomp_left_modulus_gcomp_last_source gcomp_right_modulus_gcomp_last_source gcomp_pair_gcd_gcomp_last_source. (exists ff_lt_gcrt_gcomp_last_source_left_bound. ff_lt_gcrt_gcomp_last_source_left_bound + S gcomp_left_index_gcomp_last_source = S l) -> (exists ff_lt_gcrt_gcomp_last_source_right_bound. ff_lt_gcrt_gcomp_last_source_right_bound + S gcomp_right_index_gcomp_last_source = S l) -> (((exists ff_h_gcrt_gcomp_last_source_left_residue. ff_h_gcrt_gcomp_last_source_left_residue + S (gcomp_left_residue_gcomp_last_source) = S ((S (gcomp_left_index_gcomp_last_source)) * s)) /\ exists ff_q_gcrt_gcomp_last_source_left_residue. r = ff_q_gcrt_gcomp_last_source_left_residue * S ((S (gcomp_left_index_gcomp_last_source)) * s) + (gcomp_left_residue_gcomp_last_source))) -> (((exists ff_h_gcrt_gcomp_last_source_right_residue. ff_h_gcrt_gcomp_last_source_right_residue + S (gcomp_right_residue_gcomp_last_source) = S ((S (gcomp_right_index_gcomp_last_source)) * s)) /\ exists ff_q_gcrt_gcomp_last_source_right_residue. r = ff_q_gcrt_gcomp_last_source_right_residue * S ((S (gcomp_right_index_gcomp_last_source)) * s) + (gcomp_right_residue_gcomp_last_source))) -> (((exists ff_h_gcrt_gcomp_last_source_left_modulus. ff_h_gcrt_gcomp_last_source_left_modulus + S (gcomp_left_modulus_gcomp_last_source) = S ((S (gcomp_left_index_gcomp_last_source)) * c)) /\ exists ff_q_gcrt_gcomp_last_source_left_modulus. b = ff_q_gcrt_gcomp_last_source_left_modulus * S ((S (gcomp_left_index_gcomp_last_source)) * c) + (gcomp_left_modulus_gcomp_last_source))) -> (((exists ff_h_gcrt_gcomp_last_source_right_modulus. ff_h_gcrt_gcomp_last_source_right_modulus + S (gcomp_right_modulus_gcomp_last_source) = S ((S (gcomp_right_index_gcomp_last_source)) * c)) /\ exists ff_q_gcrt_gcomp_last_source_right_modulus. b = ff_q_gcrt_gcomp_last_source_right_modulus * S ((S (gcomp_right_index_gcomp_last_source)) * c) + (gcomp_right_modulus_gcomp_last_source))) -> ((((exists hag_left_factor_gcomp_gcomp_last_source_gcd. gcomp_left_modulus_gcomp_last_source = gcomp_pair_gcd_gcomp_last_source * hag_left_factor_gcomp_gcomp_last_source_gcd) /\ (exists hag_right_factor_gcomp_gcomp_last_source_gcd. gcomp_right_modulus_gcomp_last_source = gcomp_pair_gcd_gcomp_last_source * hag_right_factor_gcomp_gcomp_last_source_gcd)) /\ forall hag_divisor_gcomp_gcomp_last_source_gcd. (exists hag_common_left_gcomp_gcomp_last_source_gcd. gcomp_left_modulus_gcomp_last_source = hag_divisor_gcomp_gcomp_last_source_gcd * hag_common_left_gcomp_gcomp_last_source_gcd) -> (exists hag_common_right_gcomp_gcomp_last_source_gcd. gcomp_right_modulus_gcomp_last_source = hag_divisor_gcomp_gcomp_last_source_gcd * hag_common_right_gcomp_gcomp_last_source_gcd) -> exists hag_greatest_factor_gcomp_gcomp_last_source_gcd. gcomp_pair_gcd_gcomp_last_source = hag_divisor_gcomp_gcomp_last_source_gcd * hag_greatest_factor_gcomp_gcomp_last_source_gcd)) -> (exists hgcrt_mod_left_gcrt_gcomp_last_source_result hgcrt_mod_right_gcrt_gcomp_last_source_result. gcomp_left_residue_gcomp_last_source + gcomp_pair_gcd_gcomp_last_source * hgcrt_mod_left_gcrt_gcomp_last_source_result = gcomp_right_residue_gcomp_last_source + gcomp_pair_gcd_gcomp_last_source * hgcrt_mod_right_gcrt_gcomp_last_source_result)) -> (exists ff_lt_gcrt_gcomp_last_old_bound. ff_lt_gcrt_gcomp_last_old_bound + S i = l) -> (((exists ff_h_gcrt_gcomp_last_old_residue. ff_h_gcrt_gcomp_last_old_residue + S (a) = S ((S (i)) * s)) /\ exists ff_q_gcrt_gcomp_last_old_residue. r = ff_q_gcrt_gcomp_last_old_residue * S ((S (i)) * s) + (a))) -> (((exists ff_h_gcrt_gcomp_last_new_residue. ff_h_gcrt_gcomp_last_new_residue + S (d) = S ((S (l)) * s)) /\ exists ff_q_gcrt_gcomp_last_new_residue. r = ff_q_gcrt_gcomp_last_new_residue * S ((S (l)) * s) + (d))) -> (((exists ff_h_gcrt_gcomp_last_old_modulus. ff_h_gcrt_gcomp_last_old_modulus + S (m) = S ((S (i)) * c)) /\ exists ff_q_gcrt_gcomp_last_old_modulus. b = ff_q_gcrt_gcomp_last_old_modulus * S ((S (i)) * c) + (m))) -> (((exists ff_h_gcrt_gcomp_last_new_modulus. ff_h_gcrt_gcomp_last_new_modulus + S (n) = S ((S (l)) * c)) /\ exists ff_q_gcrt_gcomp_last_new_modulus. b = ff_q_gcrt_gcomp_last_new_modulus * S ((S (l)) * c) + (n))) -> ((((exists hag_left_factor_gcomp_last_actual_gcd. m = g * hag_left_factor_gcomp_last_actual_gcd) /\ (exists hag_right_factor_gcomp_last_actual_gcd. n = g * hag_right_factor_gcomp_last_actual_gcd)) /\ forall hag_divisor_gcomp_last_actual_gcd. (exists hag_common_left_gcomp_last_actual_gcd. m = hag_divisor_gcomp_last_actual_gcd * hag_common_left_gcomp_last_actual_gcd) -> (exists hag_common_right_gcomp_last_actual_gcd. n = hag_divisor_gcomp_last_actual_gcd * hag_common_right_gcomp_last_actual_gcd) -> exists hag_greatest_factor_gcomp_last_actual_gcd. g = hag_divisor_gcomp_last_actual_gcd * hag_greatest_factor_gcomp_last_actual_gcd)) -> (exists hgcrt_mod_left_gcrt_gcomp_last_result hgcrt_mod_right_gcrt_gcomp_last_result. a + g * hgcrt_mod_left_gcrt_gcomp_last_result = d + g * hgcrt_mod_right_gcrt_gcomp_last_result)