beta_prefix_append_two_orbit_closed

Exact expanded PA statement

forall u v b c z d l a e. (((((exists wpo_beta_height_closure_trace_first. wpo_beta_height_closure_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_closure_trace_first. z = wpo_beta_quotient_closure_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_closure_trace_second. wpo_beta_height_closure_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_closure_trace_second. z = wpo_beta_quotient_closure_trace_second * S ((S (S (l))) * d) + (e))) /\ (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 wpo_position_closure_before wpo_source_closure_before wpo_mate_closure_before. (exists wpo_gap_closure_before_position_bound. wpo_gap_closure_before_position_bound + S (wpo_position_closure_before) = l) -> (((exists wpo_beta_height_closure_before_source_entry. wpo_beta_height_closure_before_source_entry + S (wpo_source_closure_before) = S ((S (wpo_position_closure_before)) * c)) /\ exists wpo_beta_quotient_closure_before_source_entry. b = wpo_beta_quotient_closure_before_source_entry * S ((S (wpo_position_closure_before)) * c) + (wpo_source_closure_before))) -> (((exists wpo_beta_height_closure_before_inverse_entry. wpo_beta_height_closure_before_inverse_entry + S (wpo_mate_closure_before) = S ((S (wpo_source_closure_before)) * v)) /\ exists wpo_beta_quotient_closure_before_inverse_entry. u = wpo_beta_quotient_closure_before_inverse_entry * S ((S (wpo_source_closure_before)) * v) + (wpo_mate_closure_before))) -> exists wpo_mate_position_closure_before. ((exists wpo_gap_closure_before_mate_bound. wpo_gap_closure_before_mate_bound + S (wpo_mate_position_closure_before) = l) /\ (((exists wpo_beta_height_closure_before_mate_entry. wpo_beta_height_closure_before_mate_entry + S (wpo_mate_closure_before) = S ((S (wpo_mate_position_closure_before)) * c)) /\ exists wpo_beta_quotient_closure_before_mate_entry. b = wpo_beta_quotient_closure_before_mate_entry * S ((S (wpo_mate_position_closure_before)) * c) + (wpo_mate_closure_before))))) -> (((exists wpo_beta_height_closure_forward. wpo_beta_height_closure_forward + S (e) = S ((S (a)) * v)) /\ exists wpo_beta_quotient_closure_forward. u = wpo_beta_quotient_closure_forward * S ((S (a)) * v) + (e))) -> (((exists wpo_beta_height_closure_back. wpo_beta_height_closure_back + S (a) = S ((S (e)) * v)) /\ exists wpo_beta_quotient_closure_back. u = wpo_beta_quotient_closure_back * S ((S (e)) * v) + (a))) -> (forall wpo_position_closure_after wpo_source_closure_after wpo_mate_closure_after. (exists wpo_gap_closure_after_position_bound. wpo_gap_closure_after_position_bound + S (wpo_position_closure_after) = S (S l)) -> (((exists wpo_beta_height_closure_after_source_entry. wpo_beta_height_closure_after_source_entry + S (wpo_source_closure_after) = S ((S (wpo_position_closure_after)) * d)) /\ exists wpo_beta_quotient_closure_after_source_entry. z = wpo_beta_quotient_closure_after_source_entry * S ((S (wpo_position_closure_after)) * d) + (wpo_source_closure_after))) -> (((exists wpo_beta_height_closure_after_inverse_entry. wpo_beta_height_closure_after_inverse_entry + S (wpo_mate_closure_after) = S ((S (wpo_source_closure_after)) * v)) /\ exists wpo_beta_quotient_closure_after_inverse_entry. u = wpo_beta_quotient_closure_after_inverse_entry * S ((S (wpo_source_closure_after)) * v) + (wpo_mate_closure_after))) -> exists wpo_mate_position_closure_after. ((exists wpo_gap_closure_after_mate_bound. wpo_gap_closure_after_mate_bound + S (wpo_mate_position_closure_after) = S (S l)) /\ (((exists wpo_beta_height_closure_after_mate_entry. wpo_beta_height_closure_after_mate_entry + S (wpo_mate_closure_after) = S ((S (wpo_mate_position_closure_after)) * d)) /\ exists wpo_beta_quotient_closure_after_mate_entry. z = wpo_beta_quotient_closure_after_mate_entry * S ((S (wpo_mate_position_closure_after)) * d) + (wpo_mate_closure_after)))))