pair_order_terminal_state_magnitude_range

Exact expanded PA statement

forall u v b c l n. n = S (S l) -> (((forall wpo_position_wtp_terminal_state_closed wpo_source_wtp_terminal_state_closed wpo_mate_wtp_terminal_state_closed. (exists wpo_gap_wtp_terminal_state_closed_position_bound. wpo_gap_wtp_terminal_state_closed_position_bound + S (wpo_position_wtp_terminal_state_closed) = l) -> (((exists wpo_beta_height_wtp_terminal_state_closed_source_entry. wpo_beta_height_wtp_terminal_state_closed_source_entry + S (wpo_source_wtp_terminal_state_closed) = S ((S (wpo_position_wtp_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_closed_source_entry. b = wpo_beta_quotient_wtp_terminal_state_closed_source_entry * S ((S (wpo_position_wtp_terminal_state_closed)) * c) + (wpo_source_wtp_terminal_state_closed))) -> (((exists wpo_beta_height_wtp_terminal_state_closed_inverse_entry. wpo_beta_height_wtp_terminal_state_closed_inverse_entry + S (wpo_mate_wtp_terminal_state_closed) = S ((S (wpo_source_wtp_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_wtp_terminal_state_closed_inverse_entry. u = wpo_beta_quotient_wtp_terminal_state_closed_inverse_entry * S ((S (wpo_source_wtp_terminal_state_closed)) * v) + (wpo_mate_wtp_terminal_state_closed))) -> exists wpo_mate_position_wtp_terminal_state_closed. ((exists wpo_gap_wtp_terminal_state_closed_mate_bound. wpo_gap_wtp_terminal_state_closed_mate_bound + S (wpo_mate_position_wtp_terminal_state_closed) = l) /\ (((exists wpo_beta_height_wtp_terminal_state_closed_mate_entry. wpo_beta_height_wtp_terminal_state_closed_mate_entry + S (wpo_mate_wtp_terminal_state_closed) = S ((S (wpo_mate_position_wtp_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_closed_mate_entry. b = wpo_beta_quotient_wtp_terminal_state_closed_mate_entry * S ((S (wpo_mate_position_wtp_terminal_state_closed)) * c) + (wpo_mate_wtp_terminal_state_closed))))) /\ ((forall fom_index_wtp_terminal_state_bounded. (exists fom_gap_wtp_terminal_state_bounded_index_bound. fom_gap_wtp_terminal_state_bounded_index_bound + S (fom_index_wtp_terminal_state_bounded) = l) -> exists fom_value_wtp_terminal_state_bounded. ((((exists fom_beta_height_wtp_terminal_state_bounded_entry. fom_beta_height_wtp_terminal_state_bounded_entry + S (fom_value_wtp_terminal_state_bounded) = S ((S (fom_index_wtp_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_wtp_terminal_state_bounded_entry. b = fom_beta_quotient_wtp_terminal_state_bounded_entry * S ((S (fom_index_wtp_terminal_state_bounded)) * c) + (fom_value_wtp_terminal_state_bounded))) /\ (exists fom_gap_wtp_terminal_state_bounded_value_bound. fom_gap_wtp_terminal_state_bounded_value_bound + S (fom_value_wtp_terminal_state_bounded) = n))) /\ ((forall wpo_position_wtp_terminal_state_nonendpoint wpo_value_wtp_terminal_state_nonendpoint. (exists wpo_gap_wtp_terminal_state_nonendpoint_position_bound. wpo_gap_wtp_terminal_state_nonendpoint_position_bound + S (wpo_position_wtp_terminal_state_nonendpoint) = l) -> (((exists wpo_beta_height_wtp_terminal_state_nonendpoint_entry. wpo_beta_height_wtp_terminal_state_nonendpoint_entry + S (wpo_value_wtp_terminal_state_nonendpoint) = S ((S (wpo_position_wtp_terminal_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_nonendpoint_entry. b = wpo_beta_quotient_wtp_terminal_state_nonendpoint_entry * S ((S (wpo_position_wtp_terminal_state_nonendpoint)) * c) + (wpo_value_wtp_terminal_state_nonendpoint))) -> (~(wpo_value_wtp_terminal_state_nonendpoint = 0) /\ ~((S wpo_value_wtp_terminal_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_terminal_state_injective wpo_injective_right_wtp_terminal_state_injective wpo_injective_value_wtp_terminal_state_injective. (exists wpo_gap_wtp_terminal_state_injective_left_bound. wpo_gap_wtp_terminal_state_injective_left_bound + S (wpo_injective_left_wtp_terminal_state_injective) = l) -> (exists wpo_gap_wtp_terminal_state_injective_right_bound. wpo_gap_wtp_terminal_state_injective_right_bound + S (wpo_injective_right_wtp_terminal_state_injective) = l) -> (((exists wpo_beta_height_wtp_terminal_state_injective_left_entry. wpo_beta_height_wtp_terminal_state_injective_left_entry + S (wpo_injective_value_wtp_terminal_state_injective) = S ((S (wpo_injective_left_wtp_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_injective_left_entry. b = wpo_beta_quotient_wtp_terminal_state_injective_left_entry * S ((S (wpo_injective_left_wtp_terminal_state_injective)) * c) + (wpo_injective_value_wtp_terminal_state_injective))) -> (((exists wpo_beta_height_wtp_terminal_state_injective_right_entry. wpo_beta_height_wtp_terminal_state_injective_right_entry + S (wpo_injective_value_wtp_terminal_state_injective) = S ((S (wpo_injective_right_wtp_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_terminal_state_injective_right_entry. b = wpo_beta_quotient_wtp_terminal_state_injective_right_entry * S ((S (wpo_injective_right_wtp_terminal_state_injective)) * c) + (wpo_injective_value_wtp_terminal_state_injective))) -> wpo_injective_left_wtp_terminal_state_injective = wpo_injective_right_wtp_terminal_state_injective))))) -> (forall gmp_index_wtp_terminal_range. (exists gsp_lt_gap_wtp_terminal_range_index_bound. gsp_lt_gap_wtp_terminal_range_index_bound + S gmp_index_wtp_terminal_range = l) -> exists gmp_magnitude_wtp_terminal_range. ((((exists ff_h_gmp_wtp_terminal_range_decoded. ff_h_gmp_wtp_terminal_range_decoded + S (gmp_magnitude_wtp_terminal_range) = S ((S (gmp_index_wtp_terminal_range)) * c)) /\ exists ff_q_gmp_wtp_terminal_range_decoded. b = ff_q_gmp_wtp_terminal_range_decoded * S ((S (gmp_index_wtp_terminal_range)) * c) + (gmp_magnitude_wtp_terminal_range))) /\ ((exists gsp_lt_gap_wtp_terminal_range_positive. gsp_lt_gap_wtp_terminal_range_positive + S 0 = gmp_magnitude_wtp_terminal_range) /\ (exists gsp_le_gap_wtp_terminal_range_bounded. gsp_le_gap_wtp_terminal_range_bounded + gmp_magnitude_wtp_terminal_range = l))))