pair_order_predecessor_range_two_successor_lift_aligned

Exact expanded PA statement

forall b c r s z d f g l. (forall gmp_index_wtp_alignment_range. (exists gsp_lt_gap_wtp_alignment_range_index_bound. gsp_lt_gap_wtp_alignment_range_index_bound + S gmp_index_wtp_alignment_range = l) -> exists gmp_magnitude_wtp_alignment_range. ((((exists ff_h_gmp_wtp_alignment_range_decoded. ff_h_gmp_wtp_alignment_range_decoded + S (gmp_magnitude_wtp_alignment_range) = S ((S (gmp_index_wtp_alignment_range)) * c)) /\ exists ff_q_gmp_wtp_alignment_range_decoded. b = ff_q_gmp_wtp_alignment_range_decoded * S ((S (gmp_index_wtp_alignment_range)) * c) + (gmp_magnitude_wtp_alignment_range))) /\ ((exists gsp_lt_gap_wtp_alignment_range_positive. gsp_lt_gap_wtp_alignment_range_positive + S 0 = gmp_magnitude_wtp_alignment_range) /\ (exists gsp_le_gap_wtp_alignment_range_bounded. gsp_le_gap_wtp_alignment_range_bounded + gmp_magnitude_wtp_alignment_range = l)))) -> (forall gmp_index_wtp_alignment_recode gmp_predecessor_wtp_alignment_recode. (exists gsp_lt_gap_wtp_alignment_recode_index_bound. gsp_lt_gap_wtp_alignment_recode_index_bound + S gmp_index_wtp_alignment_recode = l) -> (((exists gsp_beta_height_gmp_wtp_alignment_recode_source. gsp_beta_height_gmp_wtp_alignment_recode_source + S (S gmp_predecessor_wtp_alignment_recode) = S ((S (gmp_index_wtp_alignment_recode)) * c)) /\ exists gsp_beta_quotient_gmp_wtp_alignment_recode_source. b = gsp_beta_quotient_gmp_wtp_alignment_recode_source * S ((S (gmp_index_wtp_alignment_recode)) * c) + (S gmp_predecessor_wtp_alignment_recode))) -> (((exists ff_h_gmp_wtp_alignment_recode_target. ff_h_gmp_wtp_alignment_recode_target + S (gmp_predecessor_wtp_alignment_recode) = S ((S (gmp_index_wtp_alignment_recode)) * s)) /\ exists ff_q_gmp_wtp_alignment_recode_target. r = ff_q_gmp_wtp_alignment_recode_target * S ((S (gmp_index_wtp_alignment_recode)) * s) + (gmp_predecessor_wtp_alignment_recode)))) -> (forall wsl_index_wtp_alignment_lift wsl_value_wtp_alignment_lift. (exists wpo_gap_wtp_alignment_lift_bound. wpo_gap_wtp_alignment_lift_bound + S (wsl_index_wtp_alignment_lift) = l) -> (((exists wpo_beta_height_wtp_alignment_lift_source. wpo_beta_height_wtp_alignment_lift_source + S (wsl_value_wtp_alignment_lift) = S ((S (wsl_index_wtp_alignment_lift)) * c)) /\ exists wpo_beta_quotient_wtp_alignment_lift_source. b = wpo_beta_quotient_wtp_alignment_lift_source * S ((S (wsl_index_wtp_alignment_lift)) * c) + (wsl_value_wtp_alignment_lift))) -> (((exists wpo_beta_height_wtp_alignment_lift_target. wpo_beta_height_wtp_alignment_lift_target + S (S wsl_value_wtp_alignment_lift) = S ((S (wsl_index_wtp_alignment_lift)) * g)) /\ exists wpo_beta_quotient_wtp_alignment_lift_target. f = wpo_beta_quotient_wtp_alignment_lift_target * S ((S (wsl_index_wtp_alignment_lift)) * g) + (S wsl_value_wtp_alignment_lift)))) -> (forall wtp_range_index_wtp_alignment_range_two. (exists wtp_range_gap_wtp_alignment_range_two. wtp_range_gap_wtp_alignment_range_two + S wtp_range_index_wtp_alignment_range_two = l) -> (((exists ff_h_wtp_alignment_range_two_decoded. ff_h_wtp_alignment_range_two_decoded + S (2 + wtp_range_index_wtp_alignment_range_two) = S ((S (wtp_range_index_wtp_alignment_range_two)) * d)) /\ exists ff_q_wtp_alignment_range_two_decoded. z = ff_q_wtp_alignment_range_two_decoded * S ((S (wtp_range_index_wtp_alignment_range_two)) * d) + (2 + wtp_range_index_wtp_alignment_range_two)))) -> (forall fpr_i_wtp_alignment fpr_j_wtp_alignment fpr_x_wtp_alignment. (exists fpr_h_wtp_alignment. fpr_h_wtp_alignment + S fpr_i_wtp_alignment = l) -> (((exists ff_h_wtp_alignment_map. ff_h_wtp_alignment_map + S (fpr_j_wtp_alignment) = S ((S (fpr_i_wtp_alignment)) * s)) /\ exists ff_q_wtp_alignment_map. r = ff_q_wtp_alignment_map * S ((S (fpr_i_wtp_alignment)) * s) + (fpr_j_wtp_alignment))) -> (((exists ff_h_wtp_alignment_source. ff_h_wtp_alignment_source + S (fpr_x_wtp_alignment) = S ((S (fpr_j_wtp_alignment)) * d)) /\ exists ff_q_wtp_alignment_source. z = ff_q_wtp_alignment_source * S ((S (fpr_j_wtp_alignment)) * d) + (fpr_x_wtp_alignment))) -> (((exists ff_h_wtp_alignment_target. ff_h_wtp_alignment_target + S (fpr_x_wtp_alignment) = S ((S (fpr_i_wtp_alignment)) * g)) /\ exists ff_q_wtp_alignment_target. f = ff_q_wtp_alignment_target * S ((S (fpr_i_wtp_alignment)) * g) + (fpr_x_wtp_alignment))))