beta_magnitude_predecessor_recode_injective

Exact expanded PA statement

forall mb mc rb rc l. (forall gmp_index_predecessor_transport_finite_range. (exists gsp_lt_gap_predecessor_transport_finite_range_index_bound. gsp_lt_gap_predecessor_transport_finite_range_index_bound + S gmp_index_predecessor_transport_finite_range = l) -> exists gmp_magnitude_predecessor_transport_finite_range. ((((exists ff_h_gmp_predecessor_transport_finite_range_decoded. ff_h_gmp_predecessor_transport_finite_range_decoded + S (gmp_magnitude_predecessor_transport_finite_range) = S ((S (gmp_index_predecessor_transport_finite_range)) * mc)) /\ exists ff_q_gmp_predecessor_transport_finite_range_decoded. mb = ff_q_gmp_predecessor_transport_finite_range_decoded * S ((S (gmp_index_predecessor_transport_finite_range)) * mc) + (gmp_magnitude_predecessor_transport_finite_range))) /\ ((exists gsp_lt_gap_predecessor_transport_finite_range_positive. gsp_lt_gap_predecessor_transport_finite_range_positive + S 0 = gmp_magnitude_predecessor_transport_finite_range) /\ (exists gsp_le_gap_predecessor_transport_finite_range_bounded. gsp_le_gap_predecessor_transport_finite_range_bounded + gmp_magnitude_predecessor_transport_finite_range = l)))) -> (forall fp_i_predecessor_transport_magnitude_injective fp_j_predecessor_transport_magnitude_injective fp_value_predecessor_transport_magnitude_injective. (exists fp_gap_predecessor_transport_magnitude_injective_i. fp_gap_predecessor_transport_magnitude_injective_i + S fp_i_predecessor_transport_magnitude_injective = l) -> (exists fp_gap_predecessor_transport_magnitude_injective_j. fp_gap_predecessor_transport_magnitude_injective_j + S fp_j_predecessor_transport_magnitude_injective = l) -> (((exists ff_h_predecessor_transport_magnitude_injective_left. ff_h_predecessor_transport_magnitude_injective_left + S (fp_value_predecessor_transport_magnitude_injective) = S ((S (fp_i_predecessor_transport_magnitude_injective)) * mc)) /\ exists ff_q_predecessor_transport_magnitude_injective_left. mb = ff_q_predecessor_transport_magnitude_injective_left * S ((S (fp_i_predecessor_transport_magnitude_injective)) * mc) + (fp_value_predecessor_transport_magnitude_injective))) -> (((exists ff_h_predecessor_transport_magnitude_injective_right. ff_h_predecessor_transport_magnitude_injective_right + S (fp_value_predecessor_transport_magnitude_injective) = S ((S (fp_j_predecessor_transport_magnitude_injective)) * mc)) /\ exists ff_q_predecessor_transport_magnitude_injective_right. mb = ff_q_predecessor_transport_magnitude_injective_right * S ((S (fp_j_predecessor_transport_magnitude_injective)) * mc) + (fp_value_predecessor_transport_magnitude_injective))) -> fp_i_predecessor_transport_magnitude_injective = fp_j_predecessor_transport_magnitude_injective) -> (forall gmp_index_predecessor_transport_recode gmp_predecessor_predecessor_transport_recode. (exists gsp_lt_gap_predecessor_transport_recode_index_bound. gsp_lt_gap_predecessor_transport_recode_index_bound + S gmp_index_predecessor_transport_recode = l) -> (((exists gsp_beta_height_gmp_predecessor_transport_recode_source. gsp_beta_height_gmp_predecessor_transport_recode_source + S (S gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_transport_recode_source. mb = gsp_beta_quotient_gmp_predecessor_transport_recode_source * S ((S (gmp_index_predecessor_transport_recode)) * mc) + (S gmp_predecessor_predecessor_transport_recode))) -> (((exists ff_h_gmp_predecessor_transport_recode_target. ff_h_gmp_predecessor_transport_recode_target + S (gmp_predecessor_predecessor_transport_recode) = S ((S (gmp_index_predecessor_transport_recode)) * rc)) /\ exists ff_q_gmp_predecessor_transport_recode_target. rb = ff_q_gmp_predecessor_transport_recode_target * S ((S (gmp_index_predecessor_transport_recode)) * rc) + (gmp_predecessor_predecessor_transport_recode)))) -> (forall fp_i_predecessor_transport_target_injective fp_j_predecessor_transport_target_injective fp_value_predecessor_transport_target_injective. (exists fp_gap_predecessor_transport_target_injective_i. fp_gap_predecessor_transport_target_injective_i + S fp_i_predecessor_transport_target_injective = l) -> (exists fp_gap_predecessor_transport_target_injective_j. fp_gap_predecessor_transport_target_injective_j + S fp_j_predecessor_transport_target_injective = l) -> (((exists ff_h_predecessor_transport_target_injective_left. ff_h_predecessor_transport_target_injective_left + S (fp_value_predecessor_transport_target_injective) = S ((S (fp_i_predecessor_transport_target_injective)) * rc)) /\ exists ff_q_predecessor_transport_target_injective_left. rb = ff_q_predecessor_transport_target_injective_left * S ((S (fp_i_predecessor_transport_target_injective)) * rc) + (fp_value_predecessor_transport_target_injective))) -> (((exists ff_h_predecessor_transport_target_injective_right. ff_h_predecessor_transport_target_injective_right + S (fp_value_predecessor_transport_target_injective) = S ((S (fp_j_predecessor_transport_target_injective)) * rc)) /\ exists ff_q_predecessor_transport_target_injective_right. rb = ff_q_predecessor_transport_target_injective_right * S ((S (fp_j_predecessor_transport_target_injective)) * rc) + (fp_value_predecessor_transport_target_injective))) -> fp_i_predecessor_transport_target_injective = fp_j_predecessor_transport_target_injective)