BT010P · Bertrand theorem

prime_contribution_interval_prefix_shift

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Align a full contribution prefix with its independent suffix.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ n. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ l. (∀ x. Lt(x,a + l) → ∃ y. BetaAt(b,c,x,y) ∧ (Prime(S x) ∧ (∃ z. PowerValuation(S x,n,z) ∧ Pow(S x,z,y)) ∨ ¬Prime(S x) ∧ y = 1)) → (∀ x. Lt(x,l) → ∃ y. BetaAt(d,e,x,y) ∧ (Prime(S (a + x)) ∧ (∃ z. PowerValuation(S (a + x),n,z) ∧ Pow(S (a + x),z,y)) ∨ ¬Prime(S (a + x)) ∧ y = 1)) → ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,a + x,y) → BetaAt(d,e,x,y)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime PD0013 BetaAt PD0020 Pow PD0046 PowerValuation

15 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0004 Prime PD0013 BetaAt PD0020 Pow PD0046 PowerValuation

12 occurrences

Exact expanded native-PA statement
forall n a b c d e l. (forall bpr_prefix_index_bpcips_source. (exists bpr_gap_bpcips_source_bound. bpr_gap_bpcips_source_bound + S (bpr_prefix_index_bpcips_source) = a + l) -> exists bpr_prefix_value_bpcips_source. ((((exists bpr_height_bpcips_source_decoded. bpr_height_bpcips_source_decoded + S (bpr_prefix_value_bpcips_source) = S ((S (bpr_prefix_index_bpcips_source)) * c)) /\ exists bpr_quotient_bpcips_source_decoded. b = bpr_quotient_bpcips_source_decoded * S ((S (bpr_prefix_index_bpcips_source)) * c) + (bpr_prefix_value_bpcips_source))) /\ (((((~(S (bpr_prefix_index_bpcips_source) = 1) /\ forall bpr_left_bpcips_source_choice_prime bpr_right_bpcips_source_choice_prime. S (bpr_prefix_index_bpcips_source) = bpr_left_bpcips_source_choice_prime * bpr_right_bpcips_source_choice_prime -> bpr_left_bpcips_source_choice_prime = 1 \/ bpr_right_bpcips_source_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcips_source_choice. ((((exists bpr_le_gap_bpcips_source_choice_valuation_selected_bound. bpr_le_gap_bpcips_source_choice_valuation_selected_bound + (bpr_choice_exponent_bpcips_source_choice) = (n)) /\ (exists bpr_power_value_bpcips_source_choice_valuation_selected. ((exists bpr_power_code_bpcips_source_choice_valuation_selected_power bpr_power_scale_bpcips_source_choice_valuation_selected_power. ((forall bpr_power_index_bpcips_source_choice_valuation_selected_power. (exists bpr_gap_bpcips_source_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcips_source_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcips_source_choice_valuation_selected_power) = bpr_choice_exponent_bpcips_source_choice) -> (((exists bpr_height_bpcips_source_choice_valuation_selected_power_repeat_entry. bpr_height_bpcips_source_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcips_source)) = S ((S (bpr_power_index_bpcips_source_choice_valuation_selected_power)) * bpr_power_scale_bpcips_source_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcips_source_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcips_source_choice_valuation_selected_power = bpr_quotient_bpcips_source_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcips_source_choice_valuation_selected_power)) * bpr_power_scale_bpcips_source_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcips_source))))) /\ (exists ff_u_bpcips_source_choice_valuation_selected_power_product ff_v_bpcips_source_choice_valuation_selected_power_product. ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_start. ff_h_bpcips_source_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_start. ff_u_bpcips_source_choice_valuation_selected_power_product = ff_q_bpcips_source_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcips_source_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_terminal. ff_h_bpcips_source_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcips_source_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcips_source_choice)) * ff_v_bpcips_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_terminal. ff_u_bpcips_source_choice_valuation_selected_power_product = ff_q_bpcips_source_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcips_source_choice)) * ff_v_bpcips_source_choice_valuation_selected_power_product) + (bpr_power_value_bpcips_source_choice_valuation_selected))) /\ forall ff_i_bpcips_source_choice_valuation_selected_power_product. (exists ff_lt_bpcips_source_choice_valuation_selected_power_product_bound. ff_lt_bpcips_source_choice_valuation_selected_power_product_bound + S ff_i_bpcips_source_choice_valuation_selected_power_product = bpr_choice_exponent_bpcips_source_choice) -> exists ff_p_bpcips_source_choice_valuation_selected_power_product ff_r_bpcips_source_choice_valuation_selected_power_product ff_s_bpcips_source_choice_valuation_selected_power_product. ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_factor. ff_h_bpcips_source_choice_valuation_selected_power_product_factor + S (ff_p_bpcips_source_choice_valuation_selected_power_product) = S ((S (ff_i_bpcips_source_choice_valuation_selected_power_product)) * bpr_power_scale_bpcips_source_choice_valuation_selected_power)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_factor. bpr_power_code_bpcips_source_choice_valuation_selected_power = ff_q_bpcips_source_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcips_source_choice_valuation_selected_power_product)) * bpr_power_scale_bpcips_source_choice_valuation_selected_power) + (ff_p_bpcips_source_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_partial. ff_h_bpcips_source_choice_valuation_selected_power_product_partial + S (ff_r_bpcips_source_choice_valuation_selected_power_product) = S ((S (ff_i_bpcips_source_choice_valuation_selected_power_product)) * ff_v_bpcips_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_partial. ff_u_bpcips_source_choice_valuation_selected_power_product = ff_q_bpcips_source_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcips_source_choice_valuation_selected_power_product)) * ff_v_bpcips_source_choice_valuation_selected_power_product) + (ff_r_bpcips_source_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_successor. ff_h_bpcips_source_choice_valuation_selected_power_product_successor + S (ff_s_bpcips_source_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcips_source_choice_valuation_selected_power_product)) * ff_v_bpcips_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_successor. ff_u_bpcips_source_choice_valuation_selected_power_product = ff_q_bpcips_source_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcips_source_choice_valuation_selected_power_product)) * ff_v_bpcips_source_choice_valuation_selected_power_product) + (ff_s_bpcips_source_choice_valuation_selected_power_product))) /\ ff_s_bpcips_source_choice_valuation_selected_power_product = ff_r_bpcips_source_choice_valuation_selected_power_product * ff_p_bpcips_source_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcips_source_choice_valuation_selected_divides. n = (bpr_power_value_bpcips_source_choice_valuation_selected) * bpr_divides_quotient_bpcips_source_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcips_source_choice_valuation. (exists bpr_le_gap_bpcips_source_choice_valuation_candidate_bound. bpr_le_gap_bpcips_source_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcips_source_choice_valuation) = (n)) -> (exists bpr_power_value_bpcips_source_choice_valuation_candidate. ((exists bpr_power_code_bpcips_source_choice_valuation_candidate_power bpr_power_scale_bpcips_source_choice_valuation_candidate_power. ((forall bpr_power_index_bpcips_source_choice_valuation_candidate_power. (exists bpr_gap_bpcips_source_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcips_source_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcips_source_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcips_source_choice_valuation) -> (((exists bpr_height_bpcips_source_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcips_source_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcips_source)) = S ((S (bpr_power_index_bpcips_source_choice_valuation_candidate_power)) * bpr_power_scale_bpcips_source_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcips_source_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcips_source_choice_valuation_candidate_power = bpr_quotient_bpcips_source_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcips_source_choice_valuation_candidate_power)) * bpr_power_scale_bpcips_source_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcips_source))))) /\ (exists ff_u_bpcips_source_choice_valuation_candidate_power_product ff_v_bpcips_source_choice_valuation_candidate_power_product. ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_start. ff_h_bpcips_source_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_start. ff_u_bpcips_source_choice_valuation_candidate_power_product = ff_q_bpcips_source_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcips_source_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_terminal. ff_h_bpcips_source_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcips_source_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcips_source_choice_valuation)) * ff_v_bpcips_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_terminal. ff_u_bpcips_source_choice_valuation_candidate_power_product = ff_q_bpcips_source_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcips_source_choice_valuation)) * ff_v_bpcips_source_choice_valuation_candidate_power_product) + (bpr_power_value_bpcips_source_choice_valuation_candidate))) /\ forall ff_i_bpcips_source_choice_valuation_candidate_power_product. (exists ff_lt_bpcips_source_choice_valuation_candidate_power_product_bound. ff_lt_bpcips_source_choice_valuation_candidate_power_product_bound + S ff_i_bpcips_source_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcips_source_choice_valuation) -> exists ff_p_bpcips_source_choice_valuation_candidate_power_product ff_r_bpcips_source_choice_valuation_candidate_power_product ff_s_bpcips_source_choice_valuation_candidate_power_product. ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_factor. ff_h_bpcips_source_choice_valuation_candidate_power_product_factor + S (ff_p_bpcips_source_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcips_source_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcips_source_choice_valuation_candidate_power)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcips_source_choice_valuation_candidate_power = ff_q_bpcips_source_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcips_source_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcips_source_choice_valuation_candidate_power) + (ff_p_bpcips_source_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_partial. ff_h_bpcips_source_choice_valuation_candidate_power_product_partial + S (ff_r_bpcips_source_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcips_source_choice_valuation_candidate_power_product)) * ff_v_bpcips_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_partial. ff_u_bpcips_source_choice_valuation_candidate_power_product = ff_q_bpcips_source_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcips_source_choice_valuation_candidate_power_product)) * ff_v_bpcips_source_choice_valuation_candidate_power_product) + (ff_r_bpcips_source_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_successor. ff_h_bpcips_source_choice_valuation_candidate_power_product_successor + S (ff_s_bpcips_source_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcips_source_choice_valuation_candidate_power_product)) * ff_v_bpcips_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_successor. ff_u_bpcips_source_choice_valuation_candidate_power_product = ff_q_bpcips_source_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcips_source_choice_valuation_candidate_power_product)) * ff_v_bpcips_source_choice_valuation_candidate_power_product) + (ff_s_bpcips_source_choice_valuation_candidate_power_product))) /\ ff_s_bpcips_source_choice_valuation_candidate_power_product = ff_r_bpcips_source_choice_valuation_candidate_power_product * ff_p_bpcips_source_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcips_source_choice_valuation_candidate_divides. n = (bpr_power_value_bpcips_source_choice_valuation_candidate) * bpr_divides_quotient_bpcips_source_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcips_source_choice_valuation_candidate_below. bpr_le_gap_bpcips_source_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcips_source_choice_valuation) = (bpr_choice_exponent_bpcips_source_choice))) /\ (exists bpr_power_code_bpcips_source_choice_power bpr_power_scale_bpcips_source_choice_power. ((forall bpr_power_index_bpcips_source_choice_power. (exists bpr_gap_bpcips_source_choice_power_repeat_bound. bpr_gap_bpcips_source_choice_power_repeat_bound + S (bpr_power_index_bpcips_source_choice_power) = bpr_choice_exponent_bpcips_source_choice) -> (((exists bpr_height_bpcips_source_choice_power_repeat_entry. bpr_height_bpcips_source_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcips_source)) = S ((S (bpr_power_index_bpcips_source_choice_power)) * bpr_power_scale_bpcips_source_choice_power)) /\ exists bpr_quotient_bpcips_source_choice_power_repeat_entry. bpr_power_code_bpcips_source_choice_power = bpr_quotient_bpcips_source_choice_power_repeat_entry * S ((S (bpr_power_index_bpcips_source_choice_power)) * bpr_power_scale_bpcips_source_choice_power) + (S (bpr_prefix_index_bpcips_source))))) /\ (exists ff_u_bpcips_source_choice_power_product ff_v_bpcips_source_choice_power_product. ((((exists ff_h_bpcips_source_choice_power_product_start. ff_h_bpcips_source_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_source_choice_power_product)) /\ exists ff_q_bpcips_source_choice_power_product_start. ff_u_bpcips_source_choice_power_product = ff_q_bpcips_source_choice_power_product_start * S ((S (0)) * ff_v_bpcips_source_choice_power_product) + (1))) /\ ((((exists ff_h_bpcips_source_choice_power_product_terminal. ff_h_bpcips_source_choice_power_product_terminal + S (bpr_prefix_value_bpcips_source) = S ((S (bpr_choice_exponent_bpcips_source_choice)) * ff_v_bpcips_source_choice_power_product)) /\ exists ff_q_bpcips_source_choice_power_product_terminal. ff_u_bpcips_source_choice_power_product = ff_q_bpcips_source_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcips_source_choice)) * ff_v_bpcips_source_choice_power_product) + (bpr_prefix_value_bpcips_source))) /\ forall ff_i_bpcips_source_choice_power_product. (exists ff_lt_bpcips_source_choice_power_product_bound. ff_lt_bpcips_source_choice_power_product_bound + S ff_i_bpcips_source_choice_power_product = bpr_choice_exponent_bpcips_source_choice) -> exists ff_p_bpcips_source_choice_power_product ff_r_bpcips_source_choice_power_product ff_s_bpcips_source_choice_power_product. ((((exists ff_h_bpcips_source_choice_power_product_factor. ff_h_bpcips_source_choice_power_product_factor + S (ff_p_bpcips_source_choice_power_product) = S ((S (ff_i_bpcips_source_choice_power_product)) * bpr_power_scale_bpcips_source_choice_power)) /\ exists ff_q_bpcips_source_choice_power_product_factor. bpr_power_code_bpcips_source_choice_power = ff_q_bpcips_source_choice_power_product_factor * S ((S (ff_i_bpcips_source_choice_power_product)) * bpr_power_scale_bpcips_source_choice_power) + (ff_p_bpcips_source_choice_power_product))) /\ ((((exists ff_h_bpcips_source_choice_power_product_partial. ff_h_bpcips_source_choice_power_product_partial + S (ff_r_bpcips_source_choice_power_product) = S ((S (ff_i_bpcips_source_choice_power_product)) * ff_v_bpcips_source_choice_power_product)) /\ exists ff_q_bpcips_source_choice_power_product_partial. ff_u_bpcips_source_choice_power_product = ff_q_bpcips_source_choice_power_product_partial * S ((S (ff_i_bpcips_source_choice_power_product)) * ff_v_bpcips_source_choice_power_product) + (ff_r_bpcips_source_choice_power_product))) /\ ((((exists ff_h_bpcips_source_choice_power_product_successor. ff_h_bpcips_source_choice_power_product_successor + S (ff_s_bpcips_source_choice_power_product) = S ((S (S ff_i_bpcips_source_choice_power_product)) * ff_v_bpcips_source_choice_power_product)) /\ exists ff_q_bpcips_source_choice_power_product_successor. ff_u_bpcips_source_choice_power_product = ff_q_bpcips_source_choice_power_product_successor * S ((S (S ff_i_bpcips_source_choice_power_product)) * ff_v_bpcips_source_choice_power_product) + (ff_s_bpcips_source_choice_power_product))) /\ ff_s_bpcips_source_choice_power_product = ff_r_bpcips_source_choice_power_product * ff_p_bpcips_source_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcips_source) = 1) /\ forall bpr_left_bpcips_source_choice_prime bpr_right_bpcips_source_choice_prime. S (bpr_prefix_index_bpcips_source) = bpr_left_bpcips_source_choice_prime * bpr_right_bpcips_source_choice_prime -> bpr_left_bpcips_source_choice_prime = 1 \/ bpr_right_bpcips_source_choice_prime = 1)) /\ bpr_prefix_value_bpcips_source = 1))))) -> (forall bpr_index_bpcips_interval. (exists bpr_gap_bpcips_interval_bound. bpr_gap_bpcips_interval_bound + S (bpr_index_bpcips_interval) = l) -> exists bpr_value_bpcips_interval. ((((exists bpr_height_bpcips_interval_decoded. bpr_height_bpcips_interval_decoded + S (bpr_value_bpcips_interval) = S ((S (bpr_index_bpcips_interval)) * e)) /\ exists bpr_quotient_bpcips_interval_decoded. d = bpr_quotient_bpcips_interval_decoded * S ((S (bpr_index_bpcips_interval)) * e) + (bpr_value_bpcips_interval))) /\ (((((~(S (a + bpr_index_bpcips_interval) = 1) /\ forall bpr_left_bpcips_interval_choice_prime bpr_right_bpcips_interval_choice_prime. S (a + bpr_index_bpcips_interval) = bpr_left_bpcips_interval_choice_prime * bpr_right_bpcips_interval_choice_prime -> bpr_left_bpcips_interval_choice_prime = 1 \/ bpr_right_bpcips_interval_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcips_interval_choice. ((((exists bpr_le_gap_bpcips_interval_choice_valuation_selected_bound. bpr_le_gap_bpcips_interval_choice_valuation_selected_bound + (bpr_choice_exponent_bpcips_interval_choice) = (n)) /\ (exists bpr_power_value_bpcips_interval_choice_valuation_selected. ((exists bpr_power_code_bpcips_interval_choice_valuation_selected_power bpr_power_scale_bpcips_interval_choice_valuation_selected_power. ((forall bpr_power_index_bpcips_interval_choice_valuation_selected_power. (exists bpr_gap_bpcips_interval_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcips_interval_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcips_interval_choice_valuation_selected_power) = bpr_choice_exponent_bpcips_interval_choice) -> (((exists bpr_height_bpcips_interval_choice_valuation_selected_power_repeat_entry. bpr_height_bpcips_interval_choice_valuation_selected_power_repeat_entry + S (S (a + bpr_index_bpcips_interval)) = S ((S (bpr_power_index_bpcips_interval_choice_valuation_selected_power)) * bpr_power_scale_bpcips_interval_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcips_interval_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcips_interval_choice_valuation_selected_power = bpr_quotient_bpcips_interval_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcips_interval_choice_valuation_selected_power)) * bpr_power_scale_bpcips_interval_choice_valuation_selected_power) + (S (a + bpr_index_bpcips_interval))))) /\ (exists ff_u_bpcips_interval_choice_valuation_selected_power_product ff_v_bpcips_interval_choice_valuation_selected_power_product. ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_start. ff_h_bpcips_interval_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_interval_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_start. ff_u_bpcips_interval_choice_valuation_selected_power_product = ff_q_bpcips_interval_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcips_interval_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_terminal. ff_h_bpcips_interval_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcips_interval_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcips_interval_choice)) * ff_v_bpcips_interval_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_terminal. ff_u_bpcips_interval_choice_valuation_selected_power_product = ff_q_bpcips_interval_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcips_interval_choice)) * ff_v_bpcips_interval_choice_valuation_selected_power_product) + (bpr_power_value_bpcips_interval_choice_valuation_selected))) /\ forall ff_i_bpcips_interval_choice_valuation_selected_power_product. (exists ff_lt_bpcips_interval_choice_valuation_selected_power_product_bound. ff_lt_bpcips_interval_choice_valuation_selected_power_product_bound + S ff_i_bpcips_interval_choice_valuation_selected_power_product = bpr_choice_exponent_bpcips_interval_choice) -> exists ff_p_bpcips_interval_choice_valuation_selected_power_product ff_r_bpcips_interval_choice_valuation_selected_power_product ff_s_bpcips_interval_choice_valuation_selected_power_product. ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_factor. ff_h_bpcips_interval_choice_valuation_selected_power_product_factor + S (ff_p_bpcips_interval_choice_valuation_selected_power_product) = S ((S (ff_i_bpcips_interval_choice_valuation_selected_power_product)) * bpr_power_scale_bpcips_interval_choice_valuation_selected_power)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_factor. bpr_power_code_bpcips_interval_choice_valuation_selected_power = ff_q_bpcips_interval_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcips_interval_choice_valuation_selected_power_product)) * bpr_power_scale_bpcips_interval_choice_valuation_selected_power) + (ff_p_bpcips_interval_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_partial. ff_h_bpcips_interval_choice_valuation_selected_power_product_partial + S (ff_r_bpcips_interval_choice_valuation_selected_power_product) = S ((S (ff_i_bpcips_interval_choice_valuation_selected_power_product)) * ff_v_bpcips_interval_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_partial. ff_u_bpcips_interval_choice_valuation_selected_power_product = ff_q_bpcips_interval_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcips_interval_choice_valuation_selected_power_product)) * ff_v_bpcips_interval_choice_valuation_selected_power_product) + (ff_r_bpcips_interval_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_successor. ff_h_bpcips_interval_choice_valuation_selected_power_product_successor + S (ff_s_bpcips_interval_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcips_interval_choice_valuation_selected_power_product)) * ff_v_bpcips_interval_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_successor. ff_u_bpcips_interval_choice_valuation_selected_power_product = ff_q_bpcips_interval_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcips_interval_choice_valuation_selected_power_product)) * ff_v_bpcips_interval_choice_valuation_selected_power_product) + (ff_s_bpcips_interval_choice_valuation_selected_power_product))) /\ ff_s_bpcips_interval_choice_valuation_selected_power_product = ff_r_bpcips_interval_choice_valuation_selected_power_product * ff_p_bpcips_interval_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcips_interval_choice_valuation_selected_divides. n = (bpr_power_value_bpcips_interval_choice_valuation_selected) * bpr_divides_quotient_bpcips_interval_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcips_interval_choice_valuation. (exists bpr_le_gap_bpcips_interval_choice_valuation_candidate_bound. bpr_le_gap_bpcips_interval_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcips_interval_choice_valuation) = (n)) -> (exists bpr_power_value_bpcips_interval_choice_valuation_candidate. ((exists bpr_power_code_bpcips_interval_choice_valuation_candidate_power bpr_power_scale_bpcips_interval_choice_valuation_candidate_power. ((forall bpr_power_index_bpcips_interval_choice_valuation_candidate_power. (exists bpr_gap_bpcips_interval_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcips_interval_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcips_interval_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcips_interval_choice_valuation) -> (((exists bpr_height_bpcips_interval_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcips_interval_choice_valuation_candidate_power_repeat_entry + S (S (a + bpr_index_bpcips_interval)) = S ((S (bpr_power_index_bpcips_interval_choice_valuation_candidate_power)) * bpr_power_scale_bpcips_interval_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcips_interval_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcips_interval_choice_valuation_candidate_power = bpr_quotient_bpcips_interval_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcips_interval_choice_valuation_candidate_power)) * bpr_power_scale_bpcips_interval_choice_valuation_candidate_power) + (S (a + bpr_index_bpcips_interval))))) /\ (exists ff_u_bpcips_interval_choice_valuation_candidate_power_product ff_v_bpcips_interval_choice_valuation_candidate_power_product. ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_start. ff_h_bpcips_interval_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_start. ff_u_bpcips_interval_choice_valuation_candidate_power_product = ff_q_bpcips_interval_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_terminal. ff_h_bpcips_interval_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcips_interval_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcips_interval_choice_valuation)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_terminal. ff_u_bpcips_interval_choice_valuation_candidate_power_product = ff_q_bpcips_interval_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcips_interval_choice_valuation)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product) + (bpr_power_value_bpcips_interval_choice_valuation_candidate))) /\ forall ff_i_bpcips_interval_choice_valuation_candidate_power_product. (exists ff_lt_bpcips_interval_choice_valuation_candidate_power_product_bound. ff_lt_bpcips_interval_choice_valuation_candidate_power_product_bound + S ff_i_bpcips_interval_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcips_interval_choice_valuation) -> exists ff_p_bpcips_interval_choice_valuation_candidate_power_product ff_r_bpcips_interval_choice_valuation_candidate_power_product ff_s_bpcips_interval_choice_valuation_candidate_power_product. ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_factor. ff_h_bpcips_interval_choice_valuation_candidate_power_product_factor + S (ff_p_bpcips_interval_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcips_interval_choice_valuation_candidate_power)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcips_interval_choice_valuation_candidate_power = ff_q_bpcips_interval_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcips_interval_choice_valuation_candidate_power) + (ff_p_bpcips_interval_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_partial. ff_h_bpcips_interval_choice_valuation_candidate_power_product_partial + S (ff_r_bpcips_interval_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_partial. ff_u_bpcips_interval_choice_valuation_candidate_power_product = ff_q_bpcips_interval_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product) + (ff_r_bpcips_interval_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_successor. ff_h_bpcips_interval_choice_valuation_candidate_power_product_successor + S (ff_s_bpcips_interval_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_successor. ff_u_bpcips_interval_choice_valuation_candidate_power_product = ff_q_bpcips_interval_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product) + (ff_s_bpcips_interval_choice_valuation_candidate_power_product))) /\ ff_s_bpcips_interval_choice_valuation_candidate_power_product = ff_r_bpcips_interval_choice_valuation_candidate_power_product * ff_p_bpcips_interval_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcips_interval_choice_valuation_candidate_divides. n = (bpr_power_value_bpcips_interval_choice_valuation_candidate) * bpr_divides_quotient_bpcips_interval_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcips_interval_choice_valuation_candidate_below. bpr_le_gap_bpcips_interval_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcips_interval_choice_valuation) = (bpr_choice_exponent_bpcips_interval_choice))) /\ (exists bpr_power_code_bpcips_interval_choice_power bpr_power_scale_bpcips_interval_choice_power. ((forall bpr_power_index_bpcips_interval_choice_power. (exists bpr_gap_bpcips_interval_choice_power_repeat_bound. bpr_gap_bpcips_interval_choice_power_repeat_bound + S (bpr_power_index_bpcips_interval_choice_power) = bpr_choice_exponent_bpcips_interval_choice) -> (((exists bpr_height_bpcips_interval_choice_power_repeat_entry. bpr_height_bpcips_interval_choice_power_repeat_entry + S (S (a + bpr_index_bpcips_interval)) = S ((S (bpr_power_index_bpcips_interval_choice_power)) * bpr_power_scale_bpcips_interval_choice_power)) /\ exists bpr_quotient_bpcips_interval_choice_power_repeat_entry. bpr_power_code_bpcips_interval_choice_power = bpr_quotient_bpcips_interval_choice_power_repeat_entry * S ((S (bpr_power_index_bpcips_interval_choice_power)) * bpr_power_scale_bpcips_interval_choice_power) + (S (a + bpr_index_bpcips_interval))))) /\ (exists ff_u_bpcips_interval_choice_power_product ff_v_bpcips_interval_choice_power_product. ((((exists ff_h_bpcips_interval_choice_power_product_start. ff_h_bpcips_interval_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_interval_choice_power_product)) /\ exists ff_q_bpcips_interval_choice_power_product_start. ff_u_bpcips_interval_choice_power_product = ff_q_bpcips_interval_choice_power_product_start * S ((S (0)) * ff_v_bpcips_interval_choice_power_product) + (1))) /\ ((((exists ff_h_bpcips_interval_choice_power_product_terminal. ff_h_bpcips_interval_choice_power_product_terminal + S (bpr_value_bpcips_interval) = S ((S (bpr_choice_exponent_bpcips_interval_choice)) * ff_v_bpcips_interval_choice_power_product)) /\ exists ff_q_bpcips_interval_choice_power_product_terminal. ff_u_bpcips_interval_choice_power_product = ff_q_bpcips_interval_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcips_interval_choice)) * ff_v_bpcips_interval_choice_power_product) + (bpr_value_bpcips_interval))) /\ forall ff_i_bpcips_interval_choice_power_product. (exists ff_lt_bpcips_interval_choice_power_product_bound. ff_lt_bpcips_interval_choice_power_product_bound + S ff_i_bpcips_interval_choice_power_product = bpr_choice_exponent_bpcips_interval_choice) -> exists ff_p_bpcips_interval_choice_power_product ff_r_bpcips_interval_choice_power_product ff_s_bpcips_interval_choice_power_product. ((((exists ff_h_bpcips_interval_choice_power_product_factor. ff_h_bpcips_interval_choice_power_product_factor + S (ff_p_bpcips_interval_choice_power_product) = S ((S (ff_i_bpcips_interval_choice_power_product)) * bpr_power_scale_bpcips_interval_choice_power)) /\ exists ff_q_bpcips_interval_choice_power_product_factor. bpr_power_code_bpcips_interval_choice_power = ff_q_bpcips_interval_choice_power_product_factor * S ((S (ff_i_bpcips_interval_choice_power_product)) * bpr_power_scale_bpcips_interval_choice_power) + (ff_p_bpcips_interval_choice_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_power_product_partial. ff_h_bpcips_interval_choice_power_product_partial + S (ff_r_bpcips_interval_choice_power_product) = S ((S (ff_i_bpcips_interval_choice_power_product)) * ff_v_bpcips_interval_choice_power_product)) /\ exists ff_q_bpcips_interval_choice_power_product_partial. ff_u_bpcips_interval_choice_power_product = ff_q_bpcips_interval_choice_power_product_partial * S ((S (ff_i_bpcips_interval_choice_power_product)) * ff_v_bpcips_interval_choice_power_product) + (ff_r_bpcips_interval_choice_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_power_product_successor. ff_h_bpcips_interval_choice_power_product_successor + S (ff_s_bpcips_interval_choice_power_product) = S ((S (S ff_i_bpcips_interval_choice_power_product)) * ff_v_bpcips_interval_choice_power_product)) /\ exists ff_q_bpcips_interval_choice_power_product_successor. ff_u_bpcips_interval_choice_power_product = ff_q_bpcips_interval_choice_power_product_successor * S ((S (S ff_i_bpcips_interval_choice_power_product)) * ff_v_bpcips_interval_choice_power_product) + (ff_s_bpcips_interval_choice_power_product))) /\ ff_s_bpcips_interval_choice_power_product = ff_r_bpcips_interval_choice_power_product * ff_p_bpcips_interval_choice_power_product)))))))))) \/ (~((~(S (a + bpr_index_bpcips_interval) = 1) /\ forall bpr_left_bpcips_interval_choice_prime bpr_right_bpcips_interval_choice_prime. S (a + bpr_index_bpcips_interval) = bpr_left_bpcips_interval_choice_prime * bpr_right_bpcips_interval_choice_prime -> bpr_left_bpcips_interval_choice_prime = 1 \/ bpr_right_bpcips_interval_choice_prime = 1)) /\ bpr_value_bpcips_interval = 1))))) -> forall i p. (exists bpr_gap_bpcips_bound. bpr_gap_bpcips_bound + S (i) = l) -> (((exists bpr_height_bpcips_source_entry. bpr_height_bpcips_source_entry + S (p) = S ((S (a + i)) * c)) /\ exists bpr_quotient_bpcips_source_entry. b = bpr_quotient_bpcips_source_entry * S ((S (a + i)) * c) + (p))) -> (((exists bpr_height_bpcips_target_entry. bpr_height_bpcips_target_entry + S (p) = S ((S (i)) * e)) /\ exists bpr_quotient_bpcips_target_entry. d = bpr_quotient_bpcips_target_entry * S ((S (i)) * e) + (p)))

Proof neighborhood

Direct theorem prerequisites

BT0015 add_le_add_left BT0042 beta_at_unique BT00YO prime_contribution_choice_functional

Direct theorem dependents

BT010R prime_contribution_prefix_interval_split

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

53 script commands · 12 reading checkpoints · 8 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
add le add leftbeta at uniqueprime contribution choice functional
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro l
  8. L8
    intro hsource
  9. L9
    intro hinterval
  10. L10
    intro i
02Fix variables and assumptionsL11–13

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro p
  2. L12
    intro hi
  3. L13
    intro hp
03Establish hsource_bound_rawL14–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add le add left.

  1. L14
    have hsource_bound_raw : Le(a + S i,a + l)Definitions: Le(a + S i,a + l)Original native command in the exact edition
  2. L15
    specialize add_le_add_left (S i)
  3. L16
    specialize add_le_add_left l
  4. L17
    specialize add_le_add_left a
  5. L18
    apply add_le_add_left
  6. L19
    exact hi
04Establish hadd_succL20–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA4.

  1. L20
    have hadd_succ : a + S i = S (a + i)
  2. L21
    apply PA4
  3. L22
    rewrite hadd_succ at hsource_bound_raw
05Establish hsource_boundL23–24

Establish this local claim before using it. It is not an additional assumption.

  1. L23
    have hsource_bound : Lt(a + i,a + l)Definitions: Lt(a + i,a + l)Original native command in the exact edition
  2. L24
    exact hsource_bound_raw
06Establish hsource_entryL25–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hsource.

  1. L25
    have hsource_entry : ∃ q. BetaAt(b,c,a + i,q) ∧ (Prime(S (a + i)) ∧ (∃ x. PowerValuation(S (a + i),n,x) ∧ Pow(S (a + i),x,q)) ∨ ¬Prime(S (a + i)) ∧ q = 1)Definitions: BetaAt(b,c,a + i,q)Prime(S (a + i))PowerValuation(S (a + i),n,x)Pow(S (a + i),x,q)Original native command in the exact edition
  2. L26
    apply hsource
  3. L27
    exact hsource_bound
07Separate the logical casesL28–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L28
    cases hsource_entry
  2. L29
    cases hsource_entry_witness
08Establish hinterval_entryL30–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hinterval.

  1. L30
    have hinterval_entry : ∃ r. BetaAt(d,e,i,r) ∧ (Prime(S (a + i)) ∧ (∃ x. PowerValuation(S (a + i),n,x) ∧ Pow(S (a + i),x,r)) ∨ ¬Prime(S (a + i)) ∧ r = 1)Definitions: BetaAt(d,e,i,r)Prime(S (a + i))PowerValuation(S (a + i),n,x)Pow(S (a + i),x,r)Original native command in the exact edition
  2. L31
    apply hinterval
  3. L32
    exact hi
09Separate the logical casesL33–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L33
    cases hinterval_entry
  2. L34
    cases hinterval_entry_witness
10Establish hpqL35–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L35
    have hpq : p = x
  2. L36
    apply beta_at_unique
  3. L37
    exact hp
  4. L38
    exact hsource_entry_witness_left
11Establish hqrL39–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution choice functional.

  1. L39
    have hqr : x = x1
  2. L40
    specialize prime_contribution_choice_functional n
  3. L41
    specialize prime_contribution_choice_functional (a + i)
  4. L42
    specialize prime_contribution_choice_functional x
  5. L43
    specialize prime_contribution_choice_functional x1
  6. L44
    apply prime_contribution_choice_functional
  7. L45
    exact hsource_entry_witness_right
  8. L46
    exact hinterval_entry_witness_right
12Establish hprL47–53

Establish this local claim before using it. It is not an additional assumption.

  1. L47
    have hpr : p = x1
  2. L48
    trans x
  3. L49
    exact hpq
  4. L50
    exact hqr
  5. L51
    rewrite hpr
  6. L52
    rewrite hpr
  7. L53
    exact hinterval_entry_witness_left

Library-wide reading audit

Original defined command ledger · 53 lines
  1. 0001intro n
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro l
  8. 0008intro hsource
  9. 0009intro hinterval
  10. 0010intro i
  11. 0011intro p
  12. 0012intro hi
  13. 0013intro hp
  14. 0014have hsource_bound_raw : Le(a + S i,a + l)
    Exact native replay linehave hsource_bound_raw : exists bpr_gap_bpcips_shifted_bound. bpr_gap_bpcips_shifted_bound + (a + S i) = a + l
  15. 0015specialize add_le_add_left (S i)
  16. 0016specialize add_le_add_left l
  17. 0017specialize add_le_add_left a
  18. 0018apply add_le_add_left
  19. 0019exact hi
  20. 0020have hadd_succ : a + S i = S (a + i)
  21. 0021apply PA4
  22. 0022rewrite hadd_succ at hsource_bound_raw
  23. 0023have hsource_bound : Lt(a + i,a + l)
    Exact native replay linehave hsource_bound : exists bpr_gap_bpcips_source_bound. bpr_gap_bpcips_source_bound + S (a + i) = a + l
  24. 0024exact hsource_bound_raw
  25. 0025have hsource_entry : ∃ q. BetaAt(b,c,a + i,q) ∧ (Prime(S (a + i)) ∧ (∃ x. PowerValuation(S (a + i),n,x) ∧ Pow(S (a + i),x,q)) ∨ ¬Prime(S (a + i)) ∧ q = 1)
    Exact native replay linehave hsource_entry : exists q. ((((exists bpr_height_bpcips_source_local. bpr_height_bpcips_source_local + S (q) = S ((S (a + i)) * c)) /\ exists bpr_quotient_bpcips_source_local. b = bpr_quotient_bpcips_source_local * S ((S (a + i)) * c) + (q))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpcips_source_choice_prime bpr_right_bpcips_source_choice_prime. S (a + i) = bpr_left_bpcips_source_choice_prime * bpr_right_bpcips_source_choice_prime -> bpr_left_bpcips_source_choice_prime = 1 \/ bpr_right_bpcips_source_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcips_source_choice. ((((exists bpr_le_gap_bpcips_source_choice_valuation_selected_bound. bpr_le_gap_bpcips_source_choice_valuation_selected_bound + (bpr_choice_exponent_bpcips_source_choice) = (n)) /\ (exists bpr_power_value_bpcips_source_choice_valuation_selected. ((exists bpr_power_code_bpcips_source_choice_valuation_selected_power bpr_power_scale_bpcips_source_choice_valuation_selected_power. ((forall bpr_power_index_bpcips_source_choice_valuation_selected_power. (exists bpr_gap_bpcips_source_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcips_source_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcips_source_choice_valuation_selected_power) = bpr_choice_exponent_bpcips_source_choice) -> (((exists bpr_height_bpcips_source_choice_valuation_selected_power_repeat_entry. bpr_height_bpcips_source_choice_valuation_selected_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcips_source_choice_valuation_selected_power)) * bpr_power_scale_bpcips_source_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcips_source_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcips_source_choice_valuation_selected_power = bpr_quotient_bpcips_source_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcips_source_choice_valuation_selected_power)) * bpr_power_scale_bpcips_source_choice_valuation_selected_power) + (S (a + i))))) /\ (exists ff_u_bpcips_source_choice_valuation_selected_power_product ff_v_bpcips_source_choice_valuation_selected_power_product. ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_start. ff_h_bpcips_source_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_start. ff_u_bpcips_source_choice_valuation_selected_power_product = ff_q_bpcips_source_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcips_source_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_terminal. ff_h_bpcips_source_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcips_source_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcips_source_choice)) * ff_v_bpcips_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_terminal. ff_u_bpcips_source_choice_valuation_selected_power_product = ff_q_bpcips_source_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcips_source_choice)) * ff_v_bpcips_source_choice_valuation_selected_power_product) + (bpr_power_value_bpcips_source_choice_valuation_selected))) /\ forall ff_i_bpcips_source_choice_valuation_selected_power_product. (exists ff_lt_bpcips_source_choice_valuation_selected_power_product_bound. ff_lt_bpcips_source_choice_valuation_selected_power_product_bound + S ff_i_bpcips_source_choice_valuation_selected_power_product = bpr_choice_exponent_bpcips_source_choice) -> exists ff_p_bpcips_source_choice_valuation_selected_power_product ff_r_bpcips_source_choice_valuation_selected_power_product ff_s_bpcips_source_choice_valuation_selected_power_product. ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_factor. ff_h_bpcips_source_choice_valuation_selected_power_product_factor + S (ff_p_bpcips_source_choice_valuation_selected_power_product) = S ((S (ff_i_bpcips_source_choice_valuation_selected_power_product)) * bpr_power_scale_bpcips_source_choice_valuation_selected_power)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_factor. bpr_power_code_bpcips_source_choice_valuation_selected_power = ff_q_bpcips_source_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcips_source_choice_valuation_selected_power_product)) * bpr_power_scale_bpcips_source_choice_valuation_selected_power) + (ff_p_bpcips_source_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_partial. ff_h_bpcips_source_choice_valuation_selected_power_product_partial + S (ff_r_bpcips_source_choice_valuation_selected_power_product) = S ((S (ff_i_bpcips_source_choice_valuation_selected_power_product)) * ff_v_bpcips_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_partial. ff_u_bpcips_source_choice_valuation_selected_power_product = ff_q_bpcips_source_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcips_source_choice_valuation_selected_power_product)) * ff_v_bpcips_source_choice_valuation_selected_power_product) + (ff_r_bpcips_source_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcips_source_choice_valuation_selected_power_product_successor. ff_h_bpcips_source_choice_valuation_selected_power_product_successor + S (ff_s_bpcips_source_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcips_source_choice_valuation_selected_power_product)) * ff_v_bpcips_source_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_selected_power_product_successor. ff_u_bpcips_source_choice_valuation_selected_power_product = ff_q_bpcips_source_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcips_source_choice_valuation_selected_power_product)) * ff_v_bpcips_source_choice_valuation_selected_power_product) + (ff_s_bpcips_source_choice_valuation_selected_power_product))) /\ ff_s_bpcips_source_choice_valuation_selected_power_product = ff_r_bpcips_source_choice_valuation_selected_power_product * ff_p_bpcips_source_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcips_source_choice_valuation_selected_divides. n = (bpr_power_value_bpcips_source_choice_valuation_selected) * bpr_divides_quotient_bpcips_source_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcips_source_choice_valuation. (exists bpr_le_gap_bpcips_source_choice_valuation_candidate_bound. bpr_le_gap_bpcips_source_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcips_source_choice_valuation) = (n)) -> (exists bpr_power_value_bpcips_source_choice_valuation_candidate. ((exists bpr_power_code_bpcips_source_choice_valuation_candidate_power bpr_power_scale_bpcips_source_choice_valuation_candidate_power. ((forall bpr_power_index_bpcips_source_choice_valuation_candidate_power. (exists bpr_gap_bpcips_source_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcips_source_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcips_source_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcips_source_choice_valuation) -> (((exists bpr_height_bpcips_source_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcips_source_choice_valuation_candidate_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcips_source_choice_valuation_candidate_power)) * bpr_power_scale_bpcips_source_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcips_source_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcips_source_choice_valuation_candidate_power = bpr_quotient_bpcips_source_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcips_source_choice_valuation_candidate_power)) * bpr_power_scale_bpcips_source_choice_valuation_candidate_power) + (S (a + i))))) /\ (exists ff_u_bpcips_source_choice_valuation_candidate_power_product ff_v_bpcips_source_choice_valuation_candidate_power_product. ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_start. ff_h_bpcips_source_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_start. ff_u_bpcips_source_choice_valuation_candidate_power_product = ff_q_bpcips_source_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcips_source_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_terminal. ff_h_bpcips_source_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcips_source_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcips_source_choice_valuation)) * ff_v_bpcips_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_terminal. ff_u_bpcips_source_choice_valuation_candidate_power_product = ff_q_bpcips_source_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcips_source_choice_valuation)) * ff_v_bpcips_source_choice_valuation_candidate_power_product) + (bpr_power_value_bpcips_source_choice_valuation_candidate))) /\ forall ff_i_bpcips_source_choice_valuation_candidate_power_product. (exists ff_lt_bpcips_source_choice_valuation_candidate_power_product_bound. ff_lt_bpcips_source_choice_valuation_candidate_power_product_bound + S ff_i_bpcips_source_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcips_source_choice_valuation) -> exists ff_p_bpcips_source_choice_valuation_candidate_power_product ff_r_bpcips_source_choice_valuation_candidate_power_product ff_s_bpcips_source_choice_valuation_candidate_power_product. ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_factor. ff_h_bpcips_source_choice_valuation_candidate_power_product_factor + S (ff_p_bpcips_source_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcips_source_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcips_source_choice_valuation_candidate_power)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcips_source_choice_valuation_candidate_power = ff_q_bpcips_source_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcips_source_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcips_source_choice_valuation_candidate_power) + (ff_p_bpcips_source_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_partial. ff_h_bpcips_source_choice_valuation_candidate_power_product_partial + S (ff_r_bpcips_source_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcips_source_choice_valuation_candidate_power_product)) * ff_v_bpcips_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_partial. ff_u_bpcips_source_choice_valuation_candidate_power_product = ff_q_bpcips_source_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcips_source_choice_valuation_candidate_power_product)) * ff_v_bpcips_source_choice_valuation_candidate_power_product) + (ff_r_bpcips_source_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcips_source_choice_valuation_candidate_power_product_successor. ff_h_bpcips_source_choice_valuation_candidate_power_product_successor + S (ff_s_bpcips_source_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcips_source_choice_valuation_candidate_power_product)) * ff_v_bpcips_source_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_source_choice_valuation_candidate_power_product_successor. ff_u_bpcips_source_choice_valuation_candidate_power_product = ff_q_bpcips_source_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcips_source_choice_valuation_candidate_power_product)) * ff_v_bpcips_source_choice_valuation_candidate_power_product) + (ff_s_bpcips_source_choice_valuation_candidate_power_product))) /\ ff_s_bpcips_source_choice_valuation_candidate_power_product = ff_r_bpcips_source_choice_valuation_candidate_power_product * ff_p_bpcips_source_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcips_source_choice_valuation_candidate_divides. n = (bpr_power_value_bpcips_source_choice_valuation_candidate) * bpr_divides_quotient_bpcips_source_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcips_source_choice_valuation_candidate_below. bpr_le_gap_bpcips_source_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcips_source_choice_valuation) = (bpr_choice_exponent_bpcips_source_choice))) /\ (exists bpr_power_code_bpcips_source_choice_power bpr_power_scale_bpcips_source_choice_power. ((forall bpr_power_index_bpcips_source_choice_power. (exists bpr_gap_bpcips_source_choice_power_repeat_bound. bpr_gap_bpcips_source_choice_power_repeat_bound + S (bpr_power_index_bpcips_source_choice_power) = bpr_choice_exponent_bpcips_source_choice) -> (((exists bpr_height_bpcips_source_choice_power_repeat_entry. bpr_height_bpcips_source_choice_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcips_source_choice_power)) * bpr_power_scale_bpcips_source_choice_power)) /\ exists bpr_quotient_bpcips_source_choice_power_repeat_entry. bpr_power_code_bpcips_source_choice_power = bpr_quotient_bpcips_source_choice_power_repeat_entry * S ((S (bpr_power_index_bpcips_source_choice_power)) * bpr_power_scale_bpcips_source_choice_power) + (S (a + i))))) /\ (exists ff_u_bpcips_source_choice_power_product ff_v_bpcips_source_choice_power_product. ((((exists ff_h_bpcips_source_choice_power_product_start. ff_h_bpcips_source_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_source_choice_power_product)) /\ exists ff_q_bpcips_source_choice_power_product_start. ff_u_bpcips_source_choice_power_product = ff_q_bpcips_source_choice_power_product_start * S ((S (0)) * ff_v_bpcips_source_choice_power_product) + (1))) /\ ((((exists ff_h_bpcips_source_choice_power_product_terminal. ff_h_bpcips_source_choice_power_product_terminal + S (q) = S ((S (bpr_choice_exponent_bpcips_source_choice)) * ff_v_bpcips_source_choice_power_product)) /\ exists ff_q_bpcips_source_choice_power_product_terminal. ff_u_bpcips_source_choice_power_product = ff_q_bpcips_source_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcips_source_choice)) * ff_v_bpcips_source_choice_power_product) + (q))) /\ forall ff_i_bpcips_source_choice_power_product. (exists ff_lt_bpcips_source_choice_power_product_bound. ff_lt_bpcips_source_choice_power_product_bound + S ff_i_bpcips_source_choice_power_product = bpr_choice_exponent_bpcips_source_choice) -> exists ff_p_bpcips_source_choice_power_product ff_r_bpcips_source_choice_power_product ff_s_bpcips_source_choice_power_product. ((((exists ff_h_bpcips_source_choice_power_product_factor. ff_h_bpcips_source_choice_power_product_factor + S (ff_p_bpcips_source_choice_power_product) = S ((S (ff_i_bpcips_source_choice_power_product)) * bpr_power_scale_bpcips_source_choice_power)) /\ exists ff_q_bpcips_source_choice_power_product_factor. bpr_power_code_bpcips_source_choice_power = ff_q_bpcips_source_choice_power_product_factor * S ((S (ff_i_bpcips_source_choice_power_product)) * bpr_power_scale_bpcips_source_choice_power) + (ff_p_bpcips_source_choice_power_product))) /\ ((((exists ff_h_bpcips_source_choice_power_product_partial. ff_h_bpcips_source_choice_power_product_partial + S (ff_r_bpcips_source_choice_power_product) = S ((S (ff_i_bpcips_source_choice_power_product)) * ff_v_bpcips_source_choice_power_product)) /\ exists ff_q_bpcips_source_choice_power_product_partial. ff_u_bpcips_source_choice_power_product = ff_q_bpcips_source_choice_power_product_partial * S ((S (ff_i_bpcips_source_choice_power_product)) * ff_v_bpcips_source_choice_power_product) + (ff_r_bpcips_source_choice_power_product))) /\ ((((exists ff_h_bpcips_source_choice_power_product_successor. ff_h_bpcips_source_choice_power_product_successor + S (ff_s_bpcips_source_choice_power_product) = S ((S (S ff_i_bpcips_source_choice_power_product)) * ff_v_bpcips_source_choice_power_product)) /\ exists ff_q_bpcips_source_choice_power_product_successor. ff_u_bpcips_source_choice_power_product = ff_q_bpcips_source_choice_power_product_successor * S ((S (S ff_i_bpcips_source_choice_power_product)) * ff_v_bpcips_source_choice_power_product) + (ff_s_bpcips_source_choice_power_product))) /\ ff_s_bpcips_source_choice_power_product = ff_r_bpcips_source_choice_power_product * ff_p_bpcips_source_choice_power_product)))))))))) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpcips_source_choice_prime bpr_right_bpcips_source_choice_prime. S (a + i) = bpr_left_bpcips_source_choice_prime * bpr_right_bpcips_source_choice_prime -> bpr_left_bpcips_source_choice_prime = 1 \/ bpr_right_bpcips_source_choice_prime = 1)) /\ q = 1))))
  26. 0026apply hsource
  27. 0027exact hsource_bound
  28. 0028cases hsource_entry
  29. 0029cases hsource_entry_witness
  30. 0030have hinterval_entry : ∃ r. BetaAt(d,e,i,r) ∧ (Prime(S (a + i)) ∧ (∃ x. PowerValuation(S (a + i),n,x) ∧ Pow(S (a + i),x,r)) ∨ ¬Prime(S (a + i)) ∧ r = 1)
    Exact native replay linehave hinterval_entry : exists r. ((((exists bpr_height_bpcips_interval_local. bpr_height_bpcips_interval_local + S (r) = S ((S (i)) * e)) /\ exists bpr_quotient_bpcips_interval_local. d = bpr_quotient_bpcips_interval_local * S ((S (i)) * e) + (r))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpcips_interval_choice_prime bpr_right_bpcips_interval_choice_prime. S (a + i) = bpr_left_bpcips_interval_choice_prime * bpr_right_bpcips_interval_choice_prime -> bpr_left_bpcips_interval_choice_prime = 1 \/ bpr_right_bpcips_interval_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcips_interval_choice. ((((exists bpr_le_gap_bpcips_interval_choice_valuation_selected_bound. bpr_le_gap_bpcips_interval_choice_valuation_selected_bound + (bpr_choice_exponent_bpcips_interval_choice) = (n)) /\ (exists bpr_power_value_bpcips_interval_choice_valuation_selected. ((exists bpr_power_code_bpcips_interval_choice_valuation_selected_power bpr_power_scale_bpcips_interval_choice_valuation_selected_power. ((forall bpr_power_index_bpcips_interval_choice_valuation_selected_power. (exists bpr_gap_bpcips_interval_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcips_interval_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcips_interval_choice_valuation_selected_power) = bpr_choice_exponent_bpcips_interval_choice) -> (((exists bpr_height_bpcips_interval_choice_valuation_selected_power_repeat_entry. bpr_height_bpcips_interval_choice_valuation_selected_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcips_interval_choice_valuation_selected_power)) * bpr_power_scale_bpcips_interval_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcips_interval_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcips_interval_choice_valuation_selected_power = bpr_quotient_bpcips_interval_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcips_interval_choice_valuation_selected_power)) * bpr_power_scale_bpcips_interval_choice_valuation_selected_power) + (S (a + i))))) /\ (exists ff_u_bpcips_interval_choice_valuation_selected_power_product ff_v_bpcips_interval_choice_valuation_selected_power_product. ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_start. ff_h_bpcips_interval_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_interval_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_start. ff_u_bpcips_interval_choice_valuation_selected_power_product = ff_q_bpcips_interval_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcips_interval_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_terminal. ff_h_bpcips_interval_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcips_interval_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcips_interval_choice)) * ff_v_bpcips_interval_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_terminal. ff_u_bpcips_interval_choice_valuation_selected_power_product = ff_q_bpcips_interval_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcips_interval_choice)) * ff_v_bpcips_interval_choice_valuation_selected_power_product) + (bpr_power_value_bpcips_interval_choice_valuation_selected))) /\ forall ff_i_bpcips_interval_choice_valuation_selected_power_product. (exists ff_lt_bpcips_interval_choice_valuation_selected_power_product_bound. ff_lt_bpcips_interval_choice_valuation_selected_power_product_bound + S ff_i_bpcips_interval_choice_valuation_selected_power_product = bpr_choice_exponent_bpcips_interval_choice) -> exists ff_p_bpcips_interval_choice_valuation_selected_power_product ff_r_bpcips_interval_choice_valuation_selected_power_product ff_s_bpcips_interval_choice_valuation_selected_power_product. ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_factor. ff_h_bpcips_interval_choice_valuation_selected_power_product_factor + S (ff_p_bpcips_interval_choice_valuation_selected_power_product) = S ((S (ff_i_bpcips_interval_choice_valuation_selected_power_product)) * bpr_power_scale_bpcips_interval_choice_valuation_selected_power)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_factor. bpr_power_code_bpcips_interval_choice_valuation_selected_power = ff_q_bpcips_interval_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcips_interval_choice_valuation_selected_power_product)) * bpr_power_scale_bpcips_interval_choice_valuation_selected_power) + (ff_p_bpcips_interval_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_partial. ff_h_bpcips_interval_choice_valuation_selected_power_product_partial + S (ff_r_bpcips_interval_choice_valuation_selected_power_product) = S ((S (ff_i_bpcips_interval_choice_valuation_selected_power_product)) * ff_v_bpcips_interval_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_partial. ff_u_bpcips_interval_choice_valuation_selected_power_product = ff_q_bpcips_interval_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcips_interval_choice_valuation_selected_power_product)) * ff_v_bpcips_interval_choice_valuation_selected_power_product) + (ff_r_bpcips_interval_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_selected_power_product_successor. ff_h_bpcips_interval_choice_valuation_selected_power_product_successor + S (ff_s_bpcips_interval_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcips_interval_choice_valuation_selected_power_product)) * ff_v_bpcips_interval_choice_valuation_selected_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_selected_power_product_successor. ff_u_bpcips_interval_choice_valuation_selected_power_product = ff_q_bpcips_interval_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcips_interval_choice_valuation_selected_power_product)) * ff_v_bpcips_interval_choice_valuation_selected_power_product) + (ff_s_bpcips_interval_choice_valuation_selected_power_product))) /\ ff_s_bpcips_interval_choice_valuation_selected_power_product = ff_r_bpcips_interval_choice_valuation_selected_power_product * ff_p_bpcips_interval_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcips_interval_choice_valuation_selected_divides. n = (bpr_power_value_bpcips_interval_choice_valuation_selected) * bpr_divides_quotient_bpcips_interval_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcips_interval_choice_valuation. (exists bpr_le_gap_bpcips_interval_choice_valuation_candidate_bound. bpr_le_gap_bpcips_interval_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcips_interval_choice_valuation) = (n)) -> (exists bpr_power_value_bpcips_interval_choice_valuation_candidate. ((exists bpr_power_code_bpcips_interval_choice_valuation_candidate_power bpr_power_scale_bpcips_interval_choice_valuation_candidate_power. ((forall bpr_power_index_bpcips_interval_choice_valuation_candidate_power. (exists bpr_gap_bpcips_interval_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcips_interval_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcips_interval_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcips_interval_choice_valuation) -> (((exists bpr_height_bpcips_interval_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcips_interval_choice_valuation_candidate_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcips_interval_choice_valuation_candidate_power)) * bpr_power_scale_bpcips_interval_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcips_interval_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcips_interval_choice_valuation_candidate_power = bpr_quotient_bpcips_interval_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcips_interval_choice_valuation_candidate_power)) * bpr_power_scale_bpcips_interval_choice_valuation_candidate_power) + (S (a + i))))) /\ (exists ff_u_bpcips_interval_choice_valuation_candidate_power_product ff_v_bpcips_interval_choice_valuation_candidate_power_product. ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_start. ff_h_bpcips_interval_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_start. ff_u_bpcips_interval_choice_valuation_candidate_power_product = ff_q_bpcips_interval_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_terminal. ff_h_bpcips_interval_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcips_interval_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcips_interval_choice_valuation)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_terminal. ff_u_bpcips_interval_choice_valuation_candidate_power_product = ff_q_bpcips_interval_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcips_interval_choice_valuation)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product) + (bpr_power_value_bpcips_interval_choice_valuation_candidate))) /\ forall ff_i_bpcips_interval_choice_valuation_candidate_power_product. (exists ff_lt_bpcips_interval_choice_valuation_candidate_power_product_bound. ff_lt_bpcips_interval_choice_valuation_candidate_power_product_bound + S ff_i_bpcips_interval_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcips_interval_choice_valuation) -> exists ff_p_bpcips_interval_choice_valuation_candidate_power_product ff_r_bpcips_interval_choice_valuation_candidate_power_product ff_s_bpcips_interval_choice_valuation_candidate_power_product. ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_factor. ff_h_bpcips_interval_choice_valuation_candidate_power_product_factor + S (ff_p_bpcips_interval_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcips_interval_choice_valuation_candidate_power)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcips_interval_choice_valuation_candidate_power = ff_q_bpcips_interval_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcips_interval_choice_valuation_candidate_power) + (ff_p_bpcips_interval_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_partial. ff_h_bpcips_interval_choice_valuation_candidate_power_product_partial + S (ff_r_bpcips_interval_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_partial. ff_u_bpcips_interval_choice_valuation_candidate_power_product = ff_q_bpcips_interval_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product) + (ff_r_bpcips_interval_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_valuation_candidate_power_product_successor. ff_h_bpcips_interval_choice_valuation_candidate_power_product_successor + S (ff_s_bpcips_interval_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcips_interval_choice_valuation_candidate_power_product_successor. ff_u_bpcips_interval_choice_valuation_candidate_power_product = ff_q_bpcips_interval_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcips_interval_choice_valuation_candidate_power_product)) * ff_v_bpcips_interval_choice_valuation_candidate_power_product) + (ff_s_bpcips_interval_choice_valuation_candidate_power_product))) /\ ff_s_bpcips_interval_choice_valuation_candidate_power_product = ff_r_bpcips_interval_choice_valuation_candidate_power_product * ff_p_bpcips_interval_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcips_interval_choice_valuation_candidate_divides. n = (bpr_power_value_bpcips_interval_choice_valuation_candidate) * bpr_divides_quotient_bpcips_interval_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcips_interval_choice_valuation_candidate_below. bpr_le_gap_bpcips_interval_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcips_interval_choice_valuation) = (bpr_choice_exponent_bpcips_interval_choice))) /\ (exists bpr_power_code_bpcips_interval_choice_power bpr_power_scale_bpcips_interval_choice_power. ((forall bpr_power_index_bpcips_interval_choice_power. (exists bpr_gap_bpcips_interval_choice_power_repeat_bound. bpr_gap_bpcips_interval_choice_power_repeat_bound + S (bpr_power_index_bpcips_interval_choice_power) = bpr_choice_exponent_bpcips_interval_choice) -> (((exists bpr_height_bpcips_interval_choice_power_repeat_entry. bpr_height_bpcips_interval_choice_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcips_interval_choice_power)) * bpr_power_scale_bpcips_interval_choice_power)) /\ exists bpr_quotient_bpcips_interval_choice_power_repeat_entry. bpr_power_code_bpcips_interval_choice_power = bpr_quotient_bpcips_interval_choice_power_repeat_entry * S ((S (bpr_power_index_bpcips_interval_choice_power)) * bpr_power_scale_bpcips_interval_choice_power) + (S (a + i))))) /\ (exists ff_u_bpcips_interval_choice_power_product ff_v_bpcips_interval_choice_power_product. ((((exists ff_h_bpcips_interval_choice_power_product_start. ff_h_bpcips_interval_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcips_interval_choice_power_product)) /\ exists ff_q_bpcips_interval_choice_power_product_start. ff_u_bpcips_interval_choice_power_product = ff_q_bpcips_interval_choice_power_product_start * S ((S (0)) * ff_v_bpcips_interval_choice_power_product) + (1))) /\ ((((exists ff_h_bpcips_interval_choice_power_product_terminal. ff_h_bpcips_interval_choice_power_product_terminal + S (r) = S ((S (bpr_choice_exponent_bpcips_interval_choice)) * ff_v_bpcips_interval_choice_power_product)) /\ exists ff_q_bpcips_interval_choice_power_product_terminal. ff_u_bpcips_interval_choice_power_product = ff_q_bpcips_interval_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcips_interval_choice)) * ff_v_bpcips_interval_choice_power_product) + (r))) /\ forall ff_i_bpcips_interval_choice_power_product. (exists ff_lt_bpcips_interval_choice_power_product_bound. ff_lt_bpcips_interval_choice_power_product_bound + S ff_i_bpcips_interval_choice_power_product = bpr_choice_exponent_bpcips_interval_choice) -> exists ff_p_bpcips_interval_choice_power_product ff_r_bpcips_interval_choice_power_product ff_s_bpcips_interval_choice_power_product. ((((exists ff_h_bpcips_interval_choice_power_product_factor. ff_h_bpcips_interval_choice_power_product_factor + S (ff_p_bpcips_interval_choice_power_product) = S ((S (ff_i_bpcips_interval_choice_power_product)) * bpr_power_scale_bpcips_interval_choice_power)) /\ exists ff_q_bpcips_interval_choice_power_product_factor. bpr_power_code_bpcips_interval_choice_power = ff_q_bpcips_interval_choice_power_product_factor * S ((S (ff_i_bpcips_interval_choice_power_product)) * bpr_power_scale_bpcips_interval_choice_power) + (ff_p_bpcips_interval_choice_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_power_product_partial. ff_h_bpcips_interval_choice_power_product_partial + S (ff_r_bpcips_interval_choice_power_product) = S ((S (ff_i_bpcips_interval_choice_power_product)) * ff_v_bpcips_interval_choice_power_product)) /\ exists ff_q_bpcips_interval_choice_power_product_partial. ff_u_bpcips_interval_choice_power_product = ff_q_bpcips_interval_choice_power_product_partial * S ((S (ff_i_bpcips_interval_choice_power_product)) * ff_v_bpcips_interval_choice_power_product) + (ff_r_bpcips_interval_choice_power_product))) /\ ((((exists ff_h_bpcips_interval_choice_power_product_successor. ff_h_bpcips_interval_choice_power_product_successor + S (ff_s_bpcips_interval_choice_power_product) = S ((S (S ff_i_bpcips_interval_choice_power_product)) * ff_v_bpcips_interval_choice_power_product)) /\ exists ff_q_bpcips_interval_choice_power_product_successor. ff_u_bpcips_interval_choice_power_product = ff_q_bpcips_interval_choice_power_product_successor * S ((S (S ff_i_bpcips_interval_choice_power_product)) * ff_v_bpcips_interval_choice_power_product) + (ff_s_bpcips_interval_choice_power_product))) /\ ff_s_bpcips_interval_choice_power_product = ff_r_bpcips_interval_choice_power_product * ff_p_bpcips_interval_choice_power_product)))))))))) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpcips_interval_choice_prime bpr_right_bpcips_interval_choice_prime. S (a + i) = bpr_left_bpcips_interval_choice_prime * bpr_right_bpcips_interval_choice_prime -> bpr_left_bpcips_interval_choice_prime = 1 \/ bpr_right_bpcips_interval_choice_prime = 1)) /\ r = 1))))
  31. 0031apply hinterval
  32. 0032exact hi
  33. 0033cases hinterval_entry
  34. 0034cases hinterval_entry_witness
  35. 0035have hpq : p = x
  36. 0036apply beta_at_unique
  37. 0037exact hp
  38. 0038exact hsource_entry_witness_left
  39. 0039have hqr : x = x1
  40. 0040specialize prime_contribution_choice_functional n
  41. 0041specialize prime_contribution_choice_functional (a + i)
  42. 0042specialize prime_contribution_choice_functional x
  43. 0043specialize prime_contribution_choice_functional x1
  44. 0044apply prime_contribution_choice_functional
  45. 0045exact hsource_entry_witness_right
  46. 0046exact hinterval_entry_witness_right
  47. 0047have hpr : p = x1
  48. 0048trans x
  49. 0049exact hpq
  50. 0050exact hqr
  51. 0051rewrite hpr
  52. 0052rewrite hpr
  53. 0053exact hinterval_entry_witness_left