beta_sign_factor_product_power_exists

Exact expanded PA statement

forall p r sb sc l e. p = S r -> (((exists ff_u_recode_count_sum ff_v_recode_count_sum. ((((exists ff_h_recode_count_sum_start. ff_h_recode_count_sum_start + S (0) = S ((S (0)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_start. ff_u_recode_count_sum = ff_q_recode_count_sum_start * S ((S (0)) * ff_v_recode_count_sum) + (0))) /\ ((((exists ff_h_recode_count_sum_terminal. ff_h_recode_count_sum_terminal + S (e) = S ((S (l)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_terminal. ff_u_recode_count_sum = ff_q_recode_count_sum_terminal * S ((S (l)) * ff_v_recode_count_sum) + (e))) /\ forall ff_i_recode_count_sum. (exists ff_lt_recode_count_sum_bound. ff_lt_recode_count_sum_bound + S ff_i_recode_count_sum = l) -> exists ff_a_recode_count_sum ff_r_recode_count_sum ff_s_recode_count_sum. ((((exists ff_h_recode_count_sum_summand. ff_h_recode_count_sum_summand + S (ff_a_recode_count_sum) = S ((S (ff_i_recode_count_sum)) * sc)) /\ exists ff_q_recode_count_sum_summand. sb = ff_q_recode_count_sum_summand * S ((S (ff_i_recode_count_sum)) * sc) + (ff_a_recode_count_sum))) /\ ((((exists ff_h_recode_count_sum_partial. ff_h_recode_count_sum_partial + S (ff_r_recode_count_sum) = S ((S (ff_i_recode_count_sum)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_partial. ff_u_recode_count_sum = ff_q_recode_count_sum_partial * S ((S (ff_i_recode_count_sum)) * ff_v_recode_count_sum) + (ff_r_recode_count_sum))) /\ ((((exists ff_h_recode_count_sum_successor. ff_h_recode_count_sum_successor + S (ff_s_recode_count_sum) = S ((S (S ff_i_recode_count_sum)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_successor. ff_u_recode_count_sum = ff_q_recode_count_sum_successor * S ((S (S ff_i_recode_count_sum)) * ff_v_recode_count_sum) + (ff_s_recode_count_sum))) /\ ff_s_recode_count_sum = ff_r_recode_count_sum + ff_a_recode_count_sum)))))) /\ (forall ff_i_recode_count_bits. (exists ff_lt_recode_count_bits_bound. ff_lt_recode_count_bits_bound + S ff_i_recode_count_bits = l) -> exists ff_bit_recode_count_bits. ((((exists ff_h_recode_count_bits_decoded. ff_h_recode_count_bits_decoded + S (ff_bit_recode_count_bits) = S ((S (ff_i_recode_count_bits)) * sc)) /\ exists ff_q_recode_count_bits_decoded. sb = ff_q_recode_count_bits_decoded * S ((S (ff_i_recode_count_bits)) * sc) + (ff_bit_recode_count_bits))) /\ (ff_bit_recode_count_bits = 0 \/ ff_bit_recode_count_bits = 1))))) -> (exists fb fc F R. ((forall gspf_index_recode_endpoint_signs gspf_bit_recode_endpoint_signs. (exists gsp_lt_gap_recode_endpoint_signs_bound. gsp_lt_gap_recode_endpoint_signs_bound + S gspf_index_recode_endpoint_signs = l) -> (((exists ff_h_gspf_recode_endpoint_signs_bit. ff_h_gspf_recode_endpoint_signs_bit + S (gspf_bit_recode_endpoint_signs) = S ((S (gspf_index_recode_endpoint_signs)) * sc)) /\ exists ff_q_gspf_recode_endpoint_signs_bit. sb = ff_q_gspf_recode_endpoint_signs_bit * S ((S (gspf_index_recode_endpoint_signs)) * sc) + (gspf_bit_recode_endpoint_signs))) -> (((gspf_bit_recode_endpoint_signs = 0) /\ (((exists gsp_beta_height_gspf_recode_endpoint_signs_one. gsp_beta_height_gspf_recode_endpoint_signs_one + S (1) = S ((S (gspf_index_recode_endpoint_signs)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_endpoint_signs_one. fb = gsp_beta_quotient_gspf_recode_endpoint_signs_one * S ((S (gspf_index_recode_endpoint_signs)) * fc) + (1)))) \/ ((gspf_bit_recode_endpoint_signs = 1) /\ (((exists ff_h_gspf_recode_endpoint_signs_predecessor. ff_h_gspf_recode_endpoint_signs_predecessor + S (r) = S ((S (gspf_index_recode_endpoint_signs)) * fc)) /\ exists ff_q_gspf_recode_endpoint_signs_predecessor. fb = ff_q_gspf_recode_endpoint_signs_predecessor * S ((S (gspf_index_recode_endpoint_signs)) * fc) + (r)))))) /\ ((exists ff_u_recode_endpoint_product ff_v_recode_endpoint_product. ((((exists ff_h_recode_endpoint_product_start. ff_h_recode_endpoint_product_start + S (1) = S ((S (0)) * ff_v_recode_endpoint_product)) /\ exists ff_q_recode_endpoint_product_start. ff_u_recode_endpoint_product = ff_q_recode_endpoint_product_start * S ((S (0)) * ff_v_recode_endpoint_product) + (1))) /\ ((((exists ff_h_recode_endpoint_product_terminal. ff_h_recode_endpoint_product_terminal + S (F) = S ((S (l)) * ff_v_recode_endpoint_product)) /\ exists ff_q_recode_endpoint_product_terminal. ff_u_recode_endpoint_product = ff_q_recode_endpoint_product_terminal * S ((S (l)) * ff_v_recode_endpoint_product) + (F))) /\ forall ff_i_recode_endpoint_product. (exists ff_lt_recode_endpoint_product_bound. ff_lt_recode_endpoint_product_bound + S ff_i_recode_endpoint_product = l) -> exists ff_p_recode_endpoint_product ff_r_recode_endpoint_product ff_s_recode_endpoint_product. ((((exists ff_h_recode_endpoint_product_factor. ff_h_recode_endpoint_product_factor + S (ff_p_recode_endpoint_product) = S ((S (ff_i_recode_endpoint_product)) * fc)) /\ exists ff_q_recode_endpoint_product_factor. fb = ff_q_recode_endpoint_product_factor * S ((S (ff_i_recode_endpoint_product)) * fc) + (ff_p_recode_endpoint_product))) /\ ((((exists ff_h_recode_endpoint_product_partial. ff_h_recode_endpoint_product_partial + S (ff_r_recode_endpoint_product) = S ((S (ff_i_recode_endpoint_product)) * ff_v_recode_endpoint_product)) /\ exists ff_q_recode_endpoint_product_partial. ff_u_recode_endpoint_product = ff_q_recode_endpoint_product_partial * S ((S (ff_i_recode_endpoint_product)) * ff_v_recode_endpoint_product) + (ff_r_recode_endpoint_product))) /\ ((((exists ff_h_recode_endpoint_product_successor. ff_h_recode_endpoint_product_successor + S (ff_s_recode_endpoint_product) = S ((S (S ff_i_recode_endpoint_product)) * ff_v_recode_endpoint_product)) /\ exists ff_q_recode_endpoint_product_successor. ff_u_recode_endpoint_product = ff_q_recode_endpoint_product_successor * S ((S (S ff_i_recode_endpoint_product)) * ff_v_recode_endpoint_product) + (ff_s_recode_endpoint_product))) /\ ff_s_recode_endpoint_product = ff_r_recode_endpoint_product * ff_p_recode_endpoint_product)))))) /\ ((exists ff_b_recode_endpoint_power ff_c_recode_endpoint_power. ((forall ff_i_recode_endpoint_power_repeat. (exists ff_lt_recode_endpoint_power_repeat_bound. ff_lt_recode_endpoint_power_repeat_bound + S ff_i_recode_endpoint_power_repeat = e) -> (((exists ff_h_recode_endpoint_power_repeat_decoded. ff_h_recode_endpoint_power_repeat_decoded + S (r) = S ((S (ff_i_recode_endpoint_power_repeat)) * ff_c_recode_endpoint_power)) /\ exists ff_q_recode_endpoint_power_repeat_decoded. ff_b_recode_endpoint_power = ff_q_recode_endpoint_power_repeat_decoded * S ((S (ff_i_recode_endpoint_power_repeat)) * ff_c_recode_endpoint_power) + (r)))) /\ (exists ff_u_recode_endpoint_power_product ff_v_recode_endpoint_power_product. ((((exists ff_h_recode_endpoint_power_product_start. ff_h_recode_endpoint_power_product_start + S (1) = S ((S (0)) * ff_v_recode_endpoint_power_product)) /\ exists ff_q_recode_endpoint_power_product_start. ff_u_recode_endpoint_power_product = ff_q_recode_endpoint_power_product_start * S ((S (0)) * ff_v_recode_endpoint_power_product) + (1))) /\ ((((exists ff_h_recode_endpoint_power_product_terminal. ff_h_recode_endpoint_power_product_terminal + S (R) = S ((S (e)) * ff_v_recode_endpoint_power_product)) /\ exists ff_q_recode_endpoint_power_product_terminal. ff_u_recode_endpoint_power_product = ff_q_recode_endpoint_power_product_terminal * S ((S (e)) * ff_v_recode_endpoint_power_product) + (R))) /\ forall ff_i_recode_endpoint_power_product. (exists ff_lt_recode_endpoint_power_product_bound. ff_lt_recode_endpoint_power_product_bound + S ff_i_recode_endpoint_power_product = e) -> exists ff_p_recode_endpoint_power_product ff_r_recode_endpoint_power_product ff_s_recode_endpoint_power_product. ((((exists ff_h_recode_endpoint_power_product_factor. ff_h_recode_endpoint_power_product_factor + S (ff_p_recode_endpoint_power_product) = S ((S (ff_i_recode_endpoint_power_product)) * ff_c_recode_endpoint_power)) /\ exists ff_q_recode_endpoint_power_product_factor. ff_b_recode_endpoint_power = ff_q_recode_endpoint_power_product_factor * S ((S (ff_i_recode_endpoint_power_product)) * ff_c_recode_endpoint_power) + (ff_p_recode_endpoint_power_product))) /\ ((((exists ff_h_recode_endpoint_power_product_partial. ff_h_recode_endpoint_power_product_partial + S (ff_r_recode_endpoint_power_product) = S ((S (ff_i_recode_endpoint_power_product)) * ff_v_recode_endpoint_power_product)) /\ exists ff_q_recode_endpoint_power_product_partial. ff_u_recode_endpoint_power_product = ff_q_recode_endpoint_power_product_partial * S ((S (ff_i_recode_endpoint_power_product)) * ff_v_recode_endpoint_power_product) + (ff_r_recode_endpoint_power_product))) /\ ((((exists ff_h_recode_endpoint_power_product_successor. ff_h_recode_endpoint_power_product_successor + S (ff_s_recode_endpoint_power_product) = S ((S (S ff_i_recode_endpoint_power_product)) * ff_v_recode_endpoint_power_product)) /\ exists ff_q_recode_endpoint_power_product_successor. ff_u_recode_endpoint_power_product = ff_q_recode_endpoint_power_product_successor * S ((S (S ff_i_recode_endpoint_power_product)) * ff_v_recode_endpoint_power_product) + (ff_s_recode_endpoint_power_product))) /\ ff_s_recode_endpoint_power_product = ff_r_recode_endpoint_power_product * ff_p_recode_endpoint_power_product)))))))) /\ F = R))))