crt_merge_compatible_prefix_drop_last

forall r s b c l. (forall gcomp_merge_index_merge_drop_source gcomp_merge_solution_merge_drop_source gcomp_merge_lcm_merge_drop_source gcomp_merge_residue_merge_drop_source gcomp_merge_modulus_merge_drop_source gcomp_merge_gcd_merge_drop_source. (exists ff_lt_gcrt_merge_drop_source_bound. ff_lt_gcrt_merge_drop_source_bound + S gcomp_merge_index_merge_drop_source = S l) -> (((forall gcrt_common_index_merge_drop_source_lcm_own gcrt_common_modulus_merge_drop_source_lcm_own. (exists ff_lt_gcrt_merge_drop_source_lcm_own_bound. ff_lt_gcrt_merge_drop_source_lcm_own_bound + S gcrt_common_index_merge_drop_source_lcm_own = gcomp_merge_index_merge_drop_source) -> (((exists ff_h_gcrt_merge_drop_source_lcm_own_entry. ff_h_gcrt_merge_drop_source_lcm_own_entry + S (gcrt_common_modulus_merge_drop_source_lcm_own) = S ((S (gcrt_common_index_merge_drop_source_lcm_own)) * c)) /\ exists ff_q_gcrt_merge_drop_source_lcm_own_entry. b = ff_q_gcrt_merge_drop_source_lcm_own_entry * S ((S (gcrt_common_index_merge_drop_source_lcm_own)) * c) + (gcrt_common_modulus_merge_drop_source_lcm_own))) -> exists gcrt_common_quotient_merge_drop_source_lcm_own. gcomp_merge_lcm_merge_drop_source = gcrt_common_modulus_merge_drop_source_lcm_own * gcrt_common_quotient_merge_drop_source_lcm_own) /\ forall gcrt_lcm_common_merge_drop_source_lcm. (forall gcrt_common_index_merge_drop_source_lcm_other gcrt_common_modulus_merge_drop_source_lcm_other. (exists ff_lt_gcrt_merge_drop_source_lcm_other_bound. ff_lt_gcrt_merge_drop_source_lcm_other_bound + S gcrt_common_index_merge_drop_source_lcm_other = gcomp_merge_index_merge_drop_source) -> (((exists ff_h_gcrt_merge_drop_source_lcm_other_entry. ff_h_gcrt_merge_drop_source_lcm_other_entry + S (gcrt_common_modulus_merge_drop_source_lcm_other) = S ((S (gcrt_common_index_merge_drop_source_lcm_other)) * c)) /\ exists ff_q_gcrt_merge_drop_source_lcm_other_entry. b = ff_q_gcrt_merge_drop_source_lcm_other_entry * S ((S (gcrt_common_index_merge_drop_source_lcm_other)) * c) + (gcrt_common_modulus_merge_drop_source_lcm_other))) -> exists gcrt_common_quotient_merge_drop_source_lcm_other. gcrt_lcm_common_merge_drop_source_lcm = gcrt_common_modulus_merge_drop_source_lcm_other * gcrt_common_quotient_merge_drop_source_lcm_other) -> exists gcrt_lcm_quotient_merge_drop_source_lcm. gcrt_lcm_common_merge_drop_source_lcm = gcomp_merge_lcm_merge_drop_source * gcrt_lcm_quotient_merge_drop_source_lcm)) -> (forall gcrt_solution_index_merge_drop_source_solution gcrt_solution_residue_merge_drop_source_solution gcrt_solution_modulus_merge_drop_source_solution. (exists ff_lt_gcrt_merge_drop_source_solution_bound. ff_lt_gcrt_merge_drop_source_solution_bound + S gcrt_solution_index_merge_drop_source_solution = gcomp_merge_index_merge_drop_source) -> (((exists ff_h_gcrt_merge_drop_source_solution_residue. ff_h_gcrt_merge_drop_source_solution_residue + S (gcrt_solution_residue_merge_drop_source_solution) = S ((S (gcrt_solution_index_merge_drop_source_solution)) * s)) /\ exists ff_q_gcrt_merge_drop_source_solution_residue. r = ff_q_gcrt_merge_drop_source_solution_residue * S ((S (gcrt_solution_index_merge_drop_source_solution)) * s) + (gcrt_solution_residue_merge_drop_source_solution))) -> (((exists ff_h_gcrt_merge_drop_source_solution_modulus. ff_h_gcrt_merge_drop_source_solution_modulus + S (gcrt_solution_modulus_merge_drop_source_solution) = S ((S (gcrt_solution_index_merge_drop_source_solution)) * c)) /\ exists ff_q_gcrt_merge_drop_source_solution_modulus. b = ff_q_gcrt_merge_drop_source_solution_modulus * S ((S (gcrt_solution_index_merge_drop_source_solution)) * c) + (gcrt_solution_modulus_merge_drop_source_solution))) -> (exists hgcrt_mod_left_gcrt_merge_drop_source_solution_congruence hgcrt_mod_right_gcrt_merge_drop_source_solution_congruence. gcomp_merge_solution_merge_drop_source + gcrt_solution_modulus_merge_drop_source_solution * hgcrt_mod_left_gcrt_merge_drop_source_solution_congruence = gcrt_solution_residue_merge_drop_source_solution + gcrt_solution_modulus_merge_drop_source_solution * hgcrt_mod_right_gcrt_merge_drop_source_solution_congruence)) -> (((exists ff_h_gcrt_merge_drop_source_residue. ff_h_gcrt_merge_drop_source_residue + S (gcomp_merge_residue_merge_drop_source) = S ((S (gcomp_merge_index_merge_drop_source)) * s)) /\ exists ff_q_gcrt_merge_drop_source_residue. r = ff_q_gcrt_merge_drop_source_residue * S ((S (gcomp_merge_index_merge_drop_source)) * s) + (gcomp_merge_residue_merge_drop_source))) -> (((exists ff_h_gcrt_merge_drop_source_modulus. ff_h_gcrt_merge_drop_source_modulus + S (gcomp_merge_modulus_merge_drop_source) = S ((S (gcomp_merge_index_merge_drop_source)) * c)) /\ exists ff_q_gcrt_merge_drop_source_modulus. b = ff_q_gcrt_merge_drop_source_modulus * S ((S (gcomp_merge_index_merge_drop_source)) * c) + (gcomp_merge_modulus_merge_drop_source))) -> ((((exists hag_left_factor_gcomp_merge_drop_source_gcd. gcomp_merge_lcm_merge_drop_source = gcomp_merge_gcd_merge_drop_source * hag_left_factor_gcomp_merge_drop_source_gcd) /\ (exists hag_right_factor_gcomp_merge_drop_source_gcd. gcomp_merge_modulus_merge_drop_source = gcomp_merge_gcd_merge_drop_source * hag_right_factor_gcomp_merge_drop_source_gcd)) /\ forall hag_divisor_gcomp_merge_drop_source_gcd. (exists hag_common_left_gcomp_merge_drop_source_gcd. gcomp_merge_lcm_merge_drop_source = hag_divisor_gcomp_merge_drop_source_gcd * hag_common_left_gcomp_merge_drop_source_gcd) -> (exists hag_common_right_gcomp_merge_drop_source_gcd. gcomp_merge_modulus_merge_drop_source = hag_divisor_gcomp_merge_drop_source_gcd * hag_common_right_gcomp_merge_drop_source_gcd) -> exists hag_greatest_factor_gcomp_merge_drop_source_gcd. gcomp_merge_gcd_merge_drop_source = hag_divisor_gcomp_merge_drop_source_gcd * hag_greatest_factor_gcomp_merge_drop_source_gcd)) -> (exists hgcrt_mod_left_gcrt_merge_drop_source_result hgcrt_mod_right_gcrt_merge_drop_source_result. gcomp_merge_solution_merge_drop_source + gcomp_merge_gcd_merge_drop_source * hgcrt_mod_left_gcrt_merge_drop_source_result = gcomp_merge_residue_merge_drop_source + gcomp_merge_gcd_merge_drop_source * hgcrt_mod_right_gcrt_merge_drop_source_result)) -> (forall gcomp_merge_index_merge_drop_result gcomp_merge_solution_merge_drop_result gcomp_merge_lcm_merge_drop_result gcomp_merge_residue_merge_drop_result gcomp_merge_modulus_merge_drop_result gcomp_merge_gcd_merge_drop_result. (exists ff_lt_gcrt_merge_drop_result_bound. ff_lt_gcrt_merge_drop_result_bound + S gcomp_merge_index_merge_drop_result = l) -> (((forall gcrt_common_index_merge_drop_result_lcm_own gcrt_common_modulus_merge_drop_result_lcm_own. (exists ff_lt_gcrt_merge_drop_result_lcm_own_bound. ff_lt_gcrt_merge_drop_result_lcm_own_bound + S gcrt_common_index_merge_drop_result_lcm_own = gcomp_merge_index_merge_drop_result) -> (((exists ff_h_gcrt_merge_drop_result_lcm_own_entry. ff_h_gcrt_merge_drop_result_lcm_own_entry + S (gcrt_common_modulus_merge_drop_result_lcm_own) = S ((S (gcrt_common_index_merge_drop_result_lcm_own)) * c)) /\ exists ff_q_gcrt_merge_drop_result_lcm_own_entry. b = ff_q_gcrt_merge_drop_result_lcm_own_entry * S ((S (gcrt_common_index_merge_drop_result_lcm_own)) * c) + (gcrt_common_modulus_merge_drop_result_lcm_own))) -> exists gcrt_common_quotient_merge_drop_result_lcm_own. gcomp_merge_lcm_merge_drop_result = gcrt_common_modulus_merge_drop_result_lcm_own * gcrt_common_quotient_merge_drop_result_lcm_own) /\ forall gcrt_lcm_common_merge_drop_result_lcm. (forall gcrt_common_index_merge_drop_result_lcm_other gcrt_common_modulus_merge_drop_result_lcm_other. (exists ff_lt_gcrt_merge_drop_result_lcm_other_bound. ff_lt_gcrt_merge_drop_result_lcm_other_bound + S gcrt_common_index_merge_drop_result_lcm_other = gcomp_merge_index_merge_drop_result) -> (((exists ff_h_gcrt_merge_drop_result_lcm_other_entry. ff_h_gcrt_merge_drop_result_lcm_other_entry + S (gcrt_common_modulus_merge_drop_result_lcm_other) = S ((S (gcrt_common_index_merge_drop_result_lcm_other)) * c)) /\ exists ff_q_gcrt_merge_drop_result_lcm_other_entry. b = ff_q_gcrt_merge_drop_result_lcm_other_entry * S ((S (gcrt_common_index_merge_drop_result_lcm_other)) * c) + (gcrt_common_modulus_merge_drop_result_lcm_other))) -> exists gcrt_common_quotient_merge_drop_result_lcm_other. gcrt_lcm_common_merge_drop_result_lcm = gcrt_common_modulus_merge_drop_result_lcm_other * gcrt_common_quotient_merge_drop_result_lcm_other) -> exists gcrt_lcm_quotient_merge_drop_result_lcm. gcrt_lcm_common_merge_drop_result_lcm = gcomp_merge_lcm_merge_drop_result * gcrt_lcm_quotient_merge_drop_result_lcm)) -> (forall gcrt_solution_index_merge_drop_result_solution gcrt_solution_residue_merge_drop_result_solution gcrt_solution_modulus_merge_drop_result_solution. (exists ff_lt_gcrt_merge_drop_result_solution_bound. ff_lt_gcrt_merge_drop_result_solution_bound + S gcrt_solution_index_merge_drop_result_solution = gcomp_merge_index_merge_drop_result) -> (((exists ff_h_gcrt_merge_drop_result_solution_residue. ff_h_gcrt_merge_drop_result_solution_residue + S (gcrt_solution_residue_merge_drop_result_solution) = S ((S (gcrt_solution_index_merge_drop_result_solution)) * s)) /\ exists ff_q_gcrt_merge_drop_result_solution_residue. r = ff_q_gcrt_merge_drop_result_solution_residue * S ((S (gcrt_solution_index_merge_drop_result_solution)) * s) + (gcrt_solution_residue_merge_drop_result_solution))) -> (((exists ff_h_gcrt_merge_drop_result_solution_modulus. ff_h_gcrt_merge_drop_result_solution_modulus + S (gcrt_solution_modulus_merge_drop_result_solution) = S ((S (gcrt_solution_index_merge_drop_result_solution)) * c)) /\ exists ff_q_gcrt_merge_drop_result_solution_modulus. b = ff_q_gcrt_merge_drop_result_solution_modulus * S ((S (gcrt_solution_index_merge_drop_result_solution)) * c) + (gcrt_solution_modulus_merge_drop_result_solution))) -> (exists hgcrt_mod_left_gcrt_merge_drop_result_solution_congruence hgcrt_mod_right_gcrt_merge_drop_result_solution_congruence. gcomp_merge_solution_merge_drop_result + gcrt_solution_modulus_merge_drop_result_solution * hgcrt_mod_left_gcrt_merge_drop_result_solution_congruence = gcrt_solution_residue_merge_drop_result_solution + gcrt_solution_modulus_merge_drop_result_solution * hgcrt_mod_right_gcrt_merge_drop_result_solution_congruence)) -> (((exists ff_h_gcrt_merge_drop_result_residue. ff_h_gcrt_merge_drop_result_residue + S (gcomp_merge_residue_merge_drop_result) = S ((S (gcomp_merge_index_merge_drop_result)) * s)) /\ exists ff_q_gcrt_merge_drop_result_residue. r = ff_q_gcrt_merge_drop_result_residue * S ((S (gcomp_merge_index_merge_drop_result)) * s) + (gcomp_merge_residue_merge_drop_result))) -> (((exists ff_h_gcrt_merge_drop_result_modulus. ff_h_gcrt_merge_drop_result_modulus + S (gcomp_merge_modulus_merge_drop_result) = S ((S (gcomp_merge_index_merge_drop_result)) * c)) /\ exists ff_q_gcrt_merge_drop_result_modulus. b = ff_q_gcrt_merge_drop_result_modulus * S ((S (gcomp_merge_index_merge_drop_result)) * c) + (gcomp_merge_modulus_merge_drop_result))) -> ((((exists hag_left_factor_gcomp_merge_drop_result_gcd. gcomp_merge_lcm_merge_drop_result = gcomp_merge_gcd_merge_drop_result * hag_left_factor_gcomp_merge_drop_result_gcd) /\ (exists hag_right_factor_gcomp_merge_drop_result_gcd. gcomp_merge_modulus_merge_drop_result = gcomp_merge_gcd_merge_drop_result * hag_right_factor_gcomp_merge_drop_result_gcd)) /\ forall hag_divisor_gcomp_merge_drop_result_gcd. (exists hag_common_left_gcomp_merge_drop_result_gcd. gcomp_merge_lcm_merge_drop_result = hag_divisor_gcomp_merge_drop_result_gcd * hag_common_left_gcomp_merge_drop_result_gcd) -> (exists hag_common_right_gcomp_merge_drop_result_gcd. gcomp_merge_modulus_merge_drop_result = hag_divisor_gcomp_merge_drop_result_gcd * hag_common_right_gcomp_merge_drop_result_gcd) -> exists hag_greatest_factor_gcomp_merge_drop_result_gcd. gcomp_merge_gcd_merge_drop_result = hag_divisor_gcomp_merge_drop_result_gcd * hag_greatest_factor_gcomp_merge_drop_result_gcd)) -> (exists hgcrt_mod_left_gcrt_merge_drop_result_result hgcrt_mod_right_gcrt_merge_drop_result_result. gcomp_merge_solution_merge_drop_result + gcomp_merge_gcd_merge_drop_result * hgcrt_mod_left_gcrt_merge_drop_result_result = gcomp_merge_residue_merge_drop_result + gcomp_merge_gcd_merge_drop_result * hgcrt_mod_right_gcrt_merge_drop_result_result))