prime_pair_order_choose_append

Exact expanded PA statement

forall p n u v b c l r. p = S n -> ((~(p = 1) /\ forall wip_prime_left_choose_orbit_prime wip_prime_right_choose_orbit_prime. p = wip_prime_left_choose_orbit_prime * wip_prime_right_choose_orbit_prime -> wip_prime_left_choose_orbit_prime = 1 \/ wip_prime_right_choose_orbit_prime = 1)) -> (forall wip_index_choose_orbit_full_prefix. (exists wip_gap_choose_orbit_full_prefix_prefix_bound. wip_gap_choose_orbit_full_prefix_prefix_bound + S wip_index_choose_orbit_full_prefix = n) -> exists wip_mate_choose_orbit_full_prefix. ((((exists wip_beta_height_choose_orbit_full_prefix_decoded. wip_beta_height_choose_orbit_full_prefix_decoded + S (wip_mate_choose_orbit_full_prefix) = S ((S (wip_index_choose_orbit_full_prefix)) * v)) /\ exists wip_beta_quotient_choose_orbit_full_prefix_decoded. u = wip_beta_quotient_choose_orbit_full_prefix_decoded * S ((S (wip_index_choose_orbit_full_prefix)) * v) + (wip_mate_choose_orbit_full_prefix))) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_index_bound. wip_gap_choose_orbit_full_prefix_inverse_index_bound + S wip_index_choose_orbit_full_prefix = n) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_mate_bound. wip_gap_choose_orbit_full_prefix_inverse_mate_bound + S wip_mate_choose_orbit_full_prefix = n) /\ (exists wip_mod_left_choose_orbit_full_prefix_inverse_mod wip_mod_right_choose_orbit_full_prefix_inverse_mod. ((S wip_index_choose_orbit_full_prefix) * S wip_mate_choose_orbit_full_prefix) + p * wip_mod_left_choose_orbit_full_prefix_inverse_mod = 1 + p * wip_mod_right_choose_orbit_full_prefix_inverse_mod))))) -> n = S r -> (exists h. h + S (S (S l)) = n) -> (forall wpo_position_step_closed_before wpo_source_step_closed_before wpo_mate_step_closed_before. (exists wpo_gap_step_closed_before_position_bound. wpo_gap_step_closed_before_position_bound + S (wpo_position_step_closed_before) = l) -> (((exists wpo_beta_height_step_closed_before_source_entry. wpo_beta_height_step_closed_before_source_entry + S (wpo_source_step_closed_before) = S ((S (wpo_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 (wpo_position_step_closed_before)) * c) + (wpo_source_step_closed_before))) -> (((exists wpo_beta_height_step_closed_before_inverse_entry. wpo_beta_height_step_closed_before_inverse_entry + S (wpo_mate_step_closed_before) = S ((S (wpo_source_step_closed_before)) * v)) /\ exists wpo_beta_quotient_step_closed_before_inverse_entry. u = wpo_beta_quotient_step_closed_before_inverse_entry * S ((S (wpo_source_step_closed_before)) * v) + (wpo_mate_step_closed_before))) -> exists wpo_mate_position_step_closed_before. ((exists wpo_gap_step_closed_before_mate_bound. wpo_gap_step_closed_before_mate_bound + S (wpo_mate_position_step_closed_before) = l) /\ (((exists wpo_beta_height_step_closed_before_mate_entry. wpo_beta_height_step_closed_before_mate_entry + S (wpo_mate_step_closed_before) = S ((S (wpo_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 (wpo_mate_position_step_closed_before)) * c) + (wpo_mate_step_closed_before))))) -> (forall wpo_position_step_nonendpoint_before wpo_value_step_nonendpoint_before. (exists wpo_gap_step_nonendpoint_before_position_bound. wpo_gap_step_nonendpoint_before_position_bound + S (wpo_position_step_nonendpoint_before) = l) -> (((exists wpo_beta_height_step_nonendpoint_before_entry. wpo_beta_height_step_nonendpoint_before_entry + S (wpo_value_step_nonendpoint_before) = S ((S (wpo_position_step_nonendpoint_before)) * c)) /\ exists wpo_beta_quotient_step_nonendpoint_before_entry. b = wpo_beta_quotient_step_nonendpoint_before_entry * S ((S (wpo_position_step_nonendpoint_before)) * c) + (wpo_value_step_nonendpoint_before))) -> (~(wpo_value_step_nonendpoint_before = 0) /\ ~((S wpo_value_step_nonendpoint_before) = n))) -> (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_choose_orbit_source_bound. wpo_gap_choose_orbit_source_bound + S (i) = n) /\ ((~(i = 0) /\ ~((S i) = n)) /\ ((~(exists wpo_index_choose_orbit_source_omit_contains. ((exists wpo_gap_choose_orbit_source_omit_contains_bound. wpo_gap_choose_orbit_source_omit_contains_bound + S (wpo_index_choose_orbit_source_omit_contains) = l) /\ (((exists wpo_beta_height_choose_orbit_source_omit_contains_entry. wpo_beta_height_choose_orbit_source_omit_contains_entry + S (i) = S ((S (wpo_index_choose_orbit_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_choose_orbit_source_omit_contains_entry. b = wpo_beta_quotient_choose_orbit_source_omit_contains_entry * S ((S (wpo_index_choose_orbit_source_omit_contains)) * c) + (i)))))) /\ ((((exists wpo_beta_height_choose_orbit_forward. wpo_beta_height_choose_orbit_forward + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_choose_orbit_forward. u = wpo_beta_quotient_choose_orbit_forward * S ((S (i)) * v) + (j))) /\ ((exists wpo_gap_choose_orbit_mate_bound. wpo_gap_choose_orbit_mate_bound + S (j) = n) /\ ((~(j = 0) /\ ~((S j) = n)) /\ (~(i = j) /\ ((((exists wpo_beta_height_choose_orbit_back. wpo_beta_height_choose_orbit_back + S (i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_choose_orbit_back. u = wpo_beta_quotient_choose_orbit_back * S ((S (j)) * v) + (i))) /\ ((~(exists wpo_index_step_mate_omit_contains. ((exists wpo_gap_step_mate_omit_contains_bound. wpo_gap_step_mate_omit_contains_bound + S (wpo_index_step_mate_omit_contains) = l) /\ (((exists wpo_beta_height_step_mate_omit_contains_entry. wpo_beta_height_step_mate_omit_contains_entry + S (j) = S ((S (wpo_index_step_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_mate_omit_contains_entry. b = wpo_beta_quotient_step_mate_omit_contains_entry * S ((S (wpo_index_step_mate_omit_contains)) * c) + (j)))))) /\ ((forall wpo_position_step_closed_after wpo_source_step_closed_after wpo_mate_step_closed_after. (exists wpo_gap_step_closed_after_position_bound. wpo_gap_step_closed_after_position_bound + S (wpo_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 (wpo_source_step_closed_after) = S ((S (wpo_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 (wpo_position_step_closed_after)) * d) + (wpo_source_step_closed_after))) -> (((exists wpo_beta_height_step_closed_after_inverse_entry. wpo_beta_height_step_closed_after_inverse_entry + S (wpo_mate_step_closed_after) = S ((S (wpo_source_step_closed_after)) * v)) /\ exists wpo_beta_quotient_step_closed_after_inverse_entry. u = wpo_beta_quotient_step_closed_after_inverse_entry * S ((S (wpo_source_step_closed_after)) * v) + (wpo_mate_step_closed_after))) -> exists wpo_mate_position_step_closed_after. ((exists wpo_gap_step_closed_after_mate_bound. wpo_gap_step_closed_after_mate_bound + S (wpo_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 (wpo_mate_step_closed_after) = S ((S (wpo_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 (wpo_mate_position_step_closed_after)) * d) + (wpo_mate_step_closed_after))))) /\ (forall wpo_position_step_nonendpoint_after wpo_value_step_nonendpoint_after. (exists wpo_gap_step_nonendpoint_after_position_bound. wpo_gap_step_nonendpoint_after_position_bound + S (wpo_position_step_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_step_nonendpoint_after_entry. wpo_beta_height_step_nonendpoint_after_entry + S (wpo_value_step_nonendpoint_after) = S ((S (wpo_position_step_nonendpoint_after)) * d)) /\ exists wpo_beta_quotient_step_nonendpoint_after_entry. z = wpo_beta_quotient_step_nonendpoint_after_entry * S ((S (wpo_position_step_nonendpoint_after)) * d) + (wpo_value_step_nonendpoint_after))) -> (~(wpo_value_step_nonendpoint_after = 0) /\ ~((S wpo_value_step_nonendpoint_after) = n)))))))))))))))