gauss_magnitude_product_eq_half_range

Exact expanded PA statement

forall mb mc rb rc b c h P Q. (forall gmp_index_product_magnitude_range. (exists gsp_lt_gap_product_magnitude_range_index_bound. gsp_lt_gap_product_magnitude_range_index_bound + S gmp_index_product_magnitude_range = h) -> exists gmp_magnitude_product_magnitude_range. ((((exists ff_h_gmp_product_magnitude_range_decoded. ff_h_gmp_product_magnitude_range_decoded + S (gmp_magnitude_product_magnitude_range) = S ((S (gmp_index_product_magnitude_range)) * mc)) /\ exists ff_q_gmp_product_magnitude_range_decoded. mb = ff_q_gmp_product_magnitude_range_decoded * S ((S (gmp_index_product_magnitude_range)) * mc) + (gmp_magnitude_product_magnitude_range))) /\ ((exists gsp_lt_gap_product_magnitude_range_positive. gsp_lt_gap_product_magnitude_range_positive + S 0 = gmp_magnitude_product_magnitude_range) /\ (exists gsp_le_gap_product_magnitude_range_bounded. gsp_le_gap_product_magnitude_range_bounded + gmp_magnitude_product_magnitude_range = h)))) -> (forall fp_i_product_magnitude_injective fp_j_product_magnitude_injective fp_value_product_magnitude_injective. (exists fp_gap_product_magnitude_injective_i. fp_gap_product_magnitude_injective_i + S fp_i_product_magnitude_injective = h) -> (exists fp_gap_product_magnitude_injective_j. fp_gap_product_magnitude_injective_j + S fp_j_product_magnitude_injective = h) -> (((exists ff_h_product_magnitude_injective_left. ff_h_product_magnitude_injective_left + S (fp_value_product_magnitude_injective) = S ((S (fp_i_product_magnitude_injective)) * mc)) /\ exists ff_q_product_magnitude_injective_left. mb = ff_q_product_magnitude_injective_left * S ((S (fp_i_product_magnitude_injective)) * mc) + (fp_value_product_magnitude_injective))) -> (((exists ff_h_product_magnitude_injective_right. ff_h_product_magnitude_injective_right + S (fp_value_product_magnitude_injective) = S ((S (fp_j_product_magnitude_injective)) * mc)) /\ exists ff_q_product_magnitude_injective_right. mb = ff_q_product_magnitude_injective_right * S ((S (fp_j_product_magnitude_injective)) * mc) + (fp_value_product_magnitude_injective))) -> fp_i_product_magnitude_injective = fp_j_product_magnitude_injective) -> (forall gmp_index_product_predecessor_recode gmp_predecessor_product_predecessor_recode. (exists gsp_lt_gap_product_predecessor_recode_index_bound. gsp_lt_gap_product_predecessor_recode_index_bound + S gmp_index_product_predecessor_recode = h) -> (((exists gsp_beta_height_gmp_product_predecessor_recode_source. gsp_beta_height_gmp_product_predecessor_recode_source + S (S gmp_predecessor_product_predecessor_recode) = S ((S (gmp_index_product_predecessor_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_product_predecessor_recode_source. mb = gsp_beta_quotient_gmp_product_predecessor_recode_source * S ((S (gmp_index_product_predecessor_recode)) * mc) + (S gmp_predecessor_product_predecessor_recode))) -> (((exists ff_h_gmp_product_predecessor_recode_target. ff_h_gmp_product_predecessor_recode_target + S (gmp_predecessor_product_predecessor_recode) = S ((S (gmp_index_product_predecessor_recode)) * rc)) /\ exists ff_q_gmp_product_predecessor_recode_target. rb = ff_q_gmp_product_predecessor_recode_target * S ((S (gmp_index_product_predecessor_recode)) * rc) + (gmp_predecessor_product_predecessor_recode)))) -> (forall gsp_range_index_product_canonical_half_range. (exists gsp_lt_gap_product_canonical_half_range_range_bound. gsp_lt_gap_product_canonical_half_range_range_bound + S gsp_range_index_product_canonical_half_range = h) -> (((exists gsp_beta_height_product_canonical_half_range_range_entry. gsp_beta_height_product_canonical_half_range_range_entry + S (1 + gsp_range_index_product_canonical_half_range) = S ((S (gsp_range_index_product_canonical_half_range)) * c)) /\ exists gsp_beta_quotient_product_canonical_half_range_range_entry. b = gsp_beta_quotient_product_canonical_half_range_range_entry * S ((S (gsp_range_index_product_canonical_half_range)) * c) + (1 + gsp_range_index_product_canonical_half_range)))) -> (exists ff_u_product_canonical_product ff_v_product_canonical_product. ((((exists ff_h_product_canonical_product_start. ff_h_product_canonical_product_start + S (1) = S ((S (0)) * ff_v_product_canonical_product)) /\ exists ff_q_product_canonical_product_start. ff_u_product_canonical_product = ff_q_product_canonical_product_start * S ((S (0)) * ff_v_product_canonical_product) + (1))) /\ ((((exists ff_h_product_canonical_product_terminal. ff_h_product_canonical_product_terminal + S (P) = S ((S (h)) * ff_v_product_canonical_product)) /\ exists ff_q_product_canonical_product_terminal. ff_u_product_canonical_product = ff_q_product_canonical_product_terminal * S ((S (h)) * ff_v_product_canonical_product) + (P))) /\ forall ff_i_product_canonical_product. (exists ff_lt_product_canonical_product_bound. ff_lt_product_canonical_product_bound + S ff_i_product_canonical_product = h) -> exists ff_p_product_canonical_product ff_r_product_canonical_product ff_s_product_canonical_product. ((((exists ff_h_product_canonical_product_factor. ff_h_product_canonical_product_factor + S (ff_p_product_canonical_product) = S ((S (ff_i_product_canonical_product)) * c)) /\ exists ff_q_product_canonical_product_factor. b = ff_q_product_canonical_product_factor * S ((S (ff_i_product_canonical_product)) * c) + (ff_p_product_canonical_product))) /\ ((((exists ff_h_product_canonical_product_partial. ff_h_product_canonical_product_partial + S (ff_r_product_canonical_product) = S ((S (ff_i_product_canonical_product)) * ff_v_product_canonical_product)) /\ exists ff_q_product_canonical_product_partial. ff_u_product_canonical_product = ff_q_product_canonical_product_partial * S ((S (ff_i_product_canonical_product)) * ff_v_product_canonical_product) + (ff_r_product_canonical_product))) /\ ((((exists ff_h_product_canonical_product_successor. ff_h_product_canonical_product_successor + S (ff_s_product_canonical_product) = S ((S (S ff_i_product_canonical_product)) * ff_v_product_canonical_product)) /\ exists ff_q_product_canonical_product_successor. ff_u_product_canonical_product = ff_q_product_canonical_product_successor * S ((S (S ff_i_product_canonical_product)) * ff_v_product_canonical_product) + (ff_s_product_canonical_product))) /\ ff_s_product_canonical_product = ff_r_product_canonical_product * ff_p_product_canonical_product)))))) -> (exists ff_u_product_magnitude_product ff_v_product_magnitude_product. ((((exists ff_h_product_magnitude_product_start. ff_h_product_magnitude_product_start + S (1) = S ((S (0)) * ff_v_product_magnitude_product)) /\ exists ff_q_product_magnitude_product_start. ff_u_product_magnitude_product = ff_q_product_magnitude_product_start * S ((S (0)) * ff_v_product_magnitude_product) + (1))) /\ ((((exists ff_h_product_magnitude_product_terminal. ff_h_product_magnitude_product_terminal + S (Q) = S ((S (h)) * ff_v_product_magnitude_product)) /\ exists ff_q_product_magnitude_product_terminal. ff_u_product_magnitude_product = ff_q_product_magnitude_product_terminal * S ((S (h)) * ff_v_product_magnitude_product) + (Q))) /\ forall ff_i_product_magnitude_product. (exists ff_lt_product_magnitude_product_bound. ff_lt_product_magnitude_product_bound + S ff_i_product_magnitude_product = h) -> exists ff_p_product_magnitude_product ff_r_product_magnitude_product ff_s_product_magnitude_product. ((((exists ff_h_product_magnitude_product_factor. ff_h_product_magnitude_product_factor + S (ff_p_product_magnitude_product) = S ((S (ff_i_product_magnitude_product)) * mc)) /\ exists ff_q_product_magnitude_product_factor. mb = ff_q_product_magnitude_product_factor * S ((S (ff_i_product_magnitude_product)) * mc) + (ff_p_product_magnitude_product))) /\ ((((exists ff_h_product_magnitude_product_partial. ff_h_product_magnitude_product_partial + S (ff_r_product_magnitude_product) = S ((S (ff_i_product_magnitude_product)) * ff_v_product_magnitude_product)) /\ exists ff_q_product_magnitude_product_partial. ff_u_product_magnitude_product = ff_q_product_magnitude_product_partial * S ((S (ff_i_product_magnitude_product)) * ff_v_product_magnitude_product) + (ff_r_product_magnitude_product))) /\ ((((exists ff_h_product_magnitude_product_successor. ff_h_product_magnitude_product_successor + S (ff_s_product_magnitude_product) = S ((S (S ff_i_product_magnitude_product)) * ff_v_product_magnitude_product)) /\ exists ff_q_product_magnitude_product_successor. ff_u_product_magnitude_product = ff_q_product_magnitude_product_successor * S ((S (S ff_i_product_magnitude_product)) * ff_v_product_magnitude_product) + (ff_s_product_magnitude_product))) /\ ff_s_product_magnitude_product = ff_r_product_magnitude_product * ff_p_product_magnitude_product)))))) -> P = Q