beta_prefix_append_two_bounded_into

Exact expanded PA statement

forall b c z d l n a e. (((((exists wpo_beta_height_wpoi_append_bounded_trace_first. wpo_beta_height_wpoi_append_bounded_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_wpoi_append_bounded_trace_first. z = wpo_beta_quotient_wpoi_append_bounded_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_wpoi_append_bounded_trace_second. wpo_beta_height_wpoi_append_bounded_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_wpoi_append_bounded_trace_second. z = wpo_beta_quotient_wpoi_append_bounded_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_wpoi_append_bounded_trace wpo_old_value_wpoi_append_bounded_trace. (exists wpo_gap_wpoi_append_bounded_trace_old_bound. wpo_gap_wpoi_append_bounded_trace_old_bound + S (wpo_old_index_wpoi_append_bounded_trace) = l) -> (((exists wpo_beta_height_wpoi_append_bounded_trace_old_entry. wpo_beta_height_wpoi_append_bounded_trace_old_entry + S (wpo_old_value_wpoi_append_bounded_trace) = S ((S (wpo_old_index_wpoi_append_bounded_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_append_bounded_trace_old_entry. b = wpo_beta_quotient_wpoi_append_bounded_trace_old_entry * S ((S (wpo_old_index_wpoi_append_bounded_trace)) * c) + (wpo_old_value_wpoi_append_bounded_trace))) -> (((exists wpo_beta_height_wpoi_append_bounded_trace_new_entry. wpo_beta_height_wpoi_append_bounded_trace_new_entry + S (wpo_old_value_wpoi_append_bounded_trace) = S ((S (wpo_old_index_wpoi_append_bounded_trace)) * d)) /\ exists wpo_beta_quotient_wpoi_append_bounded_trace_new_entry. z = wpo_beta_quotient_wpoi_append_bounded_trace_new_entry * S ((S (wpo_old_index_wpoi_append_bounded_trace)) * d) + (wpo_old_value_wpoi_append_bounded_trace))))))) -> (forall fom_index_wpoi_append_bounded_before. (exists fom_gap_wpoi_append_bounded_before_index_bound. fom_gap_wpoi_append_bounded_before_index_bound + S (fom_index_wpoi_append_bounded_before) = l) -> exists fom_value_wpoi_append_bounded_before. ((((exists fom_beta_height_wpoi_append_bounded_before_entry. fom_beta_height_wpoi_append_bounded_before_entry + S (fom_value_wpoi_append_bounded_before) = S ((S (fom_index_wpoi_append_bounded_before)) * c)) /\ exists fom_beta_quotient_wpoi_append_bounded_before_entry. b = fom_beta_quotient_wpoi_append_bounded_before_entry * S ((S (fom_index_wpoi_append_bounded_before)) * c) + (fom_value_wpoi_append_bounded_before))) /\ (exists fom_gap_wpoi_append_bounded_before_value_bound. fom_gap_wpoi_append_bounded_before_value_bound + S (fom_value_wpoi_append_bounded_before) = n))) -> (exists wpo_gap_wpoi_append_first_bound. wpo_gap_wpoi_append_first_bound + S (a) = n) -> (exists wpo_gap_wpoi_append_second_bound. wpo_gap_wpoi_append_second_bound + S (e) = n) -> (forall fom_index_wpoi_append_bounded_after. (exists fom_gap_wpoi_append_bounded_after_index_bound. fom_gap_wpoi_append_bounded_after_index_bound + S (fom_index_wpoi_append_bounded_after) = S (S l)) -> exists fom_value_wpoi_append_bounded_after. ((((exists fom_beta_height_wpoi_append_bounded_after_entry. fom_beta_height_wpoi_append_bounded_after_entry + S (fom_value_wpoi_append_bounded_after) = S ((S (fom_index_wpoi_append_bounded_after)) * d)) /\ exists fom_beta_quotient_wpoi_append_bounded_after_entry. z = fom_beta_quotient_wpoi_append_bounded_after_entry * S ((S (fom_index_wpoi_append_bounded_after)) * d) + (fom_value_wpoi_append_bounded_after))) /\ (exists fom_gap_wpoi_append_bounded_after_value_bound. fom_gap_wpoi_append_bounded_after_value_bound + S (fom_value_wpoi_append_bounded_after) = n)))