beta_prefix_append_two_nonendpoint

Exact expanded PA statement

forall b c z d l n a e. (((((exists wpo_beta_height_nonendpoint_trace_first. wpo_beta_height_nonendpoint_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_nonendpoint_trace_first. z = wpo_beta_quotient_nonendpoint_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_nonendpoint_trace_second. wpo_beta_height_nonendpoint_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_nonendpoint_trace_second. z = wpo_beta_quotient_nonendpoint_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_nonendpoint_trace wpo_old_value_nonendpoint_trace. (exists wpo_gap_nonendpoint_trace_old_bound. wpo_gap_nonendpoint_trace_old_bound + S (wpo_old_index_nonendpoint_trace) = l) -> (((exists wpo_beta_height_nonendpoint_trace_old_entry. wpo_beta_height_nonendpoint_trace_old_entry + S (wpo_old_value_nonendpoint_trace) = S ((S (wpo_old_index_nonendpoint_trace)) * c)) /\ exists wpo_beta_quotient_nonendpoint_trace_old_entry. b = wpo_beta_quotient_nonendpoint_trace_old_entry * S ((S (wpo_old_index_nonendpoint_trace)) * c) + (wpo_old_value_nonendpoint_trace))) -> (((exists wpo_beta_height_nonendpoint_trace_new_entry. wpo_beta_height_nonendpoint_trace_new_entry + S (wpo_old_value_nonendpoint_trace) = S ((S (wpo_old_index_nonendpoint_trace)) * d)) /\ exists wpo_beta_quotient_nonendpoint_trace_new_entry. z = wpo_beta_quotient_nonendpoint_trace_new_entry * S ((S (wpo_old_index_nonendpoint_trace)) * d) + (wpo_old_value_nonendpoint_trace))))))) -> (forall wpo_position_nonendpoint_before wpo_value_nonendpoint_before. (exists wpo_gap_nonendpoint_before_position_bound. wpo_gap_nonendpoint_before_position_bound + S (wpo_position_nonendpoint_before) = l) -> (((exists wpo_beta_height_nonendpoint_before_entry. wpo_beta_height_nonendpoint_before_entry + S (wpo_value_nonendpoint_before) = S ((S (wpo_position_nonendpoint_before)) * c)) /\ exists wpo_beta_quotient_nonendpoint_before_entry. b = wpo_beta_quotient_nonendpoint_before_entry * S ((S (wpo_position_nonendpoint_before)) * c) + (wpo_value_nonendpoint_before))) -> (~(wpo_value_nonendpoint_before = 0) /\ ~((S wpo_value_nonendpoint_before) = n))) -> ((~(a = 0) /\ ~((S a) = n))) -> ((~(e = 0) /\ ~((S e) = n))) -> (forall wpo_position_nonendpoint_after wpo_value_nonendpoint_after. (exists wpo_gap_nonendpoint_after_position_bound. wpo_gap_nonendpoint_after_position_bound + S (wpo_position_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_nonendpoint_after_entry. wpo_beta_height_nonendpoint_after_entry + S (wpo_value_nonendpoint_after) = S ((S (wpo_position_nonendpoint_after)) * d)) /\ exists wpo_beta_quotient_nonendpoint_after_entry. z = wpo_beta_quotient_nonendpoint_after_entry * S ((S (wpo_position_nonendpoint_after)) * d) + (wpo_value_nonendpoint_after))) -> (~(wpo_value_nonendpoint_after = 0) /\ ~((S wpo_value_nonendpoint_after) = n)))