gauss_signed_pointwise_mul_product_mod

Exact expanded PA statement

forall p h r a b c mb mc sb sc fb fc tb tc P T A. p = S r -> r = 2 * h -> (forall gsp_index_pointwise_signed_prefix. (exists gsp_lt_gap_pointwise_signed_prefix_index_bound. gsp_lt_gap_pointwise_signed_prefix_index_bound + S gsp_index_pointwise_signed_prefix = h) -> (exists gsp_value_pointwise_signed_prefix_entry gsp_magnitude_pointwise_signed_prefix_entry gsp_sign_pointwise_signed_prefix_entry. (((exists ff_h_gsp_pointwise_signed_prefix_entry_source. ff_h_gsp_pointwise_signed_prefix_entry_source + S (gsp_value_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * c)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_source. b = ff_q_gsp_pointwise_signed_prefix_entry_source * S ((S (gsp_index_pointwise_signed_prefix)) * c) + (gsp_value_pointwise_signed_prefix_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_prefix_entry_magnitude. ff_h_gsp_pointwise_signed_prefix_entry_magnitude + S (gsp_magnitude_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * mc)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_magnitude. mb = ff_q_gsp_pointwise_signed_prefix_entry_magnitude * S ((S (gsp_index_pointwise_signed_prefix)) * mc) + (gsp_magnitude_pointwise_signed_prefix_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_prefix_entry_sign. ff_h_gsp_pointwise_signed_prefix_entry_sign + S (gsp_sign_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * sc)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_sign. sb = ff_q_gsp_pointwise_signed_prefix_entry_sign * S ((S (gsp_index_pointwise_signed_prefix)) * sc) + (gsp_sign_pointwise_signed_prefix_entry))) /\ ((exists gsp_lt_gap_pointwise_signed_prefix_entry_positive. gsp_lt_gap_pointwise_signed_prefix_entry_positive + S 0 = gsp_magnitude_pointwise_signed_prefix_entry) /\ ((exists gsp_le_gap_pointwise_signed_prefix_entry_bounded. gsp_le_gap_pointwise_signed_prefix_entry_bounded + gsp_magnitude_pointwise_signed_prefix_entry = h) /\ ((gsp_sign_pointwise_signed_prefix_entry = 0 \/ gsp_sign_pointwise_signed_prefix_entry = 1) /\ (((gsp_sign_pointwise_signed_prefix_entry = 0 /\ (exists gsp_mod_left_pointwise_signed_prefix_entry_lower gsp_mod_right_pointwise_signed_prefix_entry_lower. (a * gsp_value_pointwise_signed_prefix_entry) + p * gsp_mod_left_pointwise_signed_prefix_entry_lower = (gsp_magnitude_pointwise_signed_prefix_entry) + p * gsp_mod_right_pointwise_signed_prefix_entry_lower)) \/ (gsp_sign_pointwise_signed_prefix_entry = 1 /\ (exists gsp_mod_left_pointwise_signed_prefix_entry_reflected gsp_mod_right_pointwise_signed_prefix_entry_reflected. (a * gsp_value_pointwise_signed_prefix_entry) + p * gsp_mod_left_pointwise_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_pointwise_signed_prefix_entry) + p * gsp_mod_right_pointwise_signed_prefix_entry_reflected))))))))))) -> (forall gspf_index_pointwise_sign_factors gspf_bit_pointwise_sign_factors. (exists gsp_lt_gap_pointwise_sign_factors_bound. gsp_lt_gap_pointwise_sign_factors_bound + S gspf_index_pointwise_sign_factors = h) -> (((exists ff_h_gspf_pointwise_sign_factors_bit. ff_h_gspf_pointwise_sign_factors_bit + S (gspf_bit_pointwise_sign_factors) = S ((S (gspf_index_pointwise_sign_factors)) * sc)) /\ exists ff_q_gspf_pointwise_sign_factors_bit. sb = ff_q_gspf_pointwise_sign_factors_bit * S ((S (gspf_index_pointwise_sign_factors)) * sc) + (gspf_bit_pointwise_sign_factors))) -> (((gspf_bit_pointwise_sign_factors = 0) /\ (((exists gsp_beta_height_gspf_pointwise_sign_factors_one. gsp_beta_height_gspf_pointwise_sign_factors_one + S (1) = S ((S (gspf_index_pointwise_sign_factors)) * fc)) /\ exists gsp_beta_quotient_gspf_pointwise_sign_factors_one. fb = gsp_beta_quotient_gspf_pointwise_sign_factors_one * S ((S (gspf_index_pointwise_sign_factors)) * fc) + (1)))) \/ ((gspf_bit_pointwise_sign_factors = 1) /\ (((exists ff_h_gspf_pointwise_sign_factors_predecessor. ff_h_gspf_pointwise_sign_factors_predecessor + S (r) = S ((S (gspf_index_pointwise_sign_factors)) * fc)) /\ exists ff_q_gspf_pointwise_sign_factors_predecessor. fb = ff_q_gspf_pointwise_sign_factors_predecessor * S ((S (gspf_index_pointwise_sign_factors)) * fc) + (r)))))) -> (forall fpmp_index_pointwise_products fpmp_left_pointwise_products fpmp_right_pointwise_products fpmp_target_pointwise_products. (exists fpmp_gap_pointwise_products. fpmp_gap_pointwise_products + S fpmp_index_pointwise_products = h) -> (((exists ff_h_fpmp_pointwise_products_left. ff_h_fpmp_pointwise_products_left + S (fpmp_left_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * mc)) /\ exists ff_q_fpmp_pointwise_products_left. mb = ff_q_fpmp_pointwise_products_left * S ((S (fpmp_index_pointwise_products)) * mc) + (fpmp_left_pointwise_products))) -> (((exists ff_h_fpmp_pointwise_products_right. ff_h_fpmp_pointwise_products_right + S (fpmp_right_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * fc)) /\ exists ff_q_fpmp_pointwise_products_right. fb = ff_q_fpmp_pointwise_products_right * S ((S (fpmp_index_pointwise_products)) * fc) + (fpmp_right_pointwise_products))) -> (((exists ff_h_fpmp_pointwise_products_target. ff_h_fpmp_pointwise_products_target + S (fpmp_target_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * tc)) /\ exists ff_q_fpmp_pointwise_products_target. tb = ff_q_fpmp_pointwise_products_target * S ((S (fpmp_index_pointwise_products)) * tc) + (fpmp_target_pointwise_products))) -> fpmp_target_pointwise_products = fpmp_left_pointwise_products * fpmp_right_pointwise_products) -> (exists ff_u_pointwise_product_source ff_v_pointwise_product_source. ((((exists ff_h_pointwise_product_source_start. ff_h_pointwise_product_source_start + S (1) = S ((S (0)) * ff_v_pointwise_product_source)) /\ exists ff_q_pointwise_product_source_start. ff_u_pointwise_product_source = ff_q_pointwise_product_source_start * S ((S (0)) * ff_v_pointwise_product_source) + (1))) /\ ((((exists ff_h_pointwise_product_source_terminal. ff_h_pointwise_product_source_terminal + S (P) = S ((S (h)) * ff_v_pointwise_product_source)) /\ exists ff_q_pointwise_product_source_terminal. ff_u_pointwise_product_source = ff_q_pointwise_product_source_terminal * S ((S (h)) * ff_v_pointwise_product_source) + (P))) /\ forall ff_i_pointwise_product_source. (exists ff_lt_pointwise_product_source_bound. ff_lt_pointwise_product_source_bound + S ff_i_pointwise_product_source = h) -> exists ff_p_pointwise_product_source ff_r_pointwise_product_source ff_s_pointwise_product_source. ((((exists ff_h_pointwise_product_source_factor. ff_h_pointwise_product_source_factor + S (ff_p_pointwise_product_source) = S ((S (ff_i_pointwise_product_source)) * c)) /\ exists ff_q_pointwise_product_source_factor. b = ff_q_pointwise_product_source_factor * S ((S (ff_i_pointwise_product_source)) * c) + (ff_p_pointwise_product_source))) /\ ((((exists ff_h_pointwise_product_source_partial. ff_h_pointwise_product_source_partial + S (ff_r_pointwise_product_source) = S ((S (ff_i_pointwise_product_source)) * ff_v_pointwise_product_source)) /\ exists ff_q_pointwise_product_source_partial. ff_u_pointwise_product_source = ff_q_pointwise_product_source_partial * S ((S (ff_i_pointwise_product_source)) * ff_v_pointwise_product_source) + (ff_r_pointwise_product_source))) /\ ((((exists ff_h_pointwise_product_source_successor. ff_h_pointwise_product_source_successor + S (ff_s_pointwise_product_source) = S ((S (S ff_i_pointwise_product_source)) * ff_v_pointwise_product_source)) /\ exists ff_q_pointwise_product_source_successor. ff_u_pointwise_product_source = ff_q_pointwise_product_source_successor * S ((S (S ff_i_pointwise_product_source)) * ff_v_pointwise_product_source) + (ff_s_pointwise_product_source))) /\ ff_s_pointwise_product_source = ff_r_pointwise_product_source * ff_p_pointwise_product_source)))))) -> (exists ff_u_pointwise_product_target ff_v_pointwise_product_target. ((((exists ff_h_pointwise_product_target_start. ff_h_pointwise_product_target_start + S (1) = S ((S (0)) * ff_v_pointwise_product_target)) /\ exists ff_q_pointwise_product_target_start. ff_u_pointwise_product_target = ff_q_pointwise_product_target_start * S ((S (0)) * ff_v_pointwise_product_target) + (1))) /\ ((((exists ff_h_pointwise_product_target_terminal. ff_h_pointwise_product_target_terminal + S (T) = S ((S (h)) * ff_v_pointwise_product_target)) /\ exists ff_q_pointwise_product_target_terminal. ff_u_pointwise_product_target = ff_q_pointwise_product_target_terminal * S ((S (h)) * ff_v_pointwise_product_target) + (T))) /\ forall ff_i_pointwise_product_target. (exists ff_lt_pointwise_product_target_bound. ff_lt_pointwise_product_target_bound + S ff_i_pointwise_product_target = h) -> exists ff_p_pointwise_product_target ff_r_pointwise_product_target ff_s_pointwise_product_target. ((((exists ff_h_pointwise_product_target_factor. ff_h_pointwise_product_target_factor + S (ff_p_pointwise_product_target) = S ((S (ff_i_pointwise_product_target)) * tc)) /\ exists ff_q_pointwise_product_target_factor. tb = ff_q_pointwise_product_target_factor * S ((S (ff_i_pointwise_product_target)) * tc) + (ff_p_pointwise_product_target))) /\ ((((exists ff_h_pointwise_product_target_partial. ff_h_pointwise_product_target_partial + S (ff_r_pointwise_product_target) = S ((S (ff_i_pointwise_product_target)) * ff_v_pointwise_product_target)) /\ exists ff_q_pointwise_product_target_partial. ff_u_pointwise_product_target = ff_q_pointwise_product_target_partial * S ((S (ff_i_pointwise_product_target)) * ff_v_pointwise_product_target) + (ff_r_pointwise_product_target))) /\ ((((exists ff_h_pointwise_product_target_successor. ff_h_pointwise_product_target_successor + S (ff_s_pointwise_product_target) = S ((S (S ff_i_pointwise_product_target)) * ff_v_pointwise_product_target)) /\ exists ff_q_pointwise_product_target_successor. ff_u_pointwise_product_target = ff_q_pointwise_product_target_successor * S ((S (S ff_i_pointwise_product_target)) * ff_v_pointwise_product_target) + (ff_s_pointwise_product_target))) /\ ff_s_pointwise_product_target = ff_r_pointwise_product_target * ff_p_pointwise_product_target)))))) -> (exists ff_b_pointwise_product_power ff_c_pointwise_product_power. ((forall ff_i_pointwise_product_power_repeat. (exists ff_lt_pointwise_product_power_repeat_bound. ff_lt_pointwise_product_power_repeat_bound + S ff_i_pointwise_product_power_repeat = h) -> (((exists ff_h_pointwise_product_power_repeat_decoded. ff_h_pointwise_product_power_repeat_decoded + S (a) = S ((S (ff_i_pointwise_product_power_repeat)) * ff_c_pointwise_product_power)) /\ exists ff_q_pointwise_product_power_repeat_decoded. ff_b_pointwise_product_power = ff_q_pointwise_product_power_repeat_decoded * S ((S (ff_i_pointwise_product_power_repeat)) * ff_c_pointwise_product_power) + (a)))) /\ (exists ff_u_pointwise_product_power_product ff_v_pointwise_product_power_product. ((((exists ff_h_pointwise_product_power_product_start. ff_h_pointwise_product_power_product_start + S (1) = S ((S (0)) * ff_v_pointwise_product_power_product)) /\ exists ff_q_pointwise_product_power_product_start. ff_u_pointwise_product_power_product = ff_q_pointwise_product_power_product_start * S ((S (0)) * ff_v_pointwise_product_power_product) + (1))) /\ ((((exists ff_h_pointwise_product_power_product_terminal. ff_h_pointwise_product_power_product_terminal + S (A) = S ((S (h)) * ff_v_pointwise_product_power_product)) /\ exists ff_q_pointwise_product_power_product_terminal. ff_u_pointwise_product_power_product = ff_q_pointwise_product_power_product_terminal * S ((S (h)) * ff_v_pointwise_product_power_product) + (A))) /\ forall ff_i_pointwise_product_power_product. (exists ff_lt_pointwise_product_power_product_bound. ff_lt_pointwise_product_power_product_bound + S ff_i_pointwise_product_power_product = h) -> exists ff_p_pointwise_product_power_product ff_r_pointwise_product_power_product ff_s_pointwise_product_power_product. ((((exists ff_h_pointwise_product_power_product_factor. ff_h_pointwise_product_power_product_factor + S (ff_p_pointwise_product_power_product) = S ((S (ff_i_pointwise_product_power_product)) * ff_c_pointwise_product_power)) /\ exists ff_q_pointwise_product_power_product_factor. ff_b_pointwise_product_power = ff_q_pointwise_product_power_product_factor * S ((S (ff_i_pointwise_product_power_product)) * ff_c_pointwise_product_power) + (ff_p_pointwise_product_power_product))) /\ ((((exists ff_h_pointwise_product_power_product_partial. ff_h_pointwise_product_power_product_partial + S (ff_r_pointwise_product_power_product) = S ((S (ff_i_pointwise_product_power_product)) * ff_v_pointwise_product_power_product)) /\ exists ff_q_pointwise_product_power_product_partial. ff_u_pointwise_product_power_product = ff_q_pointwise_product_power_product_partial * S ((S (ff_i_pointwise_product_power_product)) * ff_v_pointwise_product_power_product) + (ff_r_pointwise_product_power_product))) /\ ((((exists ff_h_pointwise_product_power_product_successor. ff_h_pointwise_product_power_product_successor + S (ff_s_pointwise_product_power_product) = S ((S (S ff_i_pointwise_product_power_product)) * ff_v_pointwise_product_power_product)) /\ exists ff_q_pointwise_product_power_product_successor. ff_u_pointwise_product_power_product = ff_q_pointwise_product_power_product_successor * S ((S (S ff_i_pointwise_product_power_product)) * ff_v_pointwise_product_power_product) + (ff_s_pointwise_product_power_product))) /\ ff_s_pointwise_product_power_product = ff_r_pointwise_product_power_product * ff_p_pointwise_product_power_product)))))))) -> (exists fsp_product_mod_left_pointwise_product_result fsp_product_mod_right_pointwise_product_result. (A * P) + p * fsp_product_mod_left_pointwise_product_result = T + p * fsp_product_mod_right_pointwise_product_result)