beta_magnitude_sum_permutation_exact

Exact expanded PA statement

forall b c mb mc rb rc h X M. (forall gsp_range_index_ges_half. (exists gsp_lt_gap_ges_half_range_bound. gsp_lt_gap_ges_half_range_bound + S gsp_range_index_ges_half = h) -> (((exists gsp_beta_height_ges_half_range_entry. gsp_beta_height_ges_half_range_entry + S (1 + gsp_range_index_ges_half) = S ((S (gsp_range_index_ges_half)) * c)) /\ exists gsp_beta_quotient_ges_half_range_entry. b = gsp_beta_quotient_ges_half_range_entry * S ((S (gsp_range_index_ges_half)) * c) + (1 + gsp_range_index_ges_half)))) -> (forall gmp_index_ges_magnitude_range. (exists gsp_lt_gap_ges_magnitude_range_index_bound. gsp_lt_gap_ges_magnitude_range_index_bound + S gmp_index_ges_magnitude_range = h) -> exists gmp_magnitude_ges_magnitude_range. ((((exists ff_h_gmp_ges_magnitude_range_decoded. ff_h_gmp_ges_magnitude_range_decoded + S (gmp_magnitude_ges_magnitude_range) = S ((S (gmp_index_ges_magnitude_range)) * mc)) /\ exists ff_q_gmp_ges_magnitude_range_decoded. mb = ff_q_gmp_ges_magnitude_range_decoded * S ((S (gmp_index_ges_magnitude_range)) * mc) + (gmp_magnitude_ges_magnitude_range))) /\ ((exists gsp_lt_gap_ges_magnitude_range_positive. gsp_lt_gap_ges_magnitude_range_positive + S 0 = gmp_magnitude_ges_magnitude_range) /\ (exists gsp_le_gap_ges_magnitude_range_bounded. gsp_le_gap_ges_magnitude_range_bounded + gmp_magnitude_ges_magnitude_range = h)))) -> (forall fp_i_ges_magnitude_injective fp_j_ges_magnitude_injective fp_value_ges_magnitude_injective. (exists fp_gap_ges_magnitude_injective_i. fp_gap_ges_magnitude_injective_i + S fp_i_ges_magnitude_injective = h) -> (exists fp_gap_ges_magnitude_injective_j. fp_gap_ges_magnitude_injective_j + S fp_j_ges_magnitude_injective = h) -> (((exists ff_h_ges_magnitude_injective_left. ff_h_ges_magnitude_injective_left + S (fp_value_ges_magnitude_injective) = S ((S (fp_i_ges_magnitude_injective)) * mc)) /\ exists ff_q_ges_magnitude_injective_left. mb = ff_q_ges_magnitude_injective_left * S ((S (fp_i_ges_magnitude_injective)) * mc) + (fp_value_ges_magnitude_injective))) -> (((exists ff_h_ges_magnitude_injective_right. ff_h_ges_magnitude_injective_right + S (fp_value_ges_magnitude_injective) = S ((S (fp_j_ges_magnitude_injective)) * mc)) /\ exists ff_q_ges_magnitude_injective_right. mb = ff_q_ges_magnitude_injective_right * S ((S (fp_j_ges_magnitude_injective)) * mc) + (fp_value_ges_magnitude_injective))) -> fp_i_ges_magnitude_injective = fp_j_ges_magnitude_injective) -> (forall gmp_index_ges_recode gmp_predecessor_ges_recode. (exists gsp_lt_gap_ges_recode_index_bound. gsp_lt_gap_ges_recode_index_bound + S gmp_index_ges_recode = h) -> (((exists gsp_beta_height_gmp_ges_recode_source. gsp_beta_height_gmp_ges_recode_source + S (S gmp_predecessor_ges_recode) = S ((S (gmp_index_ges_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_ges_recode_source. mb = gsp_beta_quotient_gmp_ges_recode_source * S ((S (gmp_index_ges_recode)) * mc) + (S gmp_predecessor_ges_recode))) -> (((exists ff_h_gmp_ges_recode_target. ff_h_gmp_ges_recode_target + S (gmp_predecessor_ges_recode) = S ((S (gmp_index_ges_recode)) * rc)) /\ exists ff_q_gmp_ges_recode_target. rb = ff_q_gmp_ges_recode_target * S ((S (gmp_index_ges_recode)) * rc) + (gmp_predecessor_ges_recode)))) -> (exists ff_u_ges_half_sum ff_v_ges_half_sum. ((((exists ff_h_ges_half_sum_start. ff_h_ges_half_sum_start + S (0) = S ((S (0)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_start. ff_u_ges_half_sum = ff_q_ges_half_sum_start * S ((S (0)) * ff_v_ges_half_sum) + (0))) /\ ((((exists ff_h_ges_half_sum_terminal. ff_h_ges_half_sum_terminal + S (X) = S ((S (h)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_terminal. ff_u_ges_half_sum = ff_q_ges_half_sum_terminal * S ((S (h)) * ff_v_ges_half_sum) + (X))) /\ forall ff_i_ges_half_sum. (exists ff_lt_ges_half_sum_bound. ff_lt_ges_half_sum_bound + S ff_i_ges_half_sum = h) -> exists ff_a_ges_half_sum ff_r_ges_half_sum ff_s_ges_half_sum. ((((exists ff_h_ges_half_sum_summand. ff_h_ges_half_sum_summand + S (ff_a_ges_half_sum) = S ((S (ff_i_ges_half_sum)) * c)) /\ exists ff_q_ges_half_sum_summand. b = ff_q_ges_half_sum_summand * S ((S (ff_i_ges_half_sum)) * c) + (ff_a_ges_half_sum))) /\ ((((exists ff_h_ges_half_sum_partial. ff_h_ges_half_sum_partial + S (ff_r_ges_half_sum) = S ((S (ff_i_ges_half_sum)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_partial. ff_u_ges_half_sum = ff_q_ges_half_sum_partial * S ((S (ff_i_ges_half_sum)) * ff_v_ges_half_sum) + (ff_r_ges_half_sum))) /\ ((((exists ff_h_ges_half_sum_successor. ff_h_ges_half_sum_successor + S (ff_s_ges_half_sum) = S ((S (S ff_i_ges_half_sum)) * ff_v_ges_half_sum)) /\ exists ff_q_ges_half_sum_successor. ff_u_ges_half_sum = ff_q_ges_half_sum_successor * S ((S (S ff_i_ges_half_sum)) * ff_v_ges_half_sum) + (ff_s_ges_half_sum))) /\ ff_s_ges_half_sum = ff_r_ges_half_sum + ff_a_ges_half_sum)))))) -> (exists ff_u_ges_magnitude_sum ff_v_ges_magnitude_sum. ((((exists ff_h_ges_magnitude_sum_start. ff_h_ges_magnitude_sum_start + S (0) = S ((S (0)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_start. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_start * S ((S (0)) * ff_v_ges_magnitude_sum) + (0))) /\ ((((exists ff_h_ges_magnitude_sum_terminal. ff_h_ges_magnitude_sum_terminal + S (M) = S ((S (h)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_terminal. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_terminal * S ((S (h)) * ff_v_ges_magnitude_sum) + (M))) /\ forall ff_i_ges_magnitude_sum. (exists ff_lt_ges_magnitude_sum_bound. ff_lt_ges_magnitude_sum_bound + S ff_i_ges_magnitude_sum = h) -> exists ff_a_ges_magnitude_sum ff_r_ges_magnitude_sum ff_s_ges_magnitude_sum. ((((exists ff_h_ges_magnitude_sum_summand. ff_h_ges_magnitude_sum_summand + S (ff_a_ges_magnitude_sum) = S ((S (ff_i_ges_magnitude_sum)) * mc)) /\ exists ff_q_ges_magnitude_sum_summand. mb = ff_q_ges_magnitude_sum_summand * S ((S (ff_i_ges_magnitude_sum)) * mc) + (ff_a_ges_magnitude_sum))) /\ ((((exists ff_h_ges_magnitude_sum_partial. ff_h_ges_magnitude_sum_partial + S (ff_r_ges_magnitude_sum) = S ((S (ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_partial. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_partial * S ((S (ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum) + (ff_r_ges_magnitude_sum))) /\ ((((exists ff_h_ges_magnitude_sum_successor. ff_h_ges_magnitude_sum_successor + S (ff_s_ges_magnitude_sum) = S ((S (S ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum)) /\ exists ff_q_ges_magnitude_sum_successor. ff_u_ges_magnitude_sum = ff_q_ges_magnitude_sum_successor * S ((S (S ff_i_ges_magnitude_sum)) * ff_v_ges_magnitude_sum) + (ff_s_ges_magnitude_sum))) /\ ff_s_ges_magnitude_sum = ff_r_ges_magnitude_sum + ff_a_ges_magnitude_sum)))))) -> X = M