pair_order_terminal_successor_product_eq_range_two

Exact expanded PA statement

forall b c r s z d f g l P Q. (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 fp_i_wtp_source_injective fp_j_wtp_source_injective fp_value_wtp_source_injective. (exists fp_gap_wtp_source_injective_i. fp_gap_wtp_source_injective_i + S fp_i_wtp_source_injective = l) -> (exists fp_gap_wtp_source_injective_j. fp_gap_wtp_source_injective_j + S fp_j_wtp_source_injective = l) -> (((exists ff_h_wtp_source_injective_left. ff_h_wtp_source_injective_left + S (fp_value_wtp_source_injective) = S ((S (fp_i_wtp_source_injective)) * c)) /\ exists ff_q_wtp_source_injective_left. b = ff_q_wtp_source_injective_left * S ((S (fp_i_wtp_source_injective)) * c) + (fp_value_wtp_source_injective))) -> (((exists ff_h_wtp_source_injective_right. ff_h_wtp_source_injective_right + S (fp_value_wtp_source_injective) = S ((S (fp_j_wtp_source_injective)) * c)) /\ exists ff_q_wtp_source_injective_right. b = ff_q_wtp_source_injective_right * S ((S (fp_j_wtp_source_injective)) * c) + (fp_value_wtp_source_injective))) -> fp_i_wtp_source_injective = fp_j_wtp_source_injective) -> (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)))) -> (exists ff_u_wtp_canonical_product ff_v_wtp_canonical_product. ((((exists ff_h_wtp_canonical_product_start. ff_h_wtp_canonical_product_start + S (1) = S ((S (0)) * ff_v_wtp_canonical_product)) /\ exists ff_q_wtp_canonical_product_start. ff_u_wtp_canonical_product = ff_q_wtp_canonical_product_start * S ((S (0)) * ff_v_wtp_canonical_product) + (1))) /\ ((((exists ff_h_wtp_canonical_product_terminal. ff_h_wtp_canonical_product_terminal + S (P) = S ((S (l)) * ff_v_wtp_canonical_product)) /\ exists ff_q_wtp_canonical_product_terminal. ff_u_wtp_canonical_product = ff_q_wtp_canonical_product_terminal * S ((S (l)) * ff_v_wtp_canonical_product) + (P))) /\ forall ff_i_wtp_canonical_product. (exists ff_lt_wtp_canonical_product_bound. ff_lt_wtp_canonical_product_bound + S ff_i_wtp_canonical_product = l) -> exists ff_p_wtp_canonical_product ff_r_wtp_canonical_product ff_s_wtp_canonical_product. ((((exists ff_h_wtp_canonical_product_factor. ff_h_wtp_canonical_product_factor + S (ff_p_wtp_canonical_product) = S ((S (ff_i_wtp_canonical_product)) * d)) /\ exists ff_q_wtp_canonical_product_factor. z = ff_q_wtp_canonical_product_factor * S ((S (ff_i_wtp_canonical_product)) * d) + (ff_p_wtp_canonical_product))) /\ ((((exists ff_h_wtp_canonical_product_partial. ff_h_wtp_canonical_product_partial + S (ff_r_wtp_canonical_product) = S ((S (ff_i_wtp_canonical_product)) * ff_v_wtp_canonical_product)) /\ exists ff_q_wtp_canonical_product_partial. ff_u_wtp_canonical_product = ff_q_wtp_canonical_product_partial * S ((S (ff_i_wtp_canonical_product)) * ff_v_wtp_canonical_product) + (ff_r_wtp_canonical_product))) /\ ((((exists ff_h_wtp_canonical_product_successor. ff_h_wtp_canonical_product_successor + S (ff_s_wtp_canonical_product) = S ((S (S ff_i_wtp_canonical_product)) * ff_v_wtp_canonical_product)) /\ exists ff_q_wtp_canonical_product_successor. ff_u_wtp_canonical_product = ff_q_wtp_canonical_product_successor * S ((S (S ff_i_wtp_canonical_product)) * ff_v_wtp_canonical_product) + (ff_s_wtp_canonical_product))) /\ ff_s_wtp_canonical_product = ff_r_wtp_canonical_product * ff_p_wtp_canonical_product)))))) -> (exists ff_u_wtp_lifted_product ff_v_wtp_lifted_product. ((((exists ff_h_wtp_lifted_product_start. ff_h_wtp_lifted_product_start + S (1) = S ((S (0)) * ff_v_wtp_lifted_product)) /\ exists ff_q_wtp_lifted_product_start. ff_u_wtp_lifted_product = ff_q_wtp_lifted_product_start * S ((S (0)) * ff_v_wtp_lifted_product) + (1))) /\ ((((exists ff_h_wtp_lifted_product_terminal. ff_h_wtp_lifted_product_terminal + S (Q) = S ((S (l)) * ff_v_wtp_lifted_product)) /\ exists ff_q_wtp_lifted_product_terminal. ff_u_wtp_lifted_product = ff_q_wtp_lifted_product_terminal * S ((S (l)) * ff_v_wtp_lifted_product) + (Q))) /\ forall ff_i_wtp_lifted_product. (exists ff_lt_wtp_lifted_product_bound. ff_lt_wtp_lifted_product_bound + S ff_i_wtp_lifted_product = l) -> exists ff_p_wtp_lifted_product ff_r_wtp_lifted_product ff_s_wtp_lifted_product. ((((exists ff_h_wtp_lifted_product_factor. ff_h_wtp_lifted_product_factor + S (ff_p_wtp_lifted_product) = S ((S (ff_i_wtp_lifted_product)) * g)) /\ exists ff_q_wtp_lifted_product_factor. f = ff_q_wtp_lifted_product_factor * S ((S (ff_i_wtp_lifted_product)) * g) + (ff_p_wtp_lifted_product))) /\ ((((exists ff_h_wtp_lifted_product_partial. ff_h_wtp_lifted_product_partial + S (ff_r_wtp_lifted_product) = S ((S (ff_i_wtp_lifted_product)) * ff_v_wtp_lifted_product)) /\ exists ff_q_wtp_lifted_product_partial. ff_u_wtp_lifted_product = ff_q_wtp_lifted_product_partial * S ((S (ff_i_wtp_lifted_product)) * ff_v_wtp_lifted_product) + (ff_r_wtp_lifted_product))) /\ ((((exists ff_h_wtp_lifted_product_successor. ff_h_wtp_lifted_product_successor + S (ff_s_wtp_lifted_product) = S ((S (S ff_i_wtp_lifted_product)) * ff_v_wtp_lifted_product)) /\ exists ff_q_wtp_lifted_product_successor. ff_u_wtp_lifted_product = ff_q_wtp_lifted_product_successor * S ((S (S ff_i_wtp_lifted_product)) * ff_v_wtp_lifted_product) + (ff_s_wtp_lifted_product))) /\ ff_s_wtp_lifted_product = ff_r_wtp_lifted_product * ff_p_wtp_lifted_product)))))) -> P = Q