perfect_power_profile_data_degree_classification

forall n w pb pc eb ec vb vc l g rb rc k. (((~((n) = 1)) /\ (((exists ppf_code_0_encoded_classificationcode ppf_code_1_encoded_classificationcode ppf_code_2_encoded_classificationcode ppf_code_3_encoded_classificationcode ppf_code_4_encoded_classificationcode ppf_code_5_encoded_classificationcode ppf_code_6_encoded_classificationcode ppf_code_7_encoded_classificationcode. ((((w) = ((pb) + (ppf_code_0_encoded_classificationcode)) * S ((pb) + (ppf_code_0_encoded_classificationcode)) + ((ppf_code_0_encoded_classificationcode) + (ppf_code_0_encoded_classificationcode))) /\ ((((ppf_code_0_encoded_classificationcode) = ((pc) + (ppf_code_1_encoded_classificationcode)) * S ((pc) + (ppf_code_1_encoded_classificationcode)) + ((ppf_code_1_encoded_classificationcode) + (ppf_code_1_encoded_classificationcode))) /\ ((((ppf_code_1_encoded_classificationcode) = ((eb) + (ppf_code_2_encoded_classificationcode)) * S ((eb) + (ppf_code_2_encoded_classificationcode)) + ((ppf_code_2_encoded_classificationcode) + (ppf_code_2_encoded_classificationcode))) /\ ((((ppf_code_2_encoded_classificationcode) = ((ec) + (ppf_code_3_encoded_classificationcode)) * S ((ec) + (ppf_code_3_encoded_classificationcode)) + ((ppf_code_3_encoded_classificationcode) + (ppf_code_3_encoded_classificationcode))) /\ ((((ppf_code_3_encoded_classificationcode) = ((vb) + (ppf_code_4_encoded_classificationcode)) * S ((vb) + (ppf_code_4_encoded_classificationcode)) + ((ppf_code_4_encoded_classificationcode) + (ppf_code_4_encoded_classificationcode))) /\ ((((ppf_code_4_encoded_classificationcode) = ((vc) + (ppf_code_5_encoded_classificationcode)) * S ((vc) + (ppf_code_5_encoded_classificationcode)) + ((ppf_code_5_encoded_classificationcode) + (ppf_code_5_encoded_classificationcode))) /\ ((((ppf_code_5_encoded_classificationcode) = ((l) + (ppf_code_6_encoded_classificationcode)) * S ((l) + (ppf_code_6_encoded_classificationcode)) + ((ppf_code_6_encoded_classificationcode) + (ppf_code_6_encoded_classificationcode))) /\ ((((ppf_code_6_encoded_classificationcode) = ((g) + (ppf_code_7_encoded_classificationcode)) * S ((g) + (ppf_code_7_encoded_classificationcode)) + ((ppf_code_7_encoded_classificationcode) + (ppf_code_7_encoded_classificationcode))) /\ ((ppf_code_7_encoded_classificationcode) = ((rb) + (rc)) * S ((rb) + (rc)) + ((rc) + (rc)))))))))))))))))))) /\ (((((~((n) = 0)) /\ (((forall pfp_i_pvs_encoded_classificationsupportdistinct pfp_j_pvs_encoded_classificationsupportdistinct pfp_a_pvs_encoded_classificationsupportdistinct. (exists pfp_gap_pvs_encoded_classificationsupportdistinctfirst. pfp_gap_pvs_encoded_classificationsupportdistinctfirst + S (pfp_i_pvs_encoded_classificationsupportdistinct) = (l)) -> (exists pfp_gap_pvs_encoded_classificationsupportdistinctsecond. pfp_gap_pvs_encoded_classificationsupportdistinctsecond + S (pfp_j_pvs_encoded_classificationsupportdistinct) = (l)) -> (((exists ff_h_pfp_pvs_encoded_classificationsupportdistinctleft. ff_h_pfp_pvs_encoded_classificationsupportdistinctleft + S (pfp_a_pvs_encoded_classificationsupportdistinct) = S ((S (pfp_i_pvs_encoded_classificationsupportdistinct)) * pc)) /\ exists ff_q_pfp_pvs_encoded_classificationsupportdistinctleft. pb = ff_q_pfp_pvs_encoded_classificationsupportdistinctleft * S ((S (pfp_i_pvs_encoded_classificationsupportdistinct)) * pc) + (pfp_a_pvs_encoded_classificationsupportdistinct))) -> (((exists ff_h_pfp_pvs_encoded_classificationsupportdistinctright. ff_h_pfp_pvs_encoded_classificationsupportdistinctright + S (pfp_a_pvs_encoded_classificationsupportdistinct) = S ((S (pfp_j_pvs_encoded_classificationsupportdistinct)) * pc)) /\ exists ff_q_pfp_pvs_encoded_classificationsupportdistinctright. pb = ff_q_pfp_pvs_encoded_classificationsupportdistinctright * S ((S (pfp_j_pvs_encoded_classificationsupportdistinct)) * pc) + (pfp_a_pvs_encoded_classificationsupportdistinct))) -> pfp_i_pvs_encoded_classificationsupportdistinct = pfp_j_pvs_encoded_classificationsupportdistinct) /\ (((forall pvs_index_encoded_classificationsupportentries. (exists pvs_gap_encoded_classificationsupportentriesindex. pvs_gap_encoded_classificationsupportentriesindex + S (pvs_index_encoded_classificationsupportentries) = (l)) -> exists pvs_prime_encoded_classificationsupportentries pvs_exponent_encoded_classificationsupportentries pvs_power_encoded_classificationsupportentries. (((((exists ff_h_pvs_encoded_classificationsupportentriesprime. ff_h_pvs_encoded_classificationsupportentriesprime + S (pvs_prime_encoded_classificationsupportentries) = S ((S (pvs_index_encoded_classificationsupportentries)) * pc)) /\ exists ff_q_pvs_encoded_classificationsupportentriesprime. pb = ff_q_pvs_encoded_classificationsupportentriesprime * S ((S (pvs_index_encoded_classificationsupportentries)) * pc) + (pvs_prime_encoded_classificationsupportentries))) /\ (((((exists ff_h_pvs_encoded_classificationsupportentriesexponent. ff_h_pvs_encoded_classificationsupportentriesexponent + S (pvs_exponent_encoded_classificationsupportentries) = S ((S (pvs_index_encoded_classificationsupportentries)) * ec)) /\ exists ff_q_pvs_encoded_classificationsupportentriesexponent. eb = ff_q_pvs_encoded_classificationsupportentriesexponent * S ((S (pvs_index_encoded_classificationsupportentries)) * ec) + (pvs_exponent_encoded_classificationsupportentries))) /\ (((((exists ff_h_pvs_encoded_classificationsupportentriespower. ff_h_pvs_encoded_classificationsupportentriespower + S (pvs_power_encoded_classificationsupportentries) = S ((S (pvs_index_encoded_classificationsupportentries)) * vc)) /\ exists ff_q_pvs_encoded_classificationsupportentriespower. vb = ff_q_pvs_encoded_classificationsupportentriespower * S ((S (pvs_index_encoded_classificationsupportentries)) * vc) + (pvs_power_encoded_classificationsupportentries))) /\ (((~((pvs_prime_encoded_classificationsupportentries) = 1) /\ forall pvs_left_encoded_classificationsupportentriesdomain pvs_right_encoded_classificationsupportentriesdomain. (pvs_prime_encoded_classificationsupportentries) = pvs_left_encoded_classificationsupportentriesdomain * pvs_right_encoded_classificationsupportentriesdomain -> pvs_left_encoded_classificationsupportentriesdomain = 1 \/ pvs_right_encoded_classificationsupportentriesdomain = 1) /\ (((~(pvs_exponent_encoded_classificationsupportentries = 0)) /\ (((((exists bpd_gap_pvs_encoded_classificationsupportentriesvaluation_selected_bound. bpd_gap_pvs_encoded_classificationsupportentriesvaluation_selected_bound + (pvs_exponent_encoded_classificationsupportentries) = (n)) /\ (exists bpvi_result_pvs_encoded_classificationsupportentriesvaluation_selected. ((exists bpvi_b_pvs_encoded_classificationsupportentriesvaluation_selected_power bpvi_c_pvs_encoded_classificationsupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_encoded_classificationsupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_encoded_classificationsupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_encoded_classificationsupportentriesvaluation_selected_power + S bpvi_i_pvs_encoded_classificationsupportentriesvaluation_selected_power = pvs_exponent_encoded_classificationsupportentries) -> (((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_repeat + S (pvs_prime_encoded_classificationsupportentries) = S ((S (bpvi_i_pvs_encoded_classificationsupportentriesvaluation_selected_power)) * bpvi_c_pvs_encoded_classificationsupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_encoded_classificationsupportentriesvaluation_selected_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_encoded_classificationsupportentriesvaluation_selected_power)) * bpvi_c_pvs_encoded_classificationsupportentriesvaluation_selected_power) + (pvs_prime_encoded_classificationsupportentries)))) /\ (exists bpvi_u_pvs_encoded_classificationsupportentriesvaluation_selected_power bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_start. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_start. bpvi_u_pvs_encoded_classificationsupportentriesvaluation_selected_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_encoded_classificationsupportentriesvaluation_selected) = S ((S (pvs_exponent_encoded_classificationsupportentries)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_encoded_classificationsupportentriesvaluation_selected_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_encoded_classificationsupportentries)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power) + (bpvi_result_pvs_encoded_classificationsupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_encoded_classificationsupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_encoded_classificationsupportentriesvaluation_selected_power. bpvi_product_gap_pvs_encoded_classificationsupportentriesvaluation_selected_power + S bpvi_j_pvs_encoded_classificationsupportentriesvaluation_selected_power = pvs_exponent_encoded_classificationsupportentries) -> exists bpvi_factor_pvs_encoded_classificationsupportentriesvaluation_selected_power bpvi_partial_pvs_encoded_classificationsupportentriesvaluation_selected_power bpvi_successor_pvs_encoded_classificationsupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_factor. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_encoded_classificationsupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_encoded_classificationsupportentriesvaluation_selected_power)) * bpvi_c_pvs_encoded_classificationsupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_factor. bpvi_b_pvs_encoded_classificationsupportentriesvaluation_selected_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_encoded_classificationsupportentriesvaluation_selected_power)) * bpvi_c_pvs_encoded_classificationsupportentriesvaluation_selected_power) + (bpvi_factor_pvs_encoded_classificationsupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_partial. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_encoded_classificationsupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_encoded_classificationsupportentriesvaluation_selected_power)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_partial. bpvi_u_pvs_encoded_classificationsupportentriesvaluation_selected_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_encoded_classificationsupportentriesvaluation_selected_power)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power) + (bpvi_partial_pvs_encoded_classificationsupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_successor. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_encoded_classificationsupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_encoded_classificationsupportentriesvaluation_selected_power)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_successor. bpvi_u_pvs_encoded_classificationsupportentriesvaluation_selected_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_encoded_classificationsupportentriesvaluation_selected_power)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_selected_power) + (bpvi_successor_pvs_encoded_classificationsupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_encoded_classificationsupportentriesvaluation_selected_power = bpvi_partial_pvs_encoded_classificationsupportentriesvaluation_selected_power * bpvi_factor_pvs_encoded_classificationsupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_encoded_classificationsupportentriesvaluation_selected. n = bpvi_result_pvs_encoded_classificationsupportentriesvaluation_selected * bpvi_divisor_factor_pvs_encoded_classificationsupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_encoded_classificationsupportentriesvaluation. (exists bpd_gap_pvs_encoded_classificationsupportentriesvaluation_candidate_bound. bpd_gap_pvs_encoded_classificationsupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_encoded_classificationsupportentriesvaluation) = (n)) -> (exists bpvi_result_pvs_encoded_classificationsupportentriesvaluation_candidate. ((exists bpvi_b_pvs_encoded_classificationsupportentriesvaluation_candidate_power bpvi_c_pvs_encoded_classificationsupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_encoded_classificationsupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_encoded_classificationsupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_encoded_classificationsupportentriesvaluation_candidate_power + S bpvi_i_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpd_candidate_pvs_encoded_classificationsupportentriesvaluation) -> (((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_repeat + S (pvs_prime_encoded_classificationsupportentries) = S ((S (bpvi_i_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) * bpvi_c_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) * bpvi_c_pvs_encoded_classificationsupportentriesvaluation_candidate_power) + (pvs_prime_encoded_classificationsupportentries)))) /\ (exists bpvi_u_pvs_encoded_classificationsupportentriesvaluation_candidate_power bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_start. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_start. bpvi_u_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_encoded_classificationsupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_encoded_classificationsupportentriesvaluation)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_encoded_classificationsupportentriesvaluation)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power) + (bpvi_result_pvs_encoded_classificationsupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_encoded_classificationsupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_encoded_classificationsupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_encoded_classificationsupportentriesvaluation_candidate_power + S bpvi_j_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpd_candidate_pvs_encoded_classificationsupportentriesvaluation) -> exists bpvi_factor_pvs_encoded_classificationsupportentriesvaluation_candidate_power bpvi_partial_pvs_encoded_classificationsupportentriesvaluation_candidate_power bpvi_successor_pvs_encoded_classificationsupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_encoded_classificationsupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) * bpvi_c_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) * bpvi_c_pvs_encoded_classificationsupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_encoded_classificationsupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_encoded_classificationsupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_encoded_classificationsupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_encoded_classificationsupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_encoded_classificationsupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpvi_q_pvs_encoded_classificationsupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_encoded_classificationsupportentriesvaluation_candidate_power)) * bpvi_v_pvs_encoded_classificationsupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_encoded_classificationsupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_encoded_classificationsupportentriesvaluation_candidate_power = bpvi_partial_pvs_encoded_classificationsupportentriesvaluation_candidate_power * bpvi_factor_pvs_encoded_classificationsupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_encoded_classificationsupportentriesvaluation_candidate. n = bpvi_result_pvs_encoded_classificationsupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_encoded_classificationsupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_encoded_classificationsupportentriesvaluation_maximal. bpd_gap_pvs_encoded_classificationsupportentriesvaluation_maximal + (bpd_candidate_pvs_encoded_classificationsupportentriesvaluation) = (pvs_exponent_encoded_classificationsupportentries))) /\ (exists pa_b_pvs_encoded_classificationsupportentriesvalue pa_c_pvs_encoded_classificationsupportentriesvalue. ((forall pa_i_pvs_encoded_classificationsupportentriesvalue_repeat. (exists pa_lt_pvs_encoded_classificationsupportentriesvalue_repeat_bound. pa_lt_pvs_encoded_classificationsupportentriesvalue_repeat_bound + S pa_i_pvs_encoded_classificationsupportentriesvalue_repeat = pvs_exponent_encoded_classificationsupportentries) -> (((exists pa_h_pvs_encoded_classificationsupportentriesvalue_repeat_decoded. pa_h_pvs_encoded_classificationsupportentriesvalue_repeat_decoded + S (pvs_prime_encoded_classificationsupportentries) = S ((S (pa_i_pvs_encoded_classificationsupportentriesvalue_repeat)) * pa_c_pvs_encoded_classificationsupportentriesvalue)) /\ exists pa_q_pvs_encoded_classificationsupportentriesvalue_repeat_decoded. pa_b_pvs_encoded_classificationsupportentriesvalue = pa_q_pvs_encoded_classificationsupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_encoded_classificationsupportentriesvalue_repeat)) * pa_c_pvs_encoded_classificationsupportentriesvalue) + (pvs_prime_encoded_classificationsupportentries)))) /\ (exists pa_u_pvs_encoded_classificationsupportentriesvalue_product pa_v_pvs_encoded_classificationsupportentriesvalue_product. ((((exists pa_h_pvs_encoded_classificationsupportentriesvalue_product_start. pa_h_pvs_encoded_classificationsupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_encoded_classificationsupportentriesvalue_product)) /\ exists pa_q_pvs_encoded_classificationsupportentriesvalue_product_start. pa_u_pvs_encoded_classificationsupportentriesvalue_product = pa_q_pvs_encoded_classificationsupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_encoded_classificationsupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_encoded_classificationsupportentriesvalue_product_terminal. pa_h_pvs_encoded_classificationsupportentriesvalue_product_terminal + S (pvs_power_encoded_classificationsupportentries) = S ((S (pvs_exponent_encoded_classificationsupportentries)) * pa_v_pvs_encoded_classificationsupportentriesvalue_product)) /\ exists pa_q_pvs_encoded_classificationsupportentriesvalue_product_terminal. pa_u_pvs_encoded_classificationsupportentriesvalue_product = pa_q_pvs_encoded_classificationsupportentriesvalue_product_terminal * S ((S (pvs_exponent_encoded_classificationsupportentries)) * pa_v_pvs_encoded_classificationsupportentriesvalue_product) + (pvs_power_encoded_classificationsupportentries))) /\ forall pa_i_pvs_encoded_classificationsupportentriesvalue_product. (exists pa_lt_pvs_encoded_classificationsupportentriesvalue_product_bound. pa_lt_pvs_encoded_classificationsupportentriesvalue_product_bound + S pa_i_pvs_encoded_classificationsupportentriesvalue_product = pvs_exponent_encoded_classificationsupportentries) -> exists pa_p_pvs_encoded_classificationsupportentriesvalue_product pa_r_pvs_encoded_classificationsupportentriesvalue_product pa_s_pvs_encoded_classificationsupportentriesvalue_product. ((((exists pa_h_pvs_encoded_classificationsupportentriesvalue_product_factor. pa_h_pvs_encoded_classificationsupportentriesvalue_product_factor + S (pa_p_pvs_encoded_classificationsupportentriesvalue_product) = S ((S (pa_i_pvs_encoded_classificationsupportentriesvalue_product)) * pa_c_pvs_encoded_classificationsupportentriesvalue)) /\ exists pa_q_pvs_encoded_classificationsupportentriesvalue_product_factor. pa_b_pvs_encoded_classificationsupportentriesvalue = pa_q_pvs_encoded_classificationsupportentriesvalue_product_factor * S ((S (pa_i_pvs_encoded_classificationsupportentriesvalue_product)) * pa_c_pvs_encoded_classificationsupportentriesvalue) + (pa_p_pvs_encoded_classificationsupportentriesvalue_product))) /\ ((((exists pa_h_pvs_encoded_classificationsupportentriesvalue_product_partial. pa_h_pvs_encoded_classificationsupportentriesvalue_product_partial + S (pa_r_pvs_encoded_classificationsupportentriesvalue_product) = S ((S (pa_i_pvs_encoded_classificationsupportentriesvalue_product)) * pa_v_pvs_encoded_classificationsupportentriesvalue_product)) /\ exists pa_q_pvs_encoded_classificationsupportentriesvalue_product_partial. pa_u_pvs_encoded_classificationsupportentriesvalue_product = pa_q_pvs_encoded_classificationsupportentriesvalue_product_partial * S ((S (pa_i_pvs_encoded_classificationsupportentriesvalue_product)) * pa_v_pvs_encoded_classificationsupportentriesvalue_product) + (pa_r_pvs_encoded_classificationsupportentriesvalue_product))) /\ ((((exists pa_h_pvs_encoded_classificationsupportentriesvalue_product_successor. pa_h_pvs_encoded_classificationsupportentriesvalue_product_successor + S (pa_s_pvs_encoded_classificationsupportentriesvalue_product) = S ((S (S pa_i_pvs_encoded_classificationsupportentriesvalue_product)) * pa_v_pvs_encoded_classificationsupportentriesvalue_product)) /\ exists pa_q_pvs_encoded_classificationsupportentriesvalue_product_successor. pa_u_pvs_encoded_classificationsupportentriesvalue_product = pa_q_pvs_encoded_classificationsupportentriesvalue_product_successor * S ((S (S pa_i_pvs_encoded_classificationsupportentriesvalue_product)) * pa_v_pvs_encoded_classificationsupportentriesvalue_product) + (pa_s_pvs_encoded_classificationsupportentriesvalue_product))) /\ pa_s_pvs_encoded_classificationsupportentriesvalue_product = pa_r_pvs_encoded_classificationsupportentriesvalue_product * pa_p_pvs_encoded_classificationsupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_encoded_classificationsupportcover. (~((pvs_divisor_encoded_classificationsupportcover) = 1) /\ forall pvs_left_encoded_classificationsupportcoverprime pvs_right_encoded_classificationsupportcoverprime. (pvs_divisor_encoded_classificationsupportcover) = pvs_left_encoded_classificationsupportcoverprime * pvs_right_encoded_classificationsupportcoverprime -> pvs_left_encoded_classificationsupportcoverprime = 1 \/ pvs_right_encoded_classificationsupportcoverprime = 1) -> (exists pvs_factor_encoded_classificationsupportcoverdivides. (n) = (pvs_divisor_encoded_classificationsupportcover) * pvs_factor_encoded_classificationsupportcoverdivides) -> exists pvs_position_encoded_classificationsupportcover. (exists pvs_gap_encoded_classificationsupportcoverbound. pvs_gap_encoded_classificationsupportcoverbound + S (pvs_position_encoded_classificationsupportcover) = (l)) /\ (((exists ff_h_pvs_encoded_classificationsupportcoverentry. ff_h_pvs_encoded_classificationsupportcoverentry + S (pvs_divisor_encoded_classificationsupportcover) = S ((S (pvs_position_encoded_classificationsupportcover)) * pc)) /\ exists ff_q_pvs_encoded_classificationsupportcoverentry. pb = ff_q_pvs_encoded_classificationsupportcoverentry * S ((S (pvs_position_encoded_classificationsupportcover)) * pc) + (pvs_divisor_encoded_classificationsupportcover)))) /\ (exists ff_u_pvs_encoded_classificationsupportproduct ff_v_pvs_encoded_classificationsupportproduct. ((((exists ff_h_pvs_encoded_classificationsupportproduct_start. ff_h_pvs_encoded_classificationsupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_encoded_classificationsupportproduct)) /\ exists ff_q_pvs_encoded_classificationsupportproduct_start. ff_u_pvs_encoded_classificationsupportproduct = ff_q_pvs_encoded_classificationsupportproduct_start * S ((S (0)) * ff_v_pvs_encoded_classificationsupportproduct) + (1))) /\ ((((exists ff_h_pvs_encoded_classificationsupportproduct_terminal. ff_h_pvs_encoded_classificationsupportproduct_terminal + S (n) = S ((S (l)) * ff_v_pvs_encoded_classificationsupportproduct)) /\ exists ff_q_pvs_encoded_classificationsupportproduct_terminal. ff_u_pvs_encoded_classificationsupportproduct = ff_q_pvs_encoded_classificationsupportproduct_terminal * S ((S (l)) * ff_v_pvs_encoded_classificationsupportproduct) + (n))) /\ forall ff_i_pvs_encoded_classificationsupportproduct. (exists ff_lt_pvs_encoded_classificationsupportproduct_bound. ff_lt_pvs_encoded_classificationsupportproduct_bound + S ff_i_pvs_encoded_classificationsupportproduct = l) -> exists ff_p_pvs_encoded_classificationsupportproduct ff_r_pvs_encoded_classificationsupportproduct ff_s_pvs_encoded_classificationsupportproduct. ((((exists ff_h_pvs_encoded_classificationsupportproduct_factor. ff_h_pvs_encoded_classificationsupportproduct_factor + S (ff_p_pvs_encoded_classificationsupportproduct) = S ((S (ff_i_pvs_encoded_classificationsupportproduct)) * vc)) /\ exists ff_q_pvs_encoded_classificationsupportproduct_factor. vb = ff_q_pvs_encoded_classificationsupportproduct_factor * S ((S (ff_i_pvs_encoded_classificationsupportproduct)) * vc) + (ff_p_pvs_encoded_classificationsupportproduct))) /\ ((((exists ff_h_pvs_encoded_classificationsupportproduct_partial. ff_h_pvs_encoded_classificationsupportproduct_partial + S (ff_r_pvs_encoded_classificationsupportproduct) = S ((S (ff_i_pvs_encoded_classificationsupportproduct)) * ff_v_pvs_encoded_classificationsupportproduct)) /\ exists ff_q_pvs_encoded_classificationsupportproduct_partial. ff_u_pvs_encoded_classificationsupportproduct = ff_q_pvs_encoded_classificationsupportproduct_partial * S ((S (ff_i_pvs_encoded_classificationsupportproduct)) * ff_v_pvs_encoded_classificationsupportproduct) + (ff_r_pvs_encoded_classificationsupportproduct))) /\ ((((exists ff_h_pvs_encoded_classificationsupportproduct_successor. ff_h_pvs_encoded_classificationsupportproduct_successor + S (ff_s_pvs_encoded_classificationsupportproduct) = S ((S (S ff_i_pvs_encoded_classificationsupportproduct)) * ff_v_pvs_encoded_classificationsupportproduct)) /\ exists ff_q_pvs_encoded_classificationsupportproduct_successor. ff_u_pvs_encoded_classificationsupportproduct = ff_q_pvs_encoded_classificationsupportproduct_successor * S ((S (S ff_i_pvs_encoded_classificationsupportproduct)) * ff_v_pvs_encoded_classificationsupportproduct) + (ff_s_pvs_encoded_classificationsupportproduct))) /\ ff_s_pvs_encoded_classificationsupportproduct = ff_r_pvs_encoded_classificationsupportproduct * ff_p_pvs_encoded_classificationsupportproduct)))))))))))))) /\ (((((forall ppf_index_encoded_classificationgcdcommon ppf_entry_encoded_classificationgcdcommon. (exists pvs_gap_encoded_classificationgcdcommonbound. pvs_gap_encoded_classificationgcdcommonbound + S (ppf_index_encoded_classificationgcdcommon) = (l)) -> (((exists ff_h_pvs_encoded_classificationgcdcommonentry. ff_h_pvs_encoded_classificationgcdcommonentry + S (ppf_entry_encoded_classificationgcdcommon) = S ((S (ppf_index_encoded_classificationgcdcommon)) * ec)) /\ exists ff_q_pvs_encoded_classificationgcdcommonentry. eb = ff_q_pvs_encoded_classificationgcdcommonentry * S ((S (ppf_index_encoded_classificationgcdcommon)) * ec) + (ppf_entry_encoded_classificationgcdcommon))) -> (exists pvs_factor_encoded_classificationgcdcommondivisor. (ppf_entry_encoded_classificationgcdcommon) = (g) * pvs_factor_encoded_classificationgcdcommondivisor)) /\ (forall ppf_common_encoded_classificationgcd. (forall ppf_index_encoded_classificationgcdother ppf_entry_encoded_classificationgcdother. (exists pvs_gap_encoded_classificationgcdotherbound. pvs_gap_encoded_classificationgcdotherbound + S (ppf_index_encoded_classificationgcdother) = (l)) -> (((exists ff_h_pvs_encoded_classificationgcdotherentry. ff_h_pvs_encoded_classificationgcdotherentry + S (ppf_entry_encoded_classificationgcdother) = S ((S (ppf_index_encoded_classificationgcdother)) * ec)) /\ exists ff_q_pvs_encoded_classificationgcdotherentry. eb = ff_q_pvs_encoded_classificationgcdotherentry * S ((S (ppf_index_encoded_classificationgcdother)) * ec) + (ppf_entry_encoded_classificationgcdother))) -> (exists pvs_factor_encoded_classificationgcdotherdivisor. (ppf_entry_encoded_classificationgcdother) = (ppf_common_encoded_classificationgcd) * pvs_factor_encoded_classificationgcdotherdivisor)) -> (exists pvs_factor_encoded_classificationgcdgreatest. (g) = (ppf_common_encoded_classificationgcd) * pvs_factor_encoded_classificationgcdgreatest)))) /\ (((~((g) = 0)) /\ (forall ppf_table_degree_encoded_classificationroots. ~(ppf_table_degree_encoded_classificationroots = 0) -> (exists pvs_factor_encoded_classificationrootsdivisor. (g) = (ppf_table_degree_encoded_classificationroots) * pvs_factor_encoded_classificationrootsdivisor) -> exists ppf_table_root_encoded_classificationroots. (((exists ff_h_pvs_encoded_classificationrootsentry. ff_h_pvs_encoded_classificationrootsentry + S (ppf_table_root_encoded_classificationroots) = S ((S (ppf_table_degree_encoded_classificationroots)) * rc)) /\ exists ff_q_pvs_encoded_classificationrootsentry. rb = ff_q_pvs_encoded_classificationrootsentry * S ((S (ppf_table_degree_encoded_classificationroots)) * rc) + (ppf_table_root_encoded_classificationroots))) /\ (exists pa_b_pvs_encoded_classificationrootspower pa_c_pvs_encoded_classificationrootspower. ((forall pa_i_pvs_encoded_classificationrootspower_repeat. (exists pa_lt_pvs_encoded_classificationrootspower_repeat_bound. pa_lt_pvs_encoded_classificationrootspower_repeat_bound + S pa_i_pvs_encoded_classificationrootspower_repeat = ppf_table_degree_encoded_classificationroots) -> (((exists pa_h_pvs_encoded_classificationrootspower_repeat_decoded. pa_h_pvs_encoded_classificationrootspower_repeat_decoded + S (ppf_table_root_encoded_classificationroots) = S ((S (pa_i_pvs_encoded_classificationrootspower_repeat)) * pa_c_pvs_encoded_classificationrootspower)) /\ exists pa_q_pvs_encoded_classificationrootspower_repeat_decoded. pa_b_pvs_encoded_classificationrootspower = pa_q_pvs_encoded_classificationrootspower_repeat_decoded * S ((S (pa_i_pvs_encoded_classificationrootspower_repeat)) * pa_c_pvs_encoded_classificationrootspower) + (ppf_table_root_encoded_classificationroots)))) /\ (exists pa_u_pvs_encoded_classificationrootspower_product pa_v_pvs_encoded_classificationrootspower_product. ((((exists pa_h_pvs_encoded_classificationrootspower_product_start. pa_h_pvs_encoded_classificationrootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_encoded_classificationrootspower_product)) /\ exists pa_q_pvs_encoded_classificationrootspower_product_start. pa_u_pvs_encoded_classificationrootspower_product = pa_q_pvs_encoded_classificationrootspower_product_start * S ((S (0)) * pa_v_pvs_encoded_classificationrootspower_product) + (1))) /\ ((((exists pa_h_pvs_encoded_classificationrootspower_product_terminal. pa_h_pvs_encoded_classificationrootspower_product_terminal + S (n) = S ((S (ppf_table_degree_encoded_classificationroots)) * pa_v_pvs_encoded_classificationrootspower_product)) /\ exists pa_q_pvs_encoded_classificationrootspower_product_terminal. pa_u_pvs_encoded_classificationrootspower_product = pa_q_pvs_encoded_classificationrootspower_product_terminal * S ((S (ppf_table_degree_encoded_classificationroots)) * pa_v_pvs_encoded_classificationrootspower_product) + (n))) /\ forall pa_i_pvs_encoded_classificationrootspower_product. (exists pa_lt_pvs_encoded_classificationrootspower_product_bound. pa_lt_pvs_encoded_classificationrootspower_product_bound + S pa_i_pvs_encoded_classificationrootspower_product = ppf_table_degree_encoded_classificationroots) -> exists pa_p_pvs_encoded_classificationrootspower_product pa_r_pvs_encoded_classificationrootspower_product pa_s_pvs_encoded_classificationrootspower_product. ((((exists pa_h_pvs_encoded_classificationrootspower_product_factor. pa_h_pvs_encoded_classificationrootspower_product_factor + S (pa_p_pvs_encoded_classificationrootspower_product) = S ((S (pa_i_pvs_encoded_classificationrootspower_product)) * pa_c_pvs_encoded_classificationrootspower)) /\ exists pa_q_pvs_encoded_classificationrootspower_product_factor. pa_b_pvs_encoded_classificationrootspower = pa_q_pvs_encoded_classificationrootspower_product_factor * S ((S (pa_i_pvs_encoded_classificationrootspower_product)) * pa_c_pvs_encoded_classificationrootspower) + (pa_p_pvs_encoded_classificationrootspower_product))) /\ ((((exists pa_h_pvs_encoded_classificationrootspower_product_partial. pa_h_pvs_encoded_classificationrootspower_product_partial + S (pa_r_pvs_encoded_classificationrootspower_product) = S ((S (pa_i_pvs_encoded_classificationrootspower_product)) * pa_v_pvs_encoded_classificationrootspower_product)) /\ exists pa_q_pvs_encoded_classificationrootspower_product_partial. pa_u_pvs_encoded_classificationrootspower_product = pa_q_pvs_encoded_classificationrootspower_product_partial * S ((S (pa_i_pvs_encoded_classificationrootspower_product)) * pa_v_pvs_encoded_classificationrootspower_product) + (pa_r_pvs_encoded_classificationrootspower_product))) /\ ((((exists pa_h_pvs_encoded_classificationrootspower_product_successor. pa_h_pvs_encoded_classificationrootspower_product_successor + S (pa_s_pvs_encoded_classificationrootspower_product) = S ((S (S pa_i_pvs_encoded_classificationrootspower_product)) * pa_v_pvs_encoded_classificationrootspower_product)) /\ exists pa_q_pvs_encoded_classificationrootspower_product_successor. pa_u_pvs_encoded_classificationrootspower_product = pa_q_pvs_encoded_classificationrootspower_product_successor * S ((S (S pa_i_pvs_encoded_classificationrootspower_product)) * pa_v_pvs_encoded_classificationrootspower_product) + (pa_s_pvs_encoded_classificationrootspower_product))) /\ pa_s_pvs_encoded_classificationrootspower_product = pa_r_pvs_encoded_classificationrootspower_product * pa_p_pvs_encoded_classificationrootspower_product))))))))))))))))))) -> ~(k = 0) -> ((exists r. (exists pa_b_pvs_encoded_forward pa_c_pvs_encoded_forward. ((forall pa_i_pvs_encoded_forward_repeat. (exists pa_lt_pvs_encoded_forward_repeat_bound. pa_lt_pvs_encoded_forward_repeat_bound + S pa_i_pvs_encoded_forward_repeat = k) -> (((exists pa_h_pvs_encoded_forward_repeat_decoded. pa_h_pvs_encoded_forward_repeat_decoded + S (r) = S ((S (pa_i_pvs_encoded_forward_repeat)) * pa_c_pvs_encoded_forward)) /\ exists pa_q_pvs_encoded_forward_repeat_decoded. pa_b_pvs_encoded_forward = pa_q_pvs_encoded_forward_repeat_decoded * S ((S (pa_i_pvs_encoded_forward_repeat)) * pa_c_pvs_encoded_forward) + (r)))) /\ (exists pa_u_pvs_encoded_forward_product pa_v_pvs_encoded_forward_product. ((((exists pa_h_pvs_encoded_forward_product_start. pa_h_pvs_encoded_forward_product_start + S (1) = S ((S (0)) * pa_v_pvs_encoded_forward_product)) /\ exists pa_q_pvs_encoded_forward_product_start. pa_u_pvs_encoded_forward_product = pa_q_pvs_encoded_forward_product_start * S ((S (0)) * pa_v_pvs_encoded_forward_product) + (1))) /\ ((((exists pa_h_pvs_encoded_forward_product_terminal. pa_h_pvs_encoded_forward_product_terminal + S (n) = S ((S (k)) * pa_v_pvs_encoded_forward_product)) /\ exists pa_q_pvs_encoded_forward_product_terminal. pa_u_pvs_encoded_forward_product = pa_q_pvs_encoded_forward_product_terminal * S ((S (k)) * pa_v_pvs_encoded_forward_product) + (n))) /\ forall pa_i_pvs_encoded_forward_product. (exists pa_lt_pvs_encoded_forward_product_bound. pa_lt_pvs_encoded_forward_product_bound + S pa_i_pvs_encoded_forward_product = k) -> exists pa_p_pvs_encoded_forward_product pa_r_pvs_encoded_forward_product pa_s_pvs_encoded_forward_product. ((((exists pa_h_pvs_encoded_forward_product_factor. pa_h_pvs_encoded_forward_product_factor + S (pa_p_pvs_encoded_forward_product) = S ((S (pa_i_pvs_encoded_forward_product)) * pa_c_pvs_encoded_forward)) /\ exists pa_q_pvs_encoded_forward_product_factor. pa_b_pvs_encoded_forward = pa_q_pvs_encoded_forward_product_factor * S ((S (pa_i_pvs_encoded_forward_product)) * pa_c_pvs_encoded_forward) + (pa_p_pvs_encoded_forward_product))) /\ ((((exists pa_h_pvs_encoded_forward_product_partial. pa_h_pvs_encoded_forward_product_partial + S (pa_r_pvs_encoded_forward_product) = S ((S (pa_i_pvs_encoded_forward_product)) * pa_v_pvs_encoded_forward_product)) /\ exists pa_q_pvs_encoded_forward_product_partial. pa_u_pvs_encoded_forward_product = pa_q_pvs_encoded_forward_product_partial * S ((S (pa_i_pvs_encoded_forward_product)) * pa_v_pvs_encoded_forward_product) + (pa_r_pvs_encoded_forward_product))) /\ ((((exists pa_h_pvs_encoded_forward_product_successor. pa_h_pvs_encoded_forward_product_successor + S (pa_s_pvs_encoded_forward_product) = S ((S (S pa_i_pvs_encoded_forward_product)) * pa_v_pvs_encoded_forward_product)) /\ exists pa_q_pvs_encoded_forward_product_successor. pa_u_pvs_encoded_forward_product = pa_q_pvs_encoded_forward_product_successor * S ((S (S pa_i_pvs_encoded_forward_product)) * pa_v_pvs_encoded_forward_product) + (pa_s_pvs_encoded_forward_product))) /\ pa_s_pvs_encoded_forward_product = pa_r_pvs_encoded_forward_product * pa_p_pvs_encoded_forward_product))))))))) -> (exists pvs_factor_encoded_divisor_first. (g) = (k) * pvs_factor_encoded_divisor_first)) /\ ((exists pvs_factor_encoded_divisor_second. (g) = (k) * pvs_factor_encoded_divisor_second) -> exists r. (exists pa_b_pvs_encoded_reverse pa_c_pvs_encoded_reverse. ((forall pa_i_pvs_encoded_reverse_repeat. (exists pa_lt_pvs_encoded_reverse_repeat_bound. pa_lt_pvs_encoded_reverse_repeat_bound + S pa_i_pvs_encoded_reverse_repeat = k) -> (((exists pa_h_pvs_encoded_reverse_repeat_decoded. pa_h_pvs_encoded_reverse_repeat_decoded + S (r) = S ((S (pa_i_pvs_encoded_reverse_repeat)) * pa_c_pvs_encoded_reverse)) /\ exists pa_q_pvs_encoded_reverse_repeat_decoded. pa_b_pvs_encoded_reverse = pa_q_pvs_encoded_reverse_repeat_decoded * S ((S (pa_i_pvs_encoded_reverse_repeat)) * pa_c_pvs_encoded_reverse) + (r)))) /\ (exists pa_u_pvs_encoded_reverse_product pa_v_pvs_encoded_reverse_product. ((((exists pa_h_pvs_encoded_reverse_product_start. pa_h_pvs_encoded_reverse_product_start + S (1) = S ((S (0)) * pa_v_pvs_encoded_reverse_product)) /\ exists pa_q_pvs_encoded_reverse_product_start. pa_u_pvs_encoded_reverse_product = pa_q_pvs_encoded_reverse_product_start * S ((S (0)) * pa_v_pvs_encoded_reverse_product) + (1))) /\ ((((exists pa_h_pvs_encoded_reverse_product_terminal. pa_h_pvs_encoded_reverse_product_terminal + S (n) = S ((S (k)) * pa_v_pvs_encoded_reverse_product)) /\ exists pa_q_pvs_encoded_reverse_product_terminal. pa_u_pvs_encoded_reverse_product = pa_q_pvs_encoded_reverse_product_terminal * S ((S (k)) * pa_v_pvs_encoded_reverse_product) + (n))) /\ forall pa_i_pvs_encoded_reverse_product. (exists pa_lt_pvs_encoded_reverse_product_bound. pa_lt_pvs_encoded_reverse_product_bound + S pa_i_pvs_encoded_reverse_product = k) -> exists pa_p_pvs_encoded_reverse_product pa_r_pvs_encoded_reverse_product pa_s_pvs_encoded_reverse_product. ((((exists pa_h_pvs_encoded_reverse_product_factor. pa_h_pvs_encoded_reverse_product_factor + S (pa_p_pvs_encoded_reverse_product) = S ((S (pa_i_pvs_encoded_reverse_product)) * pa_c_pvs_encoded_reverse)) /\ exists pa_q_pvs_encoded_reverse_product_factor. pa_b_pvs_encoded_reverse = pa_q_pvs_encoded_reverse_product_factor * S ((S (pa_i_pvs_encoded_reverse_product)) * pa_c_pvs_encoded_reverse) + (pa_p_pvs_encoded_reverse_product))) /\ ((((exists pa_h_pvs_encoded_reverse_product_partial. pa_h_pvs_encoded_reverse_product_partial + S (pa_r_pvs_encoded_reverse_product) = S ((S (pa_i_pvs_encoded_reverse_product)) * pa_v_pvs_encoded_reverse_product)) /\ exists pa_q_pvs_encoded_reverse_product_partial. pa_u_pvs_encoded_reverse_product = pa_q_pvs_encoded_reverse_product_partial * S ((S (pa_i_pvs_encoded_reverse_product)) * pa_v_pvs_encoded_reverse_product) + (pa_r_pvs_encoded_reverse_product))) /\ ((((exists pa_h_pvs_encoded_reverse_product_successor. pa_h_pvs_encoded_reverse_product_successor + S (pa_s_pvs_encoded_reverse_product) = S ((S (S pa_i_pvs_encoded_reverse_product)) * pa_v_pvs_encoded_reverse_product)) /\ exists pa_q_pvs_encoded_reverse_product_successor. pa_u_pvs_encoded_reverse_product = pa_q_pvs_encoded_reverse_product_successor * S ((S (S pa_i_pvs_encoded_reverse_product)) * pa_v_pvs_encoded_reverse_product) + (pa_s_pvs_encoded_reverse_product))) /\ pa_s_pvs_encoded_reverse_product = pa_r_pvs_encoded_reverse_product * pa_p_pvs_encoded_reverse_product)))))))))