gauss_signed_products_balance_mod

Exact expanded PA statement

forall p h r a b c mb mc rb rc sb sc fb fc tb tc e P M Sprod T A R. p = S r -> r = 2 * h -> (forall gsp_index_gauss_composition_signed_prefix. (exists gsp_lt_gap_gauss_composition_signed_prefix_index_bound. gsp_lt_gap_gauss_composition_signed_prefix_index_bound + S gsp_index_gauss_composition_signed_prefix = h) -> (exists gsp_value_gauss_composition_signed_prefix_entry gsp_magnitude_gauss_composition_signed_prefix_entry gsp_sign_gauss_composition_signed_prefix_entry. (((exists ff_h_gsp_gauss_composition_signed_prefix_entry_source. ff_h_gsp_gauss_composition_signed_prefix_entry_source + S (gsp_value_gauss_composition_signed_prefix_entry) = S ((S (gsp_index_gauss_composition_signed_prefix)) * c)) /\ exists ff_q_gsp_gauss_composition_signed_prefix_entry_source. b = ff_q_gsp_gauss_composition_signed_prefix_entry_source * S ((S (gsp_index_gauss_composition_signed_prefix)) * c) + (gsp_value_gauss_composition_signed_prefix_entry))) /\ ((((exists ff_h_gsp_gauss_composition_signed_prefix_entry_magnitude. ff_h_gsp_gauss_composition_signed_prefix_entry_magnitude + S (gsp_magnitude_gauss_composition_signed_prefix_entry) = S ((S (gsp_index_gauss_composition_signed_prefix)) * mc)) /\ exists ff_q_gsp_gauss_composition_signed_prefix_entry_magnitude. mb = ff_q_gsp_gauss_composition_signed_prefix_entry_magnitude * S ((S (gsp_index_gauss_composition_signed_prefix)) * mc) + (gsp_magnitude_gauss_composition_signed_prefix_entry))) /\ ((((exists ff_h_gsp_gauss_composition_signed_prefix_entry_sign. ff_h_gsp_gauss_composition_signed_prefix_entry_sign + S (gsp_sign_gauss_composition_signed_prefix_entry) = S ((S (gsp_index_gauss_composition_signed_prefix)) * sc)) /\ exists ff_q_gsp_gauss_composition_signed_prefix_entry_sign. sb = ff_q_gsp_gauss_composition_signed_prefix_entry_sign * S ((S (gsp_index_gauss_composition_signed_prefix)) * sc) + (gsp_sign_gauss_composition_signed_prefix_entry))) /\ ((exists gsp_lt_gap_gauss_composition_signed_prefix_entry_positive. gsp_lt_gap_gauss_composition_signed_prefix_entry_positive + S 0 = gsp_magnitude_gauss_composition_signed_prefix_entry) /\ ((exists gsp_le_gap_gauss_composition_signed_prefix_entry_bounded. gsp_le_gap_gauss_composition_signed_prefix_entry_bounded + gsp_magnitude_gauss_composition_signed_prefix_entry = h) /\ ((gsp_sign_gauss_composition_signed_prefix_entry = 0 \/ gsp_sign_gauss_composition_signed_prefix_entry = 1) /\ (((gsp_sign_gauss_composition_signed_prefix_entry = 0 /\ (exists gsp_mod_left_gauss_composition_signed_prefix_entry_lower gsp_mod_right_gauss_composition_signed_prefix_entry_lower. (a * gsp_value_gauss_composition_signed_prefix_entry) + p * gsp_mod_left_gauss_composition_signed_prefix_entry_lower = (gsp_magnitude_gauss_composition_signed_prefix_entry) + p * gsp_mod_right_gauss_composition_signed_prefix_entry_lower)) \/ (gsp_sign_gauss_composition_signed_prefix_entry = 1 /\ (exists gsp_mod_left_gauss_composition_signed_prefix_entry_reflected gsp_mod_right_gauss_composition_signed_prefix_entry_reflected. (a * gsp_value_gauss_composition_signed_prefix_entry) + p * gsp_mod_left_gauss_composition_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_gauss_composition_signed_prefix_entry) + p * gsp_mod_right_gauss_composition_signed_prefix_entry_reflected))))))))))) -> (forall gspf_index_gauss_composition_sign_factors gspf_bit_gauss_composition_sign_factors. (exists gsp_lt_gap_gauss_composition_sign_factors_bound. gsp_lt_gap_gauss_composition_sign_factors_bound + S gspf_index_gauss_composition_sign_factors = h) -> (((exists ff_h_gspf_gauss_composition_sign_factors_bit. ff_h_gspf_gauss_composition_sign_factors_bit + S (gspf_bit_gauss_composition_sign_factors) = S ((S (gspf_index_gauss_composition_sign_factors)) * sc)) /\ exists ff_q_gspf_gauss_composition_sign_factors_bit. sb = ff_q_gspf_gauss_composition_sign_factors_bit * S ((S (gspf_index_gauss_composition_sign_factors)) * sc) + (gspf_bit_gauss_composition_sign_factors))) -> (((gspf_bit_gauss_composition_sign_factors = 0) /\ (((exists gsp_beta_height_gspf_gauss_composition_sign_factors_one. gsp_beta_height_gspf_gauss_composition_sign_factors_one + S (1) = S ((S (gspf_index_gauss_composition_sign_factors)) * fc)) /\ exists gsp_beta_quotient_gspf_gauss_composition_sign_factors_one. fb = gsp_beta_quotient_gspf_gauss_composition_sign_factors_one * S ((S (gspf_index_gauss_composition_sign_factors)) * fc) + (1)))) \/ ((gspf_bit_gauss_composition_sign_factors = 1) /\ (((exists ff_h_gspf_gauss_composition_sign_factors_predecessor. ff_h_gspf_gauss_composition_sign_factors_predecessor + S (r) = S ((S (gspf_index_gauss_composition_sign_factors)) * fc)) /\ exists ff_q_gspf_gauss_composition_sign_factors_predecessor. fb = ff_q_gspf_gauss_composition_sign_factors_predecessor * S ((S (gspf_index_gauss_composition_sign_factors)) * fc) + (r)))))) -> (forall fpmp_index_gauss_composition_pointwise_products fpmp_left_gauss_composition_pointwise_products fpmp_right_gauss_composition_pointwise_products fpmp_target_gauss_composition_pointwise_products. (exists fpmp_gap_gauss_composition_pointwise_products. fpmp_gap_gauss_composition_pointwise_products + S fpmp_index_gauss_composition_pointwise_products = h) -> (((exists ff_h_fpmp_gauss_composition_pointwise_products_left. ff_h_fpmp_gauss_composition_pointwise_products_left + S (fpmp_left_gauss_composition_pointwise_products) = S ((S (fpmp_index_gauss_composition_pointwise_products)) * mc)) /\ exists ff_q_fpmp_gauss_composition_pointwise_products_left. mb = ff_q_fpmp_gauss_composition_pointwise_products_left * S ((S (fpmp_index_gauss_composition_pointwise_products)) * mc) + (fpmp_left_gauss_composition_pointwise_products))) -> (((exists ff_h_fpmp_gauss_composition_pointwise_products_right. ff_h_fpmp_gauss_composition_pointwise_products_right + S (fpmp_right_gauss_composition_pointwise_products) = S ((S (fpmp_index_gauss_composition_pointwise_products)) * fc)) /\ exists ff_q_fpmp_gauss_composition_pointwise_products_right. fb = ff_q_fpmp_gauss_composition_pointwise_products_right * S ((S (fpmp_index_gauss_composition_pointwise_products)) * fc) + (fpmp_right_gauss_composition_pointwise_products))) -> (((exists ff_h_fpmp_gauss_composition_pointwise_products_target. ff_h_fpmp_gauss_composition_pointwise_products_target + S (fpmp_target_gauss_composition_pointwise_products) = S ((S (fpmp_index_gauss_composition_pointwise_products)) * tc)) /\ exists ff_q_fpmp_gauss_composition_pointwise_products_target. tb = ff_q_fpmp_gauss_composition_pointwise_products_target * S ((S (fpmp_index_gauss_composition_pointwise_products)) * tc) + (fpmp_target_gauss_composition_pointwise_products))) -> fpmp_target_gauss_composition_pointwise_products = fpmp_left_gauss_composition_pointwise_products * fpmp_right_gauss_composition_pointwise_products) -> (forall gmp_index_gauss_composition_magnitude_range. (exists gsp_lt_gap_gauss_composition_magnitude_range_index_bound. gsp_lt_gap_gauss_composition_magnitude_range_index_bound + S gmp_index_gauss_composition_magnitude_range = h) -> exists gmp_magnitude_gauss_composition_magnitude_range. ((((exists ff_h_gmp_gauss_composition_magnitude_range_decoded. ff_h_gmp_gauss_composition_magnitude_range_decoded + S (gmp_magnitude_gauss_composition_magnitude_range) = S ((S (gmp_index_gauss_composition_magnitude_range)) * mc)) /\ exists ff_q_gmp_gauss_composition_magnitude_range_decoded. mb = ff_q_gmp_gauss_composition_magnitude_range_decoded * S ((S (gmp_index_gauss_composition_magnitude_range)) * mc) + (gmp_magnitude_gauss_composition_magnitude_range))) /\ ((exists gsp_lt_gap_gauss_composition_magnitude_range_positive. gsp_lt_gap_gauss_composition_magnitude_range_positive + S 0 = gmp_magnitude_gauss_composition_magnitude_range) /\ (exists gsp_le_gap_gauss_composition_magnitude_range_bounded. gsp_le_gap_gauss_composition_magnitude_range_bounded + gmp_magnitude_gauss_composition_magnitude_range = h)))) -> (forall fp_i_gauss_composition_magnitude_injective fp_j_gauss_composition_magnitude_injective fp_value_gauss_composition_magnitude_injective. (exists fp_gap_gauss_composition_magnitude_injective_i. fp_gap_gauss_composition_magnitude_injective_i + S fp_i_gauss_composition_magnitude_injective = h) -> (exists fp_gap_gauss_composition_magnitude_injective_j. fp_gap_gauss_composition_magnitude_injective_j + S fp_j_gauss_composition_magnitude_injective = h) -> (((exists ff_h_gauss_composition_magnitude_injective_left. ff_h_gauss_composition_magnitude_injective_left + S (fp_value_gauss_composition_magnitude_injective) = S ((S (fp_i_gauss_composition_magnitude_injective)) * mc)) /\ exists ff_q_gauss_composition_magnitude_injective_left. mb = ff_q_gauss_composition_magnitude_injective_left * S ((S (fp_i_gauss_composition_magnitude_injective)) * mc) + (fp_value_gauss_composition_magnitude_injective))) -> (((exists ff_h_gauss_composition_magnitude_injective_right. ff_h_gauss_composition_magnitude_injective_right + S (fp_value_gauss_composition_magnitude_injective) = S ((S (fp_j_gauss_composition_magnitude_injective)) * mc)) /\ exists ff_q_gauss_composition_magnitude_injective_right. mb = ff_q_gauss_composition_magnitude_injective_right * S ((S (fp_j_gauss_composition_magnitude_injective)) * mc) + (fp_value_gauss_composition_magnitude_injective))) -> fp_i_gauss_composition_magnitude_injective = fp_j_gauss_composition_magnitude_injective) -> (forall gmp_index_gauss_composition_predecessor_recode gmp_predecessor_gauss_composition_predecessor_recode. (exists gsp_lt_gap_gauss_composition_predecessor_recode_index_bound. gsp_lt_gap_gauss_composition_predecessor_recode_index_bound + S gmp_index_gauss_composition_predecessor_recode = h) -> (((exists gsp_beta_height_gmp_gauss_composition_predecessor_recode_source. gsp_beta_height_gmp_gauss_composition_predecessor_recode_source + S (S gmp_predecessor_gauss_composition_predecessor_recode) = S ((S (gmp_index_gauss_composition_predecessor_recode)) * mc)) /\ exists gsp_beta_quotient_gmp_gauss_composition_predecessor_recode_source. mb = gsp_beta_quotient_gmp_gauss_composition_predecessor_recode_source * S ((S (gmp_index_gauss_composition_predecessor_recode)) * mc) + (S gmp_predecessor_gauss_composition_predecessor_recode))) -> (((exists ff_h_gmp_gauss_composition_predecessor_recode_target. ff_h_gmp_gauss_composition_predecessor_recode_target + S (gmp_predecessor_gauss_composition_predecessor_recode) = S ((S (gmp_index_gauss_composition_predecessor_recode)) * rc)) /\ exists ff_q_gmp_gauss_composition_predecessor_recode_target. rb = ff_q_gmp_gauss_composition_predecessor_recode_target * S ((S (gmp_index_gauss_composition_predecessor_recode)) * rc) + (gmp_predecessor_gauss_composition_predecessor_recode)))) -> (forall gsp_range_index_gauss_composition_half_range. (exists gsp_lt_gap_gauss_composition_half_range_range_bound. gsp_lt_gap_gauss_composition_half_range_range_bound + S gsp_range_index_gauss_composition_half_range = h) -> (((exists gsp_beta_height_gauss_composition_half_range_range_entry. gsp_beta_height_gauss_composition_half_range_range_entry + S (1 + gsp_range_index_gauss_composition_half_range) = S ((S (gsp_range_index_gauss_composition_half_range)) * c)) /\ exists gsp_beta_quotient_gauss_composition_half_range_range_entry. b = gsp_beta_quotient_gauss_composition_half_range_range_entry * S ((S (gsp_range_index_gauss_composition_half_range)) * c) + (1 + gsp_range_index_gauss_composition_half_range)))) -> (((exists ff_u_gauss_composition_sign_count_sum ff_v_gauss_composition_sign_count_sum. ((((exists ff_h_gauss_composition_sign_count_sum_start. ff_h_gauss_composition_sign_count_sum_start + S (0) = S ((S (0)) * ff_v_gauss_composition_sign_count_sum)) /\ exists ff_q_gauss_composition_sign_count_sum_start. ff_u_gauss_composition_sign_count_sum = ff_q_gauss_composition_sign_count_sum_start * S ((S (0)) * ff_v_gauss_composition_sign_count_sum) + (0))) /\ ((((exists ff_h_gauss_composition_sign_count_sum_terminal. ff_h_gauss_composition_sign_count_sum_terminal + S (e) = S ((S (h)) * ff_v_gauss_composition_sign_count_sum)) /\ exists ff_q_gauss_composition_sign_count_sum_terminal. ff_u_gauss_composition_sign_count_sum = ff_q_gauss_composition_sign_count_sum_terminal * S ((S (h)) * ff_v_gauss_composition_sign_count_sum) + (e))) /\ forall ff_i_gauss_composition_sign_count_sum. (exists ff_lt_gauss_composition_sign_count_sum_bound. ff_lt_gauss_composition_sign_count_sum_bound + S ff_i_gauss_composition_sign_count_sum = h) -> exists ff_a_gauss_composition_sign_count_sum ff_r_gauss_composition_sign_count_sum ff_s_gauss_composition_sign_count_sum. ((((exists ff_h_gauss_composition_sign_count_sum_summand. ff_h_gauss_composition_sign_count_sum_summand + S (ff_a_gauss_composition_sign_count_sum) = S ((S (ff_i_gauss_composition_sign_count_sum)) * sc)) /\ exists ff_q_gauss_composition_sign_count_sum_summand. sb = ff_q_gauss_composition_sign_count_sum_summand * S ((S (ff_i_gauss_composition_sign_count_sum)) * sc) + (ff_a_gauss_composition_sign_count_sum))) /\ ((((exists ff_h_gauss_composition_sign_count_sum_partial. ff_h_gauss_composition_sign_count_sum_partial + S (ff_r_gauss_composition_sign_count_sum) = S ((S (ff_i_gauss_composition_sign_count_sum)) * ff_v_gauss_composition_sign_count_sum)) /\ exists ff_q_gauss_composition_sign_count_sum_partial. ff_u_gauss_composition_sign_count_sum = ff_q_gauss_composition_sign_count_sum_partial * S ((S (ff_i_gauss_composition_sign_count_sum)) * ff_v_gauss_composition_sign_count_sum) + (ff_r_gauss_composition_sign_count_sum))) /\ ((((exists ff_h_gauss_composition_sign_count_sum_successor. ff_h_gauss_composition_sign_count_sum_successor + S (ff_s_gauss_composition_sign_count_sum) = S ((S (S ff_i_gauss_composition_sign_count_sum)) * ff_v_gauss_composition_sign_count_sum)) /\ exists ff_q_gauss_composition_sign_count_sum_successor. ff_u_gauss_composition_sign_count_sum = ff_q_gauss_composition_sign_count_sum_successor * S ((S (S ff_i_gauss_composition_sign_count_sum)) * ff_v_gauss_composition_sign_count_sum) + (ff_s_gauss_composition_sign_count_sum))) /\ ff_s_gauss_composition_sign_count_sum = ff_r_gauss_composition_sign_count_sum + ff_a_gauss_composition_sign_count_sum)))))) /\ (forall ff_i_gauss_composition_sign_count_bits. (exists ff_lt_gauss_composition_sign_count_bits_bound. ff_lt_gauss_composition_sign_count_bits_bound + S ff_i_gauss_composition_sign_count_bits = h) -> exists ff_bit_gauss_composition_sign_count_bits. ((((exists ff_h_gauss_composition_sign_count_bits_decoded. ff_h_gauss_composition_sign_count_bits_decoded + S (ff_bit_gauss_composition_sign_count_bits) = S ((S (ff_i_gauss_composition_sign_count_bits)) * sc)) /\ exists ff_q_gauss_composition_sign_count_bits_decoded. sb = ff_q_gauss_composition_sign_count_bits_decoded * S ((S (ff_i_gauss_composition_sign_count_bits)) * sc) + (ff_bit_gauss_composition_sign_count_bits))) /\ (ff_bit_gauss_composition_sign_count_bits = 0 \/ ff_bit_gauss_composition_sign_count_bits = 1))))) -> (exists ff_u_gauss_composition_canonical_product ff_v_gauss_composition_canonical_product. ((((exists ff_h_gauss_composition_canonical_product_start. ff_h_gauss_composition_canonical_product_start + S (1) = S ((S (0)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_start. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_start * S ((S (0)) * ff_v_gauss_composition_canonical_product) + (1))) /\ ((((exists ff_h_gauss_composition_canonical_product_terminal. ff_h_gauss_composition_canonical_product_terminal + S (P) = S ((S (h)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_terminal. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_terminal * S ((S (h)) * ff_v_gauss_composition_canonical_product) + (P))) /\ forall ff_i_gauss_composition_canonical_product. (exists ff_lt_gauss_composition_canonical_product_bound. ff_lt_gauss_composition_canonical_product_bound + S ff_i_gauss_composition_canonical_product = h) -> exists ff_p_gauss_composition_canonical_product ff_r_gauss_composition_canonical_product ff_s_gauss_composition_canonical_product. ((((exists ff_h_gauss_composition_canonical_product_factor. ff_h_gauss_composition_canonical_product_factor + S (ff_p_gauss_composition_canonical_product) = S ((S (ff_i_gauss_composition_canonical_product)) * c)) /\ exists ff_q_gauss_composition_canonical_product_factor. b = ff_q_gauss_composition_canonical_product_factor * S ((S (ff_i_gauss_composition_canonical_product)) * c) + (ff_p_gauss_composition_canonical_product))) /\ ((((exists ff_h_gauss_composition_canonical_product_partial. ff_h_gauss_composition_canonical_product_partial + S (ff_r_gauss_composition_canonical_product) = S ((S (ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_partial. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_partial * S ((S (ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product) + (ff_r_gauss_composition_canonical_product))) /\ ((((exists ff_h_gauss_composition_canonical_product_successor. ff_h_gauss_composition_canonical_product_successor + S (ff_s_gauss_composition_canonical_product) = S ((S (S ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_successor. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_successor * S ((S (S ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product) + (ff_s_gauss_composition_canonical_product))) /\ ff_s_gauss_composition_canonical_product = ff_r_gauss_composition_canonical_product * ff_p_gauss_composition_canonical_product)))))) -> (exists ff_u_gauss_composition_magnitude_product ff_v_gauss_composition_magnitude_product. ((((exists ff_h_gauss_composition_magnitude_product_start. ff_h_gauss_composition_magnitude_product_start + S (1) = S ((S (0)) * ff_v_gauss_composition_magnitude_product)) /\ exists ff_q_gauss_composition_magnitude_product_start. ff_u_gauss_composition_magnitude_product = ff_q_gauss_composition_magnitude_product_start * S ((S (0)) * ff_v_gauss_composition_magnitude_product) + (1))) /\ ((((exists ff_h_gauss_composition_magnitude_product_terminal. ff_h_gauss_composition_magnitude_product_terminal + S (M) = S ((S (h)) * ff_v_gauss_composition_magnitude_product)) /\ exists ff_q_gauss_composition_magnitude_product_terminal. ff_u_gauss_composition_magnitude_product = ff_q_gauss_composition_magnitude_product_terminal * S ((S (h)) * ff_v_gauss_composition_magnitude_product) + (M))) /\ forall ff_i_gauss_composition_magnitude_product. (exists ff_lt_gauss_composition_magnitude_product_bound. ff_lt_gauss_composition_magnitude_product_bound + S ff_i_gauss_composition_magnitude_product = h) -> exists ff_p_gauss_composition_magnitude_product ff_r_gauss_composition_magnitude_product ff_s_gauss_composition_magnitude_product. ((((exists ff_h_gauss_composition_magnitude_product_factor. ff_h_gauss_composition_magnitude_product_factor + S (ff_p_gauss_composition_magnitude_product) = S ((S (ff_i_gauss_composition_magnitude_product)) * mc)) /\ exists ff_q_gauss_composition_magnitude_product_factor. mb = ff_q_gauss_composition_magnitude_product_factor * S ((S (ff_i_gauss_composition_magnitude_product)) * mc) + (ff_p_gauss_composition_magnitude_product))) /\ ((((exists ff_h_gauss_composition_magnitude_product_partial. ff_h_gauss_composition_magnitude_product_partial + S (ff_r_gauss_composition_magnitude_product) = S ((S (ff_i_gauss_composition_magnitude_product)) * ff_v_gauss_composition_magnitude_product)) /\ exists ff_q_gauss_composition_magnitude_product_partial. ff_u_gauss_composition_magnitude_product = ff_q_gauss_composition_magnitude_product_partial * S ((S (ff_i_gauss_composition_magnitude_product)) * ff_v_gauss_composition_magnitude_product) + (ff_r_gauss_composition_magnitude_product))) /\ ((((exists ff_h_gauss_composition_magnitude_product_successor. ff_h_gauss_composition_magnitude_product_successor + S (ff_s_gauss_composition_magnitude_product) = S ((S (S ff_i_gauss_composition_magnitude_product)) * ff_v_gauss_composition_magnitude_product)) /\ exists ff_q_gauss_composition_magnitude_product_successor. ff_u_gauss_composition_magnitude_product = ff_q_gauss_composition_magnitude_product_successor * S ((S (S ff_i_gauss_composition_magnitude_product)) * ff_v_gauss_composition_magnitude_product) + (ff_s_gauss_composition_magnitude_product))) /\ ff_s_gauss_composition_magnitude_product = ff_r_gauss_composition_magnitude_product * ff_p_gauss_composition_magnitude_product)))))) -> (exists ff_u_gauss_composition_sign_product ff_v_gauss_composition_sign_product. ((((exists ff_h_gauss_composition_sign_product_start. ff_h_gauss_composition_sign_product_start + S (1) = S ((S (0)) * ff_v_gauss_composition_sign_product)) /\ exists ff_q_gauss_composition_sign_product_start. ff_u_gauss_composition_sign_product = ff_q_gauss_composition_sign_product_start * S ((S (0)) * ff_v_gauss_composition_sign_product) + (1))) /\ ((((exists ff_h_gauss_composition_sign_product_terminal. ff_h_gauss_composition_sign_product_terminal + S (Sprod) = S ((S (h)) * ff_v_gauss_composition_sign_product)) /\ exists ff_q_gauss_composition_sign_product_terminal. ff_u_gauss_composition_sign_product = ff_q_gauss_composition_sign_product_terminal * S ((S (h)) * ff_v_gauss_composition_sign_product) + (Sprod))) /\ forall ff_i_gauss_composition_sign_product. (exists ff_lt_gauss_composition_sign_product_bound. ff_lt_gauss_composition_sign_product_bound + S ff_i_gauss_composition_sign_product = h) -> exists ff_p_gauss_composition_sign_product ff_r_gauss_composition_sign_product ff_s_gauss_composition_sign_product. ((((exists ff_h_gauss_composition_sign_product_factor. ff_h_gauss_composition_sign_product_factor + S (ff_p_gauss_composition_sign_product) = S ((S (ff_i_gauss_composition_sign_product)) * fc)) /\ exists ff_q_gauss_composition_sign_product_factor. fb = ff_q_gauss_composition_sign_product_factor * S ((S (ff_i_gauss_composition_sign_product)) * fc) + (ff_p_gauss_composition_sign_product))) /\ ((((exists ff_h_gauss_composition_sign_product_partial. ff_h_gauss_composition_sign_product_partial + S (ff_r_gauss_composition_sign_product) = S ((S (ff_i_gauss_composition_sign_product)) * ff_v_gauss_composition_sign_product)) /\ exists ff_q_gauss_composition_sign_product_partial. ff_u_gauss_composition_sign_product = ff_q_gauss_composition_sign_product_partial * S ((S (ff_i_gauss_composition_sign_product)) * ff_v_gauss_composition_sign_product) + (ff_r_gauss_composition_sign_product))) /\ ((((exists ff_h_gauss_composition_sign_product_successor. ff_h_gauss_composition_sign_product_successor + S (ff_s_gauss_composition_sign_product) = S ((S (S ff_i_gauss_composition_sign_product)) * ff_v_gauss_composition_sign_product)) /\ exists ff_q_gauss_composition_sign_product_successor. ff_u_gauss_composition_sign_product = ff_q_gauss_composition_sign_product_successor * S ((S (S ff_i_gauss_composition_sign_product)) * ff_v_gauss_composition_sign_product) + (ff_s_gauss_composition_sign_product))) /\ ff_s_gauss_composition_sign_product = ff_r_gauss_composition_sign_product * ff_p_gauss_composition_sign_product)))))) -> (exists ff_u_gauss_composition_target_product ff_v_gauss_composition_target_product. ((((exists ff_h_gauss_composition_target_product_start. ff_h_gauss_composition_target_product_start + S (1) = S ((S (0)) * ff_v_gauss_composition_target_product)) /\ exists ff_q_gauss_composition_target_product_start. ff_u_gauss_composition_target_product = ff_q_gauss_composition_target_product_start * S ((S (0)) * ff_v_gauss_composition_target_product) + (1))) /\ ((((exists ff_h_gauss_composition_target_product_terminal. ff_h_gauss_composition_target_product_terminal + S (T) = S ((S (h)) * ff_v_gauss_composition_target_product)) /\ exists ff_q_gauss_composition_target_product_terminal. ff_u_gauss_composition_target_product = ff_q_gauss_composition_target_product_terminal * S ((S (h)) * ff_v_gauss_composition_target_product) + (T))) /\ forall ff_i_gauss_composition_target_product. (exists ff_lt_gauss_composition_target_product_bound. ff_lt_gauss_composition_target_product_bound + S ff_i_gauss_composition_target_product = h) -> exists ff_p_gauss_composition_target_product ff_r_gauss_composition_target_product ff_s_gauss_composition_target_product. ((((exists ff_h_gauss_composition_target_product_factor. ff_h_gauss_composition_target_product_factor + S (ff_p_gauss_composition_target_product) = S ((S (ff_i_gauss_composition_target_product)) * tc)) /\ exists ff_q_gauss_composition_target_product_factor. tb = ff_q_gauss_composition_target_product_factor * S ((S (ff_i_gauss_composition_target_product)) * tc) + (ff_p_gauss_composition_target_product))) /\ ((((exists ff_h_gauss_composition_target_product_partial. ff_h_gauss_composition_target_product_partial + S (ff_r_gauss_composition_target_product) = S ((S (ff_i_gauss_composition_target_product)) * ff_v_gauss_composition_target_product)) /\ exists ff_q_gauss_composition_target_product_partial. ff_u_gauss_composition_target_product = ff_q_gauss_composition_target_product_partial * S ((S (ff_i_gauss_composition_target_product)) * ff_v_gauss_composition_target_product) + (ff_r_gauss_composition_target_product))) /\ ((((exists ff_h_gauss_composition_target_product_successor. ff_h_gauss_composition_target_product_successor + S (ff_s_gauss_composition_target_product) = S ((S (S ff_i_gauss_composition_target_product)) * ff_v_gauss_composition_target_product)) /\ exists ff_q_gauss_composition_target_product_successor. ff_u_gauss_composition_target_product = ff_q_gauss_composition_target_product_successor * S ((S (S ff_i_gauss_composition_target_product)) * ff_v_gauss_composition_target_product) + (ff_s_gauss_composition_target_product))) /\ ff_s_gauss_composition_target_product = ff_r_gauss_composition_target_product * ff_p_gauss_composition_target_product)))))) -> (exists ff_b_gauss_composition_multiplier_power ff_c_gauss_composition_multiplier_power. ((forall ff_i_gauss_composition_multiplier_power_repeat. (exists ff_lt_gauss_composition_multiplier_power_repeat_bound. ff_lt_gauss_composition_multiplier_power_repeat_bound + S ff_i_gauss_composition_multiplier_power_repeat = h) -> (((exists ff_h_gauss_composition_multiplier_power_repeat_decoded. ff_h_gauss_composition_multiplier_power_repeat_decoded + S (a) = S ((S (ff_i_gauss_composition_multiplier_power_repeat)) * ff_c_gauss_composition_multiplier_power)) /\ exists ff_q_gauss_composition_multiplier_power_repeat_decoded. ff_b_gauss_composition_multiplier_power = ff_q_gauss_composition_multiplier_power_repeat_decoded * S ((S (ff_i_gauss_composition_multiplier_power_repeat)) * ff_c_gauss_composition_multiplier_power) + (a)))) /\ (exists ff_u_gauss_composition_multiplier_power_product ff_v_gauss_composition_multiplier_power_product. ((((exists ff_h_gauss_composition_multiplier_power_product_start. ff_h_gauss_composition_multiplier_power_product_start + S (1) = S ((S (0)) * ff_v_gauss_composition_multiplier_power_product)) /\ exists ff_q_gauss_composition_multiplier_power_product_start. ff_u_gauss_composition_multiplier_power_product = ff_q_gauss_composition_multiplier_power_product_start * S ((S (0)) * ff_v_gauss_composition_multiplier_power_product) + (1))) /\ ((((exists ff_h_gauss_composition_multiplier_power_product_terminal. ff_h_gauss_composition_multiplier_power_product_terminal + S (A) = S ((S (h)) * ff_v_gauss_composition_multiplier_power_product)) /\ exists ff_q_gauss_composition_multiplier_power_product_terminal. ff_u_gauss_composition_multiplier_power_product = ff_q_gauss_composition_multiplier_power_product_terminal * S ((S (h)) * ff_v_gauss_composition_multiplier_power_product) + (A))) /\ forall ff_i_gauss_composition_multiplier_power_product. (exists ff_lt_gauss_composition_multiplier_power_product_bound. ff_lt_gauss_composition_multiplier_power_product_bound + S ff_i_gauss_composition_multiplier_power_product = h) -> exists ff_p_gauss_composition_multiplier_power_product ff_r_gauss_composition_multiplier_power_product ff_s_gauss_composition_multiplier_power_product. ((((exists ff_h_gauss_composition_multiplier_power_product_factor. ff_h_gauss_composition_multiplier_power_product_factor + S (ff_p_gauss_composition_multiplier_power_product) = S ((S (ff_i_gauss_composition_multiplier_power_product)) * ff_c_gauss_composition_multiplier_power)) /\ exists ff_q_gauss_composition_multiplier_power_product_factor. ff_b_gauss_composition_multiplier_power = ff_q_gauss_composition_multiplier_power_product_factor * S ((S (ff_i_gauss_composition_multiplier_power_product)) * ff_c_gauss_composition_multiplier_power) + (ff_p_gauss_composition_multiplier_power_product))) /\ ((((exists ff_h_gauss_composition_multiplier_power_product_partial. ff_h_gauss_composition_multiplier_power_product_partial + S (ff_r_gauss_composition_multiplier_power_product) = S ((S (ff_i_gauss_composition_multiplier_power_product)) * ff_v_gauss_composition_multiplier_power_product)) /\ exists ff_q_gauss_composition_multiplier_power_product_partial. ff_u_gauss_composition_multiplier_power_product = ff_q_gauss_composition_multiplier_power_product_partial * S ((S (ff_i_gauss_composition_multiplier_power_product)) * ff_v_gauss_composition_multiplier_power_product) + (ff_r_gauss_composition_multiplier_power_product))) /\ ((((exists ff_h_gauss_composition_multiplier_power_product_successor. ff_h_gauss_composition_multiplier_power_product_successor + S (ff_s_gauss_composition_multiplier_power_product) = S ((S (S ff_i_gauss_composition_multiplier_power_product)) * ff_v_gauss_composition_multiplier_power_product)) /\ exists ff_q_gauss_composition_multiplier_power_product_successor. ff_u_gauss_composition_multiplier_power_product = ff_q_gauss_composition_multiplier_power_product_successor * S ((S (S ff_i_gauss_composition_multiplier_power_product)) * ff_v_gauss_composition_multiplier_power_product) + (ff_s_gauss_composition_multiplier_power_product))) /\ ff_s_gauss_composition_multiplier_power_product = ff_r_gauss_composition_multiplier_power_product * ff_p_gauss_composition_multiplier_power_product)))))))) -> (exists ff_b_gauss_composition_sign_power ff_c_gauss_composition_sign_power. ((forall ff_i_gauss_composition_sign_power_repeat. (exists ff_lt_gauss_composition_sign_power_repeat_bound. ff_lt_gauss_composition_sign_power_repeat_bound + S ff_i_gauss_composition_sign_power_repeat = e) -> (((exists ff_h_gauss_composition_sign_power_repeat_decoded. ff_h_gauss_composition_sign_power_repeat_decoded + S (r) = S ((S (ff_i_gauss_composition_sign_power_repeat)) * ff_c_gauss_composition_sign_power)) /\ exists ff_q_gauss_composition_sign_power_repeat_decoded. ff_b_gauss_composition_sign_power = ff_q_gauss_composition_sign_power_repeat_decoded * S ((S (ff_i_gauss_composition_sign_power_repeat)) * ff_c_gauss_composition_sign_power) + (r)))) /\ (exists ff_u_gauss_composition_sign_power_product ff_v_gauss_composition_sign_power_product. ((((exists ff_h_gauss_composition_sign_power_product_start. ff_h_gauss_composition_sign_power_product_start + S (1) = S ((S (0)) * ff_v_gauss_composition_sign_power_product)) /\ exists ff_q_gauss_composition_sign_power_product_start. ff_u_gauss_composition_sign_power_product = ff_q_gauss_composition_sign_power_product_start * S ((S (0)) * ff_v_gauss_composition_sign_power_product) + (1))) /\ ((((exists ff_h_gauss_composition_sign_power_product_terminal. ff_h_gauss_composition_sign_power_product_terminal + S (R) = S ((S (e)) * ff_v_gauss_composition_sign_power_product)) /\ exists ff_q_gauss_composition_sign_power_product_terminal. ff_u_gauss_composition_sign_power_product = ff_q_gauss_composition_sign_power_product_terminal * S ((S (e)) * ff_v_gauss_composition_sign_power_product) + (R))) /\ forall ff_i_gauss_composition_sign_power_product. (exists ff_lt_gauss_composition_sign_power_product_bound. ff_lt_gauss_composition_sign_power_product_bound + S ff_i_gauss_composition_sign_power_product = e) -> exists ff_p_gauss_composition_sign_power_product ff_r_gauss_composition_sign_power_product ff_s_gauss_composition_sign_power_product. ((((exists ff_h_gauss_composition_sign_power_product_factor. ff_h_gauss_composition_sign_power_product_factor + S (ff_p_gauss_composition_sign_power_product) = S ((S (ff_i_gauss_composition_sign_power_product)) * ff_c_gauss_composition_sign_power)) /\ exists ff_q_gauss_composition_sign_power_product_factor. ff_b_gauss_composition_sign_power = ff_q_gauss_composition_sign_power_product_factor * S ((S (ff_i_gauss_composition_sign_power_product)) * ff_c_gauss_composition_sign_power) + (ff_p_gauss_composition_sign_power_product))) /\ ((((exists ff_h_gauss_composition_sign_power_product_partial. ff_h_gauss_composition_sign_power_product_partial + S (ff_r_gauss_composition_sign_power_product) = S ((S (ff_i_gauss_composition_sign_power_product)) * ff_v_gauss_composition_sign_power_product)) /\ exists ff_q_gauss_composition_sign_power_product_partial. ff_u_gauss_composition_sign_power_product = ff_q_gauss_composition_sign_power_product_partial * S ((S (ff_i_gauss_composition_sign_power_product)) * ff_v_gauss_composition_sign_power_product) + (ff_r_gauss_composition_sign_power_product))) /\ ((((exists ff_h_gauss_composition_sign_power_product_successor. ff_h_gauss_composition_sign_power_product_successor + S (ff_s_gauss_composition_sign_power_product) = S ((S (S ff_i_gauss_composition_sign_power_product)) * ff_v_gauss_composition_sign_power_product)) /\ exists ff_q_gauss_composition_sign_power_product_successor. ff_u_gauss_composition_sign_power_product = ff_q_gauss_composition_sign_power_product_successor * S ((S (S ff_i_gauss_composition_sign_power_product)) * ff_v_gauss_composition_sign_power_product) + (ff_s_gauss_composition_sign_power_product))) /\ ff_s_gauss_composition_sign_power_product = ff_r_gauss_composition_sign_power_product * ff_p_gauss_composition_sign_power_product)))))))) -> (exists gpc_left_product_balance gpc_right_product_balance. A * P + p * gpc_left_product_balance = P * R + p * gpc_right_product_balance)