primorial_cutoff_count_power_bound

Exact expanded first-order arithmetic statement

forall n u b c d f L P Q. (forall pc_index_prim_count_mask. (exists pc_lt_prim_count_mask_bound. pc_lt_prim_count_mask_bound + S (pc_index_prim_count_mask) = (n)) -> exists pc_bit_prim_count_mask. (((exists fs_h_pc_prim_count_mask_entry. fs_h_pc_prim_count_mask_entry + S (pc_bit_prim_count_mask) = S ((S (pc_index_prim_count_mask)) * c)) /\ exists fs_q_pc_prim_count_mask_entry. b = fs_q_pc_prim_count_mask_entry * S ((S (pc_index_prim_count_mask)) * c) + (pc_bit_prim_count_mask))) /\ (((((~(S (pc_index_prim_count_mask) = 1) /\ forall bpr_left_pc_prim_count_mask_choice_prime bpr_right_pc_prim_count_mask_choice_prime. S (pc_index_prim_count_mask) = bpr_left_pc_prim_count_mask_choice_prime * bpr_right_pc_prim_count_mask_choice_prime -> bpr_left_pc_prim_count_mask_choice_prime = 1 \/ bpr_right_pc_prim_count_mask_choice_prime = 1)) /\ pc_bit_prim_count_mask = 1) \/ (~((~(S (pc_index_prim_count_mask) = 1) /\ forall bpr_left_pc_prim_count_mask_choice_prime bpr_right_pc_prim_count_mask_choice_prime. S (pc_index_prim_count_mask) = bpr_left_pc_prim_count_mask_choice_prime * bpr_right_pc_prim_count_mask_choice_prime -> bpr_left_pc_prim_count_mask_choice_prime = 1 \/ bpr_right_pc_prim_count_mask_choice_prime = 1)) /\ pc_bit_prim_count_mask = 0)))) -> (forall pc_index_prim_count_cutoff. (exists pc_lt_prim_count_cutoff_bound. pc_lt_prim_count_cutoff_bound + S (pc_index_prim_count_cutoff) = (n)) -> exists pc_bit_prim_count_cutoff. (((exists fs_h_pc_prim_count_cutoff_entry. fs_h_pc_prim_count_cutoff_entry + S (pc_bit_prim_count_cutoff) = S ((S (pc_index_prim_count_cutoff)) * f)) /\ exists fs_q_pc_prim_count_cutoff_entry. d = fs_q_pc_prim_count_cutoff_entry * S ((S (pc_index_prim_count_cutoff)) * f) + (pc_bit_prim_count_cutoff))) /\ ((((exists pc_lt_prim_count_cutoff_choice_below. pc_lt_prim_count_cutoff_choice_below + S (pc_index_prim_count_cutoff) = (u)) /\ pc_bit_prim_count_cutoff = 0) \/ ((exists pc_le_prim_count_cutoff_choice_above. pc_le_prim_count_cutoff_choice_above + (u) = (pc_index_prim_count_cutoff)) /\ (((exists fs_h_pc_prim_count_cutoff_choice_source. fs_h_pc_prim_count_cutoff_choice_source + S (pc_bit_prim_count_cutoff) = S ((S (pc_index_prim_count_cutoff)) * c)) /\ exists fs_q_pc_prim_count_cutoff_choice_source. b = fs_q_pc_prim_count_cutoff_choice_source * S ((S (pc_index_prim_count_cutoff)) * c) + (pc_bit_prim_count_cutoff))))))) -> (exists fs_u_pc_prim_count_sum fs_v_pc_prim_count_sum. ((((exists fs_h_pc_prim_count_sum_body_start. fs_h_pc_prim_count_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_prim_count_sum)) /\ exists fs_q_pc_prim_count_sum_body_start. fs_u_pc_prim_count_sum = fs_q_pc_prim_count_sum_body_start * S ((S (0)) * fs_v_pc_prim_count_sum) + (0))) /\ ((((exists fs_h_pc_prim_count_sum_body_terminal. fs_h_pc_prim_count_sum_body_terminal + S (L) = S ((S (n)) * fs_v_pc_prim_count_sum)) /\ exists fs_q_pc_prim_count_sum_body_terminal. fs_u_pc_prim_count_sum = fs_q_pc_prim_count_sum_body_terminal * S ((S (n)) * fs_v_pc_prim_count_sum) + (L))) /\ forall fs_i_pc_prim_count_sum_body_steps. (exists fs_lt_pc_prim_count_sum_body_steps_bound. fs_lt_pc_prim_count_sum_body_steps_bound + S fs_i_pc_prim_count_sum_body_steps = n) -> exists fs_a_pc_prim_count_sum_body_steps fs_r_pc_prim_count_sum_body_steps fs_s_pc_prim_count_sum_body_steps. ((((exists fs_h_pc_prim_count_sum_body_steps_summand. fs_h_pc_prim_count_sum_body_steps_summand + S (fs_a_pc_prim_count_sum_body_steps) = S ((S (fs_i_pc_prim_count_sum_body_steps)) * f)) /\ exists fs_q_pc_prim_count_sum_body_steps_summand. d = fs_q_pc_prim_count_sum_body_steps_summand * S ((S (fs_i_pc_prim_count_sum_body_steps)) * f) + (fs_a_pc_prim_count_sum_body_steps))) /\ ((((exists fs_h_pc_prim_count_sum_body_steps_partial. fs_h_pc_prim_count_sum_body_steps_partial + S (fs_r_pc_prim_count_sum_body_steps) = S ((S (fs_i_pc_prim_count_sum_body_steps)) * fs_v_pc_prim_count_sum)) /\ exists fs_q_pc_prim_count_sum_body_steps_partial. fs_u_pc_prim_count_sum = fs_q_pc_prim_count_sum_body_steps_partial * S ((S (fs_i_pc_prim_count_sum_body_steps)) * fs_v_pc_prim_count_sum) + (fs_r_pc_prim_count_sum_body_steps))) /\ ((((exists fs_h_pc_prim_count_sum_body_steps_successor. fs_h_pc_prim_count_sum_body_steps_successor + S (fs_s_pc_prim_count_sum_body_steps) = S ((S (S fs_i_pc_prim_count_sum_body_steps)) * fs_v_pc_prim_count_sum)) /\ exists fs_q_pc_prim_count_sum_body_steps_successor. fs_u_pc_prim_count_sum = fs_q_pc_prim_count_sum_body_steps_successor * S ((S (S fs_i_pc_prim_count_sum_body_steps)) * fs_v_pc_prim_count_sum) + (fs_s_pc_prim_count_sum_body_steps))) /\ fs_s_pc_prim_count_sum_body_steps = fs_r_pc_prim_count_sum_body_steps + fs_a_pc_prim_count_sum_body_steps)))))) -> (exists bpr_code_pc_prim_count_primorial bpr_scale_pc_prim_count_primorial. ((forall bpr_index_pc_prim_count_primorial_mask. (exists bpr_gap_pc_prim_count_primorial_mask_bound. bpr_gap_pc_prim_count_primorial_mask_bound + S (bpr_index_pc_prim_count_primorial_mask) = n) -> exists bpr_value_pc_prim_count_primorial_mask. ((((exists bpr_height_pc_prim_count_primorial_mask_decoded. bpr_height_pc_prim_count_primorial_mask_decoded + S (bpr_value_pc_prim_count_primorial_mask) = S ((S (bpr_index_pc_prim_count_primorial_mask)) * bpr_scale_pc_prim_count_primorial)) /\ exists bpr_quotient_pc_prim_count_primorial_mask_decoded. bpr_code_pc_prim_count_primorial = bpr_quotient_pc_prim_count_primorial_mask_decoded * S ((S (bpr_index_pc_prim_count_primorial_mask)) * bpr_scale_pc_prim_count_primorial) + (bpr_value_pc_prim_count_primorial_mask))) /\ (((((~(S (bpr_index_pc_prim_count_primorial_mask) = 1) /\ forall bpr_left_pc_prim_count_primorial_mask_choice_prime bpr_right_pc_prim_count_primorial_mask_choice_prime. S (bpr_index_pc_prim_count_primorial_mask) = bpr_left_pc_prim_count_primorial_mask_choice_prime * bpr_right_pc_prim_count_primorial_mask_choice_prime -> bpr_left_pc_prim_count_primorial_mask_choice_prime = 1 \/ bpr_right_pc_prim_count_primorial_mask_choice_prime = 1)) /\ bpr_value_pc_prim_count_primorial_mask = S (bpr_index_pc_prim_count_primorial_mask)) \/ (~((~(S (bpr_index_pc_prim_count_primorial_mask) = 1) /\ forall bpr_left_pc_prim_count_primorial_mask_choice_prime bpr_right_pc_prim_count_primorial_mask_choice_prime. S (bpr_index_pc_prim_count_primorial_mask) = bpr_left_pc_prim_count_primorial_mask_choice_prime * bpr_right_pc_prim_count_primorial_mask_choice_prime -> bpr_left_pc_prim_count_primorial_mask_choice_prime = 1 \/ bpr_right_pc_prim_count_primorial_mask_choice_prime = 1)) /\ bpr_value_pc_prim_count_primorial_mask = 1))))) /\ (exists ff_u_pc_prim_count_primorial_product ff_v_pc_prim_count_primorial_product. ((((exists ff_h_pc_prim_count_primorial_product_start. ff_h_pc_prim_count_primorial_product_start + S (1) = S ((S (0)) * ff_v_pc_prim_count_primorial_product)) /\ exists ff_q_pc_prim_count_primorial_product_start. ff_u_pc_prim_count_primorial_product = ff_q_pc_prim_count_primorial_product_start * S ((S (0)) * ff_v_pc_prim_count_primorial_product) + (1))) /\ ((((exists ff_h_pc_prim_count_primorial_product_terminal. ff_h_pc_prim_count_primorial_product_terminal + S (P) = S ((S (n)) * ff_v_pc_prim_count_primorial_product)) /\ exists ff_q_pc_prim_count_primorial_product_terminal. ff_u_pc_prim_count_primorial_product = ff_q_pc_prim_count_primorial_product_terminal * S ((S (n)) * ff_v_pc_prim_count_primorial_product) + (P))) /\ forall ff_i_pc_prim_count_primorial_product. (exists ff_lt_pc_prim_count_primorial_product_bound. ff_lt_pc_prim_count_primorial_product_bound + S ff_i_pc_prim_count_primorial_product = n) -> exists ff_p_pc_prim_count_primorial_product ff_r_pc_prim_count_primorial_product ff_s_pc_prim_count_primorial_product. ((((exists ff_h_pc_prim_count_primorial_product_factor. ff_h_pc_prim_count_primorial_product_factor + S (ff_p_pc_prim_count_primorial_product) = S ((S (ff_i_pc_prim_count_primorial_product)) * bpr_scale_pc_prim_count_primorial)) /\ exists ff_q_pc_prim_count_primorial_product_factor. bpr_code_pc_prim_count_primorial = ff_q_pc_prim_count_primorial_product_factor * S ((S (ff_i_pc_prim_count_primorial_product)) * bpr_scale_pc_prim_count_primorial) + (ff_p_pc_prim_count_primorial_product))) /\ ((((exists ff_h_pc_prim_count_primorial_product_partial. ff_h_pc_prim_count_primorial_product_partial + S (ff_r_pc_prim_count_primorial_product) = S ((S (ff_i_pc_prim_count_primorial_product)) * ff_v_pc_prim_count_primorial_product)) /\ exists ff_q_pc_prim_count_primorial_product_partial. ff_u_pc_prim_count_primorial_product = ff_q_pc_prim_count_primorial_product_partial * S ((S (ff_i_pc_prim_count_primorial_product)) * ff_v_pc_prim_count_primorial_product) + (ff_r_pc_prim_count_primorial_product))) /\ ((((exists ff_h_pc_prim_count_primorial_product_successor. ff_h_pc_prim_count_primorial_product_successor + S (ff_s_pc_prim_count_primorial_product) = S ((S (S ff_i_pc_prim_count_primorial_product)) * ff_v_pc_prim_count_primorial_product)) /\ exists ff_q_pc_prim_count_primorial_product_successor. ff_u_pc_prim_count_primorial_product = ff_q_pc_prim_count_primorial_product_successor * S ((S (S ff_i_pc_prim_count_primorial_product)) * ff_v_pc_prim_count_primorial_product) + (ff_s_pc_prim_count_primorial_product))) /\ ff_s_pc_prim_count_primorial_product = ff_r_pc_prim_count_primorial_product * ff_p_pc_prim_count_primorial_product)))))))) -> (exists pa_b_pc_prim_count_power pa_c_pc_prim_count_power. ((forall pa_i_pc_prim_count_power_repeat. (exists pa_lt_pc_prim_count_power_repeat_bound. pa_lt_pc_prim_count_power_repeat_bound + S pa_i_pc_prim_count_power_repeat = L) -> (((exists pa_h_pc_prim_count_power_repeat_decoded. pa_h_pc_prim_count_power_repeat_decoded + S (u) = S ((S (pa_i_pc_prim_count_power_repeat)) * pa_c_pc_prim_count_power)) /\ exists pa_q_pc_prim_count_power_repeat_decoded. pa_b_pc_prim_count_power = pa_q_pc_prim_count_power_repeat_decoded * S ((S (pa_i_pc_prim_count_power_repeat)) * pa_c_pc_prim_count_power) + (u)))) /\ (exists pa_u_pc_prim_count_power_product pa_v_pc_prim_count_power_product. ((((exists pa_h_pc_prim_count_power_product_start. pa_h_pc_prim_count_power_product_start + S (1) = S ((S (0)) * pa_v_pc_prim_count_power_product)) /\ exists pa_q_pc_prim_count_power_product_start. pa_u_pc_prim_count_power_product = pa_q_pc_prim_count_power_product_start * S ((S (0)) * pa_v_pc_prim_count_power_product) + (1))) /\ ((((exists pa_h_pc_prim_count_power_product_terminal. pa_h_pc_prim_count_power_product_terminal + S (Q) = S ((S (L)) * pa_v_pc_prim_count_power_product)) /\ exists pa_q_pc_prim_count_power_product_terminal. pa_u_pc_prim_count_power_product = pa_q_pc_prim_count_power_product_terminal * S ((S (L)) * pa_v_pc_prim_count_power_product) + (Q))) /\ forall pa_i_pc_prim_count_power_product. (exists pa_lt_pc_prim_count_power_product_bound. pa_lt_pc_prim_count_power_product_bound + S pa_i_pc_prim_count_power_product = L) -> exists pa_p_pc_prim_count_power_product pa_r_pc_prim_count_power_product pa_s_pc_prim_count_power_product. ((((exists pa_h_pc_prim_count_power_product_factor. pa_h_pc_prim_count_power_product_factor + S (pa_p_pc_prim_count_power_product) = S ((S (pa_i_pc_prim_count_power_product)) * pa_c_pc_prim_count_power)) /\ exists pa_q_pc_prim_count_power_product_factor. pa_b_pc_prim_count_power = pa_q_pc_prim_count_power_product_factor * S ((S (pa_i_pc_prim_count_power_product)) * pa_c_pc_prim_count_power) + (pa_p_pc_prim_count_power_product))) /\ ((((exists pa_h_pc_prim_count_power_product_partial. pa_h_pc_prim_count_power_product_partial + S (pa_r_pc_prim_count_power_product) = S ((S (pa_i_pc_prim_count_power_product)) * pa_v_pc_prim_count_power_product)) /\ exists pa_q_pc_prim_count_power_product_partial. pa_u_pc_prim_count_power_product = pa_q_pc_prim_count_power_product_partial * S ((S (pa_i_pc_prim_count_power_product)) * pa_v_pc_prim_count_power_product) + (pa_r_pc_prim_count_power_product))) /\ ((((exists pa_h_pc_prim_count_power_product_successor. pa_h_pc_prim_count_power_product_successor + S (pa_s_pc_prim_count_power_product) = S ((S (S pa_i_pc_prim_count_power_product)) * pa_v_pc_prim_count_power_product)) /\ exists pa_q_pc_prim_count_power_product_successor. pa_u_pc_prim_count_power_product = pa_q_pc_prim_count_power_product_successor * S ((S (S pa_i_pc_prim_count_power_product)) * pa_v_pc_prim_count_power_product) + (pa_s_pc_prim_count_power_product))) /\ pa_s_pc_prim_count_power_product = pa_r_pc_prim_count_power_product * pa_p_pc_prim_count_power_product)))))))) -> (exists pc_le_prim_count_result. pc_le_prim_count_result + (Q) = (P))