crt_normalized_prefix_solution_class_iff_lcm

Exact expanded first-order arithmetic statement

forall r s b c l M x y. (((((forall gcrt_common_index_gfull_normalized_class_source_lcm_own gcrt_common_modulus_gfull_normalized_class_source_lcm_own. (exists ff_lt_gcrt_gfull_normalized_class_source_lcm_own_bound. ff_lt_gcrt_gfull_normalized_class_source_lcm_own_bound + S gcrt_common_index_gfull_normalized_class_source_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_class_source_lcm_own_entry. ff_h_gcrt_gfull_normalized_class_source_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_class_source_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_class_source_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_source_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_class_source_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_class_source_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_class_source_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_class_source_lcm_own. M = gcrt_common_modulus_gfull_normalized_class_source_lcm_own * gcrt_common_quotient_gfull_normalized_class_source_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_class_source_lcm. (forall gcrt_common_index_gfull_normalized_class_source_lcm_other gcrt_common_modulus_gfull_normalized_class_source_lcm_other. (exists ff_lt_gcrt_gfull_normalized_class_source_lcm_other_bound. ff_lt_gcrt_gfull_normalized_class_source_lcm_other_bound + S gcrt_common_index_gfull_normalized_class_source_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_class_source_lcm_other_entry. ff_h_gcrt_gfull_normalized_class_source_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_class_source_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_class_source_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_source_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_class_source_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_class_source_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_class_source_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_class_source_lcm_other. gcrt_lcm_common_gfull_normalized_class_source_lcm = gcrt_common_modulus_gfull_normalized_class_source_lcm_other * gcrt_common_quotient_gfull_normalized_class_source_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_class_source_lcm. gcrt_lcm_common_gfull_normalized_class_source_lcm = M * gcrt_lcm_quotient_gfull_normalized_class_source_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_class_source_bound. ff_lt_gcrt_gfull_normalized_class_source_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_class_source_solution gcrt_solution_residue_gfull_normalized_class_source_solution gcrt_solution_modulus_gfull_normalized_class_source_solution. (exists ff_lt_gcrt_gfull_normalized_class_source_solution_bound. ff_lt_gcrt_gfull_normalized_class_source_solution_bound + S gcrt_solution_index_gfull_normalized_class_source_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_class_source_solution_residue. ff_h_gcrt_gfull_normalized_class_source_solution_residue + S (gcrt_solution_residue_gfull_normalized_class_source_solution) = S ((S (gcrt_solution_index_gfull_normalized_class_source_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_class_source_solution_residue. r = ff_q_gcrt_gfull_normalized_class_source_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_class_source_solution)) * s) + (gcrt_solution_residue_gfull_normalized_class_source_solution))) -> (((exists ff_h_gcrt_gfull_normalized_class_source_solution_modulus. ff_h_gcrt_gfull_normalized_class_source_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_class_source_solution) = S ((S (gcrt_solution_index_gfull_normalized_class_source_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_source_solution_modulus. b = ff_q_gcrt_gfull_normalized_class_source_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_class_source_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_class_source_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_class_source_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_class_source_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_class_source_solution * hgcrt_mod_left_gcrt_gfull_normalized_class_source_solution_congruence = gcrt_solution_residue_gfull_normalized_class_source_solution + gcrt_solution_modulus_gfull_normalized_class_source_solution * hgcrt_mod_right_gcrt_gfull_normalized_class_source_solution_congruence))))) -> (((forall gcrt_solution_index_gfull_normalized_class_solution_forward gcrt_solution_residue_gfull_normalized_class_solution_forward gcrt_solution_modulus_gfull_normalized_class_solution_forward. (exists ff_lt_gcrt_gfull_normalized_class_solution_forward_bound. ff_lt_gcrt_gfull_normalized_class_solution_forward_bound + S gcrt_solution_index_gfull_normalized_class_solution_forward = l) -> (((exists ff_h_gcrt_gfull_normalized_class_solution_forward_residue. ff_h_gcrt_gfull_normalized_class_solution_forward_residue + S (gcrt_solution_residue_gfull_normalized_class_solution_forward) = S ((S (gcrt_solution_index_gfull_normalized_class_solution_forward)) * s)) /\ exists ff_q_gcrt_gfull_normalized_class_solution_forward_residue. r = ff_q_gcrt_gfull_normalized_class_solution_forward_residue * S ((S (gcrt_solution_index_gfull_normalized_class_solution_forward)) * s) + (gcrt_solution_residue_gfull_normalized_class_solution_forward))) -> (((exists ff_h_gcrt_gfull_normalized_class_solution_forward_modulus. ff_h_gcrt_gfull_normalized_class_solution_forward_modulus + S (gcrt_solution_modulus_gfull_normalized_class_solution_forward) = S ((S (gcrt_solution_index_gfull_normalized_class_solution_forward)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_solution_forward_modulus. b = ff_q_gcrt_gfull_normalized_class_solution_forward_modulus * S ((S (gcrt_solution_index_gfull_normalized_class_solution_forward)) * c) + (gcrt_solution_modulus_gfull_normalized_class_solution_forward))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_class_solution_forward_congruence hgcrt_mod_right_gcrt_gfull_normalized_class_solution_forward_congruence. y + gcrt_solution_modulus_gfull_normalized_class_solution_forward * hgcrt_mod_left_gcrt_gfull_normalized_class_solution_forward_congruence = gcrt_solution_residue_gfull_normalized_class_solution_forward + gcrt_solution_modulus_gfull_normalized_class_solution_forward * hgcrt_mod_right_gcrt_gfull_normalized_class_solution_forward_congruence)) -> (exists hgcrt_mod_left_gfull_normalized_class_mod_forward hgcrt_mod_right_gfull_normalized_class_mod_forward. y + M * hgcrt_mod_left_gfull_normalized_class_mod_forward = x + M * hgcrt_mod_right_gfull_normalized_class_mod_forward)) /\ ((exists hgcrt_mod_left_gfull_normalized_class_mod_backward hgcrt_mod_right_gfull_normalized_class_mod_backward. y + M * hgcrt_mod_left_gfull_normalized_class_mod_backward = x + M * hgcrt_mod_right_gfull_normalized_class_mod_backward) -> (forall gcrt_solution_index_gfull_normalized_class_solution_backward gcrt_solution_residue_gfull_normalized_class_solution_backward gcrt_solution_modulus_gfull_normalized_class_solution_backward. (exists ff_lt_gcrt_gfull_normalized_class_solution_backward_bound. ff_lt_gcrt_gfull_normalized_class_solution_backward_bound + S gcrt_solution_index_gfull_normalized_class_solution_backward = l) -> (((exists ff_h_gcrt_gfull_normalized_class_solution_backward_residue. ff_h_gcrt_gfull_normalized_class_solution_backward_residue + S (gcrt_solution_residue_gfull_normalized_class_solution_backward) = S ((S (gcrt_solution_index_gfull_normalized_class_solution_backward)) * s)) /\ exists ff_q_gcrt_gfull_normalized_class_solution_backward_residue. r = ff_q_gcrt_gfull_normalized_class_solution_backward_residue * S ((S (gcrt_solution_index_gfull_normalized_class_solution_backward)) * s) + (gcrt_solution_residue_gfull_normalized_class_solution_backward))) -> (((exists ff_h_gcrt_gfull_normalized_class_solution_backward_modulus. ff_h_gcrt_gfull_normalized_class_solution_backward_modulus + S (gcrt_solution_modulus_gfull_normalized_class_solution_backward) = S ((S (gcrt_solution_index_gfull_normalized_class_solution_backward)) * c)) /\ exists ff_q_gcrt_gfull_normalized_class_solution_backward_modulus. b = ff_q_gcrt_gfull_normalized_class_solution_backward_modulus * S ((S (gcrt_solution_index_gfull_normalized_class_solution_backward)) * c) + (gcrt_solution_modulus_gfull_normalized_class_solution_backward))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_class_solution_backward_congruence hgcrt_mod_right_gcrt_gfull_normalized_class_solution_backward_congruence. y + gcrt_solution_modulus_gfull_normalized_class_solution_backward * hgcrt_mod_left_gcrt_gfull_normalized_class_solution_backward_congruence = gcrt_solution_residue_gfull_normalized_class_solution_backward + gcrt_solution_modulus_gfull_normalized_class_solution_backward * hgcrt_mod_right_gcrt_gfull_normalized_class_solution_backward_congruence))))