perfect_power_profile_data_root_lookup

forall n w pb pc eb ec vb vc l g rb rc k. (((~((n) = 1)) /\ (((exists ppf_code_0_lookup_datacode ppf_code_1_lookup_datacode ppf_code_2_lookup_datacode ppf_code_3_lookup_datacode ppf_code_4_lookup_datacode ppf_code_5_lookup_datacode ppf_code_6_lookup_datacode ppf_code_7_lookup_datacode. ((((w) = ((pb) + (ppf_code_0_lookup_datacode)) * S ((pb) + (ppf_code_0_lookup_datacode)) + ((ppf_code_0_lookup_datacode) + (ppf_code_0_lookup_datacode))) /\ ((((ppf_code_0_lookup_datacode) = ((pc) + (ppf_code_1_lookup_datacode)) * S ((pc) + (ppf_code_1_lookup_datacode)) + ((ppf_code_1_lookup_datacode) + (ppf_code_1_lookup_datacode))) /\ ((((ppf_code_1_lookup_datacode) = ((eb) + (ppf_code_2_lookup_datacode)) * S ((eb) + (ppf_code_2_lookup_datacode)) + ((ppf_code_2_lookup_datacode) + (ppf_code_2_lookup_datacode))) /\ ((((ppf_code_2_lookup_datacode) = ((ec) + (ppf_code_3_lookup_datacode)) * S ((ec) + (ppf_code_3_lookup_datacode)) + ((ppf_code_3_lookup_datacode) + (ppf_code_3_lookup_datacode))) /\ ((((ppf_code_3_lookup_datacode) = ((vb) + (ppf_code_4_lookup_datacode)) * S ((vb) + (ppf_code_4_lookup_datacode)) + ((ppf_code_4_lookup_datacode) + (ppf_code_4_lookup_datacode))) /\ ((((ppf_code_4_lookup_datacode) = ((vc) + (ppf_code_5_lookup_datacode)) * S ((vc) + (ppf_code_5_lookup_datacode)) + ((ppf_code_5_lookup_datacode) + (ppf_code_5_lookup_datacode))) /\ ((((ppf_code_5_lookup_datacode) = ((l) + (ppf_code_6_lookup_datacode)) * S ((l) + (ppf_code_6_lookup_datacode)) + ((ppf_code_6_lookup_datacode) + (ppf_code_6_lookup_datacode))) /\ ((((ppf_code_6_lookup_datacode) = ((g) + (ppf_code_7_lookup_datacode)) * S ((g) + (ppf_code_7_lookup_datacode)) + ((ppf_code_7_lookup_datacode) + (ppf_code_7_lookup_datacode))) /\ ((ppf_code_7_lookup_datacode) = ((rb) + (rc)) * S ((rb) + (rc)) + ((rc) + (rc)))))))))))))))))))) /\ (((((~((n) = 0)) /\ (((forall pfp_i_pvs_lookup_datasupportdistinct pfp_j_pvs_lookup_datasupportdistinct pfp_a_pvs_lookup_datasupportdistinct. (exists pfp_gap_pvs_lookup_datasupportdistinctfirst. pfp_gap_pvs_lookup_datasupportdistinctfirst + S (pfp_i_pvs_lookup_datasupportdistinct) = (l)) -> (exists pfp_gap_pvs_lookup_datasupportdistinctsecond. pfp_gap_pvs_lookup_datasupportdistinctsecond + S (pfp_j_pvs_lookup_datasupportdistinct) = (l)) -> (((exists ff_h_pfp_pvs_lookup_datasupportdistinctleft. ff_h_pfp_pvs_lookup_datasupportdistinctleft + S (pfp_a_pvs_lookup_datasupportdistinct) = S ((S (pfp_i_pvs_lookup_datasupportdistinct)) * pc)) /\ exists ff_q_pfp_pvs_lookup_datasupportdistinctleft. pb = ff_q_pfp_pvs_lookup_datasupportdistinctleft * S ((S (pfp_i_pvs_lookup_datasupportdistinct)) * pc) + (pfp_a_pvs_lookup_datasupportdistinct))) -> (((exists ff_h_pfp_pvs_lookup_datasupportdistinctright. ff_h_pfp_pvs_lookup_datasupportdistinctright + S (pfp_a_pvs_lookup_datasupportdistinct) = S ((S (pfp_j_pvs_lookup_datasupportdistinct)) * pc)) /\ exists ff_q_pfp_pvs_lookup_datasupportdistinctright. pb = ff_q_pfp_pvs_lookup_datasupportdistinctright * S ((S (pfp_j_pvs_lookup_datasupportdistinct)) * pc) + (pfp_a_pvs_lookup_datasupportdistinct))) -> pfp_i_pvs_lookup_datasupportdistinct = pfp_j_pvs_lookup_datasupportdistinct) /\ (((forall pvs_index_lookup_datasupportentries. (exists pvs_gap_lookup_datasupportentriesindex. pvs_gap_lookup_datasupportentriesindex + S (pvs_index_lookup_datasupportentries) = (l)) -> exists pvs_prime_lookup_datasupportentries pvs_exponent_lookup_datasupportentries pvs_power_lookup_datasupportentries. (((((exists ff_h_pvs_lookup_datasupportentriesprime. ff_h_pvs_lookup_datasupportentriesprime + S (pvs_prime_lookup_datasupportentries) = S ((S (pvs_index_lookup_datasupportentries)) * pc)) /\ exists ff_q_pvs_lookup_datasupportentriesprime. pb = ff_q_pvs_lookup_datasupportentriesprime * S ((S (pvs_index_lookup_datasupportentries)) * pc) + (pvs_prime_lookup_datasupportentries))) /\ (((((exists ff_h_pvs_lookup_datasupportentriesexponent. ff_h_pvs_lookup_datasupportentriesexponent + S (pvs_exponent_lookup_datasupportentries) = S ((S (pvs_index_lookup_datasupportentries)) * ec)) /\ exists ff_q_pvs_lookup_datasupportentriesexponent. eb = ff_q_pvs_lookup_datasupportentriesexponent * S ((S (pvs_index_lookup_datasupportentries)) * ec) + (pvs_exponent_lookup_datasupportentries))) /\ (((((exists ff_h_pvs_lookup_datasupportentriespower. ff_h_pvs_lookup_datasupportentriespower + S (pvs_power_lookup_datasupportentries) = S ((S (pvs_index_lookup_datasupportentries)) * vc)) /\ exists ff_q_pvs_lookup_datasupportentriespower. vb = ff_q_pvs_lookup_datasupportentriespower * S ((S (pvs_index_lookup_datasupportentries)) * vc) + (pvs_power_lookup_datasupportentries))) /\ (((~((pvs_prime_lookup_datasupportentries) = 1) /\ forall pvs_left_lookup_datasupportentriesdomain pvs_right_lookup_datasupportentriesdomain. (pvs_prime_lookup_datasupportentries) = pvs_left_lookup_datasupportentriesdomain * pvs_right_lookup_datasupportentriesdomain -> pvs_left_lookup_datasupportentriesdomain = 1 \/ pvs_right_lookup_datasupportentriesdomain = 1) /\ (((~(pvs_exponent_lookup_datasupportentries = 0)) /\ (((((exists bpd_gap_pvs_lookup_datasupportentriesvaluation_selected_bound. bpd_gap_pvs_lookup_datasupportentriesvaluation_selected_bound + (pvs_exponent_lookup_datasupportentries) = (n)) /\ (exists bpvi_result_pvs_lookup_datasupportentriesvaluation_selected. ((exists bpvi_b_pvs_lookup_datasupportentriesvaluation_selected_power bpvi_c_pvs_lookup_datasupportentriesvaluation_selected_power. ((forall bpvi_i_pvs_lookup_datasupportentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_lookup_datasupportentriesvaluation_selected_power. bpvi_repeat_gap_pvs_lookup_datasupportentriesvaluation_selected_power + S bpvi_i_pvs_lookup_datasupportentriesvaluation_selected_power = pvs_exponent_lookup_datasupportentries) -> (((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_repeat. bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_repeat + S (pvs_prime_lookup_datasupportentries) = S ((S (bpvi_i_pvs_lookup_datasupportentriesvaluation_selected_power)) * bpvi_c_pvs_lookup_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_repeat. bpvi_b_pvs_lookup_datasupportentriesvaluation_selected_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_lookup_datasupportentriesvaluation_selected_power)) * bpvi_c_pvs_lookup_datasupportentriesvaluation_selected_power) + (pvs_prime_lookup_datasupportentries)))) /\ (exists bpvi_u_pvs_lookup_datasupportentriesvaluation_selected_power bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_start. bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_start. bpvi_u_pvs_lookup_datasupportentriesvaluation_selected_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_terminal. bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_lookup_datasupportentriesvaluation_selected) = S ((S (pvs_exponent_lookup_datasupportentries)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_terminal. bpvi_u_pvs_lookup_datasupportentriesvaluation_selected_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_lookup_datasupportentries)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power) + (bpvi_result_pvs_lookup_datasupportentriesvaluation_selected))) /\ forall bpvi_j_pvs_lookup_datasupportentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_lookup_datasupportentriesvaluation_selected_power. bpvi_product_gap_pvs_lookup_datasupportentriesvaluation_selected_power + S bpvi_j_pvs_lookup_datasupportentriesvaluation_selected_power = pvs_exponent_lookup_datasupportentries) -> exists bpvi_factor_pvs_lookup_datasupportentriesvaluation_selected_power bpvi_partial_pvs_lookup_datasupportentriesvaluation_selected_power bpvi_successor_pvs_lookup_datasupportentriesvaluation_selected_power. ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_factor. bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_lookup_datasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_lookup_datasupportentriesvaluation_selected_power)) * bpvi_c_pvs_lookup_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_factor. bpvi_b_pvs_lookup_datasupportentriesvaluation_selected_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_lookup_datasupportentriesvaluation_selected_power)) * bpvi_c_pvs_lookup_datasupportentriesvaluation_selected_power) + (bpvi_factor_pvs_lookup_datasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_partial. bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_lookup_datasupportentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_lookup_datasupportentriesvaluation_selected_power)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_partial. bpvi_u_pvs_lookup_datasupportentriesvaluation_selected_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_lookup_datasupportentriesvaluation_selected_power)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power) + (bpvi_partial_pvs_lookup_datasupportentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_successor. bpvi_h_pvs_lookup_datasupportentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_lookup_datasupportentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_lookup_datasupportentriesvaluation_selected_power)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_successor. bpvi_u_pvs_lookup_datasupportentriesvaluation_selected_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_lookup_datasupportentriesvaluation_selected_power)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_selected_power) + (bpvi_successor_pvs_lookup_datasupportentriesvaluation_selected_power))) /\ bpvi_successor_pvs_lookup_datasupportentriesvaluation_selected_power = bpvi_partial_pvs_lookup_datasupportentriesvaluation_selected_power * bpvi_factor_pvs_lookup_datasupportentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_lookup_datasupportentriesvaluation_selected. n = bpvi_result_pvs_lookup_datasupportentriesvaluation_selected * bpvi_divisor_factor_pvs_lookup_datasupportentriesvaluation_selected))) /\ forall bpd_candidate_pvs_lookup_datasupportentriesvaluation. (exists bpd_gap_pvs_lookup_datasupportentriesvaluation_candidate_bound. bpd_gap_pvs_lookup_datasupportentriesvaluation_candidate_bound + (bpd_candidate_pvs_lookup_datasupportentriesvaluation) = (n)) -> (exists bpvi_result_pvs_lookup_datasupportentriesvaluation_candidate. ((exists bpvi_b_pvs_lookup_datasupportentriesvaluation_candidate_power bpvi_c_pvs_lookup_datasupportentriesvaluation_candidate_power. ((forall bpvi_i_pvs_lookup_datasupportentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_lookup_datasupportentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_lookup_datasupportentriesvaluation_candidate_power + S bpvi_i_pvs_lookup_datasupportentriesvaluation_candidate_power = bpd_candidate_pvs_lookup_datasupportentriesvaluation) -> (((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_repeat. bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_repeat + S (pvs_prime_lookup_datasupportentries) = S ((S (bpvi_i_pvs_lookup_datasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_lookup_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_repeat. bpvi_b_pvs_lookup_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_lookup_datasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_lookup_datasupportentriesvaluation_candidate_power) + (pvs_prime_lookup_datasupportentries)))) /\ (exists bpvi_u_pvs_lookup_datasupportentriesvaluation_candidate_power bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_start. bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_start. bpvi_u_pvs_lookup_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_terminal. bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_lookup_datasupportentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_lookup_datasupportentriesvaluation)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_terminal. bpvi_u_pvs_lookup_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_lookup_datasupportentriesvaluation)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power) + (bpvi_result_pvs_lookup_datasupportentriesvaluation_candidate))) /\ forall bpvi_j_pvs_lookup_datasupportentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_lookup_datasupportentriesvaluation_candidate_power. bpvi_product_gap_pvs_lookup_datasupportentriesvaluation_candidate_power + S bpvi_j_pvs_lookup_datasupportentriesvaluation_candidate_power = bpd_candidate_pvs_lookup_datasupportentriesvaluation) -> exists bpvi_factor_pvs_lookup_datasupportentriesvaluation_candidate_power bpvi_partial_pvs_lookup_datasupportentriesvaluation_candidate_power bpvi_successor_pvs_lookup_datasupportentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_factor. bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_lookup_datasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_lookup_datasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_lookup_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_factor. bpvi_b_pvs_lookup_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_lookup_datasupportentriesvaluation_candidate_power)) * bpvi_c_pvs_lookup_datasupportentriesvaluation_candidate_power) + (bpvi_factor_pvs_lookup_datasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_partial. bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_lookup_datasupportentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_lookup_datasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_partial. bpvi_u_pvs_lookup_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_lookup_datasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power) + (bpvi_partial_pvs_lookup_datasupportentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_successor. bpvi_h_pvs_lookup_datasupportentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_lookup_datasupportentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_lookup_datasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_successor. bpvi_u_pvs_lookup_datasupportentriesvaluation_candidate_power = bpvi_q_pvs_lookup_datasupportentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_lookup_datasupportentriesvaluation_candidate_power)) * bpvi_v_pvs_lookup_datasupportentriesvaluation_candidate_power) + (bpvi_successor_pvs_lookup_datasupportentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_lookup_datasupportentriesvaluation_candidate_power = bpvi_partial_pvs_lookup_datasupportentriesvaluation_candidate_power * bpvi_factor_pvs_lookup_datasupportentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_lookup_datasupportentriesvaluation_candidate. n = bpvi_result_pvs_lookup_datasupportentriesvaluation_candidate * bpvi_divisor_factor_pvs_lookup_datasupportentriesvaluation_candidate)) -> (exists bpd_gap_pvs_lookup_datasupportentriesvaluation_maximal. bpd_gap_pvs_lookup_datasupportentriesvaluation_maximal + (bpd_candidate_pvs_lookup_datasupportentriesvaluation) = (pvs_exponent_lookup_datasupportentries))) /\ (exists pa_b_pvs_lookup_datasupportentriesvalue pa_c_pvs_lookup_datasupportentriesvalue. ((forall pa_i_pvs_lookup_datasupportentriesvalue_repeat. (exists pa_lt_pvs_lookup_datasupportentriesvalue_repeat_bound. pa_lt_pvs_lookup_datasupportentriesvalue_repeat_bound + S pa_i_pvs_lookup_datasupportentriesvalue_repeat = pvs_exponent_lookup_datasupportentries) -> (((exists pa_h_pvs_lookup_datasupportentriesvalue_repeat_decoded. pa_h_pvs_lookup_datasupportentriesvalue_repeat_decoded + S (pvs_prime_lookup_datasupportentries) = S ((S (pa_i_pvs_lookup_datasupportentriesvalue_repeat)) * pa_c_pvs_lookup_datasupportentriesvalue)) /\ exists pa_q_pvs_lookup_datasupportentriesvalue_repeat_decoded. pa_b_pvs_lookup_datasupportentriesvalue = pa_q_pvs_lookup_datasupportentriesvalue_repeat_decoded * S ((S (pa_i_pvs_lookup_datasupportentriesvalue_repeat)) * pa_c_pvs_lookup_datasupportentriesvalue) + (pvs_prime_lookup_datasupportentries)))) /\ (exists pa_u_pvs_lookup_datasupportentriesvalue_product pa_v_pvs_lookup_datasupportentriesvalue_product. ((((exists pa_h_pvs_lookup_datasupportentriesvalue_product_start. pa_h_pvs_lookup_datasupportentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_lookup_datasupportentriesvalue_product)) /\ exists pa_q_pvs_lookup_datasupportentriesvalue_product_start. pa_u_pvs_lookup_datasupportentriesvalue_product = pa_q_pvs_lookup_datasupportentriesvalue_product_start * S ((S (0)) * pa_v_pvs_lookup_datasupportentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_lookup_datasupportentriesvalue_product_terminal. pa_h_pvs_lookup_datasupportentriesvalue_product_terminal + S (pvs_power_lookup_datasupportentries) = S ((S (pvs_exponent_lookup_datasupportentries)) * pa_v_pvs_lookup_datasupportentriesvalue_product)) /\ exists pa_q_pvs_lookup_datasupportentriesvalue_product_terminal. pa_u_pvs_lookup_datasupportentriesvalue_product = pa_q_pvs_lookup_datasupportentriesvalue_product_terminal * S ((S (pvs_exponent_lookup_datasupportentries)) * pa_v_pvs_lookup_datasupportentriesvalue_product) + (pvs_power_lookup_datasupportentries))) /\ forall pa_i_pvs_lookup_datasupportentriesvalue_product. (exists pa_lt_pvs_lookup_datasupportentriesvalue_product_bound. pa_lt_pvs_lookup_datasupportentriesvalue_product_bound + S pa_i_pvs_lookup_datasupportentriesvalue_product = pvs_exponent_lookup_datasupportentries) -> exists pa_p_pvs_lookup_datasupportentriesvalue_product pa_r_pvs_lookup_datasupportentriesvalue_product pa_s_pvs_lookup_datasupportentriesvalue_product. ((((exists pa_h_pvs_lookup_datasupportentriesvalue_product_factor. pa_h_pvs_lookup_datasupportentriesvalue_product_factor + S (pa_p_pvs_lookup_datasupportentriesvalue_product) = S ((S (pa_i_pvs_lookup_datasupportentriesvalue_product)) * pa_c_pvs_lookup_datasupportentriesvalue)) /\ exists pa_q_pvs_lookup_datasupportentriesvalue_product_factor. pa_b_pvs_lookup_datasupportentriesvalue = pa_q_pvs_lookup_datasupportentriesvalue_product_factor * S ((S (pa_i_pvs_lookup_datasupportentriesvalue_product)) * pa_c_pvs_lookup_datasupportentriesvalue) + (pa_p_pvs_lookup_datasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_lookup_datasupportentriesvalue_product_partial. pa_h_pvs_lookup_datasupportentriesvalue_product_partial + S (pa_r_pvs_lookup_datasupportentriesvalue_product) = S ((S (pa_i_pvs_lookup_datasupportentriesvalue_product)) * pa_v_pvs_lookup_datasupportentriesvalue_product)) /\ exists pa_q_pvs_lookup_datasupportentriesvalue_product_partial. pa_u_pvs_lookup_datasupportentriesvalue_product = pa_q_pvs_lookup_datasupportentriesvalue_product_partial * S ((S (pa_i_pvs_lookup_datasupportentriesvalue_product)) * pa_v_pvs_lookup_datasupportentriesvalue_product) + (pa_r_pvs_lookup_datasupportentriesvalue_product))) /\ ((((exists pa_h_pvs_lookup_datasupportentriesvalue_product_successor. pa_h_pvs_lookup_datasupportentriesvalue_product_successor + S (pa_s_pvs_lookup_datasupportentriesvalue_product) = S ((S (S pa_i_pvs_lookup_datasupportentriesvalue_product)) * pa_v_pvs_lookup_datasupportentriesvalue_product)) /\ exists pa_q_pvs_lookup_datasupportentriesvalue_product_successor. pa_u_pvs_lookup_datasupportentriesvalue_product = pa_q_pvs_lookup_datasupportentriesvalue_product_successor * S ((S (S pa_i_pvs_lookup_datasupportentriesvalue_product)) * pa_v_pvs_lookup_datasupportentriesvalue_product) + (pa_s_pvs_lookup_datasupportentriesvalue_product))) /\ pa_s_pvs_lookup_datasupportentriesvalue_product = pa_r_pvs_lookup_datasupportentriesvalue_product * pa_p_pvs_lookup_datasupportentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_lookup_datasupportcover. (~((pvs_divisor_lookup_datasupportcover) = 1) /\ forall pvs_left_lookup_datasupportcoverprime pvs_right_lookup_datasupportcoverprime. (pvs_divisor_lookup_datasupportcover) = pvs_left_lookup_datasupportcoverprime * pvs_right_lookup_datasupportcoverprime -> pvs_left_lookup_datasupportcoverprime = 1 \/ pvs_right_lookup_datasupportcoverprime = 1) -> (exists pvs_factor_lookup_datasupportcoverdivides. (n) = (pvs_divisor_lookup_datasupportcover) * pvs_factor_lookup_datasupportcoverdivides) -> exists pvs_position_lookup_datasupportcover. (exists pvs_gap_lookup_datasupportcoverbound. pvs_gap_lookup_datasupportcoverbound + S (pvs_position_lookup_datasupportcover) = (l)) /\ (((exists ff_h_pvs_lookup_datasupportcoverentry. ff_h_pvs_lookup_datasupportcoverentry + S (pvs_divisor_lookup_datasupportcover) = S ((S (pvs_position_lookup_datasupportcover)) * pc)) /\ exists ff_q_pvs_lookup_datasupportcoverentry. pb = ff_q_pvs_lookup_datasupportcoverentry * S ((S (pvs_position_lookup_datasupportcover)) * pc) + (pvs_divisor_lookup_datasupportcover)))) /\ (exists ff_u_pvs_lookup_datasupportproduct ff_v_pvs_lookup_datasupportproduct. ((((exists ff_h_pvs_lookup_datasupportproduct_start. ff_h_pvs_lookup_datasupportproduct_start + S (1) = S ((S (0)) * ff_v_pvs_lookup_datasupportproduct)) /\ exists ff_q_pvs_lookup_datasupportproduct_start. ff_u_pvs_lookup_datasupportproduct = ff_q_pvs_lookup_datasupportproduct_start * S ((S (0)) * ff_v_pvs_lookup_datasupportproduct) + (1))) /\ ((((exists ff_h_pvs_lookup_datasupportproduct_terminal. ff_h_pvs_lookup_datasupportproduct_terminal + S (n) = S ((S (l)) * ff_v_pvs_lookup_datasupportproduct)) /\ exists ff_q_pvs_lookup_datasupportproduct_terminal. ff_u_pvs_lookup_datasupportproduct = ff_q_pvs_lookup_datasupportproduct_terminal * S ((S (l)) * ff_v_pvs_lookup_datasupportproduct) + (n))) /\ forall ff_i_pvs_lookup_datasupportproduct. (exists ff_lt_pvs_lookup_datasupportproduct_bound. ff_lt_pvs_lookup_datasupportproduct_bound + S ff_i_pvs_lookup_datasupportproduct = l) -> exists ff_p_pvs_lookup_datasupportproduct ff_r_pvs_lookup_datasupportproduct ff_s_pvs_lookup_datasupportproduct. ((((exists ff_h_pvs_lookup_datasupportproduct_factor. ff_h_pvs_lookup_datasupportproduct_factor + S (ff_p_pvs_lookup_datasupportproduct) = S ((S (ff_i_pvs_lookup_datasupportproduct)) * vc)) /\ exists ff_q_pvs_lookup_datasupportproduct_factor. vb = ff_q_pvs_lookup_datasupportproduct_factor * S ((S (ff_i_pvs_lookup_datasupportproduct)) * vc) + (ff_p_pvs_lookup_datasupportproduct))) /\ ((((exists ff_h_pvs_lookup_datasupportproduct_partial. ff_h_pvs_lookup_datasupportproduct_partial + S (ff_r_pvs_lookup_datasupportproduct) = S ((S (ff_i_pvs_lookup_datasupportproduct)) * ff_v_pvs_lookup_datasupportproduct)) /\ exists ff_q_pvs_lookup_datasupportproduct_partial. ff_u_pvs_lookup_datasupportproduct = ff_q_pvs_lookup_datasupportproduct_partial * S ((S (ff_i_pvs_lookup_datasupportproduct)) * ff_v_pvs_lookup_datasupportproduct) + (ff_r_pvs_lookup_datasupportproduct))) /\ ((((exists ff_h_pvs_lookup_datasupportproduct_successor. ff_h_pvs_lookup_datasupportproduct_successor + S (ff_s_pvs_lookup_datasupportproduct) = S ((S (S ff_i_pvs_lookup_datasupportproduct)) * ff_v_pvs_lookup_datasupportproduct)) /\ exists ff_q_pvs_lookup_datasupportproduct_successor. ff_u_pvs_lookup_datasupportproduct = ff_q_pvs_lookup_datasupportproduct_successor * S ((S (S ff_i_pvs_lookup_datasupportproduct)) * ff_v_pvs_lookup_datasupportproduct) + (ff_s_pvs_lookup_datasupportproduct))) /\ ff_s_pvs_lookup_datasupportproduct = ff_r_pvs_lookup_datasupportproduct * ff_p_pvs_lookup_datasupportproduct)))))))))))))) /\ (((((forall ppf_index_lookup_datagcdcommon ppf_entry_lookup_datagcdcommon. (exists pvs_gap_lookup_datagcdcommonbound. pvs_gap_lookup_datagcdcommonbound + S (ppf_index_lookup_datagcdcommon) = (l)) -> (((exists ff_h_pvs_lookup_datagcdcommonentry. ff_h_pvs_lookup_datagcdcommonentry + S (ppf_entry_lookup_datagcdcommon) = S ((S (ppf_index_lookup_datagcdcommon)) * ec)) /\ exists ff_q_pvs_lookup_datagcdcommonentry. eb = ff_q_pvs_lookup_datagcdcommonentry * S ((S (ppf_index_lookup_datagcdcommon)) * ec) + (ppf_entry_lookup_datagcdcommon))) -> (exists pvs_factor_lookup_datagcdcommondivisor. (ppf_entry_lookup_datagcdcommon) = (g) * pvs_factor_lookup_datagcdcommondivisor)) /\ (forall ppf_common_lookup_datagcd. (forall ppf_index_lookup_datagcdother ppf_entry_lookup_datagcdother. (exists pvs_gap_lookup_datagcdotherbound. pvs_gap_lookup_datagcdotherbound + S (ppf_index_lookup_datagcdother) = (l)) -> (((exists ff_h_pvs_lookup_datagcdotherentry. ff_h_pvs_lookup_datagcdotherentry + S (ppf_entry_lookup_datagcdother) = S ((S (ppf_index_lookup_datagcdother)) * ec)) /\ exists ff_q_pvs_lookup_datagcdotherentry. eb = ff_q_pvs_lookup_datagcdotherentry * S ((S (ppf_index_lookup_datagcdother)) * ec) + (ppf_entry_lookup_datagcdother))) -> (exists pvs_factor_lookup_datagcdotherdivisor. (ppf_entry_lookup_datagcdother) = (ppf_common_lookup_datagcd) * pvs_factor_lookup_datagcdotherdivisor)) -> (exists pvs_factor_lookup_datagcdgreatest. (g) = (ppf_common_lookup_datagcd) * pvs_factor_lookup_datagcdgreatest)))) /\ (((~((g) = 0)) /\ (forall ppf_table_degree_lookup_dataroots. ~(ppf_table_degree_lookup_dataroots = 0) -> (exists pvs_factor_lookup_datarootsdivisor. (g) = (ppf_table_degree_lookup_dataroots) * pvs_factor_lookup_datarootsdivisor) -> exists ppf_table_root_lookup_dataroots. (((exists ff_h_pvs_lookup_datarootsentry. ff_h_pvs_lookup_datarootsentry + S (ppf_table_root_lookup_dataroots) = S ((S (ppf_table_degree_lookup_dataroots)) * rc)) /\ exists ff_q_pvs_lookup_datarootsentry. rb = ff_q_pvs_lookup_datarootsentry * S ((S (ppf_table_degree_lookup_dataroots)) * rc) + (ppf_table_root_lookup_dataroots))) /\ (exists pa_b_pvs_lookup_datarootspower pa_c_pvs_lookup_datarootspower. ((forall pa_i_pvs_lookup_datarootspower_repeat. (exists pa_lt_pvs_lookup_datarootspower_repeat_bound. pa_lt_pvs_lookup_datarootspower_repeat_bound + S pa_i_pvs_lookup_datarootspower_repeat = ppf_table_degree_lookup_dataroots) -> (((exists pa_h_pvs_lookup_datarootspower_repeat_decoded. pa_h_pvs_lookup_datarootspower_repeat_decoded + S (ppf_table_root_lookup_dataroots) = S ((S (pa_i_pvs_lookup_datarootspower_repeat)) * pa_c_pvs_lookup_datarootspower)) /\ exists pa_q_pvs_lookup_datarootspower_repeat_decoded. pa_b_pvs_lookup_datarootspower = pa_q_pvs_lookup_datarootspower_repeat_decoded * S ((S (pa_i_pvs_lookup_datarootspower_repeat)) * pa_c_pvs_lookup_datarootspower) + (ppf_table_root_lookup_dataroots)))) /\ (exists pa_u_pvs_lookup_datarootspower_product pa_v_pvs_lookup_datarootspower_product. ((((exists pa_h_pvs_lookup_datarootspower_product_start. pa_h_pvs_lookup_datarootspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_lookup_datarootspower_product)) /\ exists pa_q_pvs_lookup_datarootspower_product_start. pa_u_pvs_lookup_datarootspower_product = pa_q_pvs_lookup_datarootspower_product_start * S ((S (0)) * pa_v_pvs_lookup_datarootspower_product) + (1))) /\ ((((exists pa_h_pvs_lookup_datarootspower_product_terminal. pa_h_pvs_lookup_datarootspower_product_terminal + S (n) = S ((S (ppf_table_degree_lookup_dataroots)) * pa_v_pvs_lookup_datarootspower_product)) /\ exists pa_q_pvs_lookup_datarootspower_product_terminal. pa_u_pvs_lookup_datarootspower_product = pa_q_pvs_lookup_datarootspower_product_terminal * S ((S (ppf_table_degree_lookup_dataroots)) * pa_v_pvs_lookup_datarootspower_product) + (n))) /\ forall pa_i_pvs_lookup_datarootspower_product. (exists pa_lt_pvs_lookup_datarootspower_product_bound. pa_lt_pvs_lookup_datarootspower_product_bound + S pa_i_pvs_lookup_datarootspower_product = ppf_table_degree_lookup_dataroots) -> exists pa_p_pvs_lookup_datarootspower_product pa_r_pvs_lookup_datarootspower_product pa_s_pvs_lookup_datarootspower_product. ((((exists pa_h_pvs_lookup_datarootspower_product_factor. pa_h_pvs_lookup_datarootspower_product_factor + S (pa_p_pvs_lookup_datarootspower_product) = S ((S (pa_i_pvs_lookup_datarootspower_product)) * pa_c_pvs_lookup_datarootspower)) /\ exists pa_q_pvs_lookup_datarootspower_product_factor. pa_b_pvs_lookup_datarootspower = pa_q_pvs_lookup_datarootspower_product_factor * S ((S (pa_i_pvs_lookup_datarootspower_product)) * pa_c_pvs_lookup_datarootspower) + (pa_p_pvs_lookup_datarootspower_product))) /\ ((((exists pa_h_pvs_lookup_datarootspower_product_partial. pa_h_pvs_lookup_datarootspower_product_partial + S (pa_r_pvs_lookup_datarootspower_product) = S ((S (pa_i_pvs_lookup_datarootspower_product)) * pa_v_pvs_lookup_datarootspower_product)) /\ exists pa_q_pvs_lookup_datarootspower_product_partial. pa_u_pvs_lookup_datarootspower_product = pa_q_pvs_lookup_datarootspower_product_partial * S ((S (pa_i_pvs_lookup_datarootspower_product)) * pa_v_pvs_lookup_datarootspower_product) + (pa_r_pvs_lookup_datarootspower_product))) /\ ((((exists pa_h_pvs_lookup_datarootspower_product_successor. pa_h_pvs_lookup_datarootspower_product_successor + S (pa_s_pvs_lookup_datarootspower_product) = S ((S (S pa_i_pvs_lookup_datarootspower_product)) * pa_v_pvs_lookup_datarootspower_product)) /\ exists pa_q_pvs_lookup_datarootspower_product_successor. pa_u_pvs_lookup_datarootspower_product = pa_q_pvs_lookup_datarootspower_product_successor * S ((S (S pa_i_pvs_lookup_datarootspower_product)) * pa_v_pvs_lookup_datarootspower_product) + (pa_s_pvs_lookup_datarootspower_product))) /\ pa_s_pvs_lookup_datarootspower_product = pa_r_pvs_lookup_datarootspower_product * pa_p_pvs_lookup_datarootspower_product))))))))))))))))))) -> ~(k = 0) -> (exists pvs_factor_lookup_degree. (g) = (k) * pvs_factor_lookup_degree) -> exists r. (((exists ff_h_pvs_lookup_decoded. ff_h_pvs_lookup_decoded + S (r) = S ((S (k)) * rc)) /\ exists ff_q_pvs_lookup_decoded. rb = ff_q_pvs_lookup_decoded * S ((S (k)) * rc) + (r))) /\ (exists pa_b_pvs_lookup_power pa_c_pvs_lookup_power. ((forall pa_i_pvs_lookup_power_repeat. (exists pa_lt_pvs_lookup_power_repeat_bound. pa_lt_pvs_lookup_power_repeat_bound + S pa_i_pvs_lookup_power_repeat = k) -> (((exists pa_h_pvs_lookup_power_repeat_decoded. pa_h_pvs_lookup_power_repeat_decoded + S (r) = S ((S (pa_i_pvs_lookup_power_repeat)) * pa_c_pvs_lookup_power)) /\ exists pa_q_pvs_lookup_power_repeat_decoded. pa_b_pvs_lookup_power = pa_q_pvs_lookup_power_repeat_decoded * S ((S (pa_i_pvs_lookup_power_repeat)) * pa_c_pvs_lookup_power) + (r)))) /\ (exists pa_u_pvs_lookup_power_product pa_v_pvs_lookup_power_product. ((((exists pa_h_pvs_lookup_power_product_start. pa_h_pvs_lookup_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_lookup_power_product)) /\ exists pa_q_pvs_lookup_power_product_start. pa_u_pvs_lookup_power_product = pa_q_pvs_lookup_power_product_start * S ((S (0)) * pa_v_pvs_lookup_power_product) + (1))) /\ ((((exists pa_h_pvs_lookup_power_product_terminal. pa_h_pvs_lookup_power_product_terminal + S (n) = S ((S (k)) * pa_v_pvs_lookup_power_product)) /\ exists pa_q_pvs_lookup_power_product_terminal. pa_u_pvs_lookup_power_product = pa_q_pvs_lookup_power_product_terminal * S ((S (k)) * pa_v_pvs_lookup_power_product) + (n))) /\ forall pa_i_pvs_lookup_power_product. (exists pa_lt_pvs_lookup_power_product_bound. pa_lt_pvs_lookup_power_product_bound + S pa_i_pvs_lookup_power_product = k) -> exists pa_p_pvs_lookup_power_product pa_r_pvs_lookup_power_product pa_s_pvs_lookup_power_product. ((((exists pa_h_pvs_lookup_power_product_factor. pa_h_pvs_lookup_power_product_factor + S (pa_p_pvs_lookup_power_product) = S ((S (pa_i_pvs_lookup_power_product)) * pa_c_pvs_lookup_power)) /\ exists pa_q_pvs_lookup_power_product_factor. pa_b_pvs_lookup_power = pa_q_pvs_lookup_power_product_factor * S ((S (pa_i_pvs_lookup_power_product)) * pa_c_pvs_lookup_power) + (pa_p_pvs_lookup_power_product))) /\ ((((exists pa_h_pvs_lookup_power_product_partial. pa_h_pvs_lookup_power_product_partial + S (pa_r_pvs_lookup_power_product) = S ((S (pa_i_pvs_lookup_power_product)) * pa_v_pvs_lookup_power_product)) /\ exists pa_q_pvs_lookup_power_product_partial. pa_u_pvs_lookup_power_product = pa_q_pvs_lookup_power_product_partial * S ((S (pa_i_pvs_lookup_power_product)) * pa_v_pvs_lookup_power_product) + (pa_r_pvs_lookup_power_product))) /\ ((((exists pa_h_pvs_lookup_power_product_successor. pa_h_pvs_lookup_power_product_successor + S (pa_s_pvs_lookup_power_product) = S ((S (S pa_i_pvs_lookup_power_product)) * pa_v_pvs_lookup_power_product)) /\ exists pa_q_pvs_lookup_power_product_successor. pa_u_pvs_lookup_power_product = pa_q_pvs_lookup_power_product_successor * S ((S (S pa_i_pvs_lookup_power_product)) * pa_v_pvs_lookup_power_product) + (pa_s_pvs_lookup_power_product))) /\ pa_s_pvs_lookup_power_product = pa_r_pvs_lookup_power_product * pa_p_pvs_lookup_power_product))))))))