crt_merge_compatible_prefix_canonical_exists_unique

Exact expanded first-order arithmetic statement

forall r s b c l. (forall gcrt_positive_index_gcomp_canonical_positive gcrt_positive_value_gcomp_canonical_positive. (exists ff_lt_gcrt_gcomp_canonical_positive_bound. ff_lt_gcrt_gcomp_canonical_positive_bound + S gcrt_positive_index_gcomp_canonical_positive = l) -> (((exists ff_h_gcrt_gcomp_canonical_positive_entry. ff_h_gcrt_gcomp_canonical_positive_entry + S (gcrt_positive_value_gcomp_canonical_positive) = S ((S (gcrt_positive_index_gcomp_canonical_positive)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_positive_entry. b = ff_q_gcrt_gcomp_canonical_positive_entry * S ((S (gcrt_positive_index_gcomp_canonical_positive)) * c) + (gcrt_positive_value_gcomp_canonical_positive))) -> ~(gcrt_positive_value_gcomp_canonical_positive = 0)) -> (forall gcomp_merge_index_gcomp_canonical_merge gcomp_merge_solution_gcomp_canonical_merge gcomp_merge_lcm_gcomp_canonical_merge gcomp_merge_residue_gcomp_canonical_merge gcomp_merge_modulus_gcomp_canonical_merge gcomp_merge_gcd_gcomp_canonical_merge. (exists ff_lt_gcrt_gcomp_canonical_merge_bound. ff_lt_gcrt_gcomp_canonical_merge_bound + S gcomp_merge_index_gcomp_canonical_merge = l) -> (((forall gcrt_common_index_gcomp_canonical_merge_lcm_own gcrt_common_modulus_gcomp_canonical_merge_lcm_own. (exists ff_lt_gcrt_gcomp_canonical_merge_lcm_own_bound. ff_lt_gcrt_gcomp_canonical_merge_lcm_own_bound + S gcrt_common_index_gcomp_canonical_merge_lcm_own = gcomp_merge_index_gcomp_canonical_merge) -> (((exists ff_h_gcrt_gcomp_canonical_merge_lcm_own_entry. ff_h_gcrt_gcomp_canonical_merge_lcm_own_entry + S (gcrt_common_modulus_gcomp_canonical_merge_lcm_own) = S ((S (gcrt_common_index_gcomp_canonical_merge_lcm_own)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_merge_lcm_own_entry. b = ff_q_gcrt_gcomp_canonical_merge_lcm_own_entry * S ((S (gcrt_common_index_gcomp_canonical_merge_lcm_own)) * c) + (gcrt_common_modulus_gcomp_canonical_merge_lcm_own))) -> exists gcrt_common_quotient_gcomp_canonical_merge_lcm_own. gcomp_merge_lcm_gcomp_canonical_merge = gcrt_common_modulus_gcomp_canonical_merge_lcm_own * gcrt_common_quotient_gcomp_canonical_merge_lcm_own) /\ forall gcrt_lcm_common_gcomp_canonical_merge_lcm. (forall gcrt_common_index_gcomp_canonical_merge_lcm_other gcrt_common_modulus_gcomp_canonical_merge_lcm_other. (exists ff_lt_gcrt_gcomp_canonical_merge_lcm_other_bound. ff_lt_gcrt_gcomp_canonical_merge_lcm_other_bound + S gcrt_common_index_gcomp_canonical_merge_lcm_other = gcomp_merge_index_gcomp_canonical_merge) -> (((exists ff_h_gcrt_gcomp_canonical_merge_lcm_other_entry. ff_h_gcrt_gcomp_canonical_merge_lcm_other_entry + S (gcrt_common_modulus_gcomp_canonical_merge_lcm_other) = S ((S (gcrt_common_index_gcomp_canonical_merge_lcm_other)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_merge_lcm_other_entry. b = ff_q_gcrt_gcomp_canonical_merge_lcm_other_entry * S ((S (gcrt_common_index_gcomp_canonical_merge_lcm_other)) * c) + (gcrt_common_modulus_gcomp_canonical_merge_lcm_other))) -> exists gcrt_common_quotient_gcomp_canonical_merge_lcm_other. gcrt_lcm_common_gcomp_canonical_merge_lcm = gcrt_common_modulus_gcomp_canonical_merge_lcm_other * gcrt_common_quotient_gcomp_canonical_merge_lcm_other) -> exists gcrt_lcm_quotient_gcomp_canonical_merge_lcm. gcrt_lcm_common_gcomp_canonical_merge_lcm = gcomp_merge_lcm_gcomp_canonical_merge * gcrt_lcm_quotient_gcomp_canonical_merge_lcm)) -> (forall gcrt_solution_index_gcomp_canonical_merge_solution gcrt_solution_residue_gcomp_canonical_merge_solution gcrt_solution_modulus_gcomp_canonical_merge_solution. (exists ff_lt_gcrt_gcomp_canonical_merge_solution_bound. ff_lt_gcrt_gcomp_canonical_merge_solution_bound + S gcrt_solution_index_gcomp_canonical_merge_solution = gcomp_merge_index_gcomp_canonical_merge) -> (((exists ff_h_gcrt_gcomp_canonical_merge_solution_residue. ff_h_gcrt_gcomp_canonical_merge_solution_residue + S (gcrt_solution_residue_gcomp_canonical_merge_solution) = S ((S (gcrt_solution_index_gcomp_canonical_merge_solution)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_merge_solution_residue. r = ff_q_gcrt_gcomp_canonical_merge_solution_residue * S ((S (gcrt_solution_index_gcomp_canonical_merge_solution)) * s) + (gcrt_solution_residue_gcomp_canonical_merge_solution))) -> (((exists ff_h_gcrt_gcomp_canonical_merge_solution_modulus. ff_h_gcrt_gcomp_canonical_merge_solution_modulus + S (gcrt_solution_modulus_gcomp_canonical_merge_solution) = S ((S (gcrt_solution_index_gcomp_canonical_merge_solution)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_merge_solution_modulus. b = ff_q_gcrt_gcomp_canonical_merge_solution_modulus * S ((S (gcrt_solution_index_gcomp_canonical_merge_solution)) * c) + (gcrt_solution_modulus_gcomp_canonical_merge_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_merge_solution_congruence hgcrt_mod_right_gcrt_gcomp_canonical_merge_solution_congruence. gcomp_merge_solution_gcomp_canonical_merge + gcrt_solution_modulus_gcomp_canonical_merge_solution * hgcrt_mod_left_gcrt_gcomp_canonical_merge_solution_congruence = gcrt_solution_residue_gcomp_canonical_merge_solution + gcrt_solution_modulus_gcomp_canonical_merge_solution * hgcrt_mod_right_gcrt_gcomp_canonical_merge_solution_congruence)) -> (((exists ff_h_gcrt_gcomp_canonical_merge_residue. ff_h_gcrt_gcomp_canonical_merge_residue + S (gcomp_merge_residue_gcomp_canonical_merge) = S ((S (gcomp_merge_index_gcomp_canonical_merge)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_merge_residue. r = ff_q_gcrt_gcomp_canonical_merge_residue * S ((S (gcomp_merge_index_gcomp_canonical_merge)) * s) + (gcomp_merge_residue_gcomp_canonical_merge))) -> (((exists ff_h_gcrt_gcomp_canonical_merge_modulus. ff_h_gcrt_gcomp_canonical_merge_modulus + S (gcomp_merge_modulus_gcomp_canonical_merge) = S ((S (gcomp_merge_index_gcomp_canonical_merge)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_merge_modulus. b = ff_q_gcrt_gcomp_canonical_merge_modulus * S ((S (gcomp_merge_index_gcomp_canonical_merge)) * c) + (gcomp_merge_modulus_gcomp_canonical_merge))) -> ((((exists hag_left_factor_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_lcm_gcomp_canonical_merge = gcomp_merge_gcd_gcomp_canonical_merge * hag_left_factor_gcomp_gcomp_canonical_merge_gcd) /\ (exists hag_right_factor_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_modulus_gcomp_canonical_merge = gcomp_merge_gcd_gcomp_canonical_merge * hag_right_factor_gcomp_gcomp_canonical_merge_gcd)) /\ forall hag_divisor_gcomp_gcomp_canonical_merge_gcd. (exists hag_common_left_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_lcm_gcomp_canonical_merge = hag_divisor_gcomp_gcomp_canonical_merge_gcd * hag_common_left_gcomp_gcomp_canonical_merge_gcd) -> (exists hag_common_right_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_modulus_gcomp_canonical_merge = hag_divisor_gcomp_gcomp_canonical_merge_gcd * hag_common_right_gcomp_gcomp_canonical_merge_gcd) -> exists hag_greatest_factor_gcomp_gcomp_canonical_merge_gcd. gcomp_merge_gcd_gcomp_canonical_merge = hag_divisor_gcomp_gcomp_canonical_merge_gcd * hag_greatest_factor_gcomp_gcomp_canonical_merge_gcd)) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_merge_result hgcrt_mod_right_gcrt_gcomp_canonical_merge_result. gcomp_merge_solution_gcomp_canonical_merge + gcomp_merge_gcd_gcomp_canonical_merge * hgcrt_mod_left_gcrt_gcomp_canonical_merge_result = gcomp_merge_residue_gcomp_canonical_merge + gcomp_merge_gcd_gcomp_canonical_merge * hgcrt_mod_right_gcrt_gcomp_canonical_merge_result)) -> exists x M. ((((((forall gcrt_common_index_gcomp_canonical_chosen_lcm_own gcrt_common_modulus_gcomp_canonical_chosen_lcm_own. (exists ff_lt_gcrt_gcomp_canonical_chosen_lcm_own_bound. ff_lt_gcrt_gcomp_canonical_chosen_lcm_own_bound + S gcrt_common_index_gcomp_canonical_chosen_lcm_own = l) -> (((exists ff_h_gcrt_gcomp_canonical_chosen_lcm_own_entry. ff_h_gcrt_gcomp_canonical_chosen_lcm_own_entry + S (gcrt_common_modulus_gcomp_canonical_chosen_lcm_own) = S ((S (gcrt_common_index_gcomp_canonical_chosen_lcm_own)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_chosen_lcm_own_entry. b = ff_q_gcrt_gcomp_canonical_chosen_lcm_own_entry * S ((S (gcrt_common_index_gcomp_canonical_chosen_lcm_own)) * c) + (gcrt_common_modulus_gcomp_canonical_chosen_lcm_own))) -> exists gcrt_common_quotient_gcomp_canonical_chosen_lcm_own. M = gcrt_common_modulus_gcomp_canonical_chosen_lcm_own * gcrt_common_quotient_gcomp_canonical_chosen_lcm_own) /\ forall gcrt_lcm_common_gcomp_canonical_chosen_lcm. (forall gcrt_common_index_gcomp_canonical_chosen_lcm_other gcrt_common_modulus_gcomp_canonical_chosen_lcm_other. (exists ff_lt_gcrt_gcomp_canonical_chosen_lcm_other_bound. ff_lt_gcrt_gcomp_canonical_chosen_lcm_other_bound + S gcrt_common_index_gcomp_canonical_chosen_lcm_other = l) -> (((exists ff_h_gcrt_gcomp_canonical_chosen_lcm_other_entry. ff_h_gcrt_gcomp_canonical_chosen_lcm_other_entry + S (gcrt_common_modulus_gcomp_canonical_chosen_lcm_other) = S ((S (gcrt_common_index_gcomp_canonical_chosen_lcm_other)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_chosen_lcm_other_entry. b = ff_q_gcrt_gcomp_canonical_chosen_lcm_other_entry * S ((S (gcrt_common_index_gcomp_canonical_chosen_lcm_other)) * c) + (gcrt_common_modulus_gcomp_canonical_chosen_lcm_other))) -> exists gcrt_common_quotient_gcomp_canonical_chosen_lcm_other. gcrt_lcm_common_gcomp_canonical_chosen_lcm = gcrt_common_modulus_gcomp_canonical_chosen_lcm_other * gcrt_common_quotient_gcomp_canonical_chosen_lcm_other) -> exists gcrt_lcm_quotient_gcomp_canonical_chosen_lcm. gcrt_lcm_common_gcomp_canonical_chosen_lcm = M * gcrt_lcm_quotient_gcomp_canonical_chosen_lcm)) /\ ((exists ff_lt_gcrt_gcomp_canonical_chosen_bounded. ff_lt_gcrt_gcomp_canonical_chosen_bounded + S x = M) /\ (forall gcrt_solution_index_gcomp_canonical_chosen_solution gcrt_solution_residue_gcomp_canonical_chosen_solution gcrt_solution_modulus_gcomp_canonical_chosen_solution. (exists ff_lt_gcrt_gcomp_canonical_chosen_solution_bound. ff_lt_gcrt_gcomp_canonical_chosen_solution_bound + S gcrt_solution_index_gcomp_canonical_chosen_solution = l) -> (((exists ff_h_gcrt_gcomp_canonical_chosen_solution_residue. ff_h_gcrt_gcomp_canonical_chosen_solution_residue + S (gcrt_solution_residue_gcomp_canonical_chosen_solution) = S ((S (gcrt_solution_index_gcomp_canonical_chosen_solution)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_chosen_solution_residue. r = ff_q_gcrt_gcomp_canonical_chosen_solution_residue * S ((S (gcrt_solution_index_gcomp_canonical_chosen_solution)) * s) + (gcrt_solution_residue_gcomp_canonical_chosen_solution))) -> (((exists ff_h_gcrt_gcomp_canonical_chosen_solution_modulus. ff_h_gcrt_gcomp_canonical_chosen_solution_modulus + S (gcrt_solution_modulus_gcomp_canonical_chosen_solution) = S ((S (gcrt_solution_index_gcomp_canonical_chosen_solution)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_chosen_solution_modulus. b = ff_q_gcrt_gcomp_canonical_chosen_solution_modulus * S ((S (gcrt_solution_index_gcomp_canonical_chosen_solution)) * c) + (gcrt_solution_modulus_gcomp_canonical_chosen_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_chosen_solution_congruence hgcrt_mod_right_gcrt_gcomp_canonical_chosen_solution_congruence. x + gcrt_solution_modulus_gcomp_canonical_chosen_solution * hgcrt_mod_left_gcrt_gcomp_canonical_chosen_solution_congruence = gcrt_solution_residue_gcomp_canonical_chosen_solution + gcrt_solution_modulus_gcomp_canonical_chosen_solution * hgcrt_mod_right_gcrt_gcomp_canonical_chosen_solution_congruence))))) /\ forall y. (((((forall gcrt_common_index_gcomp_canonical_compared_lcm_own gcrt_common_modulus_gcomp_canonical_compared_lcm_own. (exists ff_lt_gcrt_gcomp_canonical_compared_lcm_own_bound. ff_lt_gcrt_gcomp_canonical_compared_lcm_own_bound + S gcrt_common_index_gcomp_canonical_compared_lcm_own = l) -> (((exists ff_h_gcrt_gcomp_canonical_compared_lcm_own_entry. ff_h_gcrt_gcomp_canonical_compared_lcm_own_entry + S (gcrt_common_modulus_gcomp_canonical_compared_lcm_own) = S ((S (gcrt_common_index_gcomp_canonical_compared_lcm_own)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_compared_lcm_own_entry. b = ff_q_gcrt_gcomp_canonical_compared_lcm_own_entry * S ((S (gcrt_common_index_gcomp_canonical_compared_lcm_own)) * c) + (gcrt_common_modulus_gcomp_canonical_compared_lcm_own))) -> exists gcrt_common_quotient_gcomp_canonical_compared_lcm_own. M = gcrt_common_modulus_gcomp_canonical_compared_lcm_own * gcrt_common_quotient_gcomp_canonical_compared_lcm_own) /\ forall gcrt_lcm_common_gcomp_canonical_compared_lcm. (forall gcrt_common_index_gcomp_canonical_compared_lcm_other gcrt_common_modulus_gcomp_canonical_compared_lcm_other. (exists ff_lt_gcrt_gcomp_canonical_compared_lcm_other_bound. ff_lt_gcrt_gcomp_canonical_compared_lcm_other_bound + S gcrt_common_index_gcomp_canonical_compared_lcm_other = l) -> (((exists ff_h_gcrt_gcomp_canonical_compared_lcm_other_entry. ff_h_gcrt_gcomp_canonical_compared_lcm_other_entry + S (gcrt_common_modulus_gcomp_canonical_compared_lcm_other) = S ((S (gcrt_common_index_gcomp_canonical_compared_lcm_other)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_compared_lcm_other_entry. b = ff_q_gcrt_gcomp_canonical_compared_lcm_other_entry * S ((S (gcrt_common_index_gcomp_canonical_compared_lcm_other)) * c) + (gcrt_common_modulus_gcomp_canonical_compared_lcm_other))) -> exists gcrt_common_quotient_gcomp_canonical_compared_lcm_other. gcrt_lcm_common_gcomp_canonical_compared_lcm = gcrt_common_modulus_gcomp_canonical_compared_lcm_other * gcrt_common_quotient_gcomp_canonical_compared_lcm_other) -> exists gcrt_lcm_quotient_gcomp_canonical_compared_lcm. gcrt_lcm_common_gcomp_canonical_compared_lcm = M * gcrt_lcm_quotient_gcomp_canonical_compared_lcm)) /\ ((exists ff_lt_gcrt_gcomp_canonical_compared_bounded. ff_lt_gcrt_gcomp_canonical_compared_bounded + S y = M) /\ (forall gcrt_solution_index_gcomp_canonical_compared_solution gcrt_solution_residue_gcomp_canonical_compared_solution gcrt_solution_modulus_gcomp_canonical_compared_solution. (exists ff_lt_gcrt_gcomp_canonical_compared_solution_bound. ff_lt_gcrt_gcomp_canonical_compared_solution_bound + S gcrt_solution_index_gcomp_canonical_compared_solution = l) -> (((exists ff_h_gcrt_gcomp_canonical_compared_solution_residue. ff_h_gcrt_gcomp_canonical_compared_solution_residue + S (gcrt_solution_residue_gcomp_canonical_compared_solution) = S ((S (gcrt_solution_index_gcomp_canonical_compared_solution)) * s)) /\ exists ff_q_gcrt_gcomp_canonical_compared_solution_residue. r = ff_q_gcrt_gcomp_canonical_compared_solution_residue * S ((S (gcrt_solution_index_gcomp_canonical_compared_solution)) * s) + (gcrt_solution_residue_gcomp_canonical_compared_solution))) -> (((exists ff_h_gcrt_gcomp_canonical_compared_solution_modulus. ff_h_gcrt_gcomp_canonical_compared_solution_modulus + S (gcrt_solution_modulus_gcomp_canonical_compared_solution) = S ((S (gcrt_solution_index_gcomp_canonical_compared_solution)) * c)) /\ exists ff_q_gcrt_gcomp_canonical_compared_solution_modulus. b = ff_q_gcrt_gcomp_canonical_compared_solution_modulus * S ((S (gcrt_solution_index_gcomp_canonical_compared_solution)) * c) + (gcrt_solution_modulus_gcomp_canonical_compared_solution))) -> (exists hgcrt_mod_left_gcrt_gcomp_canonical_compared_solution_congruence hgcrt_mod_right_gcrt_gcomp_canonical_compared_solution_congruence. y + gcrt_solution_modulus_gcomp_canonical_compared_solution * hgcrt_mod_left_gcrt_gcomp_canonical_compared_solution_congruence = gcrt_solution_residue_gcomp_canonical_compared_solution + gcrt_solution_modulus_gcomp_canonical_compared_solution * hgcrt_mod_right_gcrt_gcomp_canonical_compared_solution_congruence))))) -> y = x)