crt_prefix_solution_class_iff_lcm

Exact expanded first-order arithmetic statement

forall r s b c l M x y. (((forall gcrt_common_index_iff_lcm_own gcrt_common_modulus_iff_lcm_own. (exists ff_lt_gcrt_iff_lcm_own_bound. ff_lt_gcrt_iff_lcm_own_bound + S gcrt_common_index_iff_lcm_own = l) -> (((exists ff_h_gcrt_iff_lcm_own_entry. ff_h_gcrt_iff_lcm_own_entry + S (gcrt_common_modulus_iff_lcm_own) = S ((S (gcrt_common_index_iff_lcm_own)) * c)) /\ exists ff_q_gcrt_iff_lcm_own_entry. b = ff_q_gcrt_iff_lcm_own_entry * S ((S (gcrt_common_index_iff_lcm_own)) * c) + (gcrt_common_modulus_iff_lcm_own))) -> exists gcrt_common_quotient_iff_lcm_own. M = gcrt_common_modulus_iff_lcm_own * gcrt_common_quotient_iff_lcm_own) /\ forall gcrt_lcm_common_iff_lcm. (forall gcrt_common_index_iff_lcm_other gcrt_common_modulus_iff_lcm_other. (exists ff_lt_gcrt_iff_lcm_other_bound. ff_lt_gcrt_iff_lcm_other_bound + S gcrt_common_index_iff_lcm_other = l) -> (((exists ff_h_gcrt_iff_lcm_other_entry. ff_h_gcrt_iff_lcm_other_entry + S (gcrt_common_modulus_iff_lcm_other) = S ((S (gcrt_common_index_iff_lcm_other)) * c)) /\ exists ff_q_gcrt_iff_lcm_other_entry. b = ff_q_gcrt_iff_lcm_other_entry * S ((S (gcrt_common_index_iff_lcm_other)) * c) + (gcrt_common_modulus_iff_lcm_other))) -> exists gcrt_common_quotient_iff_lcm_other. gcrt_lcm_common_iff_lcm = gcrt_common_modulus_iff_lcm_other * gcrt_common_quotient_iff_lcm_other) -> exists gcrt_lcm_quotient_iff_lcm. gcrt_lcm_common_iff_lcm = M * gcrt_lcm_quotient_iff_lcm)) -> (forall gcrt_solution_index_iff_fixed gcrt_solution_residue_iff_fixed gcrt_solution_modulus_iff_fixed. (exists ff_lt_gcrt_iff_fixed_bound. ff_lt_gcrt_iff_fixed_bound + S gcrt_solution_index_iff_fixed = l) -> (((exists ff_h_gcrt_iff_fixed_residue. ff_h_gcrt_iff_fixed_residue + S (gcrt_solution_residue_iff_fixed) = S ((S (gcrt_solution_index_iff_fixed)) * s)) /\ exists ff_q_gcrt_iff_fixed_residue. r = ff_q_gcrt_iff_fixed_residue * S ((S (gcrt_solution_index_iff_fixed)) * s) + (gcrt_solution_residue_iff_fixed))) -> (((exists ff_h_gcrt_iff_fixed_modulus. ff_h_gcrt_iff_fixed_modulus + S (gcrt_solution_modulus_iff_fixed) = S ((S (gcrt_solution_index_iff_fixed)) * c)) /\ exists ff_q_gcrt_iff_fixed_modulus. b = ff_q_gcrt_iff_fixed_modulus * S ((S (gcrt_solution_index_iff_fixed)) * c) + (gcrt_solution_modulus_iff_fixed))) -> (exists hgcrt_mod_left_gcrt_iff_fixed_congruence hgcrt_mod_right_gcrt_iff_fixed_congruence. x + gcrt_solution_modulus_iff_fixed * hgcrt_mod_left_gcrt_iff_fixed_congruence = gcrt_solution_residue_iff_fixed + gcrt_solution_modulus_iff_fixed * hgcrt_mod_right_gcrt_iff_fixed_congruence)) -> (((forall gcrt_solution_index_iff_candidate_forward gcrt_solution_residue_iff_candidate_forward gcrt_solution_modulus_iff_candidate_forward. (exists ff_lt_gcrt_iff_candidate_forward_bound. ff_lt_gcrt_iff_candidate_forward_bound + S gcrt_solution_index_iff_candidate_forward = l) -> (((exists ff_h_gcrt_iff_candidate_forward_residue. ff_h_gcrt_iff_candidate_forward_residue + S (gcrt_solution_residue_iff_candidate_forward) = S ((S (gcrt_solution_index_iff_candidate_forward)) * s)) /\ exists ff_q_gcrt_iff_candidate_forward_residue. r = ff_q_gcrt_iff_candidate_forward_residue * S ((S (gcrt_solution_index_iff_candidate_forward)) * s) + (gcrt_solution_residue_iff_candidate_forward))) -> (((exists ff_h_gcrt_iff_candidate_forward_modulus. ff_h_gcrt_iff_candidate_forward_modulus + S (gcrt_solution_modulus_iff_candidate_forward) = S ((S (gcrt_solution_index_iff_candidate_forward)) * c)) /\ exists ff_q_gcrt_iff_candidate_forward_modulus. b = ff_q_gcrt_iff_candidate_forward_modulus * S ((S (gcrt_solution_index_iff_candidate_forward)) * c) + (gcrt_solution_modulus_iff_candidate_forward))) -> (exists hgcrt_mod_left_gcrt_iff_candidate_forward_congruence hgcrt_mod_right_gcrt_iff_candidate_forward_congruence. y + gcrt_solution_modulus_iff_candidate_forward * hgcrt_mod_left_gcrt_iff_candidate_forward_congruence = gcrt_solution_residue_iff_candidate_forward + gcrt_solution_modulus_iff_candidate_forward * hgcrt_mod_right_gcrt_iff_candidate_forward_congruence)) -> (exists hgcrt_mod_left_gcrt_iff_mod_forward hgcrt_mod_right_gcrt_iff_mod_forward. y + M * hgcrt_mod_left_gcrt_iff_mod_forward = x + M * hgcrt_mod_right_gcrt_iff_mod_forward)) /\ ((exists hgcrt_mod_left_gcrt_iff_mod_reverse hgcrt_mod_right_gcrt_iff_mod_reverse. y + M * hgcrt_mod_left_gcrt_iff_mod_reverse = x + M * hgcrt_mod_right_gcrt_iff_mod_reverse) -> (forall gcrt_solution_index_iff_candidate_reverse gcrt_solution_residue_iff_candidate_reverse gcrt_solution_modulus_iff_candidate_reverse. (exists ff_lt_gcrt_iff_candidate_reverse_bound. ff_lt_gcrt_iff_candidate_reverse_bound + S gcrt_solution_index_iff_candidate_reverse = l) -> (((exists ff_h_gcrt_iff_candidate_reverse_residue. ff_h_gcrt_iff_candidate_reverse_residue + S (gcrt_solution_residue_iff_candidate_reverse) = S ((S (gcrt_solution_index_iff_candidate_reverse)) * s)) /\ exists ff_q_gcrt_iff_candidate_reverse_residue. r = ff_q_gcrt_iff_candidate_reverse_residue * S ((S (gcrt_solution_index_iff_candidate_reverse)) * s) + (gcrt_solution_residue_iff_candidate_reverse))) -> (((exists ff_h_gcrt_iff_candidate_reverse_modulus. ff_h_gcrt_iff_candidate_reverse_modulus + S (gcrt_solution_modulus_iff_candidate_reverse) = S ((S (gcrt_solution_index_iff_candidate_reverse)) * c)) /\ exists ff_q_gcrt_iff_candidate_reverse_modulus. b = ff_q_gcrt_iff_candidate_reverse_modulus * S ((S (gcrt_solution_index_iff_candidate_reverse)) * c) + (gcrt_solution_modulus_iff_candidate_reverse))) -> (exists hgcrt_mod_left_gcrt_iff_candidate_reverse_congruence hgcrt_mod_right_gcrt_iff_candidate_reverse_congruence. y + gcrt_solution_modulus_iff_candidate_reverse * hgcrt_mod_left_gcrt_iff_candidate_reverse_congruence = gcrt_solution_residue_iff_candidate_reverse + gcrt_solution_modulus_iff_candidate_reverse * hgcrt_mod_right_gcrt_iff_candidate_reverse_congruence))))