pair_order_state_zero

Exact expanded PA statement

forall u v n. exists b c. (((forall wpo_position_wpoi_zero_state_closed wpo_source_wpoi_zero_state_closed wpo_mate_wpoi_zero_state_closed. (exists wpo_gap_wpoi_zero_state_closed_position_bound. wpo_gap_wpoi_zero_state_closed_position_bound + S (wpo_position_wpoi_zero_state_closed) = 0) -> (((exists wpo_beta_height_wpoi_zero_state_closed_source_entry. wpo_beta_height_wpoi_zero_state_closed_source_entry + S (wpo_source_wpoi_zero_state_closed) = S ((S (wpo_position_wpoi_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_state_closed_source_entry. b = wpo_beta_quotient_wpoi_zero_state_closed_source_entry * S ((S (wpo_position_wpoi_zero_state_closed)) * c) + (wpo_source_wpoi_zero_state_closed))) -> (((exists wpo_beta_height_wpoi_zero_state_closed_inverse_entry. wpo_beta_height_wpoi_zero_state_closed_inverse_entry + S (wpo_mate_wpoi_zero_state_closed) = S ((S (wpo_source_wpoi_zero_state_closed)) * v)) /\ exists wpo_beta_quotient_wpoi_zero_state_closed_inverse_entry. u = wpo_beta_quotient_wpoi_zero_state_closed_inverse_entry * S ((S (wpo_source_wpoi_zero_state_closed)) * v) + (wpo_mate_wpoi_zero_state_closed))) -> exists wpo_mate_position_wpoi_zero_state_closed. ((exists wpo_gap_wpoi_zero_state_closed_mate_bound. wpo_gap_wpoi_zero_state_closed_mate_bound + S (wpo_mate_position_wpoi_zero_state_closed) = 0) /\ (((exists wpo_beta_height_wpoi_zero_state_closed_mate_entry. wpo_beta_height_wpoi_zero_state_closed_mate_entry + S (wpo_mate_wpoi_zero_state_closed) = S ((S (wpo_mate_position_wpoi_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_state_closed_mate_entry. b = wpo_beta_quotient_wpoi_zero_state_closed_mate_entry * S ((S (wpo_mate_position_wpoi_zero_state_closed)) * c) + (wpo_mate_wpoi_zero_state_closed))))) /\ ((forall fom_index_wpoi_zero_state_bounded. (exists fom_gap_wpoi_zero_state_bounded_index_bound. fom_gap_wpoi_zero_state_bounded_index_bound + S (fom_index_wpoi_zero_state_bounded) = 0) -> exists fom_value_wpoi_zero_state_bounded. ((((exists fom_beta_height_wpoi_zero_state_bounded_entry. fom_beta_height_wpoi_zero_state_bounded_entry + S (fom_value_wpoi_zero_state_bounded) = S ((S (fom_index_wpoi_zero_state_bounded)) * c)) /\ exists fom_beta_quotient_wpoi_zero_state_bounded_entry. b = fom_beta_quotient_wpoi_zero_state_bounded_entry * S ((S (fom_index_wpoi_zero_state_bounded)) * c) + (fom_value_wpoi_zero_state_bounded))) /\ (exists fom_gap_wpoi_zero_state_bounded_value_bound. fom_gap_wpoi_zero_state_bounded_value_bound + S (fom_value_wpoi_zero_state_bounded) = n))) /\ ((forall wpo_position_wpoi_zero_state_nonendpoint wpo_value_wpoi_zero_state_nonendpoint. (exists wpo_gap_wpoi_zero_state_nonendpoint_position_bound. wpo_gap_wpoi_zero_state_nonendpoint_position_bound + S (wpo_position_wpoi_zero_state_nonendpoint) = 0) -> (((exists wpo_beta_height_wpoi_zero_state_nonendpoint_entry. wpo_beta_height_wpoi_zero_state_nonendpoint_entry + S (wpo_value_wpoi_zero_state_nonendpoint) = S ((S (wpo_position_wpoi_zero_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_state_nonendpoint_entry. b = wpo_beta_quotient_wpoi_zero_state_nonendpoint_entry * S ((S (wpo_position_wpoi_zero_state_nonendpoint)) * c) + (wpo_value_wpoi_zero_state_nonendpoint))) -> (~(wpo_value_wpoi_zero_state_nonendpoint = 0) /\ ~((S wpo_value_wpoi_zero_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpoi_zero_state_injective wpo_injective_right_wpoi_zero_state_injective wpo_injective_value_wpoi_zero_state_injective. (exists wpo_gap_wpoi_zero_state_injective_left_bound. wpo_gap_wpoi_zero_state_injective_left_bound + S (wpo_injective_left_wpoi_zero_state_injective) = 0) -> (exists wpo_gap_wpoi_zero_state_injective_right_bound. wpo_gap_wpoi_zero_state_injective_right_bound + S (wpo_injective_right_wpoi_zero_state_injective) = 0) -> (((exists wpo_beta_height_wpoi_zero_state_injective_left_entry. wpo_beta_height_wpoi_zero_state_injective_left_entry + S (wpo_injective_value_wpoi_zero_state_injective) = S ((S (wpo_injective_left_wpoi_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_state_injective_left_entry. b = wpo_beta_quotient_wpoi_zero_state_injective_left_entry * S ((S (wpo_injective_left_wpoi_zero_state_injective)) * c) + (wpo_injective_value_wpoi_zero_state_injective))) -> (((exists wpo_beta_height_wpoi_zero_state_injective_right_entry. wpo_beta_height_wpoi_zero_state_injective_right_entry + S (wpo_injective_value_wpoi_zero_state_injective) = S ((S (wpo_injective_right_wpoi_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_state_injective_right_entry. b = wpo_beta_quotient_wpoi_zero_state_injective_right_entry * S ((S (wpo_injective_right_wpoi_zero_state_injective)) * c) + (wpo_injective_value_wpoi_zero_state_injective))) -> wpo_injective_left_wpoi_zero_state_injective = wpo_injective_right_wpoi_zero_state_injective)))))