scaled_inverse_pair_order_choose_append

Exact expanded PA statement

forall p a n u v b c l. p = S n -> ((~(p = 1) /\ forall esi_prime_left_espo_choose_prime esi_prime_right_espo_choose_prime. p = esi_prime_left_espo_choose_prime * esi_prime_right_espo_choose_prime -> esi_prime_left_espo_choose_prime = 1 \/ esi_prime_right_espo_choose_prime = 1)) -> ~(exists qr_x_espo_choose_nonresidue. exists qr_u_espo_choose_nonresidue qr_v_espo_choose_nonresidue. qr_x_espo_choose_nonresidue * qr_x_espo_choose_nonresidue + p * qr_u_espo_choose_nonresidue = a + p * qr_v_espo_choose_nonresidue) -> (forall esip_index_espo_choose_prefix. (exists esip_gap_espo_choose_prefix_prefix_bound. esip_gap_espo_choose_prefix_prefix_bound + S (esip_index_espo_choose_prefix) = n) -> exists esip_mate_espo_choose_prefix. ((((exists ff_h_esip_espo_choose_prefix_entry. ff_h_esip_espo_choose_prefix_entry + S (esip_mate_espo_choose_prefix) = S ((S (esip_index_espo_choose_prefix)) * v)) /\ exists ff_q_esip_espo_choose_prefix_entry. u = ff_q_esip_espo_choose_prefix_entry * S ((S (esip_index_espo_choose_prefix)) * v) + (esip_mate_espo_choose_prefix))) /\ ((exists esip_gap_espo_choose_prefix_relation_index_bound. esip_gap_espo_choose_prefix_relation_index_bound + S (esip_index_espo_choose_prefix) = n) /\ ((((~((S esip_index_espo_choose_prefix) = 0) /\ (exists esip_gap_espo_choose_prefix_relation_scaled_left_bound. esip_gap_espo_choose_prefix_relation_scaled_left_bound + S (S esip_index_espo_choose_prefix) = p))) /\ (((~(esip_mate_espo_choose_prefix = 0) /\ (exists esip_gap_espo_choose_prefix_relation_scaled_right_bound. esip_gap_espo_choose_prefix_relation_scaled_right_bound + S (esip_mate_espo_choose_prefix) = p))) /\ (exists esi_mod_left_espo_choose_prefix_relation_scaled_mod esi_mod_right_espo_choose_prefix_relation_scaled_mod. ((S esip_index_espo_choose_prefix) * esip_mate_espo_choose_prefix) + p * esi_mod_left_espo_choose_prefix_relation_scaled_mod = (a) + p * esi_mod_right_espo_choose_prefix_relation_scaled_mod))))))) -> (exists wpo_gap_choose_short. wpo_gap_choose_short + S (l) = n) -> (forall espo_position_step_closed_before espo_source_step_closed_before espo_mate_step_closed_before. (exists wpo_gap_step_closed_before_position_bound. wpo_gap_step_closed_before_position_bound + S (espo_position_step_closed_before) = l) -> (((exists wpo_beta_height_step_closed_before_source_entry. wpo_beta_height_step_closed_before_source_entry + S (espo_source_step_closed_before) = S ((S (espo_position_step_closed_before)) * c)) /\ exists wpo_beta_quotient_step_closed_before_source_entry. b = wpo_beta_quotient_step_closed_before_source_entry * S ((S (espo_position_step_closed_before)) * c) + (espo_source_step_closed_before))) -> (((exists wpo_beta_height_step_closed_before_scaled_entry. wpo_beta_height_step_closed_before_scaled_entry + S (S espo_mate_step_closed_before) = S ((S (espo_source_step_closed_before)) * v)) /\ exists wpo_beta_quotient_step_closed_before_scaled_entry. u = wpo_beta_quotient_step_closed_before_scaled_entry * S ((S (espo_source_step_closed_before)) * v) + (S espo_mate_step_closed_before))) -> exists espo_mate_position_step_closed_before. ((exists wpo_gap_step_closed_before_mate_bound. wpo_gap_step_closed_before_mate_bound + S (espo_mate_position_step_closed_before) = l) /\ (((exists wpo_beta_height_step_closed_before_mate_entry. wpo_beta_height_step_closed_before_mate_entry + S (espo_mate_step_closed_before) = S ((S (espo_mate_position_step_closed_before)) * c)) /\ exists wpo_beta_quotient_step_closed_before_mate_entry. b = wpo_beta_quotient_step_closed_before_mate_entry * S ((S (espo_mate_position_step_closed_before)) * c) + (espo_mate_step_closed_before))))) -> (forall wpo_injective_left_step_injective_before wpo_injective_right_step_injective_before wpo_injective_value_step_injective_before. (exists wpo_gap_step_injective_before_left_bound. wpo_gap_step_injective_before_left_bound + S (wpo_injective_left_step_injective_before) = l) -> (exists wpo_gap_step_injective_before_right_bound. wpo_gap_step_injective_before_right_bound + S (wpo_injective_right_step_injective_before) = l) -> (((exists wpo_beta_height_step_injective_before_left_entry. wpo_beta_height_step_injective_before_left_entry + S (wpo_injective_value_step_injective_before) = S ((S (wpo_injective_left_step_injective_before)) * c)) /\ exists wpo_beta_quotient_step_injective_before_left_entry. b = wpo_beta_quotient_step_injective_before_left_entry * S ((S (wpo_injective_left_step_injective_before)) * c) + (wpo_injective_value_step_injective_before))) -> (((exists wpo_beta_height_step_injective_before_right_entry. wpo_beta_height_step_injective_before_right_entry + S (wpo_injective_value_step_injective_before) = S ((S (wpo_injective_right_step_injective_before)) * c)) /\ exists wpo_beta_quotient_step_injective_before_right_entry. b = wpo_beta_quotient_step_injective_before_right_entry * S ((S (wpo_injective_right_step_injective_before)) * c) + (wpo_injective_value_step_injective_before))) -> wpo_injective_left_step_injective_before = wpo_injective_right_step_injective_before) -> (exists z d i j. ((((((exists wpo_beta_height_step_trace_first. wpo_beta_height_step_trace_first + S (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_step_trace_first. z = wpo_beta_quotient_step_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_step_trace_second. wpo_beta_height_step_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_step_trace_second. z = wpo_beta_quotient_step_trace_second * S ((S (S (l))) * d) + (j))) /\ (forall wpo_old_index_step_trace wpo_old_value_step_trace. (exists wpo_gap_step_trace_old_bound. wpo_gap_step_trace_old_bound + S (wpo_old_index_step_trace) = l) -> (((exists wpo_beta_height_step_trace_old_entry. wpo_beta_height_step_trace_old_entry + S (wpo_old_value_step_trace) = S ((S (wpo_old_index_step_trace)) * c)) /\ exists wpo_beta_quotient_step_trace_old_entry. b = wpo_beta_quotient_step_trace_old_entry * S ((S (wpo_old_index_step_trace)) * c) + (wpo_old_value_step_trace))) -> (((exists wpo_beta_height_step_trace_new_entry. wpo_beta_height_step_trace_new_entry + S (wpo_old_value_step_trace) = S ((S (wpo_old_index_step_trace)) * d)) /\ exists wpo_beta_quotient_step_trace_new_entry. z = wpo_beta_quotient_step_trace_new_entry * S ((S (wpo_old_index_step_trace)) * d) + (wpo_old_value_step_trace))))))) /\ (((exists wpo_gap_chosen_i_bound. wpo_gap_chosen_i_bound + S (i) = n) /\ (((exists wpo_gap_chosen_j_bound. wpo_gap_chosen_j_bound + S (j) = n) /\ (((~(exists wpo_index_chosen_i_omit_contains. ((exists wpo_gap_chosen_i_omit_contains_bound. wpo_gap_chosen_i_omit_contains_bound + S (wpo_index_chosen_i_omit_contains) = l) /\ (((exists wpo_beta_height_chosen_i_omit_contains_entry. wpo_beta_height_chosen_i_omit_contains_entry + S (i) = S ((S (wpo_index_chosen_i_omit_contains)) * c)) /\ exists wpo_beta_quotient_chosen_i_omit_contains_entry. b = wpo_beta_quotient_chosen_i_omit_contains_entry * S ((S (wpo_index_chosen_i_omit_contains)) * c) + (i)))))) /\ (((~(exists wpo_index_step_j_omit_contains. ((exists wpo_gap_step_j_omit_contains_bound. wpo_gap_step_j_omit_contains_bound + S (wpo_index_step_j_omit_contains) = l) /\ (((exists wpo_beta_height_step_j_omit_contains_entry. wpo_beta_height_step_j_omit_contains_entry + S (j) = S ((S (wpo_index_step_j_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_j_omit_contains_entry. b = wpo_beta_quotient_step_j_omit_contains_entry * S ((S (wpo_index_step_j_omit_contains)) * c) + (j)))))) /\ (((~(i = j)) /\ (((((exists wpo_beta_height_chosen_forward. wpo_beta_height_chosen_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_chosen_forward. u = wpo_beta_quotient_chosen_forward * S ((S (i)) * v) + (S j))) /\ (((((exists wpo_beta_height_chosen_back. wpo_beta_height_chosen_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_chosen_back. u = wpo_beta_quotient_chosen_back * S ((S (j)) * v) + (S i))) /\ (((forall espo_position_step_closed_after espo_source_step_closed_after espo_mate_step_closed_after. (exists wpo_gap_step_closed_after_position_bound. wpo_gap_step_closed_after_position_bound + S (espo_position_step_closed_after) = S (S l)) -> (((exists wpo_beta_height_step_closed_after_source_entry. wpo_beta_height_step_closed_after_source_entry + S (espo_source_step_closed_after) = S ((S (espo_position_step_closed_after)) * d)) /\ exists wpo_beta_quotient_step_closed_after_source_entry. z = wpo_beta_quotient_step_closed_after_source_entry * S ((S (espo_position_step_closed_after)) * d) + (espo_source_step_closed_after))) -> (((exists wpo_beta_height_step_closed_after_scaled_entry. wpo_beta_height_step_closed_after_scaled_entry + S (S espo_mate_step_closed_after) = S ((S (espo_source_step_closed_after)) * v)) /\ exists wpo_beta_quotient_step_closed_after_scaled_entry. u = wpo_beta_quotient_step_closed_after_scaled_entry * S ((S (espo_source_step_closed_after)) * v) + (S espo_mate_step_closed_after))) -> exists espo_mate_position_step_closed_after. ((exists wpo_gap_step_closed_after_mate_bound. wpo_gap_step_closed_after_mate_bound + S (espo_mate_position_step_closed_after) = S (S l)) /\ (((exists wpo_beta_height_step_closed_after_mate_entry. wpo_beta_height_step_closed_after_mate_entry + S (espo_mate_step_closed_after) = S ((S (espo_mate_position_step_closed_after)) * d)) /\ exists wpo_beta_quotient_step_closed_after_mate_entry. z = wpo_beta_quotient_step_closed_after_mate_entry * S ((S (espo_mate_position_step_closed_after)) * d) + (espo_mate_step_closed_after))))) /\ (forall wpo_injective_left_step_injective_after wpo_injective_right_step_injective_after wpo_injective_value_step_injective_after. (exists wpo_gap_step_injective_after_left_bound. wpo_gap_step_injective_after_left_bound + S (wpo_injective_left_step_injective_after) = S (S l)) -> (exists wpo_gap_step_injective_after_right_bound. wpo_gap_step_injective_after_right_bound + S (wpo_injective_right_step_injective_after) = S (S l)) -> (((exists wpo_beta_height_step_injective_after_left_entry. wpo_beta_height_step_injective_after_left_entry + S (wpo_injective_value_step_injective_after) = S ((S (wpo_injective_left_step_injective_after)) * d)) /\ exists wpo_beta_quotient_step_injective_after_left_entry. z = wpo_beta_quotient_step_injective_after_left_entry * S ((S (wpo_injective_left_step_injective_after)) * d) + (wpo_injective_value_step_injective_after))) -> (((exists wpo_beta_height_step_injective_after_right_entry. wpo_beta_height_step_injective_after_right_entry + S (wpo_injective_value_step_injective_after) = S ((S (wpo_injective_right_step_injective_after)) * d)) /\ exists wpo_beta_quotient_step_injective_after_right_entry. z = wpo_beta_quotient_step_injective_after_right_entry * S ((S (wpo_injective_right_step_injective_after)) * d) + (wpo_injective_value_step_injective_after))) -> wpo_injective_left_step_injective_after = wpo_injective_right_step_injective_after)))))))))))))))))))