crt_pairwise_compatible_prefix_merge_iff

Exact expanded first-order arithmetic statement

forall r s b c l. (((forall gcomp_left_index_gfull_merge_iff_pairs_forward gcomp_right_index_gfull_merge_iff_pairs_forward gcomp_left_residue_gfull_merge_iff_pairs_forward gcomp_right_residue_gfull_merge_iff_pairs_forward gcomp_left_modulus_gfull_merge_iff_pairs_forward gcomp_right_modulus_gfull_merge_iff_pairs_forward gcomp_pair_gcd_gfull_merge_iff_pairs_forward. (exists ff_lt_gcrt_gfull_merge_iff_pairs_forward_left_bound. ff_lt_gcrt_gfull_merge_iff_pairs_forward_left_bound + S gcomp_left_index_gfull_merge_iff_pairs_forward = l) -> (exists ff_lt_gcrt_gfull_merge_iff_pairs_forward_right_bound. ff_lt_gcrt_gfull_merge_iff_pairs_forward_right_bound + S gcomp_right_index_gfull_merge_iff_pairs_forward = l) -> (((exists ff_h_gcrt_gfull_merge_iff_pairs_forward_left_residue. ff_h_gcrt_gfull_merge_iff_pairs_forward_left_residue + S (gcomp_left_residue_gfull_merge_iff_pairs_forward) = S ((S (gcomp_left_index_gfull_merge_iff_pairs_forward)) * s)) /\ exists ff_q_gcrt_gfull_merge_iff_pairs_forward_left_residue. r = ff_q_gcrt_gfull_merge_iff_pairs_forward_left_residue * S ((S (gcomp_left_index_gfull_merge_iff_pairs_forward)) * s) + (gcomp_left_residue_gfull_merge_iff_pairs_forward))) -> (((exists ff_h_gcrt_gfull_merge_iff_pairs_forward_right_residue. ff_h_gcrt_gfull_merge_iff_pairs_forward_right_residue + S (gcomp_right_residue_gfull_merge_iff_pairs_forward) = S ((S (gcomp_right_index_gfull_merge_iff_pairs_forward)) * s)) /\ exists ff_q_gcrt_gfull_merge_iff_pairs_forward_right_residue. r = ff_q_gcrt_gfull_merge_iff_pairs_forward_right_residue * S ((S (gcomp_right_index_gfull_merge_iff_pairs_forward)) * s) + (gcomp_right_residue_gfull_merge_iff_pairs_forward))) -> (((exists ff_h_gcrt_gfull_merge_iff_pairs_forward_left_modulus. ff_h_gcrt_gfull_merge_iff_pairs_forward_left_modulus + S (gcomp_left_modulus_gfull_merge_iff_pairs_forward) = S ((S (gcomp_left_index_gfull_merge_iff_pairs_forward)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_pairs_forward_left_modulus. b = ff_q_gcrt_gfull_merge_iff_pairs_forward_left_modulus * S ((S (gcomp_left_index_gfull_merge_iff_pairs_forward)) * c) + (gcomp_left_modulus_gfull_merge_iff_pairs_forward))) -> (((exists ff_h_gcrt_gfull_merge_iff_pairs_forward_right_modulus. ff_h_gcrt_gfull_merge_iff_pairs_forward_right_modulus + S (gcomp_right_modulus_gfull_merge_iff_pairs_forward) = S ((S (gcomp_right_index_gfull_merge_iff_pairs_forward)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_pairs_forward_right_modulus. b = ff_q_gcrt_gfull_merge_iff_pairs_forward_right_modulus * S ((S (gcomp_right_index_gfull_merge_iff_pairs_forward)) * c) + (gcomp_right_modulus_gfull_merge_iff_pairs_forward))) -> ((((exists hag_left_factor_gcomp_gfull_merge_iff_pairs_forward_gcd. gcomp_left_modulus_gfull_merge_iff_pairs_forward = gcomp_pair_gcd_gfull_merge_iff_pairs_forward * hag_left_factor_gcomp_gfull_merge_iff_pairs_forward_gcd) /\ (exists hag_right_factor_gcomp_gfull_merge_iff_pairs_forward_gcd. gcomp_right_modulus_gfull_merge_iff_pairs_forward = gcomp_pair_gcd_gfull_merge_iff_pairs_forward * hag_right_factor_gcomp_gfull_merge_iff_pairs_forward_gcd)) /\ forall hag_divisor_gcomp_gfull_merge_iff_pairs_forward_gcd. (exists hag_common_left_gcomp_gfull_merge_iff_pairs_forward_gcd. gcomp_left_modulus_gfull_merge_iff_pairs_forward = hag_divisor_gcomp_gfull_merge_iff_pairs_forward_gcd * hag_common_left_gcomp_gfull_merge_iff_pairs_forward_gcd) -> (exists hag_common_right_gcomp_gfull_merge_iff_pairs_forward_gcd. gcomp_right_modulus_gfull_merge_iff_pairs_forward = hag_divisor_gcomp_gfull_merge_iff_pairs_forward_gcd * hag_common_right_gcomp_gfull_merge_iff_pairs_forward_gcd) -> exists hag_greatest_factor_gcomp_gfull_merge_iff_pairs_forward_gcd. gcomp_pair_gcd_gfull_merge_iff_pairs_forward = hag_divisor_gcomp_gfull_merge_iff_pairs_forward_gcd * hag_greatest_factor_gcomp_gfull_merge_iff_pairs_forward_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_merge_iff_pairs_forward_result hgcrt_mod_right_gcrt_gfull_merge_iff_pairs_forward_result. gcomp_left_residue_gfull_merge_iff_pairs_forward + gcomp_pair_gcd_gfull_merge_iff_pairs_forward * hgcrt_mod_left_gcrt_gfull_merge_iff_pairs_forward_result = gcomp_right_residue_gfull_merge_iff_pairs_forward + gcomp_pair_gcd_gfull_merge_iff_pairs_forward * hgcrt_mod_right_gcrt_gfull_merge_iff_pairs_forward_result)) -> (forall gcomp_merge_index_gfull_merge_iff_merge_forward gcomp_merge_solution_gfull_merge_iff_merge_forward gcomp_merge_lcm_gfull_merge_iff_merge_forward gcomp_merge_residue_gfull_merge_iff_merge_forward gcomp_merge_modulus_gfull_merge_iff_merge_forward gcomp_merge_gcd_gfull_merge_iff_merge_forward. (exists ff_lt_gcrt_gfull_merge_iff_merge_forward_bound. ff_lt_gcrt_gfull_merge_iff_merge_forward_bound + S gcomp_merge_index_gfull_merge_iff_merge_forward = l) -> (((forall gcrt_common_index_gfull_merge_iff_merge_forward_lcm_own gcrt_common_modulus_gfull_merge_iff_merge_forward_lcm_own. (exists ff_lt_gcrt_gfull_merge_iff_merge_forward_lcm_own_bound. ff_lt_gcrt_gfull_merge_iff_merge_forward_lcm_own_bound + S gcrt_common_index_gfull_merge_iff_merge_forward_lcm_own = gcomp_merge_index_gfull_merge_iff_merge_forward) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_forward_lcm_own_entry. ff_h_gcrt_gfull_merge_iff_merge_forward_lcm_own_entry + S (gcrt_common_modulus_gfull_merge_iff_merge_forward_lcm_own) = S ((S (gcrt_common_index_gfull_merge_iff_merge_forward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_forward_lcm_own_entry. b = ff_q_gcrt_gfull_merge_iff_merge_forward_lcm_own_entry * S ((S (gcrt_common_index_gfull_merge_iff_merge_forward_lcm_own)) * c) + (gcrt_common_modulus_gfull_merge_iff_merge_forward_lcm_own))) -> exists gcrt_common_quotient_gfull_merge_iff_merge_forward_lcm_own. gcomp_merge_lcm_gfull_merge_iff_merge_forward = gcrt_common_modulus_gfull_merge_iff_merge_forward_lcm_own * gcrt_common_quotient_gfull_merge_iff_merge_forward_lcm_own) /\ forall gcrt_lcm_common_gfull_merge_iff_merge_forward_lcm. (forall gcrt_common_index_gfull_merge_iff_merge_forward_lcm_other gcrt_common_modulus_gfull_merge_iff_merge_forward_lcm_other. (exists ff_lt_gcrt_gfull_merge_iff_merge_forward_lcm_other_bound. ff_lt_gcrt_gfull_merge_iff_merge_forward_lcm_other_bound + S gcrt_common_index_gfull_merge_iff_merge_forward_lcm_other = gcomp_merge_index_gfull_merge_iff_merge_forward) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_forward_lcm_other_entry. ff_h_gcrt_gfull_merge_iff_merge_forward_lcm_other_entry + S (gcrt_common_modulus_gfull_merge_iff_merge_forward_lcm_other) = S ((S (gcrt_common_index_gfull_merge_iff_merge_forward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_forward_lcm_other_entry. b = ff_q_gcrt_gfull_merge_iff_merge_forward_lcm_other_entry * S ((S (gcrt_common_index_gfull_merge_iff_merge_forward_lcm_other)) * c) + (gcrt_common_modulus_gfull_merge_iff_merge_forward_lcm_other))) -> exists gcrt_common_quotient_gfull_merge_iff_merge_forward_lcm_other. gcrt_lcm_common_gfull_merge_iff_merge_forward_lcm = gcrt_common_modulus_gfull_merge_iff_merge_forward_lcm_other * gcrt_common_quotient_gfull_merge_iff_merge_forward_lcm_other) -> exists gcrt_lcm_quotient_gfull_merge_iff_merge_forward_lcm. gcrt_lcm_common_gfull_merge_iff_merge_forward_lcm = gcomp_merge_lcm_gfull_merge_iff_merge_forward * gcrt_lcm_quotient_gfull_merge_iff_merge_forward_lcm)) -> (forall gcrt_solution_index_gfull_merge_iff_merge_forward_solution gcrt_solution_residue_gfull_merge_iff_merge_forward_solution gcrt_solution_modulus_gfull_merge_iff_merge_forward_solution. (exists ff_lt_gcrt_gfull_merge_iff_merge_forward_solution_bound. ff_lt_gcrt_gfull_merge_iff_merge_forward_solution_bound + S gcrt_solution_index_gfull_merge_iff_merge_forward_solution = gcomp_merge_index_gfull_merge_iff_merge_forward) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_forward_solution_residue. ff_h_gcrt_gfull_merge_iff_merge_forward_solution_residue + S (gcrt_solution_residue_gfull_merge_iff_merge_forward_solution) = S ((S (gcrt_solution_index_gfull_merge_iff_merge_forward_solution)) * s)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_forward_solution_residue. r = ff_q_gcrt_gfull_merge_iff_merge_forward_solution_residue * S ((S (gcrt_solution_index_gfull_merge_iff_merge_forward_solution)) * s) + (gcrt_solution_residue_gfull_merge_iff_merge_forward_solution))) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_forward_solution_modulus. ff_h_gcrt_gfull_merge_iff_merge_forward_solution_modulus + S (gcrt_solution_modulus_gfull_merge_iff_merge_forward_solution) = S ((S (gcrt_solution_index_gfull_merge_iff_merge_forward_solution)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_forward_solution_modulus. b = ff_q_gcrt_gfull_merge_iff_merge_forward_solution_modulus * S ((S (gcrt_solution_index_gfull_merge_iff_merge_forward_solution)) * c) + (gcrt_solution_modulus_gfull_merge_iff_merge_forward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_merge_iff_merge_forward_solution_congruence hgcrt_mod_right_gcrt_gfull_merge_iff_merge_forward_solution_congruence. gcomp_merge_solution_gfull_merge_iff_merge_forward + gcrt_solution_modulus_gfull_merge_iff_merge_forward_solution * hgcrt_mod_left_gcrt_gfull_merge_iff_merge_forward_solution_congruence = gcrt_solution_residue_gfull_merge_iff_merge_forward_solution + gcrt_solution_modulus_gfull_merge_iff_merge_forward_solution * hgcrt_mod_right_gcrt_gfull_merge_iff_merge_forward_solution_congruence)) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_forward_residue. ff_h_gcrt_gfull_merge_iff_merge_forward_residue + S (gcomp_merge_residue_gfull_merge_iff_merge_forward) = S ((S (gcomp_merge_index_gfull_merge_iff_merge_forward)) * s)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_forward_residue. r = ff_q_gcrt_gfull_merge_iff_merge_forward_residue * S ((S (gcomp_merge_index_gfull_merge_iff_merge_forward)) * s) + (gcomp_merge_residue_gfull_merge_iff_merge_forward))) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_forward_modulus. ff_h_gcrt_gfull_merge_iff_merge_forward_modulus + S (gcomp_merge_modulus_gfull_merge_iff_merge_forward) = S ((S (gcomp_merge_index_gfull_merge_iff_merge_forward)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_forward_modulus. b = ff_q_gcrt_gfull_merge_iff_merge_forward_modulus * S ((S (gcomp_merge_index_gfull_merge_iff_merge_forward)) * c) + (gcomp_merge_modulus_gfull_merge_iff_merge_forward))) -> ((((exists hag_left_factor_gcomp_gfull_merge_iff_merge_forward_gcd. gcomp_merge_lcm_gfull_merge_iff_merge_forward = gcomp_merge_gcd_gfull_merge_iff_merge_forward * hag_left_factor_gcomp_gfull_merge_iff_merge_forward_gcd) /\ (exists hag_right_factor_gcomp_gfull_merge_iff_merge_forward_gcd. gcomp_merge_modulus_gfull_merge_iff_merge_forward = gcomp_merge_gcd_gfull_merge_iff_merge_forward * hag_right_factor_gcomp_gfull_merge_iff_merge_forward_gcd)) /\ forall hag_divisor_gcomp_gfull_merge_iff_merge_forward_gcd. (exists hag_common_left_gcomp_gfull_merge_iff_merge_forward_gcd. gcomp_merge_lcm_gfull_merge_iff_merge_forward = hag_divisor_gcomp_gfull_merge_iff_merge_forward_gcd * hag_common_left_gcomp_gfull_merge_iff_merge_forward_gcd) -> (exists hag_common_right_gcomp_gfull_merge_iff_merge_forward_gcd. gcomp_merge_modulus_gfull_merge_iff_merge_forward = hag_divisor_gcomp_gfull_merge_iff_merge_forward_gcd * hag_common_right_gcomp_gfull_merge_iff_merge_forward_gcd) -> exists hag_greatest_factor_gcomp_gfull_merge_iff_merge_forward_gcd. gcomp_merge_gcd_gfull_merge_iff_merge_forward = hag_divisor_gcomp_gfull_merge_iff_merge_forward_gcd * hag_greatest_factor_gcomp_gfull_merge_iff_merge_forward_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_merge_iff_merge_forward_result hgcrt_mod_right_gcrt_gfull_merge_iff_merge_forward_result. gcomp_merge_solution_gfull_merge_iff_merge_forward + gcomp_merge_gcd_gfull_merge_iff_merge_forward * hgcrt_mod_left_gcrt_gfull_merge_iff_merge_forward_result = gcomp_merge_residue_gfull_merge_iff_merge_forward + gcomp_merge_gcd_gfull_merge_iff_merge_forward * hgcrt_mod_right_gcrt_gfull_merge_iff_merge_forward_result))) /\ ((forall gcomp_merge_index_gfull_merge_iff_merge_backward gcomp_merge_solution_gfull_merge_iff_merge_backward gcomp_merge_lcm_gfull_merge_iff_merge_backward gcomp_merge_residue_gfull_merge_iff_merge_backward gcomp_merge_modulus_gfull_merge_iff_merge_backward gcomp_merge_gcd_gfull_merge_iff_merge_backward. (exists ff_lt_gcrt_gfull_merge_iff_merge_backward_bound. ff_lt_gcrt_gfull_merge_iff_merge_backward_bound + S gcomp_merge_index_gfull_merge_iff_merge_backward = l) -> (((forall gcrt_common_index_gfull_merge_iff_merge_backward_lcm_own gcrt_common_modulus_gfull_merge_iff_merge_backward_lcm_own. (exists ff_lt_gcrt_gfull_merge_iff_merge_backward_lcm_own_bound. ff_lt_gcrt_gfull_merge_iff_merge_backward_lcm_own_bound + S gcrt_common_index_gfull_merge_iff_merge_backward_lcm_own = gcomp_merge_index_gfull_merge_iff_merge_backward) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_backward_lcm_own_entry. ff_h_gcrt_gfull_merge_iff_merge_backward_lcm_own_entry + S (gcrt_common_modulus_gfull_merge_iff_merge_backward_lcm_own) = S ((S (gcrt_common_index_gfull_merge_iff_merge_backward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_backward_lcm_own_entry. b = ff_q_gcrt_gfull_merge_iff_merge_backward_lcm_own_entry * S ((S (gcrt_common_index_gfull_merge_iff_merge_backward_lcm_own)) * c) + (gcrt_common_modulus_gfull_merge_iff_merge_backward_lcm_own))) -> exists gcrt_common_quotient_gfull_merge_iff_merge_backward_lcm_own. gcomp_merge_lcm_gfull_merge_iff_merge_backward = gcrt_common_modulus_gfull_merge_iff_merge_backward_lcm_own * gcrt_common_quotient_gfull_merge_iff_merge_backward_lcm_own) /\ forall gcrt_lcm_common_gfull_merge_iff_merge_backward_lcm. (forall gcrt_common_index_gfull_merge_iff_merge_backward_lcm_other gcrt_common_modulus_gfull_merge_iff_merge_backward_lcm_other. (exists ff_lt_gcrt_gfull_merge_iff_merge_backward_lcm_other_bound. ff_lt_gcrt_gfull_merge_iff_merge_backward_lcm_other_bound + S gcrt_common_index_gfull_merge_iff_merge_backward_lcm_other = gcomp_merge_index_gfull_merge_iff_merge_backward) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_backward_lcm_other_entry. ff_h_gcrt_gfull_merge_iff_merge_backward_lcm_other_entry + S (gcrt_common_modulus_gfull_merge_iff_merge_backward_lcm_other) = S ((S (gcrt_common_index_gfull_merge_iff_merge_backward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_backward_lcm_other_entry. b = ff_q_gcrt_gfull_merge_iff_merge_backward_lcm_other_entry * S ((S (gcrt_common_index_gfull_merge_iff_merge_backward_lcm_other)) * c) + (gcrt_common_modulus_gfull_merge_iff_merge_backward_lcm_other))) -> exists gcrt_common_quotient_gfull_merge_iff_merge_backward_lcm_other. gcrt_lcm_common_gfull_merge_iff_merge_backward_lcm = gcrt_common_modulus_gfull_merge_iff_merge_backward_lcm_other * gcrt_common_quotient_gfull_merge_iff_merge_backward_lcm_other) -> exists gcrt_lcm_quotient_gfull_merge_iff_merge_backward_lcm. gcrt_lcm_common_gfull_merge_iff_merge_backward_lcm = gcomp_merge_lcm_gfull_merge_iff_merge_backward * gcrt_lcm_quotient_gfull_merge_iff_merge_backward_lcm)) -> (forall gcrt_solution_index_gfull_merge_iff_merge_backward_solution gcrt_solution_residue_gfull_merge_iff_merge_backward_solution gcrt_solution_modulus_gfull_merge_iff_merge_backward_solution. (exists ff_lt_gcrt_gfull_merge_iff_merge_backward_solution_bound. ff_lt_gcrt_gfull_merge_iff_merge_backward_solution_bound + S gcrt_solution_index_gfull_merge_iff_merge_backward_solution = gcomp_merge_index_gfull_merge_iff_merge_backward) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_backward_solution_residue. ff_h_gcrt_gfull_merge_iff_merge_backward_solution_residue + S (gcrt_solution_residue_gfull_merge_iff_merge_backward_solution) = S ((S (gcrt_solution_index_gfull_merge_iff_merge_backward_solution)) * s)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_backward_solution_residue. r = ff_q_gcrt_gfull_merge_iff_merge_backward_solution_residue * S ((S (gcrt_solution_index_gfull_merge_iff_merge_backward_solution)) * s) + (gcrt_solution_residue_gfull_merge_iff_merge_backward_solution))) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_backward_solution_modulus. ff_h_gcrt_gfull_merge_iff_merge_backward_solution_modulus + S (gcrt_solution_modulus_gfull_merge_iff_merge_backward_solution) = S ((S (gcrt_solution_index_gfull_merge_iff_merge_backward_solution)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_backward_solution_modulus. b = ff_q_gcrt_gfull_merge_iff_merge_backward_solution_modulus * S ((S (gcrt_solution_index_gfull_merge_iff_merge_backward_solution)) * c) + (gcrt_solution_modulus_gfull_merge_iff_merge_backward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_merge_iff_merge_backward_solution_congruence hgcrt_mod_right_gcrt_gfull_merge_iff_merge_backward_solution_congruence. gcomp_merge_solution_gfull_merge_iff_merge_backward + gcrt_solution_modulus_gfull_merge_iff_merge_backward_solution * hgcrt_mod_left_gcrt_gfull_merge_iff_merge_backward_solution_congruence = gcrt_solution_residue_gfull_merge_iff_merge_backward_solution + gcrt_solution_modulus_gfull_merge_iff_merge_backward_solution * hgcrt_mod_right_gcrt_gfull_merge_iff_merge_backward_solution_congruence)) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_backward_residue. ff_h_gcrt_gfull_merge_iff_merge_backward_residue + S (gcomp_merge_residue_gfull_merge_iff_merge_backward) = S ((S (gcomp_merge_index_gfull_merge_iff_merge_backward)) * s)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_backward_residue. r = ff_q_gcrt_gfull_merge_iff_merge_backward_residue * S ((S (gcomp_merge_index_gfull_merge_iff_merge_backward)) * s) + (gcomp_merge_residue_gfull_merge_iff_merge_backward))) -> (((exists ff_h_gcrt_gfull_merge_iff_merge_backward_modulus. ff_h_gcrt_gfull_merge_iff_merge_backward_modulus + S (gcomp_merge_modulus_gfull_merge_iff_merge_backward) = S ((S (gcomp_merge_index_gfull_merge_iff_merge_backward)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_merge_backward_modulus. b = ff_q_gcrt_gfull_merge_iff_merge_backward_modulus * S ((S (gcomp_merge_index_gfull_merge_iff_merge_backward)) * c) + (gcomp_merge_modulus_gfull_merge_iff_merge_backward))) -> ((((exists hag_left_factor_gcomp_gfull_merge_iff_merge_backward_gcd. gcomp_merge_lcm_gfull_merge_iff_merge_backward = gcomp_merge_gcd_gfull_merge_iff_merge_backward * hag_left_factor_gcomp_gfull_merge_iff_merge_backward_gcd) /\ (exists hag_right_factor_gcomp_gfull_merge_iff_merge_backward_gcd. gcomp_merge_modulus_gfull_merge_iff_merge_backward = gcomp_merge_gcd_gfull_merge_iff_merge_backward * hag_right_factor_gcomp_gfull_merge_iff_merge_backward_gcd)) /\ forall hag_divisor_gcomp_gfull_merge_iff_merge_backward_gcd. (exists hag_common_left_gcomp_gfull_merge_iff_merge_backward_gcd. gcomp_merge_lcm_gfull_merge_iff_merge_backward = hag_divisor_gcomp_gfull_merge_iff_merge_backward_gcd * hag_common_left_gcomp_gfull_merge_iff_merge_backward_gcd) -> (exists hag_common_right_gcomp_gfull_merge_iff_merge_backward_gcd. gcomp_merge_modulus_gfull_merge_iff_merge_backward = hag_divisor_gcomp_gfull_merge_iff_merge_backward_gcd * hag_common_right_gcomp_gfull_merge_iff_merge_backward_gcd) -> exists hag_greatest_factor_gcomp_gfull_merge_iff_merge_backward_gcd. gcomp_merge_gcd_gfull_merge_iff_merge_backward = hag_divisor_gcomp_gfull_merge_iff_merge_backward_gcd * hag_greatest_factor_gcomp_gfull_merge_iff_merge_backward_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_merge_iff_merge_backward_result hgcrt_mod_right_gcrt_gfull_merge_iff_merge_backward_result. gcomp_merge_solution_gfull_merge_iff_merge_backward + gcomp_merge_gcd_gfull_merge_iff_merge_backward * hgcrt_mod_left_gcrt_gfull_merge_iff_merge_backward_result = gcomp_merge_residue_gfull_merge_iff_merge_backward + gcomp_merge_gcd_gfull_merge_iff_merge_backward * hgcrt_mod_right_gcrt_gfull_merge_iff_merge_backward_result)) -> (forall gcomp_left_index_gfull_merge_iff_pairs_backward gcomp_right_index_gfull_merge_iff_pairs_backward gcomp_left_residue_gfull_merge_iff_pairs_backward gcomp_right_residue_gfull_merge_iff_pairs_backward gcomp_left_modulus_gfull_merge_iff_pairs_backward gcomp_right_modulus_gfull_merge_iff_pairs_backward gcomp_pair_gcd_gfull_merge_iff_pairs_backward. (exists ff_lt_gcrt_gfull_merge_iff_pairs_backward_left_bound. ff_lt_gcrt_gfull_merge_iff_pairs_backward_left_bound + S gcomp_left_index_gfull_merge_iff_pairs_backward = l) -> (exists ff_lt_gcrt_gfull_merge_iff_pairs_backward_right_bound. ff_lt_gcrt_gfull_merge_iff_pairs_backward_right_bound + S gcomp_right_index_gfull_merge_iff_pairs_backward = l) -> (((exists ff_h_gcrt_gfull_merge_iff_pairs_backward_left_residue. ff_h_gcrt_gfull_merge_iff_pairs_backward_left_residue + S (gcomp_left_residue_gfull_merge_iff_pairs_backward) = S ((S (gcomp_left_index_gfull_merge_iff_pairs_backward)) * s)) /\ exists ff_q_gcrt_gfull_merge_iff_pairs_backward_left_residue. r = ff_q_gcrt_gfull_merge_iff_pairs_backward_left_residue * S ((S (gcomp_left_index_gfull_merge_iff_pairs_backward)) * s) + (gcomp_left_residue_gfull_merge_iff_pairs_backward))) -> (((exists ff_h_gcrt_gfull_merge_iff_pairs_backward_right_residue. ff_h_gcrt_gfull_merge_iff_pairs_backward_right_residue + S (gcomp_right_residue_gfull_merge_iff_pairs_backward) = S ((S (gcomp_right_index_gfull_merge_iff_pairs_backward)) * s)) /\ exists ff_q_gcrt_gfull_merge_iff_pairs_backward_right_residue. r = ff_q_gcrt_gfull_merge_iff_pairs_backward_right_residue * S ((S (gcomp_right_index_gfull_merge_iff_pairs_backward)) * s) + (gcomp_right_residue_gfull_merge_iff_pairs_backward))) -> (((exists ff_h_gcrt_gfull_merge_iff_pairs_backward_left_modulus. ff_h_gcrt_gfull_merge_iff_pairs_backward_left_modulus + S (gcomp_left_modulus_gfull_merge_iff_pairs_backward) = S ((S (gcomp_left_index_gfull_merge_iff_pairs_backward)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_pairs_backward_left_modulus. b = ff_q_gcrt_gfull_merge_iff_pairs_backward_left_modulus * S ((S (gcomp_left_index_gfull_merge_iff_pairs_backward)) * c) + (gcomp_left_modulus_gfull_merge_iff_pairs_backward))) -> (((exists ff_h_gcrt_gfull_merge_iff_pairs_backward_right_modulus. ff_h_gcrt_gfull_merge_iff_pairs_backward_right_modulus + S (gcomp_right_modulus_gfull_merge_iff_pairs_backward) = S ((S (gcomp_right_index_gfull_merge_iff_pairs_backward)) * c)) /\ exists ff_q_gcrt_gfull_merge_iff_pairs_backward_right_modulus. b = ff_q_gcrt_gfull_merge_iff_pairs_backward_right_modulus * S ((S (gcomp_right_index_gfull_merge_iff_pairs_backward)) * c) + (gcomp_right_modulus_gfull_merge_iff_pairs_backward))) -> ((((exists hag_left_factor_gcomp_gfull_merge_iff_pairs_backward_gcd. gcomp_left_modulus_gfull_merge_iff_pairs_backward = gcomp_pair_gcd_gfull_merge_iff_pairs_backward * hag_left_factor_gcomp_gfull_merge_iff_pairs_backward_gcd) /\ (exists hag_right_factor_gcomp_gfull_merge_iff_pairs_backward_gcd. gcomp_right_modulus_gfull_merge_iff_pairs_backward = gcomp_pair_gcd_gfull_merge_iff_pairs_backward * hag_right_factor_gcomp_gfull_merge_iff_pairs_backward_gcd)) /\ forall hag_divisor_gcomp_gfull_merge_iff_pairs_backward_gcd. (exists hag_common_left_gcomp_gfull_merge_iff_pairs_backward_gcd. gcomp_left_modulus_gfull_merge_iff_pairs_backward = hag_divisor_gcomp_gfull_merge_iff_pairs_backward_gcd * hag_common_left_gcomp_gfull_merge_iff_pairs_backward_gcd) -> (exists hag_common_right_gcomp_gfull_merge_iff_pairs_backward_gcd. gcomp_right_modulus_gfull_merge_iff_pairs_backward = hag_divisor_gcomp_gfull_merge_iff_pairs_backward_gcd * hag_common_right_gcomp_gfull_merge_iff_pairs_backward_gcd) -> exists hag_greatest_factor_gcomp_gfull_merge_iff_pairs_backward_gcd. gcomp_pair_gcd_gfull_merge_iff_pairs_backward = hag_divisor_gcomp_gfull_merge_iff_pairs_backward_gcd * hag_greatest_factor_gcomp_gfull_merge_iff_pairs_backward_gcd)) -> (exists hgcrt_mod_left_gcrt_gfull_merge_iff_pairs_backward_result hgcrt_mod_right_gcrt_gfull_merge_iff_pairs_backward_result. gcomp_left_residue_gfull_merge_iff_pairs_backward + gcomp_pair_gcd_gfull_merge_iff_pairs_backward * hgcrt_mod_left_gcrt_gfull_merge_iff_pairs_backward_result = gcomp_right_residue_gfull_merge_iff_pairs_backward + gcomp_pair_gcd_gfull_merge_iff_pairs_backward * hgcrt_mod_right_gcrt_gfull_merge_iff_pairs_backward_result))))