crt_positive_normalized_prefix_iff_canonical

Exact expanded first-order arithmetic statement

forall r s b c l x M. (forall gcrt_positive_index_gfull_normalized_positive_hypothesis gcrt_positive_value_gfull_normalized_positive_hypothesis. (exists ff_lt_gcrt_gfull_normalized_positive_hypothesis_bound. ff_lt_gcrt_gfull_normalized_positive_hypothesis_bound + S gcrt_positive_index_gfull_normalized_positive_hypothesis = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_hypothesis_entry. ff_h_gcrt_gfull_normalized_positive_hypothesis_entry + S (gcrt_positive_value_gfull_normalized_positive_hypothesis) = S ((S (gcrt_positive_index_gfull_normalized_positive_hypothesis)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_hypothesis_entry. b = ff_q_gcrt_gfull_normalized_positive_hypothesis_entry * S ((S (gcrt_positive_index_gfull_normalized_positive_hypothesis)) * c) + (gcrt_positive_value_gfull_normalized_positive_hypothesis))) -> ~(gcrt_positive_value_gfull_normalized_positive_hypothesis = 0)) -> (((((((forall gcrt_common_index_gfull_normalized_positive_forward_lcm_own gcrt_common_modulus_gfull_normalized_positive_forward_lcm_own. (exists ff_lt_gcrt_gfull_normalized_positive_forward_lcm_own_bound. ff_lt_gcrt_gfull_normalized_positive_forward_lcm_own_bound + S gcrt_common_index_gfull_normalized_positive_forward_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_forward_lcm_own_entry. ff_h_gcrt_gfull_normalized_positive_forward_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_positive_forward_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_positive_forward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_forward_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_positive_forward_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_positive_forward_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_positive_forward_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_positive_forward_lcm_own. M = gcrt_common_modulus_gfull_normalized_positive_forward_lcm_own * gcrt_common_quotient_gfull_normalized_positive_forward_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_positive_forward_lcm. (forall gcrt_common_index_gfull_normalized_positive_forward_lcm_other gcrt_common_modulus_gfull_normalized_positive_forward_lcm_other. (exists ff_lt_gcrt_gfull_normalized_positive_forward_lcm_other_bound. ff_lt_gcrt_gfull_normalized_positive_forward_lcm_other_bound + S gcrt_common_index_gfull_normalized_positive_forward_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_forward_lcm_other_entry. ff_h_gcrt_gfull_normalized_positive_forward_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_positive_forward_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_positive_forward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_forward_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_positive_forward_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_positive_forward_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_positive_forward_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_positive_forward_lcm_other. gcrt_lcm_common_gfull_normalized_positive_forward_lcm = gcrt_common_modulus_gfull_normalized_positive_forward_lcm_other * gcrt_common_quotient_gfull_normalized_positive_forward_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_positive_forward_lcm. gcrt_lcm_common_gfull_normalized_positive_forward_lcm = M * gcrt_lcm_quotient_gfull_normalized_positive_forward_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_positive_forward_bound. ff_lt_gcrt_gfull_normalized_positive_forward_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_positive_forward_solution gcrt_solution_residue_gfull_normalized_positive_forward_solution gcrt_solution_modulus_gfull_normalized_positive_forward_solution. (exists ff_lt_gcrt_gfull_normalized_positive_forward_solution_bound. ff_lt_gcrt_gfull_normalized_positive_forward_solution_bound + S gcrt_solution_index_gfull_normalized_positive_forward_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_forward_solution_residue. ff_h_gcrt_gfull_normalized_positive_forward_solution_residue + S (gcrt_solution_residue_gfull_normalized_positive_forward_solution) = S ((S (gcrt_solution_index_gfull_normalized_positive_forward_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_positive_forward_solution_residue. r = ff_q_gcrt_gfull_normalized_positive_forward_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_positive_forward_solution)) * s) + (gcrt_solution_residue_gfull_normalized_positive_forward_solution))) -> (((exists ff_h_gcrt_gfull_normalized_positive_forward_solution_modulus. ff_h_gcrt_gfull_normalized_positive_forward_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_positive_forward_solution) = S ((S (gcrt_solution_index_gfull_normalized_positive_forward_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_forward_solution_modulus. b = ff_q_gcrt_gfull_normalized_positive_forward_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_positive_forward_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_positive_forward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_positive_forward_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_positive_forward_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_positive_forward_solution * hgcrt_mod_left_gcrt_gfull_normalized_positive_forward_solution_congruence = gcrt_solution_residue_gfull_normalized_positive_forward_solution + gcrt_solution_modulus_gfull_normalized_positive_forward_solution * hgcrt_mod_right_gcrt_gfull_normalized_positive_forward_solution_congruence))))) -> (((((forall gcrt_common_index_gfull_canonical_positive_forward_lcm_own gcrt_common_modulus_gfull_canonical_positive_forward_lcm_own. (exists ff_lt_gcrt_gfull_canonical_positive_forward_lcm_own_bound. ff_lt_gcrt_gfull_canonical_positive_forward_lcm_own_bound + S gcrt_common_index_gfull_canonical_positive_forward_lcm_own = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_forward_lcm_own_entry. ff_h_gcrt_gfull_canonical_positive_forward_lcm_own_entry + S (gcrt_common_modulus_gfull_canonical_positive_forward_lcm_own) = S ((S (gcrt_common_index_gfull_canonical_positive_forward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_forward_lcm_own_entry. b = ff_q_gcrt_gfull_canonical_positive_forward_lcm_own_entry * S ((S (gcrt_common_index_gfull_canonical_positive_forward_lcm_own)) * c) + (gcrt_common_modulus_gfull_canonical_positive_forward_lcm_own))) -> exists gcrt_common_quotient_gfull_canonical_positive_forward_lcm_own. M = gcrt_common_modulus_gfull_canonical_positive_forward_lcm_own * gcrt_common_quotient_gfull_canonical_positive_forward_lcm_own) /\ forall gcrt_lcm_common_gfull_canonical_positive_forward_lcm. (forall gcrt_common_index_gfull_canonical_positive_forward_lcm_other gcrt_common_modulus_gfull_canonical_positive_forward_lcm_other. (exists ff_lt_gcrt_gfull_canonical_positive_forward_lcm_other_bound. ff_lt_gcrt_gfull_canonical_positive_forward_lcm_other_bound + S gcrt_common_index_gfull_canonical_positive_forward_lcm_other = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_forward_lcm_other_entry. ff_h_gcrt_gfull_canonical_positive_forward_lcm_other_entry + S (gcrt_common_modulus_gfull_canonical_positive_forward_lcm_other) = S ((S (gcrt_common_index_gfull_canonical_positive_forward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_forward_lcm_other_entry. b = ff_q_gcrt_gfull_canonical_positive_forward_lcm_other_entry * S ((S (gcrt_common_index_gfull_canonical_positive_forward_lcm_other)) * c) + (gcrt_common_modulus_gfull_canonical_positive_forward_lcm_other))) -> exists gcrt_common_quotient_gfull_canonical_positive_forward_lcm_other. gcrt_lcm_common_gfull_canonical_positive_forward_lcm = gcrt_common_modulus_gfull_canonical_positive_forward_lcm_other * gcrt_common_quotient_gfull_canonical_positive_forward_lcm_other) -> exists gcrt_lcm_quotient_gfull_canonical_positive_forward_lcm. gcrt_lcm_common_gfull_canonical_positive_forward_lcm = M * gcrt_lcm_quotient_gfull_canonical_positive_forward_lcm)) /\ ((exists ff_lt_gcrt_gfull_canonical_positive_forward_bounded. ff_lt_gcrt_gfull_canonical_positive_forward_bounded + S x = M) /\ (forall gcrt_solution_index_gfull_canonical_positive_forward_solution gcrt_solution_residue_gfull_canonical_positive_forward_solution gcrt_solution_modulus_gfull_canonical_positive_forward_solution. (exists ff_lt_gcrt_gfull_canonical_positive_forward_solution_bound. ff_lt_gcrt_gfull_canonical_positive_forward_solution_bound + S gcrt_solution_index_gfull_canonical_positive_forward_solution = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_forward_solution_residue. ff_h_gcrt_gfull_canonical_positive_forward_solution_residue + S (gcrt_solution_residue_gfull_canonical_positive_forward_solution) = S ((S (gcrt_solution_index_gfull_canonical_positive_forward_solution)) * s)) /\ exists ff_q_gcrt_gfull_canonical_positive_forward_solution_residue. r = ff_q_gcrt_gfull_canonical_positive_forward_solution_residue * S ((S (gcrt_solution_index_gfull_canonical_positive_forward_solution)) * s) + (gcrt_solution_residue_gfull_canonical_positive_forward_solution))) -> (((exists ff_h_gcrt_gfull_canonical_positive_forward_solution_modulus. ff_h_gcrt_gfull_canonical_positive_forward_solution_modulus + S (gcrt_solution_modulus_gfull_canonical_positive_forward_solution) = S ((S (gcrt_solution_index_gfull_canonical_positive_forward_solution)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_forward_solution_modulus. b = ff_q_gcrt_gfull_canonical_positive_forward_solution_modulus * S ((S (gcrt_solution_index_gfull_canonical_positive_forward_solution)) * c) + (gcrt_solution_modulus_gfull_canonical_positive_forward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_canonical_positive_forward_solution_congruence hgcrt_mod_right_gcrt_gfull_canonical_positive_forward_solution_congruence. x + gcrt_solution_modulus_gfull_canonical_positive_forward_solution * hgcrt_mod_left_gcrt_gfull_canonical_positive_forward_solution_congruence = gcrt_solution_residue_gfull_canonical_positive_forward_solution + gcrt_solution_modulus_gfull_canonical_positive_forward_solution * hgcrt_mod_right_gcrt_gfull_canonical_positive_forward_solution_congruence)))))) /\ ((((((forall gcrt_common_index_gfull_canonical_positive_backward_lcm_own gcrt_common_modulus_gfull_canonical_positive_backward_lcm_own. (exists ff_lt_gcrt_gfull_canonical_positive_backward_lcm_own_bound. ff_lt_gcrt_gfull_canonical_positive_backward_lcm_own_bound + S gcrt_common_index_gfull_canonical_positive_backward_lcm_own = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_backward_lcm_own_entry. ff_h_gcrt_gfull_canonical_positive_backward_lcm_own_entry + S (gcrt_common_modulus_gfull_canonical_positive_backward_lcm_own) = S ((S (gcrt_common_index_gfull_canonical_positive_backward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_backward_lcm_own_entry. b = ff_q_gcrt_gfull_canonical_positive_backward_lcm_own_entry * S ((S (gcrt_common_index_gfull_canonical_positive_backward_lcm_own)) * c) + (gcrt_common_modulus_gfull_canonical_positive_backward_lcm_own))) -> exists gcrt_common_quotient_gfull_canonical_positive_backward_lcm_own. M = gcrt_common_modulus_gfull_canonical_positive_backward_lcm_own * gcrt_common_quotient_gfull_canonical_positive_backward_lcm_own) /\ forall gcrt_lcm_common_gfull_canonical_positive_backward_lcm. (forall gcrt_common_index_gfull_canonical_positive_backward_lcm_other gcrt_common_modulus_gfull_canonical_positive_backward_lcm_other. (exists ff_lt_gcrt_gfull_canonical_positive_backward_lcm_other_bound. ff_lt_gcrt_gfull_canonical_positive_backward_lcm_other_bound + S gcrt_common_index_gfull_canonical_positive_backward_lcm_other = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_backward_lcm_other_entry. ff_h_gcrt_gfull_canonical_positive_backward_lcm_other_entry + S (gcrt_common_modulus_gfull_canonical_positive_backward_lcm_other) = S ((S (gcrt_common_index_gfull_canonical_positive_backward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_backward_lcm_other_entry. b = ff_q_gcrt_gfull_canonical_positive_backward_lcm_other_entry * S ((S (gcrt_common_index_gfull_canonical_positive_backward_lcm_other)) * c) + (gcrt_common_modulus_gfull_canonical_positive_backward_lcm_other))) -> exists gcrt_common_quotient_gfull_canonical_positive_backward_lcm_other. gcrt_lcm_common_gfull_canonical_positive_backward_lcm = gcrt_common_modulus_gfull_canonical_positive_backward_lcm_other * gcrt_common_quotient_gfull_canonical_positive_backward_lcm_other) -> exists gcrt_lcm_quotient_gfull_canonical_positive_backward_lcm. gcrt_lcm_common_gfull_canonical_positive_backward_lcm = M * gcrt_lcm_quotient_gfull_canonical_positive_backward_lcm)) /\ ((exists ff_lt_gcrt_gfull_canonical_positive_backward_bounded. ff_lt_gcrt_gfull_canonical_positive_backward_bounded + S x = M) /\ (forall gcrt_solution_index_gfull_canonical_positive_backward_solution gcrt_solution_residue_gfull_canonical_positive_backward_solution gcrt_solution_modulus_gfull_canonical_positive_backward_solution. (exists ff_lt_gcrt_gfull_canonical_positive_backward_solution_bound. ff_lt_gcrt_gfull_canonical_positive_backward_solution_bound + S gcrt_solution_index_gfull_canonical_positive_backward_solution = l) -> (((exists ff_h_gcrt_gfull_canonical_positive_backward_solution_residue. ff_h_gcrt_gfull_canonical_positive_backward_solution_residue + S (gcrt_solution_residue_gfull_canonical_positive_backward_solution) = S ((S (gcrt_solution_index_gfull_canonical_positive_backward_solution)) * s)) /\ exists ff_q_gcrt_gfull_canonical_positive_backward_solution_residue. r = ff_q_gcrt_gfull_canonical_positive_backward_solution_residue * S ((S (gcrt_solution_index_gfull_canonical_positive_backward_solution)) * s) + (gcrt_solution_residue_gfull_canonical_positive_backward_solution))) -> (((exists ff_h_gcrt_gfull_canonical_positive_backward_solution_modulus. ff_h_gcrt_gfull_canonical_positive_backward_solution_modulus + S (gcrt_solution_modulus_gfull_canonical_positive_backward_solution) = S ((S (gcrt_solution_index_gfull_canonical_positive_backward_solution)) * c)) /\ exists ff_q_gcrt_gfull_canonical_positive_backward_solution_modulus. b = ff_q_gcrt_gfull_canonical_positive_backward_solution_modulus * S ((S (gcrt_solution_index_gfull_canonical_positive_backward_solution)) * c) + (gcrt_solution_modulus_gfull_canonical_positive_backward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_canonical_positive_backward_solution_congruence hgcrt_mod_right_gcrt_gfull_canonical_positive_backward_solution_congruence. x + gcrt_solution_modulus_gfull_canonical_positive_backward_solution * hgcrt_mod_left_gcrt_gfull_canonical_positive_backward_solution_congruence = gcrt_solution_residue_gfull_canonical_positive_backward_solution + gcrt_solution_modulus_gfull_canonical_positive_backward_solution * hgcrt_mod_right_gcrt_gfull_canonical_positive_backward_solution_congruence))))) -> (((((forall gcrt_common_index_gfull_normalized_positive_backward_lcm_own gcrt_common_modulus_gfull_normalized_positive_backward_lcm_own. (exists ff_lt_gcrt_gfull_normalized_positive_backward_lcm_own_bound. ff_lt_gcrt_gfull_normalized_positive_backward_lcm_own_bound + S gcrt_common_index_gfull_normalized_positive_backward_lcm_own = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_backward_lcm_own_entry. ff_h_gcrt_gfull_normalized_positive_backward_lcm_own_entry + S (gcrt_common_modulus_gfull_normalized_positive_backward_lcm_own) = S ((S (gcrt_common_index_gfull_normalized_positive_backward_lcm_own)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_backward_lcm_own_entry. b = ff_q_gcrt_gfull_normalized_positive_backward_lcm_own_entry * S ((S (gcrt_common_index_gfull_normalized_positive_backward_lcm_own)) * c) + (gcrt_common_modulus_gfull_normalized_positive_backward_lcm_own))) -> exists gcrt_common_quotient_gfull_normalized_positive_backward_lcm_own. M = gcrt_common_modulus_gfull_normalized_positive_backward_lcm_own * gcrt_common_quotient_gfull_normalized_positive_backward_lcm_own) /\ forall gcrt_lcm_common_gfull_normalized_positive_backward_lcm. (forall gcrt_common_index_gfull_normalized_positive_backward_lcm_other gcrt_common_modulus_gfull_normalized_positive_backward_lcm_other. (exists ff_lt_gcrt_gfull_normalized_positive_backward_lcm_other_bound. ff_lt_gcrt_gfull_normalized_positive_backward_lcm_other_bound + S gcrt_common_index_gfull_normalized_positive_backward_lcm_other = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_backward_lcm_other_entry. ff_h_gcrt_gfull_normalized_positive_backward_lcm_other_entry + S (gcrt_common_modulus_gfull_normalized_positive_backward_lcm_other) = S ((S (gcrt_common_index_gfull_normalized_positive_backward_lcm_other)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_backward_lcm_other_entry. b = ff_q_gcrt_gfull_normalized_positive_backward_lcm_other_entry * S ((S (gcrt_common_index_gfull_normalized_positive_backward_lcm_other)) * c) + (gcrt_common_modulus_gfull_normalized_positive_backward_lcm_other))) -> exists gcrt_common_quotient_gfull_normalized_positive_backward_lcm_other. gcrt_lcm_common_gfull_normalized_positive_backward_lcm = gcrt_common_modulus_gfull_normalized_positive_backward_lcm_other * gcrt_common_quotient_gfull_normalized_positive_backward_lcm_other) -> exists gcrt_lcm_quotient_gfull_normalized_positive_backward_lcm. gcrt_lcm_common_gfull_normalized_positive_backward_lcm = M * gcrt_lcm_quotient_gfull_normalized_positive_backward_lcm)) /\ ((M = 0 \/ (exists ff_lt_gcrt_gfull_normalized_positive_backward_bound. ff_lt_gcrt_gfull_normalized_positive_backward_bound + S x = M)) /\ (forall gcrt_solution_index_gfull_normalized_positive_backward_solution gcrt_solution_residue_gfull_normalized_positive_backward_solution gcrt_solution_modulus_gfull_normalized_positive_backward_solution. (exists ff_lt_gcrt_gfull_normalized_positive_backward_solution_bound. ff_lt_gcrt_gfull_normalized_positive_backward_solution_bound + S gcrt_solution_index_gfull_normalized_positive_backward_solution = l) -> (((exists ff_h_gcrt_gfull_normalized_positive_backward_solution_residue. ff_h_gcrt_gfull_normalized_positive_backward_solution_residue + S (gcrt_solution_residue_gfull_normalized_positive_backward_solution) = S ((S (gcrt_solution_index_gfull_normalized_positive_backward_solution)) * s)) /\ exists ff_q_gcrt_gfull_normalized_positive_backward_solution_residue. r = ff_q_gcrt_gfull_normalized_positive_backward_solution_residue * S ((S (gcrt_solution_index_gfull_normalized_positive_backward_solution)) * s) + (gcrt_solution_residue_gfull_normalized_positive_backward_solution))) -> (((exists ff_h_gcrt_gfull_normalized_positive_backward_solution_modulus. ff_h_gcrt_gfull_normalized_positive_backward_solution_modulus + S (gcrt_solution_modulus_gfull_normalized_positive_backward_solution) = S ((S (gcrt_solution_index_gfull_normalized_positive_backward_solution)) * c)) /\ exists ff_q_gcrt_gfull_normalized_positive_backward_solution_modulus. b = ff_q_gcrt_gfull_normalized_positive_backward_solution_modulus * S ((S (gcrt_solution_index_gfull_normalized_positive_backward_solution)) * c) + (gcrt_solution_modulus_gfull_normalized_positive_backward_solution))) -> (exists hgcrt_mod_left_gcrt_gfull_normalized_positive_backward_solution_congruence hgcrt_mod_right_gcrt_gfull_normalized_positive_backward_solution_congruence. x + gcrt_solution_modulus_gfull_normalized_positive_backward_solution * hgcrt_mod_left_gcrt_gfull_normalized_positive_backward_solution_congruence = gcrt_solution_residue_gfull_normalized_positive_backward_solution + gcrt_solution_modulus_gfull_normalized_positive_backward_solution * hgcrt_mod_right_gcrt_gfull_normalized_positive_backward_solution_congruence)))))))