paired_pair_order_product_one_exists

Exact expanded PA statement

forall p n u v b c m. (forall wip_index_wsl_inverse. (exists wip_gap_wsl_inverse_prefix_bound. wip_gap_wsl_inverse_prefix_bound + S wip_index_wsl_inverse = n) -> exists wip_mate_wsl_inverse. ((((exists wip_beta_height_wsl_inverse_decoded. wip_beta_height_wsl_inverse_decoded + S (wip_mate_wsl_inverse) = S ((S (wip_index_wsl_inverse)) * v)) /\ exists wip_beta_quotient_wsl_inverse_decoded. u = wip_beta_quotient_wsl_inverse_decoded * S ((S (wip_index_wsl_inverse)) * v) + (wip_mate_wsl_inverse))) /\ ((exists wip_gap_wsl_inverse_inverse_index_bound. wip_gap_wsl_inverse_inverse_index_bound + S wip_index_wsl_inverse = n) /\ ((exists wip_gap_wsl_inverse_inverse_mate_bound. wip_gap_wsl_inverse_inverse_mate_bound + S wip_mate_wsl_inverse = n) /\ (exists wip_mod_left_wsl_inverse_inverse_mod wip_mod_right_wsl_inverse_inverse_mod. ((S wip_index_wsl_inverse) * S wip_mate_wsl_inverse) + p * wip_mod_left_wsl_inverse_inverse_mod = 1 + p * wip_mod_right_wsl_inverse_inverse_mod))))) -> (forall fom_index_wsl_bounded. (exists fom_gap_wsl_bounded_index_bound. fom_gap_wsl_bounded_index_bound + S (fom_index_wsl_bounded) = m + m) -> exists fom_value_wsl_bounded. ((((exists fom_beta_height_wsl_bounded_entry. fom_beta_height_wsl_bounded_entry + S (fom_value_wsl_bounded) = S ((S (fom_index_wsl_bounded)) * c)) /\ exists fom_beta_quotient_wsl_bounded_entry. b = fom_beta_quotient_wsl_bounded_entry * S ((S (fom_index_wsl_bounded)) * c) + (fom_value_wsl_bounded))) /\ (exists fom_gap_wsl_bounded_value_bound. fom_gap_wsl_bounded_value_bound + S (fom_value_wsl_bounded) = n))) -> (forall wpop_pair_wsl_pairs. (exists wpo_gap_wsl_pairs_pair_bound. wpo_gap_wsl_pairs_pair_bound + S (wpop_pair_wsl_pairs) = m) -> exists wpop_left_wsl_pairs wpop_right_wsl_pairs. ((((exists wpo_beta_height_wsl_pairs_left_entry. wpo_beta_height_wsl_pairs_left_entry + S (wpop_left_wsl_pairs) = S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c)) /\ exists wpo_beta_quotient_wsl_pairs_left_entry. b = wpo_beta_quotient_wsl_pairs_left_entry * S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c) + (wpop_left_wsl_pairs))) /\ ((((exists wpo_beta_height_wsl_pairs_right_entry. wpo_beta_height_wsl_pairs_right_entry + S (wpop_right_wsl_pairs) = S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c)) /\ exists wpo_beta_quotient_wsl_pairs_right_entry. b = wpo_beta_quotient_wsl_pairs_right_entry * S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c) + (wpop_right_wsl_pairs))) /\ (((exists wpo_beta_height_wsl_pairs_inverse_entry. wpo_beta_height_wsl_pairs_inverse_entry + S (wpop_right_wsl_pairs) = S ((S (wpop_left_wsl_pairs)) * v)) /\ exists wpo_beta_quotient_wsl_pairs_inverse_entry. u = wpo_beta_quotient_wsl_pairs_inverse_entry * S ((S (wpop_left_wsl_pairs)) * v) + (wpop_right_wsl_pairs)))))) -> (exists f g Q. ((forall wsl_index_wsl_lift wsl_value_wsl_lift. (exists wpo_gap_wsl_lift_bound. wpo_gap_wsl_lift_bound + S (wsl_index_wsl_lift) = m + m) -> (((exists wpo_beta_height_wsl_lift_source. wpo_beta_height_wsl_lift_source + S (wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * c)) /\ exists wpo_beta_quotient_wsl_lift_source. b = wpo_beta_quotient_wsl_lift_source * S ((S (wsl_index_wsl_lift)) * c) + (wsl_value_wsl_lift))) -> (((exists wpo_beta_height_wsl_lift_target. wpo_beta_height_wsl_lift_target + S (S wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * g)) /\ exists wpo_beta_quotient_wsl_lift_target. f = wpo_beta_quotient_wsl_lift_target * S ((S (wsl_index_wsl_lift)) * g) + (S wsl_value_wsl_lift)))) /\ ((forall wpp_pair_wsl_adjacent wpp_left_wsl_adjacent wpp_right_wsl_adjacent. (exists wpp_gap_wsl_adjacent_pair_bound. wpp_gap_wsl_adjacent_pair_bound + S (wpp_pair_wsl_adjacent) = m) -> (((exists wpp_beta_height_wsl_adjacent_left_entry. wpp_beta_height_wsl_adjacent_left_entry + S (wpp_left_wsl_adjacent) = S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_left_entry. f = wpp_beta_quotient_wsl_adjacent_left_entry * S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_left_wsl_adjacent))) -> (((exists wpp_beta_height_wsl_adjacent_right_entry. wpp_beta_height_wsl_adjacent_right_entry + S (wpp_right_wsl_adjacent) = S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_right_entry. f = wpp_beta_quotient_wsl_adjacent_right_entry * S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_right_wsl_adjacent))) -> (exists wpp_mod_left_wsl_adjacent_pair_mod wpp_mod_right_wsl_adjacent_pair_mod. (wpp_left_wsl_adjacent * wpp_right_wsl_adjacent) + p * wpp_mod_left_wsl_adjacent_pair_mod = (1) + p * wpp_mod_right_wsl_adjacent_pair_mod)) /\ ((exists wpp_trace_code_wsl_product wpp_trace_scale_wsl_product. ((((exists wpp_beta_height_wsl_product_start. wpp_beta_height_wsl_product_start + S (1) = S ((S (0)) * wpp_trace_scale_wsl_product)) /\ exists wpp_beta_quotient_wsl_product_start. wpp_trace_code_wsl_product = wpp_beta_quotient_wsl_product_start * S ((S (0)) * wpp_trace_scale_wsl_product) + (1))) /\ ((((exists wpp_beta_height_wsl_product_terminal. wpp_beta_height_wsl_product_terminal + S (Q) = S ((S (m + m)) * wpp_trace_scale_wsl_product)) /\ exists wpp_beta_quotient_wsl_product_terminal. wpp_trace_code_wsl_product = wpp_beta_quotient_wsl_product_terminal * S ((S (m + m)) * wpp_trace_scale_wsl_product) + (Q))) /\ forall wpp_index_wsl_product. (exists wpp_gap_wsl_product_bound. wpp_gap_wsl_product_bound + S (wpp_index_wsl_product) = m + m) -> exists wpp_factor_wsl_product wpp_prefix_wsl_product wpp_successor_wsl_product. ((((exists wpp_beta_height_wsl_product_factor. wpp_beta_height_wsl_product_factor + S (wpp_factor_wsl_product) = S ((S (wpp_index_wsl_product)) * g)) /\ exists wpp_beta_quotient_wsl_product_factor. f = wpp_beta_quotient_wsl_product_factor * S ((S (wpp_index_wsl_product)) * g) + (wpp_factor_wsl_product))) /\ ((((exists wpp_beta_height_wsl_product_prefix. wpp_beta_height_wsl_product_prefix + S (wpp_prefix_wsl_product) = S ((S (wpp_index_wsl_product)) * wpp_trace_scale_wsl_product)) /\ exists wpp_beta_quotient_wsl_product_prefix. wpp_trace_code_wsl_product = wpp_beta_quotient_wsl_product_prefix * S ((S (wpp_index_wsl_product)) * wpp_trace_scale_wsl_product) + (wpp_prefix_wsl_product))) /\ ((((exists wpp_beta_height_wsl_product_successor. wpp_beta_height_wsl_product_successor + S (wpp_successor_wsl_product) = S ((S (S (wpp_index_wsl_product))) * wpp_trace_scale_wsl_product)) /\ exists wpp_beta_quotient_wsl_product_successor. wpp_trace_code_wsl_product = wpp_beta_quotient_wsl_product_successor * S ((S (S (wpp_index_wsl_product))) * wpp_trace_scale_wsl_product) + (wpp_successor_wsl_product))) /\ wpp_successor_wsl_product = wpp_prefix_wsl_product * wpp_factor_wsl_product)))))) /\ (exists wpp_mod_left_wsl_product_mod_one wpp_mod_right_wsl_product_mod_one. (Q) + p * wpp_mod_left_wsl_product_mod_one = (1) + p * wpp_mod_right_wsl_product_mod_one)))))