lte_power_difference_valuation_step

Exact expanded first-order arithmetic statement

forall p a b d n A B Q e f g. e + f = g -> (~((p) = 1) /\ forall pvs_left_valuation_step_prime pvs_right_valuation_step_prime. (p) = pvs_left_valuation_step_prime * pvs_right_valuation_step_prime -> pvs_left_valuation_step_prime = 1 \/ pvs_right_valuation_step_prime = 1) -> ~(d = 0) -> (exists olte_factor_valuation_step_divisor. (d) = (p) * olte_factor_valuation_step_divisor) -> ~(exists olte_factor_valuation_step_base. (b) = (p) * olte_factor_valuation_step_base) -> ~(Q = 0) -> (((exists bpd_gap_pvs_valuation_step_input_selected_bound. bpd_gap_pvs_valuation_step_input_selected_bound + (e) = (d)) /\ (exists bpvi_result_pvs_valuation_step_input_selected. ((exists bpvi_b_pvs_valuation_step_input_selected_power bpvi_c_pvs_valuation_step_input_selected_power. ((forall bpvi_i_pvs_valuation_step_input_selected_power. (exists bpvi_repeat_gap_pvs_valuation_step_input_selected_power. bpvi_repeat_gap_pvs_valuation_step_input_selected_power + S bpvi_i_pvs_valuation_step_input_selected_power = e) -> (((exists bpvi_h_pvs_valuation_step_input_selected_power_repeat. bpvi_h_pvs_valuation_step_input_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_valuation_step_input_selected_power)) * bpvi_c_pvs_valuation_step_input_selected_power)) /\ exists bpvi_q_pvs_valuation_step_input_selected_power_repeat. bpvi_b_pvs_valuation_step_input_selected_power = bpvi_q_pvs_valuation_step_input_selected_power_repeat * S ((S (bpvi_i_pvs_valuation_step_input_selected_power)) * bpvi_c_pvs_valuation_step_input_selected_power) + (p)))) /\ (exists bpvi_u_pvs_valuation_step_input_selected_power bpvi_v_pvs_valuation_step_input_selected_power. ((((exists bpvi_h_pvs_valuation_step_input_selected_power_start. bpvi_h_pvs_valuation_step_input_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_valuation_step_input_selected_power)) /\ exists bpvi_q_pvs_valuation_step_input_selected_power_start. bpvi_u_pvs_valuation_step_input_selected_power = bpvi_q_pvs_valuation_step_input_selected_power_start * S ((S (0)) * bpvi_v_pvs_valuation_step_input_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_valuation_step_input_selected_power_terminal. bpvi_h_pvs_valuation_step_input_selected_power_terminal + S (bpvi_result_pvs_valuation_step_input_selected) = S ((S (e)) * bpvi_v_pvs_valuation_step_input_selected_power)) /\ exists bpvi_q_pvs_valuation_step_input_selected_power_terminal. bpvi_u_pvs_valuation_step_input_selected_power = bpvi_q_pvs_valuation_step_input_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_valuation_step_input_selected_power) + (bpvi_result_pvs_valuation_step_input_selected))) /\ forall bpvi_j_pvs_valuation_step_input_selected_power. (exists bpvi_product_gap_pvs_valuation_step_input_selected_power. bpvi_product_gap_pvs_valuation_step_input_selected_power + S bpvi_j_pvs_valuation_step_input_selected_power = e) -> exists bpvi_factor_pvs_valuation_step_input_selected_power bpvi_partial_pvs_valuation_step_input_selected_power bpvi_successor_pvs_valuation_step_input_selected_power. ((((exists bpvi_h_pvs_valuation_step_input_selected_power_factor. bpvi_h_pvs_valuation_step_input_selected_power_factor + S (bpvi_factor_pvs_valuation_step_input_selected_power) = S ((S (bpvi_j_pvs_valuation_step_input_selected_power)) * bpvi_c_pvs_valuation_step_input_selected_power)) /\ exists bpvi_q_pvs_valuation_step_input_selected_power_factor. bpvi_b_pvs_valuation_step_input_selected_power = bpvi_q_pvs_valuation_step_input_selected_power_factor * S ((S (bpvi_j_pvs_valuation_step_input_selected_power)) * bpvi_c_pvs_valuation_step_input_selected_power) + (bpvi_factor_pvs_valuation_step_input_selected_power))) /\ ((((exists bpvi_h_pvs_valuation_step_input_selected_power_partial. bpvi_h_pvs_valuation_step_input_selected_power_partial + S (bpvi_partial_pvs_valuation_step_input_selected_power) = S ((S (bpvi_j_pvs_valuation_step_input_selected_power)) * bpvi_v_pvs_valuation_step_input_selected_power)) /\ exists bpvi_q_pvs_valuation_step_input_selected_power_partial. bpvi_u_pvs_valuation_step_input_selected_power = bpvi_q_pvs_valuation_step_input_selected_power_partial * S ((S (bpvi_j_pvs_valuation_step_input_selected_power)) * bpvi_v_pvs_valuation_step_input_selected_power) + (bpvi_partial_pvs_valuation_step_input_selected_power))) /\ ((((exists bpvi_h_pvs_valuation_step_input_selected_power_successor. bpvi_h_pvs_valuation_step_input_selected_power_successor + S (bpvi_successor_pvs_valuation_step_input_selected_power) = S ((S (S bpvi_j_pvs_valuation_step_input_selected_power)) * bpvi_v_pvs_valuation_step_input_selected_power)) /\ exists bpvi_q_pvs_valuation_step_input_selected_power_successor. bpvi_u_pvs_valuation_step_input_selected_power = bpvi_q_pvs_valuation_step_input_selected_power_successor * S ((S (S bpvi_j_pvs_valuation_step_input_selected_power)) * bpvi_v_pvs_valuation_step_input_selected_power) + (bpvi_successor_pvs_valuation_step_input_selected_power))) /\ bpvi_successor_pvs_valuation_step_input_selected_power = bpvi_partial_pvs_valuation_step_input_selected_power * bpvi_factor_pvs_valuation_step_input_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_valuation_step_input_selected. d = bpvi_result_pvs_valuation_step_input_selected * bpvi_divisor_factor_pvs_valuation_step_input_selected))) /\ forall bpd_candidate_pvs_valuation_step_input. (exists bpd_gap_pvs_valuation_step_input_candidate_bound. bpd_gap_pvs_valuation_step_input_candidate_bound + (bpd_candidate_pvs_valuation_step_input) = (d)) -> (exists bpvi_result_pvs_valuation_step_input_candidate. ((exists bpvi_b_pvs_valuation_step_input_candidate_power bpvi_c_pvs_valuation_step_input_candidate_power. ((forall bpvi_i_pvs_valuation_step_input_candidate_power. (exists bpvi_repeat_gap_pvs_valuation_step_input_candidate_power. bpvi_repeat_gap_pvs_valuation_step_input_candidate_power + S bpvi_i_pvs_valuation_step_input_candidate_power = bpd_candidate_pvs_valuation_step_input) -> (((exists bpvi_h_pvs_valuation_step_input_candidate_power_repeat. bpvi_h_pvs_valuation_step_input_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_valuation_step_input_candidate_power)) * bpvi_c_pvs_valuation_step_input_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_input_candidate_power_repeat. bpvi_b_pvs_valuation_step_input_candidate_power = bpvi_q_pvs_valuation_step_input_candidate_power_repeat * S ((S (bpvi_i_pvs_valuation_step_input_candidate_power)) * bpvi_c_pvs_valuation_step_input_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_valuation_step_input_candidate_power bpvi_v_pvs_valuation_step_input_candidate_power. ((((exists bpvi_h_pvs_valuation_step_input_candidate_power_start. bpvi_h_pvs_valuation_step_input_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_valuation_step_input_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_input_candidate_power_start. bpvi_u_pvs_valuation_step_input_candidate_power = bpvi_q_pvs_valuation_step_input_candidate_power_start * S ((S (0)) * bpvi_v_pvs_valuation_step_input_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_valuation_step_input_candidate_power_terminal. bpvi_h_pvs_valuation_step_input_candidate_power_terminal + S (bpvi_result_pvs_valuation_step_input_candidate) = S ((S (bpd_candidate_pvs_valuation_step_input)) * bpvi_v_pvs_valuation_step_input_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_input_candidate_power_terminal. bpvi_u_pvs_valuation_step_input_candidate_power = bpvi_q_pvs_valuation_step_input_candidate_power_terminal * S ((S (bpd_candidate_pvs_valuation_step_input)) * bpvi_v_pvs_valuation_step_input_candidate_power) + (bpvi_result_pvs_valuation_step_input_candidate))) /\ forall bpvi_j_pvs_valuation_step_input_candidate_power. (exists bpvi_product_gap_pvs_valuation_step_input_candidate_power. bpvi_product_gap_pvs_valuation_step_input_candidate_power + S bpvi_j_pvs_valuation_step_input_candidate_power = bpd_candidate_pvs_valuation_step_input) -> exists bpvi_factor_pvs_valuation_step_input_candidate_power bpvi_partial_pvs_valuation_step_input_candidate_power bpvi_successor_pvs_valuation_step_input_candidate_power. ((((exists bpvi_h_pvs_valuation_step_input_candidate_power_factor. bpvi_h_pvs_valuation_step_input_candidate_power_factor + S (bpvi_factor_pvs_valuation_step_input_candidate_power) = S ((S (bpvi_j_pvs_valuation_step_input_candidate_power)) * bpvi_c_pvs_valuation_step_input_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_input_candidate_power_factor. bpvi_b_pvs_valuation_step_input_candidate_power = bpvi_q_pvs_valuation_step_input_candidate_power_factor * S ((S (bpvi_j_pvs_valuation_step_input_candidate_power)) * bpvi_c_pvs_valuation_step_input_candidate_power) + (bpvi_factor_pvs_valuation_step_input_candidate_power))) /\ ((((exists bpvi_h_pvs_valuation_step_input_candidate_power_partial. bpvi_h_pvs_valuation_step_input_candidate_power_partial + S (bpvi_partial_pvs_valuation_step_input_candidate_power) = S ((S (bpvi_j_pvs_valuation_step_input_candidate_power)) * bpvi_v_pvs_valuation_step_input_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_input_candidate_power_partial. bpvi_u_pvs_valuation_step_input_candidate_power = bpvi_q_pvs_valuation_step_input_candidate_power_partial * S ((S (bpvi_j_pvs_valuation_step_input_candidate_power)) * bpvi_v_pvs_valuation_step_input_candidate_power) + (bpvi_partial_pvs_valuation_step_input_candidate_power))) /\ ((((exists bpvi_h_pvs_valuation_step_input_candidate_power_successor. bpvi_h_pvs_valuation_step_input_candidate_power_successor + S (bpvi_successor_pvs_valuation_step_input_candidate_power) = S ((S (S bpvi_j_pvs_valuation_step_input_candidate_power)) * bpvi_v_pvs_valuation_step_input_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_input_candidate_power_successor. bpvi_u_pvs_valuation_step_input_candidate_power = bpvi_q_pvs_valuation_step_input_candidate_power_successor * S ((S (S bpvi_j_pvs_valuation_step_input_candidate_power)) * bpvi_v_pvs_valuation_step_input_candidate_power) + (bpvi_successor_pvs_valuation_step_input_candidate_power))) /\ bpvi_successor_pvs_valuation_step_input_candidate_power = bpvi_partial_pvs_valuation_step_input_candidate_power * bpvi_factor_pvs_valuation_step_input_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_valuation_step_input_candidate. d = bpvi_result_pvs_valuation_step_input_candidate * bpvi_divisor_factor_pvs_valuation_step_input_candidate)) -> (exists bpd_gap_pvs_valuation_step_input_maximal. bpd_gap_pvs_valuation_step_input_maximal + (bpd_candidate_pvs_valuation_step_input) = (e))) -> (((exists bpd_gap_pvs_valuation_step_quotient_selected_bound. bpd_gap_pvs_valuation_step_quotient_selected_bound + (f) = (Q)) /\ (exists bpvi_result_pvs_valuation_step_quotient_selected. ((exists bpvi_b_pvs_valuation_step_quotient_selected_power bpvi_c_pvs_valuation_step_quotient_selected_power. ((forall bpvi_i_pvs_valuation_step_quotient_selected_power. (exists bpvi_repeat_gap_pvs_valuation_step_quotient_selected_power. bpvi_repeat_gap_pvs_valuation_step_quotient_selected_power + S bpvi_i_pvs_valuation_step_quotient_selected_power = f) -> (((exists bpvi_h_pvs_valuation_step_quotient_selected_power_repeat. bpvi_h_pvs_valuation_step_quotient_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_valuation_step_quotient_selected_power)) * bpvi_c_pvs_valuation_step_quotient_selected_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_selected_power_repeat. bpvi_b_pvs_valuation_step_quotient_selected_power = bpvi_q_pvs_valuation_step_quotient_selected_power_repeat * S ((S (bpvi_i_pvs_valuation_step_quotient_selected_power)) * bpvi_c_pvs_valuation_step_quotient_selected_power) + (p)))) /\ (exists bpvi_u_pvs_valuation_step_quotient_selected_power bpvi_v_pvs_valuation_step_quotient_selected_power. ((((exists bpvi_h_pvs_valuation_step_quotient_selected_power_start. bpvi_h_pvs_valuation_step_quotient_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_valuation_step_quotient_selected_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_selected_power_start. bpvi_u_pvs_valuation_step_quotient_selected_power = bpvi_q_pvs_valuation_step_quotient_selected_power_start * S ((S (0)) * bpvi_v_pvs_valuation_step_quotient_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_valuation_step_quotient_selected_power_terminal. bpvi_h_pvs_valuation_step_quotient_selected_power_terminal + S (bpvi_result_pvs_valuation_step_quotient_selected) = S ((S (f)) * bpvi_v_pvs_valuation_step_quotient_selected_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_selected_power_terminal. bpvi_u_pvs_valuation_step_quotient_selected_power = bpvi_q_pvs_valuation_step_quotient_selected_power_terminal * S ((S (f)) * bpvi_v_pvs_valuation_step_quotient_selected_power) + (bpvi_result_pvs_valuation_step_quotient_selected))) /\ forall bpvi_j_pvs_valuation_step_quotient_selected_power. (exists bpvi_product_gap_pvs_valuation_step_quotient_selected_power. bpvi_product_gap_pvs_valuation_step_quotient_selected_power + S bpvi_j_pvs_valuation_step_quotient_selected_power = f) -> exists bpvi_factor_pvs_valuation_step_quotient_selected_power bpvi_partial_pvs_valuation_step_quotient_selected_power bpvi_successor_pvs_valuation_step_quotient_selected_power. ((((exists bpvi_h_pvs_valuation_step_quotient_selected_power_factor. bpvi_h_pvs_valuation_step_quotient_selected_power_factor + S (bpvi_factor_pvs_valuation_step_quotient_selected_power) = S ((S (bpvi_j_pvs_valuation_step_quotient_selected_power)) * bpvi_c_pvs_valuation_step_quotient_selected_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_selected_power_factor. bpvi_b_pvs_valuation_step_quotient_selected_power = bpvi_q_pvs_valuation_step_quotient_selected_power_factor * S ((S (bpvi_j_pvs_valuation_step_quotient_selected_power)) * bpvi_c_pvs_valuation_step_quotient_selected_power) + (bpvi_factor_pvs_valuation_step_quotient_selected_power))) /\ ((((exists bpvi_h_pvs_valuation_step_quotient_selected_power_partial. bpvi_h_pvs_valuation_step_quotient_selected_power_partial + S (bpvi_partial_pvs_valuation_step_quotient_selected_power) = S ((S (bpvi_j_pvs_valuation_step_quotient_selected_power)) * bpvi_v_pvs_valuation_step_quotient_selected_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_selected_power_partial. bpvi_u_pvs_valuation_step_quotient_selected_power = bpvi_q_pvs_valuation_step_quotient_selected_power_partial * S ((S (bpvi_j_pvs_valuation_step_quotient_selected_power)) * bpvi_v_pvs_valuation_step_quotient_selected_power) + (bpvi_partial_pvs_valuation_step_quotient_selected_power))) /\ ((((exists bpvi_h_pvs_valuation_step_quotient_selected_power_successor. bpvi_h_pvs_valuation_step_quotient_selected_power_successor + S (bpvi_successor_pvs_valuation_step_quotient_selected_power) = S ((S (S bpvi_j_pvs_valuation_step_quotient_selected_power)) * bpvi_v_pvs_valuation_step_quotient_selected_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_selected_power_successor. bpvi_u_pvs_valuation_step_quotient_selected_power = bpvi_q_pvs_valuation_step_quotient_selected_power_successor * S ((S (S bpvi_j_pvs_valuation_step_quotient_selected_power)) * bpvi_v_pvs_valuation_step_quotient_selected_power) + (bpvi_successor_pvs_valuation_step_quotient_selected_power))) /\ bpvi_successor_pvs_valuation_step_quotient_selected_power = bpvi_partial_pvs_valuation_step_quotient_selected_power * bpvi_factor_pvs_valuation_step_quotient_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_valuation_step_quotient_selected. Q = bpvi_result_pvs_valuation_step_quotient_selected * bpvi_divisor_factor_pvs_valuation_step_quotient_selected))) /\ forall bpd_candidate_pvs_valuation_step_quotient. (exists bpd_gap_pvs_valuation_step_quotient_candidate_bound. bpd_gap_pvs_valuation_step_quotient_candidate_bound + (bpd_candidate_pvs_valuation_step_quotient) = (Q)) -> (exists bpvi_result_pvs_valuation_step_quotient_candidate. ((exists bpvi_b_pvs_valuation_step_quotient_candidate_power bpvi_c_pvs_valuation_step_quotient_candidate_power. ((forall bpvi_i_pvs_valuation_step_quotient_candidate_power. (exists bpvi_repeat_gap_pvs_valuation_step_quotient_candidate_power. bpvi_repeat_gap_pvs_valuation_step_quotient_candidate_power + S bpvi_i_pvs_valuation_step_quotient_candidate_power = bpd_candidate_pvs_valuation_step_quotient) -> (((exists bpvi_h_pvs_valuation_step_quotient_candidate_power_repeat. bpvi_h_pvs_valuation_step_quotient_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_valuation_step_quotient_candidate_power)) * bpvi_c_pvs_valuation_step_quotient_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_candidate_power_repeat. bpvi_b_pvs_valuation_step_quotient_candidate_power = bpvi_q_pvs_valuation_step_quotient_candidate_power_repeat * S ((S (bpvi_i_pvs_valuation_step_quotient_candidate_power)) * bpvi_c_pvs_valuation_step_quotient_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_valuation_step_quotient_candidate_power bpvi_v_pvs_valuation_step_quotient_candidate_power. ((((exists bpvi_h_pvs_valuation_step_quotient_candidate_power_start. bpvi_h_pvs_valuation_step_quotient_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_valuation_step_quotient_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_candidate_power_start. bpvi_u_pvs_valuation_step_quotient_candidate_power = bpvi_q_pvs_valuation_step_quotient_candidate_power_start * S ((S (0)) * bpvi_v_pvs_valuation_step_quotient_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_valuation_step_quotient_candidate_power_terminal. bpvi_h_pvs_valuation_step_quotient_candidate_power_terminal + S (bpvi_result_pvs_valuation_step_quotient_candidate) = S ((S (bpd_candidate_pvs_valuation_step_quotient)) * bpvi_v_pvs_valuation_step_quotient_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_candidate_power_terminal. bpvi_u_pvs_valuation_step_quotient_candidate_power = bpvi_q_pvs_valuation_step_quotient_candidate_power_terminal * S ((S (bpd_candidate_pvs_valuation_step_quotient)) * bpvi_v_pvs_valuation_step_quotient_candidate_power) + (bpvi_result_pvs_valuation_step_quotient_candidate))) /\ forall bpvi_j_pvs_valuation_step_quotient_candidate_power. (exists bpvi_product_gap_pvs_valuation_step_quotient_candidate_power. bpvi_product_gap_pvs_valuation_step_quotient_candidate_power + S bpvi_j_pvs_valuation_step_quotient_candidate_power = bpd_candidate_pvs_valuation_step_quotient) -> exists bpvi_factor_pvs_valuation_step_quotient_candidate_power bpvi_partial_pvs_valuation_step_quotient_candidate_power bpvi_successor_pvs_valuation_step_quotient_candidate_power. ((((exists bpvi_h_pvs_valuation_step_quotient_candidate_power_factor. bpvi_h_pvs_valuation_step_quotient_candidate_power_factor + S (bpvi_factor_pvs_valuation_step_quotient_candidate_power) = S ((S (bpvi_j_pvs_valuation_step_quotient_candidate_power)) * bpvi_c_pvs_valuation_step_quotient_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_candidate_power_factor. bpvi_b_pvs_valuation_step_quotient_candidate_power = bpvi_q_pvs_valuation_step_quotient_candidate_power_factor * S ((S (bpvi_j_pvs_valuation_step_quotient_candidate_power)) * bpvi_c_pvs_valuation_step_quotient_candidate_power) + (bpvi_factor_pvs_valuation_step_quotient_candidate_power))) /\ ((((exists bpvi_h_pvs_valuation_step_quotient_candidate_power_partial. bpvi_h_pvs_valuation_step_quotient_candidate_power_partial + S (bpvi_partial_pvs_valuation_step_quotient_candidate_power) = S ((S (bpvi_j_pvs_valuation_step_quotient_candidate_power)) * bpvi_v_pvs_valuation_step_quotient_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_candidate_power_partial. bpvi_u_pvs_valuation_step_quotient_candidate_power = bpvi_q_pvs_valuation_step_quotient_candidate_power_partial * S ((S (bpvi_j_pvs_valuation_step_quotient_candidate_power)) * bpvi_v_pvs_valuation_step_quotient_candidate_power) + (bpvi_partial_pvs_valuation_step_quotient_candidate_power))) /\ ((((exists bpvi_h_pvs_valuation_step_quotient_candidate_power_successor. bpvi_h_pvs_valuation_step_quotient_candidate_power_successor + S (bpvi_successor_pvs_valuation_step_quotient_candidate_power) = S ((S (S bpvi_j_pvs_valuation_step_quotient_candidate_power)) * bpvi_v_pvs_valuation_step_quotient_candidate_power)) /\ exists bpvi_q_pvs_valuation_step_quotient_candidate_power_successor. bpvi_u_pvs_valuation_step_quotient_candidate_power = bpvi_q_pvs_valuation_step_quotient_candidate_power_successor * S ((S (S bpvi_j_pvs_valuation_step_quotient_candidate_power)) * bpvi_v_pvs_valuation_step_quotient_candidate_power) + (bpvi_successor_pvs_valuation_step_quotient_candidate_power))) /\ bpvi_successor_pvs_valuation_step_quotient_candidate_power = bpvi_partial_pvs_valuation_step_quotient_candidate_power * bpvi_factor_pvs_valuation_step_quotient_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_valuation_step_quotient_candidate. Q = bpvi_result_pvs_valuation_step_quotient_candidate * bpvi_divisor_factor_pvs_valuation_step_quotient_candidate)) -> (exists bpd_gap_pvs_valuation_step_quotient_maximal. bpd_gap_pvs_valuation_step_quotient_maximal + (bpd_candidate_pvs_valuation_step_quotient) = (f))) -> (exists pa_b_olte_valuation_step_A pa_c_olte_valuation_step_A. ((forall pa_i_olte_valuation_step_A_repeat. (exists pa_lt_olte_valuation_step_A_repeat_bound. pa_lt_olte_valuation_step_A_repeat_bound + S pa_i_olte_valuation_step_A_repeat = n) -> (((exists pa_h_olte_valuation_step_A_repeat_decoded. pa_h_olte_valuation_step_A_repeat_decoded + S (a) = S ((S (pa_i_olte_valuation_step_A_repeat)) * pa_c_olte_valuation_step_A)) /\ exists pa_q_olte_valuation_step_A_repeat_decoded. pa_b_olte_valuation_step_A = pa_q_olte_valuation_step_A_repeat_decoded * S ((S (pa_i_olte_valuation_step_A_repeat)) * pa_c_olte_valuation_step_A) + (a)))) /\ (exists pa_u_olte_valuation_step_A_product pa_v_olte_valuation_step_A_product. ((((exists pa_h_olte_valuation_step_A_product_start. pa_h_olte_valuation_step_A_product_start + S (1) = S ((S (0)) * pa_v_olte_valuation_step_A_product)) /\ exists pa_q_olte_valuation_step_A_product_start. pa_u_olte_valuation_step_A_product = pa_q_olte_valuation_step_A_product_start * S ((S (0)) * pa_v_olte_valuation_step_A_product) + (1))) /\ ((((exists pa_h_olte_valuation_step_A_product_terminal. pa_h_olte_valuation_step_A_product_terminal + S (A) = S ((S (n)) * pa_v_olte_valuation_step_A_product)) /\ exists pa_q_olte_valuation_step_A_product_terminal. pa_u_olte_valuation_step_A_product = pa_q_olte_valuation_step_A_product_terminal * S ((S (n)) * pa_v_olte_valuation_step_A_product) + (A))) /\ forall pa_i_olte_valuation_step_A_product. (exists pa_lt_olte_valuation_step_A_product_bound. pa_lt_olte_valuation_step_A_product_bound + S pa_i_olte_valuation_step_A_product = n) -> exists pa_p_olte_valuation_step_A_product pa_r_olte_valuation_step_A_product pa_s_olte_valuation_step_A_product. ((((exists pa_h_olte_valuation_step_A_product_factor. pa_h_olte_valuation_step_A_product_factor + S (pa_p_olte_valuation_step_A_product) = S ((S (pa_i_olte_valuation_step_A_product)) * pa_c_olte_valuation_step_A)) /\ exists pa_q_olte_valuation_step_A_product_factor. pa_b_olte_valuation_step_A = pa_q_olte_valuation_step_A_product_factor * S ((S (pa_i_olte_valuation_step_A_product)) * pa_c_olte_valuation_step_A) + (pa_p_olte_valuation_step_A_product))) /\ ((((exists pa_h_olte_valuation_step_A_product_partial. pa_h_olte_valuation_step_A_product_partial + S (pa_r_olte_valuation_step_A_product) = S ((S (pa_i_olte_valuation_step_A_product)) * pa_v_olte_valuation_step_A_product)) /\ exists pa_q_olte_valuation_step_A_product_partial. pa_u_olte_valuation_step_A_product = pa_q_olte_valuation_step_A_product_partial * S ((S (pa_i_olte_valuation_step_A_product)) * pa_v_olte_valuation_step_A_product) + (pa_r_olte_valuation_step_A_product))) /\ ((((exists pa_h_olte_valuation_step_A_product_successor. pa_h_olte_valuation_step_A_product_successor + S (pa_s_olte_valuation_step_A_product) = S ((S (S pa_i_olte_valuation_step_A_product)) * pa_v_olte_valuation_step_A_product)) /\ exists pa_q_olte_valuation_step_A_product_successor. pa_u_olte_valuation_step_A_product = pa_q_olte_valuation_step_A_product_successor * S ((S (S pa_i_olte_valuation_step_A_product)) * pa_v_olte_valuation_step_A_product) + (pa_s_olte_valuation_step_A_product))) /\ pa_s_olte_valuation_step_A_product = pa_r_olte_valuation_step_A_product * pa_p_olte_valuation_step_A_product)))))))) -> (exists pa_b_olte_valuation_step_B pa_c_olte_valuation_step_B. ((forall pa_i_olte_valuation_step_B_repeat. (exists pa_lt_olte_valuation_step_B_repeat_bound. pa_lt_olte_valuation_step_B_repeat_bound + S pa_i_olte_valuation_step_B_repeat = n) -> (((exists pa_h_olte_valuation_step_B_repeat_decoded. pa_h_olte_valuation_step_B_repeat_decoded + S (b) = S ((S (pa_i_olte_valuation_step_B_repeat)) * pa_c_olte_valuation_step_B)) /\ exists pa_q_olte_valuation_step_B_repeat_decoded. pa_b_olte_valuation_step_B = pa_q_olte_valuation_step_B_repeat_decoded * S ((S (pa_i_olte_valuation_step_B_repeat)) * pa_c_olte_valuation_step_B) + (b)))) /\ (exists pa_u_olte_valuation_step_B_product pa_v_olte_valuation_step_B_product. ((((exists pa_h_olte_valuation_step_B_product_start. pa_h_olte_valuation_step_B_product_start + S (1) = S ((S (0)) * pa_v_olte_valuation_step_B_product)) /\ exists pa_q_olte_valuation_step_B_product_start. pa_u_olte_valuation_step_B_product = pa_q_olte_valuation_step_B_product_start * S ((S (0)) * pa_v_olte_valuation_step_B_product) + (1))) /\ ((((exists pa_h_olte_valuation_step_B_product_terminal. pa_h_olte_valuation_step_B_product_terminal + S (B) = S ((S (n)) * pa_v_olte_valuation_step_B_product)) /\ exists pa_q_olte_valuation_step_B_product_terminal. pa_u_olte_valuation_step_B_product = pa_q_olte_valuation_step_B_product_terminal * S ((S (n)) * pa_v_olte_valuation_step_B_product) + (B))) /\ forall pa_i_olte_valuation_step_B_product. (exists pa_lt_olte_valuation_step_B_product_bound. pa_lt_olte_valuation_step_B_product_bound + S pa_i_olte_valuation_step_B_product = n) -> exists pa_p_olte_valuation_step_B_product pa_r_olte_valuation_step_B_product pa_s_olte_valuation_step_B_product. ((((exists pa_h_olte_valuation_step_B_product_factor. pa_h_olte_valuation_step_B_product_factor + S (pa_p_olte_valuation_step_B_product) = S ((S (pa_i_olte_valuation_step_B_product)) * pa_c_olte_valuation_step_B)) /\ exists pa_q_olte_valuation_step_B_product_factor. pa_b_olte_valuation_step_B = pa_q_olte_valuation_step_B_product_factor * S ((S (pa_i_olte_valuation_step_B_product)) * pa_c_olte_valuation_step_B) + (pa_p_olte_valuation_step_B_product))) /\ ((((exists pa_h_olte_valuation_step_B_product_partial. pa_h_olte_valuation_step_B_product_partial + S (pa_r_olte_valuation_step_B_product) = S ((S (pa_i_olte_valuation_step_B_product)) * pa_v_olte_valuation_step_B_product)) /\ exists pa_q_olte_valuation_step_B_product_partial. pa_u_olte_valuation_step_B_product = pa_q_olte_valuation_step_B_product_partial * S ((S (pa_i_olte_valuation_step_B_product)) * pa_v_olte_valuation_step_B_product) + (pa_r_olte_valuation_step_B_product))) /\ ((((exists pa_h_olte_valuation_step_B_product_successor. pa_h_olte_valuation_step_B_product_successor + S (pa_s_olte_valuation_step_B_product) = S ((S (S pa_i_olte_valuation_step_B_product)) * pa_v_olte_valuation_step_B_product)) /\ exists pa_q_olte_valuation_step_B_product_successor. pa_u_olte_valuation_step_B_product = pa_q_olte_valuation_step_B_product_successor * S ((S (S pa_i_olte_valuation_step_B_product)) * pa_v_olte_valuation_step_B_product) + (pa_s_olte_valuation_step_B_product))) /\ pa_s_olte_valuation_step_B_product = pa_r_olte_valuation_step_B_product * pa_p_olte_valuation_step_B_product)))))))) -> A = B + d * Q -> (((exists pa_b_olte_valuation_step_resultA pa_c_olte_valuation_step_resultA. ((forall pa_i_olte_valuation_step_resultA_repeat. (exists pa_lt_olte_valuation_step_resultA_repeat_bound. pa_lt_olte_valuation_step_resultA_repeat_bound + S pa_i_olte_valuation_step_resultA_repeat = n) -> (((exists pa_h_olte_valuation_step_resultA_repeat_decoded. pa_h_olte_valuation_step_resultA_repeat_decoded + S (a) = S ((S (pa_i_olte_valuation_step_resultA_repeat)) * pa_c_olte_valuation_step_resultA)) /\ exists pa_q_olte_valuation_step_resultA_repeat_decoded. pa_b_olte_valuation_step_resultA = pa_q_olte_valuation_step_resultA_repeat_decoded * S ((S (pa_i_olte_valuation_step_resultA_repeat)) * pa_c_olte_valuation_step_resultA) + (a)))) /\ (exists pa_u_olte_valuation_step_resultA_product pa_v_olte_valuation_step_resultA_product. ((((exists pa_h_olte_valuation_step_resultA_product_start. pa_h_olte_valuation_step_resultA_product_start + S (1) = S ((S (0)) * pa_v_olte_valuation_step_resultA_product)) /\ exists pa_q_olte_valuation_step_resultA_product_start. pa_u_olte_valuation_step_resultA_product = pa_q_olte_valuation_step_resultA_product_start * S ((S (0)) * pa_v_olte_valuation_step_resultA_product) + (1))) /\ ((((exists pa_h_olte_valuation_step_resultA_product_terminal. pa_h_olte_valuation_step_resultA_product_terminal + S (A) = S ((S (n)) * pa_v_olte_valuation_step_resultA_product)) /\ exists pa_q_olte_valuation_step_resultA_product_terminal. pa_u_olte_valuation_step_resultA_product = pa_q_olte_valuation_step_resultA_product_terminal * S ((S (n)) * pa_v_olte_valuation_step_resultA_product) + (A))) /\ forall pa_i_olte_valuation_step_resultA_product. (exists pa_lt_olte_valuation_step_resultA_product_bound. pa_lt_olte_valuation_step_resultA_product_bound + S pa_i_olte_valuation_step_resultA_product = n) -> exists pa_p_olte_valuation_step_resultA_product pa_r_olte_valuation_step_resultA_product pa_s_olte_valuation_step_resultA_product. ((((exists pa_h_olte_valuation_step_resultA_product_factor. pa_h_olte_valuation_step_resultA_product_factor + S (pa_p_olte_valuation_step_resultA_product) = S ((S (pa_i_olte_valuation_step_resultA_product)) * pa_c_olte_valuation_step_resultA)) /\ exists pa_q_olte_valuation_step_resultA_product_factor. pa_b_olte_valuation_step_resultA = pa_q_olte_valuation_step_resultA_product_factor * S ((S (pa_i_olte_valuation_step_resultA_product)) * pa_c_olte_valuation_step_resultA) + (pa_p_olte_valuation_step_resultA_product))) /\ ((((exists pa_h_olte_valuation_step_resultA_product_partial. pa_h_olte_valuation_step_resultA_product_partial + S (pa_r_olte_valuation_step_resultA_product) = S ((S (pa_i_olte_valuation_step_resultA_product)) * pa_v_olte_valuation_step_resultA_product)) /\ exists pa_q_olte_valuation_step_resultA_product_partial. pa_u_olte_valuation_step_resultA_product = pa_q_olte_valuation_step_resultA_product_partial * S ((S (pa_i_olte_valuation_step_resultA_product)) * pa_v_olte_valuation_step_resultA_product) + (pa_r_olte_valuation_step_resultA_product))) /\ ((((exists pa_h_olte_valuation_step_resultA_product_successor. pa_h_olte_valuation_step_resultA_product_successor + S (pa_s_olte_valuation_step_resultA_product) = S ((S (S pa_i_olte_valuation_step_resultA_product)) * pa_v_olte_valuation_step_resultA_product)) /\ exists pa_q_olte_valuation_step_resultA_product_successor. pa_u_olte_valuation_step_resultA_product = pa_q_olte_valuation_step_resultA_product_successor * S ((S (S pa_i_olte_valuation_step_resultA_product)) * pa_v_olte_valuation_step_resultA_product) + (pa_s_olte_valuation_step_resultA_product))) /\ pa_s_olte_valuation_step_resultA_product = pa_r_olte_valuation_step_resultA_product * pa_p_olte_valuation_step_resultA_product)))))))) /\ (((exists pa_b_olte_valuation_step_resultB pa_c_olte_valuation_step_resultB. ((forall pa_i_olte_valuation_step_resultB_repeat. (exists pa_lt_olte_valuation_step_resultB_repeat_bound. pa_lt_olte_valuation_step_resultB_repeat_bound + S pa_i_olte_valuation_step_resultB_repeat = n) -> (((exists pa_h_olte_valuation_step_resultB_repeat_decoded. pa_h_olte_valuation_step_resultB_repeat_decoded + S (b) = S ((S (pa_i_olte_valuation_step_resultB_repeat)) * pa_c_olte_valuation_step_resultB)) /\ exists pa_q_olte_valuation_step_resultB_repeat_decoded. pa_b_olte_valuation_step_resultB = pa_q_olte_valuation_step_resultB_repeat_decoded * S ((S (pa_i_olte_valuation_step_resultB_repeat)) * pa_c_olte_valuation_step_resultB) + (b)))) /\ (exists pa_u_olte_valuation_step_resultB_product pa_v_olte_valuation_step_resultB_product. ((((exists pa_h_olte_valuation_step_resultB_product_start. pa_h_olte_valuation_step_resultB_product_start + S (1) = S ((S (0)) * pa_v_olte_valuation_step_resultB_product)) /\ exists pa_q_olte_valuation_step_resultB_product_start. pa_u_olte_valuation_step_resultB_product = pa_q_olte_valuation_step_resultB_product_start * S ((S (0)) * pa_v_olte_valuation_step_resultB_product) + (1))) /\ ((((exists pa_h_olte_valuation_step_resultB_product_terminal. pa_h_olte_valuation_step_resultB_product_terminal + S (B) = S ((S (n)) * pa_v_olte_valuation_step_resultB_product)) /\ exists pa_q_olte_valuation_step_resultB_product_terminal. pa_u_olte_valuation_step_resultB_product = pa_q_olte_valuation_step_resultB_product_terminal * S ((S (n)) * pa_v_olte_valuation_step_resultB_product) + (B))) /\ forall pa_i_olte_valuation_step_resultB_product. (exists pa_lt_olte_valuation_step_resultB_product_bound. pa_lt_olte_valuation_step_resultB_product_bound + S pa_i_olte_valuation_step_resultB_product = n) -> exists pa_p_olte_valuation_step_resultB_product pa_r_olte_valuation_step_resultB_product pa_s_olte_valuation_step_resultB_product. ((((exists pa_h_olte_valuation_step_resultB_product_factor. pa_h_olte_valuation_step_resultB_product_factor + S (pa_p_olte_valuation_step_resultB_product) = S ((S (pa_i_olte_valuation_step_resultB_product)) * pa_c_olte_valuation_step_resultB)) /\ exists pa_q_olte_valuation_step_resultB_product_factor. pa_b_olte_valuation_step_resultB = pa_q_olte_valuation_step_resultB_product_factor * S ((S (pa_i_olte_valuation_step_resultB_product)) * pa_c_olte_valuation_step_resultB) + (pa_p_olte_valuation_step_resultB_product))) /\ ((((exists pa_h_olte_valuation_step_resultB_product_partial. pa_h_olte_valuation_step_resultB_product_partial + S (pa_r_olte_valuation_step_resultB_product) = S ((S (pa_i_olte_valuation_step_resultB_product)) * pa_v_olte_valuation_step_resultB_product)) /\ exists pa_q_olte_valuation_step_resultB_product_partial. pa_u_olte_valuation_step_resultB_product = pa_q_olte_valuation_step_resultB_product_partial * S ((S (pa_i_olte_valuation_step_resultB_product)) * pa_v_olte_valuation_step_resultB_product) + (pa_r_olte_valuation_step_resultB_product))) /\ ((((exists pa_h_olte_valuation_step_resultB_product_successor. pa_h_olte_valuation_step_resultB_product_successor + S (pa_s_olte_valuation_step_resultB_product) = S ((S (S pa_i_olte_valuation_step_resultB_product)) * pa_v_olte_valuation_step_resultB_product)) /\ exists pa_q_olte_valuation_step_resultB_product_successor. pa_u_olte_valuation_step_resultB_product = pa_q_olte_valuation_step_resultB_product_successor * S ((S (S pa_i_olte_valuation_step_resultB_product)) * pa_v_olte_valuation_step_resultB_product) + (pa_s_olte_valuation_step_resultB_product))) /\ pa_s_olte_valuation_step_resultB_product = pa_r_olte_valuation_step_resultB_product * pa_p_olte_valuation_step_resultB_product)))))))) /\ ((((A) = (B) + (d * Q)) /\ (((~((d * Q) = 0)) /\ (((exists olte_factor_valuation_step_resultdivides. (d * Q) = (p) * olte_factor_valuation_step_resultdivides) /\ (((~(exists olte_factor_valuation_step_resultunit. (B) = (p) * olte_factor_valuation_step_resultunit)) /\ (((exists bpd_gap_pvs_olte_valuation_step_resultvaluation_selected_bound. bpd_gap_pvs_olte_valuation_step_resultvaluation_selected_bound + (g) = (d * Q)) /\ (exists bpvi_result_pvs_olte_valuation_step_resultvaluation_selected. ((exists bpvi_b_pvs_olte_valuation_step_resultvaluation_selected_power bpvi_c_pvs_olte_valuation_step_resultvaluation_selected_power. ((forall bpvi_i_pvs_olte_valuation_step_resultvaluation_selected_power. (exists bpvi_repeat_gap_pvs_olte_valuation_step_resultvaluation_selected_power. bpvi_repeat_gap_pvs_olte_valuation_step_resultvaluation_selected_power + S bpvi_i_pvs_olte_valuation_step_resultvaluation_selected_power = g) -> (((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_repeat. bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_olte_valuation_step_resultvaluation_selected_power)) * bpvi_c_pvs_olte_valuation_step_resultvaluation_selected_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_repeat. bpvi_b_pvs_olte_valuation_step_resultvaluation_selected_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_olte_valuation_step_resultvaluation_selected_power)) * bpvi_c_pvs_olte_valuation_step_resultvaluation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_olte_valuation_step_resultvaluation_selected_power bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power. ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_start. bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_start. bpvi_u_pvs_olte_valuation_step_resultvaluation_selected_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_terminal. bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_terminal + S (bpvi_result_pvs_olte_valuation_step_resultvaluation_selected) = S ((S (g)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_terminal. bpvi_u_pvs_olte_valuation_step_resultvaluation_selected_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_terminal * S ((S (g)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power) + (bpvi_result_pvs_olte_valuation_step_resultvaluation_selected))) /\ forall bpvi_j_pvs_olte_valuation_step_resultvaluation_selected_power. (exists bpvi_product_gap_pvs_olte_valuation_step_resultvaluation_selected_power. bpvi_product_gap_pvs_olte_valuation_step_resultvaluation_selected_power + S bpvi_j_pvs_olte_valuation_step_resultvaluation_selected_power = g) -> exists bpvi_factor_pvs_olte_valuation_step_resultvaluation_selected_power bpvi_partial_pvs_olte_valuation_step_resultvaluation_selected_power bpvi_successor_pvs_olte_valuation_step_resultvaluation_selected_power. ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_factor. bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_factor + S (bpvi_factor_pvs_olte_valuation_step_resultvaluation_selected_power) = S ((S (bpvi_j_pvs_olte_valuation_step_resultvaluation_selected_power)) * bpvi_c_pvs_olte_valuation_step_resultvaluation_selected_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_factor. bpvi_b_pvs_olte_valuation_step_resultvaluation_selected_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_factor * S ((S (bpvi_j_pvs_olte_valuation_step_resultvaluation_selected_power)) * bpvi_c_pvs_olte_valuation_step_resultvaluation_selected_power) + (bpvi_factor_pvs_olte_valuation_step_resultvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_partial. bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_partial + S (bpvi_partial_pvs_olte_valuation_step_resultvaluation_selected_power) = S ((S (bpvi_j_pvs_olte_valuation_step_resultvaluation_selected_power)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_partial. bpvi_u_pvs_olte_valuation_step_resultvaluation_selected_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_partial * S ((S (bpvi_j_pvs_olte_valuation_step_resultvaluation_selected_power)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power) + (bpvi_partial_pvs_olte_valuation_step_resultvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_successor. bpvi_h_pvs_olte_valuation_step_resultvaluation_selected_power_successor + S (bpvi_successor_pvs_olte_valuation_step_resultvaluation_selected_power) = S ((S (S bpvi_j_pvs_olte_valuation_step_resultvaluation_selected_power)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_successor. bpvi_u_pvs_olte_valuation_step_resultvaluation_selected_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_olte_valuation_step_resultvaluation_selected_power)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_selected_power) + (bpvi_successor_pvs_olte_valuation_step_resultvaluation_selected_power))) /\ bpvi_successor_pvs_olte_valuation_step_resultvaluation_selected_power = bpvi_partial_pvs_olte_valuation_step_resultvaluation_selected_power * bpvi_factor_pvs_olte_valuation_step_resultvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_olte_valuation_step_resultvaluation_selected. d * Q = bpvi_result_pvs_olte_valuation_step_resultvaluation_selected * bpvi_divisor_factor_pvs_olte_valuation_step_resultvaluation_selected))) /\ forall bpd_candidate_pvs_olte_valuation_step_resultvaluation. (exists bpd_gap_pvs_olte_valuation_step_resultvaluation_candidate_bound. bpd_gap_pvs_olte_valuation_step_resultvaluation_candidate_bound + (bpd_candidate_pvs_olte_valuation_step_resultvaluation) = (d * Q)) -> (exists bpvi_result_pvs_olte_valuation_step_resultvaluation_candidate. ((exists bpvi_b_pvs_olte_valuation_step_resultvaluation_candidate_power bpvi_c_pvs_olte_valuation_step_resultvaluation_candidate_power. ((forall bpvi_i_pvs_olte_valuation_step_resultvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_olte_valuation_step_resultvaluation_candidate_power. bpvi_repeat_gap_pvs_olte_valuation_step_resultvaluation_candidate_power + S bpvi_i_pvs_olte_valuation_step_resultvaluation_candidate_power = bpd_candidate_pvs_olte_valuation_step_resultvaluation) -> (((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_repeat. bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_olte_valuation_step_resultvaluation_candidate_power)) * bpvi_c_pvs_olte_valuation_step_resultvaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_repeat. bpvi_b_pvs_olte_valuation_step_resultvaluation_candidate_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_olte_valuation_step_resultvaluation_candidate_power)) * bpvi_c_pvs_olte_valuation_step_resultvaluation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_olte_valuation_step_resultvaluation_candidate_power bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power. ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_start. bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_start. bpvi_u_pvs_olte_valuation_step_resultvaluation_candidate_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_terminal. bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_terminal + S (bpvi_result_pvs_olte_valuation_step_resultvaluation_candidate) = S ((S (bpd_candidate_pvs_olte_valuation_step_resultvaluation)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_terminal. bpvi_u_pvs_olte_valuation_step_resultvaluation_candidate_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_olte_valuation_step_resultvaluation)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power) + (bpvi_result_pvs_olte_valuation_step_resultvaluation_candidate))) /\ forall bpvi_j_pvs_olte_valuation_step_resultvaluation_candidate_power. (exists bpvi_product_gap_pvs_olte_valuation_step_resultvaluation_candidate_power. bpvi_product_gap_pvs_olte_valuation_step_resultvaluation_candidate_power + S bpvi_j_pvs_olte_valuation_step_resultvaluation_candidate_power = bpd_candidate_pvs_olte_valuation_step_resultvaluation) -> exists bpvi_factor_pvs_olte_valuation_step_resultvaluation_candidate_power bpvi_partial_pvs_olte_valuation_step_resultvaluation_candidate_power bpvi_successor_pvs_olte_valuation_step_resultvaluation_candidate_power. ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_factor. bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_factor + S (bpvi_factor_pvs_olte_valuation_step_resultvaluation_candidate_power) = S ((S (bpvi_j_pvs_olte_valuation_step_resultvaluation_candidate_power)) * bpvi_c_pvs_olte_valuation_step_resultvaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_factor. bpvi_b_pvs_olte_valuation_step_resultvaluation_candidate_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_olte_valuation_step_resultvaluation_candidate_power)) * bpvi_c_pvs_olte_valuation_step_resultvaluation_candidate_power) + (bpvi_factor_pvs_olte_valuation_step_resultvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_partial. bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_partial + S (bpvi_partial_pvs_olte_valuation_step_resultvaluation_candidate_power) = S ((S (bpvi_j_pvs_olte_valuation_step_resultvaluation_candidate_power)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_partial. bpvi_u_pvs_olte_valuation_step_resultvaluation_candidate_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_olte_valuation_step_resultvaluation_candidate_power)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power) + (bpvi_partial_pvs_olte_valuation_step_resultvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_successor. bpvi_h_pvs_olte_valuation_step_resultvaluation_candidate_power_successor + S (bpvi_successor_pvs_olte_valuation_step_resultvaluation_candidate_power) = S ((S (S bpvi_j_pvs_olte_valuation_step_resultvaluation_candidate_power)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_successor. bpvi_u_pvs_olte_valuation_step_resultvaluation_candidate_power = bpvi_q_pvs_olte_valuation_step_resultvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_olte_valuation_step_resultvaluation_candidate_power)) * bpvi_v_pvs_olte_valuation_step_resultvaluation_candidate_power) + (bpvi_successor_pvs_olte_valuation_step_resultvaluation_candidate_power))) /\ bpvi_successor_pvs_olte_valuation_step_resultvaluation_candidate_power = bpvi_partial_pvs_olte_valuation_step_resultvaluation_candidate_power * bpvi_factor_pvs_olte_valuation_step_resultvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_olte_valuation_step_resultvaluation_candidate. d * Q = bpvi_result_pvs_olte_valuation_step_resultvaluation_candidate * bpvi_divisor_factor_pvs_olte_valuation_step_resultvaluation_candidate)) -> (exists bpd_gap_pvs_olte_valuation_step_resultvaluation_maximal. bpd_gap_pvs_olte_valuation_step_resultvaluation_maximal + (bpd_candidate_pvs_olte_valuation_step_resultvaluation) = (g)))))))))))))))