beta_prefix_append_two_scaled_orbit_closed

Exact expanded PA statement

forall u v b c z d l i j. (((((exists wpo_beta_height_closure_trace_first. wpo_beta_height_closure_trace_first + S (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_closure_trace_first. z = wpo_beta_quotient_closure_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_closure_trace_second. wpo_beta_height_closure_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_closure_trace_second. z = wpo_beta_quotient_closure_trace_second * S ((S (S (l))) * d) + (j))) /\ (forall wpo_old_index_closure_trace wpo_old_value_closure_trace. (exists wpo_gap_closure_trace_old_bound. wpo_gap_closure_trace_old_bound + S (wpo_old_index_closure_trace) = l) -> (((exists wpo_beta_height_closure_trace_old_entry. wpo_beta_height_closure_trace_old_entry + S (wpo_old_value_closure_trace) = S ((S (wpo_old_index_closure_trace)) * c)) /\ exists wpo_beta_quotient_closure_trace_old_entry. b = wpo_beta_quotient_closure_trace_old_entry * S ((S (wpo_old_index_closure_trace)) * c) + (wpo_old_value_closure_trace))) -> (((exists wpo_beta_height_closure_trace_new_entry. wpo_beta_height_closure_trace_new_entry + S (wpo_old_value_closure_trace) = S ((S (wpo_old_index_closure_trace)) * d)) /\ exists wpo_beta_quotient_closure_trace_new_entry. z = wpo_beta_quotient_closure_trace_new_entry * S ((S (wpo_old_index_closure_trace)) * d) + (wpo_old_value_closure_trace))))))) -> (forall espo_position_closure_before espo_source_closure_before espo_mate_closure_before. (exists wpo_gap_closure_before_position_bound. wpo_gap_closure_before_position_bound + S (espo_position_closure_before) = l) -> (((exists wpo_beta_height_closure_before_source_entry. wpo_beta_height_closure_before_source_entry + S (espo_source_closure_before) = S ((S (espo_position_closure_before)) * c)) /\ exists wpo_beta_quotient_closure_before_source_entry. b = wpo_beta_quotient_closure_before_source_entry * S ((S (espo_position_closure_before)) * c) + (espo_source_closure_before))) -> (((exists wpo_beta_height_closure_before_scaled_entry. wpo_beta_height_closure_before_scaled_entry + S (S espo_mate_closure_before) = S ((S (espo_source_closure_before)) * v)) /\ exists wpo_beta_quotient_closure_before_scaled_entry. u = wpo_beta_quotient_closure_before_scaled_entry * S ((S (espo_source_closure_before)) * v) + (S espo_mate_closure_before))) -> exists espo_mate_position_closure_before. ((exists wpo_gap_closure_before_mate_bound. wpo_gap_closure_before_mate_bound + S (espo_mate_position_closure_before) = l) /\ (((exists wpo_beta_height_closure_before_mate_entry. wpo_beta_height_closure_before_mate_entry + S (espo_mate_closure_before) = S ((S (espo_mate_position_closure_before)) * c)) /\ exists wpo_beta_quotient_closure_before_mate_entry. b = wpo_beta_quotient_closure_before_mate_entry * S ((S (espo_mate_position_closure_before)) * c) + (espo_mate_closure_before))))) -> (((exists wpo_beta_height_closure_forward. wpo_beta_height_closure_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_closure_forward. u = wpo_beta_quotient_closure_forward * S ((S (i)) * v) + (S j))) -> (((exists wpo_beta_height_closure_back. wpo_beta_height_closure_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_closure_back. u = wpo_beta_quotient_closure_back * S ((S (j)) * v) + (S i))) -> (forall espo_position_closure_after espo_source_closure_after espo_mate_closure_after. (exists wpo_gap_closure_after_position_bound. wpo_gap_closure_after_position_bound + S (espo_position_closure_after) = S (S l)) -> (((exists wpo_beta_height_closure_after_source_entry. wpo_beta_height_closure_after_source_entry + S (espo_source_closure_after) = S ((S (espo_position_closure_after)) * d)) /\ exists wpo_beta_quotient_closure_after_source_entry. z = wpo_beta_quotient_closure_after_source_entry * S ((S (espo_position_closure_after)) * d) + (espo_source_closure_after))) -> (((exists wpo_beta_height_closure_after_scaled_entry. wpo_beta_height_closure_after_scaled_entry + S (S espo_mate_closure_after) = S ((S (espo_source_closure_after)) * v)) /\ exists wpo_beta_quotient_closure_after_scaled_entry. u = wpo_beta_quotient_closure_after_scaled_entry * S ((S (espo_source_closure_after)) * v) + (S espo_mate_closure_after))) -> exists espo_mate_position_closure_after. ((exists wpo_gap_closure_after_mate_bound. wpo_gap_closure_after_mate_bound + S (espo_mate_position_closure_after) = S (S l)) /\ (((exists wpo_beta_height_closure_after_mate_entry. wpo_beta_height_closure_after_mate_entry + S (espo_mate_closure_after) = S ((S (espo_mate_position_closure_after)) * d)) /\ exists wpo_beta_quotient_closure_after_mate_entry. z = wpo_beta_quotient_closure_after_mate_entry * S ((S (espo_mate_position_closure_after)) * d) + (espo_mate_closure_after)))))