pair_order_state_terminal_coverage

Exact expanded PA statement

forall u v b c l. (((forall wpo_position_wpoi_terminal_state_closed wpo_source_wpoi_terminal_state_closed wpo_mate_wpoi_terminal_state_closed. (exists wpo_gap_wpoi_terminal_state_closed_position_bound. wpo_gap_wpoi_terminal_state_closed_position_bound + S (wpo_position_wpoi_terminal_state_closed) = l) -> (((exists wpo_beta_height_wpoi_terminal_state_closed_source_entry. wpo_beta_height_wpoi_terminal_state_closed_source_entry + S (wpo_source_wpoi_terminal_state_closed) = S ((S (wpo_position_wpoi_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_closed_source_entry. b = wpo_beta_quotient_wpoi_terminal_state_closed_source_entry * S ((S (wpo_position_wpoi_terminal_state_closed)) * c) + (wpo_source_wpoi_terminal_state_closed))) -> (((exists wpo_beta_height_wpoi_terminal_state_closed_inverse_entry. wpo_beta_height_wpoi_terminal_state_closed_inverse_entry + S (wpo_mate_wpoi_terminal_state_closed) = S ((S (wpo_source_wpoi_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_wpoi_terminal_state_closed_inverse_entry. u = wpo_beta_quotient_wpoi_terminal_state_closed_inverse_entry * S ((S (wpo_source_wpoi_terminal_state_closed)) * v) + (wpo_mate_wpoi_terminal_state_closed))) -> exists wpo_mate_position_wpoi_terminal_state_closed. ((exists wpo_gap_wpoi_terminal_state_closed_mate_bound. wpo_gap_wpoi_terminal_state_closed_mate_bound + S (wpo_mate_position_wpoi_terminal_state_closed) = l) /\ (((exists wpo_beta_height_wpoi_terminal_state_closed_mate_entry. wpo_beta_height_wpoi_terminal_state_closed_mate_entry + S (wpo_mate_wpoi_terminal_state_closed) = S ((S (wpo_mate_position_wpoi_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_closed_mate_entry. b = wpo_beta_quotient_wpoi_terminal_state_closed_mate_entry * S ((S (wpo_mate_position_wpoi_terminal_state_closed)) * c) + (wpo_mate_wpoi_terminal_state_closed))))) /\ ((forall fom_index_wpoi_terminal_state_bounded. (exists fom_gap_wpoi_terminal_state_bounded_index_bound. fom_gap_wpoi_terminal_state_bounded_index_bound + S (fom_index_wpoi_terminal_state_bounded) = l) -> exists fom_value_wpoi_terminal_state_bounded. ((((exists fom_beta_height_wpoi_terminal_state_bounded_entry. fom_beta_height_wpoi_terminal_state_bounded_entry + S (fom_value_wpoi_terminal_state_bounded) = S ((S (fom_index_wpoi_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_wpoi_terminal_state_bounded_entry. b = fom_beta_quotient_wpoi_terminal_state_bounded_entry * S ((S (fom_index_wpoi_terminal_state_bounded)) * c) + (fom_value_wpoi_terminal_state_bounded))) /\ (exists fom_gap_wpoi_terminal_state_bounded_value_bound. fom_gap_wpoi_terminal_state_bounded_value_bound + S (fom_value_wpoi_terminal_state_bounded) = S (S l)))) /\ ((forall wpo_position_wpoi_terminal_state_nonendpoint wpo_value_wpoi_terminal_state_nonendpoint. (exists wpo_gap_wpoi_terminal_state_nonendpoint_position_bound. wpo_gap_wpoi_terminal_state_nonendpoint_position_bound + S (wpo_position_wpoi_terminal_state_nonendpoint) = l) -> (((exists wpo_beta_height_wpoi_terminal_state_nonendpoint_entry. wpo_beta_height_wpoi_terminal_state_nonendpoint_entry + S (wpo_value_wpoi_terminal_state_nonendpoint) = S ((S (wpo_position_wpoi_terminal_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_nonendpoint_entry. b = wpo_beta_quotient_wpoi_terminal_state_nonendpoint_entry * S ((S (wpo_position_wpoi_terminal_state_nonendpoint)) * c) + (wpo_value_wpoi_terminal_state_nonendpoint))) -> (~(wpo_value_wpoi_terminal_state_nonendpoint = 0) /\ ~((S wpo_value_wpoi_terminal_state_nonendpoint) = S (S l)))) /\ (forall wpo_injective_left_wpoi_terminal_state_injective wpo_injective_right_wpoi_terminal_state_injective wpo_injective_value_wpoi_terminal_state_injective. (exists wpo_gap_wpoi_terminal_state_injective_left_bound. wpo_gap_wpoi_terminal_state_injective_left_bound + S (wpo_injective_left_wpoi_terminal_state_injective) = l) -> (exists wpo_gap_wpoi_terminal_state_injective_right_bound. wpo_gap_wpoi_terminal_state_injective_right_bound + S (wpo_injective_right_wpoi_terminal_state_injective) = l) -> (((exists wpo_beta_height_wpoi_terminal_state_injective_left_entry. wpo_beta_height_wpoi_terminal_state_injective_left_entry + S (wpo_injective_value_wpoi_terminal_state_injective) = S ((S (wpo_injective_left_wpoi_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_injective_left_entry. b = wpo_beta_quotient_wpoi_terminal_state_injective_left_entry * S ((S (wpo_injective_left_wpoi_terminal_state_injective)) * c) + (wpo_injective_value_wpoi_terminal_state_injective))) -> (((exists wpo_beta_height_wpoi_terminal_state_injective_right_entry. wpo_beta_height_wpoi_terminal_state_injective_right_entry + S (wpo_injective_value_wpoi_terminal_state_injective) = S ((S (wpo_injective_right_wpoi_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_injective_right_entry. b = wpo_beta_quotient_wpoi_terminal_state_injective_right_entry * S ((S (wpo_injective_right_wpoi_terminal_state_injective)) * c) + (wpo_injective_value_wpoi_terminal_state_injective))) -> wpo_injective_left_wpoi_terminal_state_injective = wpo_injective_right_wpoi_terminal_state_injective))))) -> forall s. (exists wpo_gap_wpoi_terminal_value_bound. wpo_gap_wpoi_terminal_value_bound + S (s) = S (S l)) -> (~(s = 0) /\ ~((S s) = S (S l))) -> (exists q. ((exists wpo_gap_wpoi_terminal_index_bound. wpo_gap_wpoi_terminal_index_bound + S (q) = l) /\ (((exists wpo_beta_height_wpoi_terminal_entry. wpo_beta_height_wpoi_terminal_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_entry. b = wpo_beta_quotient_wpoi_terminal_entry * S ((S (q)) * c) + (s)))))