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. ∀ l. ∃ b. ∃ c. ∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,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)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
6 occurrences
In local proof propositions
12 occurrences
Exact expanded native-PA statement
forall n a l. exists b c. (forall bpr_index_bpcipx_result. (exists bpr_gap_bpcipx_result_bound. bpr_gap_bpcipx_result_bound + S (bpr_index_bpcipx_result) = l) -> exists bpr_value_bpcipx_result. ((((exists bpr_height_bpcipx_result_decoded. bpr_height_bpcipx_result_decoded + S (bpr_value_bpcipx_result) = S ((S (bpr_index_bpcipx_result)) * c)) /\ exists bpr_quotient_bpcipx_result_decoded. b = bpr_quotient_bpcipx_result_decoded * S ((S (bpr_index_bpcipx_result)) * c) + (bpr_value_bpcipx_result))) /\ (((((~(S (a + bpr_index_bpcipx_result) = 1) /\ forall bpr_left_bpcipx_result_choice_prime bpr_right_bpcipx_result_choice_prime. S (a + bpr_index_bpcipx_result) = bpr_left_bpcipx_result_choice_prime * bpr_right_bpcipx_result_choice_prime -> bpr_left_bpcipx_result_choice_prime = 1 \/ bpr_right_bpcipx_result_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcipx_result_choice. ((((exists bpr_le_gap_bpcipx_result_choice_valuation_selected_bound. bpr_le_gap_bpcipx_result_choice_valuation_selected_bound + (bpr_choice_exponent_bpcipx_result_choice) = (n)) /\ (exists bpr_power_value_bpcipx_result_choice_valuation_selected. ((exists bpr_power_code_bpcipx_result_choice_valuation_selected_power bpr_power_scale_bpcipx_result_choice_valuation_selected_power. ((forall bpr_power_index_bpcipx_result_choice_valuation_selected_power. (exists bpr_gap_bpcipx_result_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcipx_result_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcipx_result_choice_valuation_selected_power) = bpr_choice_exponent_bpcipx_result_choice) -> (((exists bpr_height_bpcipx_result_choice_valuation_selected_power_repeat_entry. bpr_height_bpcipx_result_choice_valuation_selected_power_repeat_entry + S (S (a + bpr_index_bpcipx_result)) = S ((S (bpr_power_index_bpcipx_result_choice_valuation_selected_power)) * bpr_power_scale_bpcipx_result_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcipx_result_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcipx_result_choice_valuation_selected_power = bpr_quotient_bpcipx_result_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcipx_result_choice_valuation_selected_power)) * bpr_power_scale_bpcipx_result_choice_valuation_selected_power) + (S (a + bpr_index_bpcipx_result))))) /\ (exists ff_u_bpcipx_result_choice_valuation_selected_power_product ff_v_bpcipx_result_choice_valuation_selected_power_product. ((((exists ff_h_bpcipx_result_choice_valuation_selected_power_product_start. ff_h_bpcipx_result_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_result_choice_valuation_selected_power_product_start. ff_u_bpcipx_result_choice_valuation_selected_power_product = ff_q_bpcipx_result_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcipx_result_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcipx_result_choice_valuation_selected_power_product_terminal. ff_h_bpcipx_result_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcipx_result_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcipx_result_choice)) * ff_v_bpcipx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_result_choice_valuation_selected_power_product_terminal. ff_u_bpcipx_result_choice_valuation_selected_power_product = ff_q_bpcipx_result_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcipx_result_choice)) * ff_v_bpcipx_result_choice_valuation_selected_power_product) + (bpr_power_value_bpcipx_result_choice_valuation_selected))) /\ forall ff_i_bpcipx_result_choice_valuation_selected_power_product. (exists ff_lt_bpcipx_result_choice_valuation_selected_power_product_bound. ff_lt_bpcipx_result_choice_valuation_selected_power_product_bound + S ff_i_bpcipx_result_choice_valuation_selected_power_product = bpr_choice_exponent_bpcipx_result_choice) -> exists ff_p_bpcipx_result_choice_valuation_selected_power_product ff_r_bpcipx_result_choice_valuation_selected_power_product ff_s_bpcipx_result_choice_valuation_selected_power_product. ((((exists ff_h_bpcipx_result_choice_valuation_selected_power_product_factor. ff_h_bpcipx_result_choice_valuation_selected_power_product_factor + S (ff_p_bpcipx_result_choice_valuation_selected_power_product) = S ((S (ff_i_bpcipx_result_choice_valuation_selected_power_product)) * bpr_power_scale_bpcipx_result_choice_valuation_selected_power)) /\ exists ff_q_bpcipx_result_choice_valuation_selected_power_product_factor. bpr_power_code_bpcipx_result_choice_valuation_selected_power = ff_q_bpcipx_result_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcipx_result_choice_valuation_selected_power_product)) * bpr_power_scale_bpcipx_result_choice_valuation_selected_power) + (ff_p_bpcipx_result_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcipx_result_choice_valuation_selected_power_product_partial. ff_h_bpcipx_result_choice_valuation_selected_power_product_partial + S (ff_r_bpcipx_result_choice_valuation_selected_power_product) = S ((S (ff_i_bpcipx_result_choice_valuation_selected_power_product)) * ff_v_bpcipx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_result_choice_valuation_selected_power_product_partial. ff_u_bpcipx_result_choice_valuation_selected_power_product = ff_q_bpcipx_result_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcipx_result_choice_valuation_selected_power_product)) * ff_v_bpcipx_result_choice_valuation_selected_power_product) + (ff_r_bpcipx_result_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcipx_result_choice_valuation_selected_power_product_successor. ff_h_bpcipx_result_choice_valuation_selected_power_product_successor + S (ff_s_bpcipx_result_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcipx_result_choice_valuation_selected_power_product)) * ff_v_bpcipx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_result_choice_valuation_selected_power_product_successor. ff_u_bpcipx_result_choice_valuation_selected_power_product = ff_q_bpcipx_result_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcipx_result_choice_valuation_selected_power_product)) * ff_v_bpcipx_result_choice_valuation_selected_power_product) + (ff_s_bpcipx_result_choice_valuation_selected_power_product))) /\ ff_s_bpcipx_result_choice_valuation_selected_power_product = ff_r_bpcipx_result_choice_valuation_selected_power_product * ff_p_bpcipx_result_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcipx_result_choice_valuation_selected_divides. n = (bpr_power_value_bpcipx_result_choice_valuation_selected) * bpr_divides_quotient_bpcipx_result_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcipx_result_choice_valuation. (exists bpr_le_gap_bpcipx_result_choice_valuation_candidate_bound. bpr_le_gap_bpcipx_result_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcipx_result_choice_valuation) = (n)) -> (exists bpr_power_value_bpcipx_result_choice_valuation_candidate. ((exists bpr_power_code_bpcipx_result_choice_valuation_candidate_power bpr_power_scale_bpcipx_result_choice_valuation_candidate_power. ((forall bpr_power_index_bpcipx_result_choice_valuation_candidate_power. (exists bpr_gap_bpcipx_result_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcipx_result_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcipx_result_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcipx_result_choice_valuation) -> (((exists bpr_height_bpcipx_result_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcipx_result_choice_valuation_candidate_power_repeat_entry + S (S (a + bpr_index_bpcipx_result)) = S ((S (bpr_power_index_bpcipx_result_choice_valuation_candidate_power)) * bpr_power_scale_bpcipx_result_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcipx_result_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcipx_result_choice_valuation_candidate_power = bpr_quotient_bpcipx_result_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcipx_result_choice_valuation_candidate_power)) * bpr_power_scale_bpcipx_result_choice_valuation_candidate_power) + (S (a + bpr_index_bpcipx_result))))) /\ (exists ff_u_bpcipx_result_choice_valuation_candidate_power_product ff_v_bpcipx_result_choice_valuation_candidate_power_product. ((((exists ff_h_bpcipx_result_choice_valuation_candidate_power_product_start. ff_h_bpcipx_result_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_result_choice_valuation_candidate_power_product_start. ff_u_bpcipx_result_choice_valuation_candidate_power_product = ff_q_bpcipx_result_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcipx_result_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcipx_result_choice_valuation_candidate_power_product_terminal. ff_h_bpcipx_result_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcipx_result_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcipx_result_choice_valuation)) * ff_v_bpcipx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_result_choice_valuation_candidate_power_product_terminal. ff_u_bpcipx_result_choice_valuation_candidate_power_product = ff_q_bpcipx_result_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcipx_result_choice_valuation)) * ff_v_bpcipx_result_choice_valuation_candidate_power_product) + (bpr_power_value_bpcipx_result_choice_valuation_candidate))) /\ forall ff_i_bpcipx_result_choice_valuation_candidate_power_product. (exists ff_lt_bpcipx_result_choice_valuation_candidate_power_product_bound. ff_lt_bpcipx_result_choice_valuation_candidate_power_product_bound + S ff_i_bpcipx_result_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcipx_result_choice_valuation) -> exists ff_p_bpcipx_result_choice_valuation_candidate_power_product ff_r_bpcipx_result_choice_valuation_candidate_power_product ff_s_bpcipx_result_choice_valuation_candidate_power_product. ((((exists ff_h_bpcipx_result_choice_valuation_candidate_power_product_factor. ff_h_bpcipx_result_choice_valuation_candidate_power_product_factor + S (ff_p_bpcipx_result_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcipx_result_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcipx_result_choice_valuation_candidate_power)) /\ exists ff_q_bpcipx_result_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcipx_result_choice_valuation_candidate_power = ff_q_bpcipx_result_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcipx_result_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcipx_result_choice_valuation_candidate_power) + (ff_p_bpcipx_result_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcipx_result_choice_valuation_candidate_power_product_partial. ff_h_bpcipx_result_choice_valuation_candidate_power_product_partial + S (ff_r_bpcipx_result_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcipx_result_choice_valuation_candidate_power_product)) * ff_v_bpcipx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_result_choice_valuation_candidate_power_product_partial. ff_u_bpcipx_result_choice_valuation_candidate_power_product = ff_q_bpcipx_result_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcipx_result_choice_valuation_candidate_power_product)) * ff_v_bpcipx_result_choice_valuation_candidate_power_product) + (ff_r_bpcipx_result_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcipx_result_choice_valuation_candidate_power_product_successor. ff_h_bpcipx_result_choice_valuation_candidate_power_product_successor + S (ff_s_bpcipx_result_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcipx_result_choice_valuation_candidate_power_product)) * ff_v_bpcipx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_result_choice_valuation_candidate_power_product_successor. ff_u_bpcipx_result_choice_valuation_candidate_power_product = ff_q_bpcipx_result_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcipx_result_choice_valuation_candidate_power_product)) * ff_v_bpcipx_result_choice_valuation_candidate_power_product) + (ff_s_bpcipx_result_choice_valuation_candidate_power_product))) /\ ff_s_bpcipx_result_choice_valuation_candidate_power_product = ff_r_bpcipx_result_choice_valuation_candidate_power_product * ff_p_bpcipx_result_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcipx_result_choice_valuation_candidate_divides. n = (bpr_power_value_bpcipx_result_choice_valuation_candidate) * bpr_divides_quotient_bpcipx_result_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcipx_result_choice_valuation_candidate_below. bpr_le_gap_bpcipx_result_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcipx_result_choice_valuation) = (bpr_choice_exponent_bpcipx_result_choice))) /\ (exists bpr_power_code_bpcipx_result_choice_power bpr_power_scale_bpcipx_result_choice_power. ((forall bpr_power_index_bpcipx_result_choice_power. (exists bpr_gap_bpcipx_result_choice_power_repeat_bound. bpr_gap_bpcipx_result_choice_power_repeat_bound + S (bpr_power_index_bpcipx_result_choice_power) = bpr_choice_exponent_bpcipx_result_choice) -> (((exists bpr_height_bpcipx_result_choice_power_repeat_entry. bpr_height_bpcipx_result_choice_power_repeat_entry + S (S (a + bpr_index_bpcipx_result)) = S ((S (bpr_power_index_bpcipx_result_choice_power)) * bpr_power_scale_bpcipx_result_choice_power)) /\ exists bpr_quotient_bpcipx_result_choice_power_repeat_entry. bpr_power_code_bpcipx_result_choice_power = bpr_quotient_bpcipx_result_choice_power_repeat_entry * S ((S (bpr_power_index_bpcipx_result_choice_power)) * bpr_power_scale_bpcipx_result_choice_power) + (S (a + bpr_index_bpcipx_result))))) /\ (exists ff_u_bpcipx_result_choice_power_product ff_v_bpcipx_result_choice_power_product. ((((exists ff_h_bpcipx_result_choice_power_product_start. ff_h_bpcipx_result_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_result_choice_power_product)) /\ exists ff_q_bpcipx_result_choice_power_product_start. ff_u_bpcipx_result_choice_power_product = ff_q_bpcipx_result_choice_power_product_start * S ((S (0)) * ff_v_bpcipx_result_choice_power_product) + (1))) /\ ((((exists ff_h_bpcipx_result_choice_power_product_terminal. ff_h_bpcipx_result_choice_power_product_terminal + S (bpr_value_bpcipx_result) = S ((S (bpr_choice_exponent_bpcipx_result_choice)) * ff_v_bpcipx_result_choice_power_product)) /\ exists ff_q_bpcipx_result_choice_power_product_terminal. ff_u_bpcipx_result_choice_power_product = ff_q_bpcipx_result_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcipx_result_choice)) * ff_v_bpcipx_result_choice_power_product) + (bpr_value_bpcipx_result))) /\ forall ff_i_bpcipx_result_choice_power_product. (exists ff_lt_bpcipx_result_choice_power_product_bound. ff_lt_bpcipx_result_choice_power_product_bound + S ff_i_bpcipx_result_choice_power_product = bpr_choice_exponent_bpcipx_result_choice) -> exists ff_p_bpcipx_result_choice_power_product ff_r_bpcipx_result_choice_power_product ff_s_bpcipx_result_choice_power_product. ((((exists ff_h_bpcipx_result_choice_power_product_factor. ff_h_bpcipx_result_choice_power_product_factor + S (ff_p_bpcipx_result_choice_power_product) = S ((S (ff_i_bpcipx_result_choice_power_product)) * bpr_power_scale_bpcipx_result_choice_power)) /\ exists ff_q_bpcipx_result_choice_power_product_factor. bpr_power_code_bpcipx_result_choice_power = ff_q_bpcipx_result_choice_power_product_factor * S ((S (ff_i_bpcipx_result_choice_power_product)) * bpr_power_scale_bpcipx_result_choice_power) + (ff_p_bpcipx_result_choice_power_product))) /\ ((((exists ff_h_bpcipx_result_choice_power_product_partial. ff_h_bpcipx_result_choice_power_product_partial + S (ff_r_bpcipx_result_choice_power_product) = S ((S (ff_i_bpcipx_result_choice_power_product)) * ff_v_bpcipx_result_choice_power_product)) /\ exists ff_q_bpcipx_result_choice_power_product_partial. ff_u_bpcipx_result_choice_power_product = ff_q_bpcipx_result_choice_power_product_partial * S ((S (ff_i_bpcipx_result_choice_power_product)) * ff_v_bpcipx_result_choice_power_product) + (ff_r_bpcipx_result_choice_power_product))) /\ ((((exists ff_h_bpcipx_result_choice_power_product_successor. ff_h_bpcipx_result_choice_power_product_successor + S (ff_s_bpcipx_result_choice_power_product) = S ((S (S ff_i_bpcipx_result_choice_power_product)) * ff_v_bpcipx_result_choice_power_product)) /\ exists ff_q_bpcipx_result_choice_power_product_successor. ff_u_bpcipx_result_choice_power_product = ff_q_bpcipx_result_choice_power_product_successor * S ((S (S ff_i_bpcipx_result_choice_power_product)) * ff_v_bpcipx_result_choice_power_product) + (ff_s_bpcipx_result_choice_power_product))) /\ ff_s_bpcipx_result_choice_power_product = ff_r_bpcipx_result_choice_power_product * ff_p_bpcipx_result_choice_power_product)))))))))) \/ (~((~(S (a + bpr_index_bpcipx_result) = 1) /\ forall bpr_left_bpcipx_result_choice_prime bpr_right_bpcipx_result_choice_prime. S (a + bpr_index_bpcipx_result) = bpr_left_bpcipx_result_choice_prime * bpr_right_bpcipx_result_choice_prime -> bpr_left_bpcipx_result_choice_prime = 1 \/ bpr_right_bpcipx_result_choice_prime = 1)) /\ bpr_value_bpcipx_result = 1)))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
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
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.
Named ingredients (3)
01Fix variables and assumptionsL1–2
02Induction on lL3–3
Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.
- L3
induction l
03Construct an explicit witnessL4–5
04Fix variables and assumptionsL6–7
05Separate the logical casesL8–9
06Establish hsiL10–14
07Establish hpreviousL15–16
Establish this local claim before using it. It is not an additional assumption.
- L15
have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,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)Definitions: Lt(x,l)BetaAt(b,c,x,y)Prime(S (a + x))PowerValuation(S (a + x),n,z)Pow(S (a + x),z,y)Original native command in the exact edition - L16
exact IH
08Separate the logical casesL17–18
09Establish hnextL19–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution interval prefix extend.
- L19
have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S l) → ∃ y. BetaAt(b,c,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)Definitions: Lt(x,S l)BetaAt(b,c,x,y)Prime(S (a + x))PowerValuation(S (a + x),n,z)Pow(S (a + x),z,y)Original native command in the exact edition - L20
apply prime_contribution_interval_prefix_extend - L21
exact hprevious_witness_witness - L22
exact hnext
Original defined command ledger · 22 lines
- 0001
intro n - 0002
intro a - 0003
induction l - 0004
exists 0 - 0005
exists 0 - 0006
intro i - 0007
intro hi - 0008
exfalso - 0009
cases hi - 0010
have hsi : S i = 0 - 0011
apply add_eq_zero_right - 0012
exact hi_witness - 0013
apply succ_ne_zero - 0014
exact hsi - 0015
have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,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)Exact native replay line
have hprevious : exists b c. (forall bpr_index_bpcipx_previous. (exists bpr_gap_bpcipx_previous_bound. bpr_gap_bpcipx_previous_bound + S (bpr_index_bpcipx_previous) = l) -> exists bpr_value_bpcipx_previous. ((((exists bpr_height_bpcipx_previous_decoded. bpr_height_bpcipx_previous_decoded + S (bpr_value_bpcipx_previous) = S ((S (bpr_index_bpcipx_previous)) * c)) /\ exists bpr_quotient_bpcipx_previous_decoded. b = bpr_quotient_bpcipx_previous_decoded * S ((S (bpr_index_bpcipx_previous)) * c) + (bpr_value_bpcipx_previous))) /\ (((((~(S (a + bpr_index_bpcipx_previous) = 1) /\ forall bpr_left_bpcipx_previous_choice_prime bpr_right_bpcipx_previous_choice_prime. S (a + bpr_index_bpcipx_previous) = bpr_left_bpcipx_previous_choice_prime * bpr_right_bpcipx_previous_choice_prime -> bpr_left_bpcipx_previous_choice_prime = 1 \/ bpr_right_bpcipx_previous_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcipx_previous_choice. ((((exists bpr_le_gap_bpcipx_previous_choice_valuation_selected_bound. bpr_le_gap_bpcipx_previous_choice_valuation_selected_bound + (bpr_choice_exponent_bpcipx_previous_choice) = (n)) /\ (exists bpr_power_value_bpcipx_previous_choice_valuation_selected. ((exists bpr_power_code_bpcipx_previous_choice_valuation_selected_power bpr_power_scale_bpcipx_previous_choice_valuation_selected_power. ((forall bpr_power_index_bpcipx_previous_choice_valuation_selected_power. (exists bpr_gap_bpcipx_previous_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcipx_previous_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcipx_previous_choice_valuation_selected_power) = bpr_choice_exponent_bpcipx_previous_choice) -> (((exists bpr_height_bpcipx_previous_choice_valuation_selected_power_repeat_entry. bpr_height_bpcipx_previous_choice_valuation_selected_power_repeat_entry + S (S (a + bpr_index_bpcipx_previous)) = S ((S (bpr_power_index_bpcipx_previous_choice_valuation_selected_power)) * bpr_power_scale_bpcipx_previous_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcipx_previous_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcipx_previous_choice_valuation_selected_power = bpr_quotient_bpcipx_previous_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcipx_previous_choice_valuation_selected_power)) * bpr_power_scale_bpcipx_previous_choice_valuation_selected_power) + (S (a + bpr_index_bpcipx_previous))))) /\ (exists ff_u_bpcipx_previous_choice_valuation_selected_power_product ff_v_bpcipx_previous_choice_valuation_selected_power_product. ((((exists ff_h_bpcipx_previous_choice_valuation_selected_power_product_start. ff_h_bpcipx_previous_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_previous_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_previous_choice_valuation_selected_power_product_start. ff_u_bpcipx_previous_choice_valuation_selected_power_product = ff_q_bpcipx_previous_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcipx_previous_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcipx_previous_choice_valuation_selected_power_product_terminal. ff_h_bpcipx_previous_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcipx_previous_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcipx_previous_choice)) * ff_v_bpcipx_previous_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_previous_choice_valuation_selected_power_product_terminal. ff_u_bpcipx_previous_choice_valuation_selected_power_product = ff_q_bpcipx_previous_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcipx_previous_choice)) * ff_v_bpcipx_previous_choice_valuation_selected_power_product) + (bpr_power_value_bpcipx_previous_choice_valuation_selected))) /\ forall ff_i_bpcipx_previous_choice_valuation_selected_power_product. (exists ff_lt_bpcipx_previous_choice_valuation_selected_power_product_bound. ff_lt_bpcipx_previous_choice_valuation_selected_power_product_bound + S ff_i_bpcipx_previous_choice_valuation_selected_power_product = bpr_choice_exponent_bpcipx_previous_choice) -> exists ff_p_bpcipx_previous_choice_valuation_selected_power_product ff_r_bpcipx_previous_choice_valuation_selected_power_product ff_s_bpcipx_previous_choice_valuation_selected_power_product. ((((exists ff_h_bpcipx_previous_choice_valuation_selected_power_product_factor. ff_h_bpcipx_previous_choice_valuation_selected_power_product_factor + S (ff_p_bpcipx_previous_choice_valuation_selected_power_product) = S ((S (ff_i_bpcipx_previous_choice_valuation_selected_power_product)) * bpr_power_scale_bpcipx_previous_choice_valuation_selected_power)) /\ exists ff_q_bpcipx_previous_choice_valuation_selected_power_product_factor. bpr_power_code_bpcipx_previous_choice_valuation_selected_power = ff_q_bpcipx_previous_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcipx_previous_choice_valuation_selected_power_product)) * bpr_power_scale_bpcipx_previous_choice_valuation_selected_power) + (ff_p_bpcipx_previous_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcipx_previous_choice_valuation_selected_power_product_partial. ff_h_bpcipx_previous_choice_valuation_selected_power_product_partial + S (ff_r_bpcipx_previous_choice_valuation_selected_power_product) = S ((S (ff_i_bpcipx_previous_choice_valuation_selected_power_product)) * ff_v_bpcipx_previous_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_previous_choice_valuation_selected_power_product_partial. ff_u_bpcipx_previous_choice_valuation_selected_power_product = ff_q_bpcipx_previous_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcipx_previous_choice_valuation_selected_power_product)) * ff_v_bpcipx_previous_choice_valuation_selected_power_product) + (ff_r_bpcipx_previous_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcipx_previous_choice_valuation_selected_power_product_successor. ff_h_bpcipx_previous_choice_valuation_selected_power_product_successor + S (ff_s_bpcipx_previous_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcipx_previous_choice_valuation_selected_power_product)) * ff_v_bpcipx_previous_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_previous_choice_valuation_selected_power_product_successor. ff_u_bpcipx_previous_choice_valuation_selected_power_product = ff_q_bpcipx_previous_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcipx_previous_choice_valuation_selected_power_product)) * ff_v_bpcipx_previous_choice_valuation_selected_power_product) + (ff_s_bpcipx_previous_choice_valuation_selected_power_product))) /\ ff_s_bpcipx_previous_choice_valuation_selected_power_product = ff_r_bpcipx_previous_choice_valuation_selected_power_product * ff_p_bpcipx_previous_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcipx_previous_choice_valuation_selected_divides. n = (bpr_power_value_bpcipx_previous_choice_valuation_selected) * bpr_divides_quotient_bpcipx_previous_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcipx_previous_choice_valuation. (exists bpr_le_gap_bpcipx_previous_choice_valuation_candidate_bound. bpr_le_gap_bpcipx_previous_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcipx_previous_choice_valuation) = (n)) -> (exists bpr_power_value_bpcipx_previous_choice_valuation_candidate. ((exists bpr_power_code_bpcipx_previous_choice_valuation_candidate_power bpr_power_scale_bpcipx_previous_choice_valuation_candidate_power. ((forall bpr_power_index_bpcipx_previous_choice_valuation_candidate_power. (exists bpr_gap_bpcipx_previous_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcipx_previous_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcipx_previous_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcipx_previous_choice_valuation) -> (((exists bpr_height_bpcipx_previous_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcipx_previous_choice_valuation_candidate_power_repeat_entry + S (S (a + bpr_index_bpcipx_previous)) = S ((S (bpr_power_index_bpcipx_previous_choice_valuation_candidate_power)) * bpr_power_scale_bpcipx_previous_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcipx_previous_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcipx_previous_choice_valuation_candidate_power = bpr_quotient_bpcipx_previous_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcipx_previous_choice_valuation_candidate_power)) * bpr_power_scale_bpcipx_previous_choice_valuation_candidate_power) + (S (a + bpr_index_bpcipx_previous))))) /\ (exists ff_u_bpcipx_previous_choice_valuation_candidate_power_product ff_v_bpcipx_previous_choice_valuation_candidate_power_product. ((((exists ff_h_bpcipx_previous_choice_valuation_candidate_power_product_start. ff_h_bpcipx_previous_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_previous_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_previous_choice_valuation_candidate_power_product_start. ff_u_bpcipx_previous_choice_valuation_candidate_power_product = ff_q_bpcipx_previous_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcipx_previous_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcipx_previous_choice_valuation_candidate_power_product_terminal. ff_h_bpcipx_previous_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcipx_previous_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcipx_previous_choice_valuation)) * ff_v_bpcipx_previous_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_previous_choice_valuation_candidate_power_product_terminal. ff_u_bpcipx_previous_choice_valuation_candidate_power_product = ff_q_bpcipx_previous_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcipx_previous_choice_valuation)) * ff_v_bpcipx_previous_choice_valuation_candidate_power_product) + (bpr_power_value_bpcipx_previous_choice_valuation_candidate))) /\ forall ff_i_bpcipx_previous_choice_valuation_candidate_power_product. (exists ff_lt_bpcipx_previous_choice_valuation_candidate_power_product_bound. ff_lt_bpcipx_previous_choice_valuation_candidate_power_product_bound + S ff_i_bpcipx_previous_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcipx_previous_choice_valuation) -> exists ff_p_bpcipx_previous_choice_valuation_candidate_power_product ff_r_bpcipx_previous_choice_valuation_candidate_power_product ff_s_bpcipx_previous_choice_valuation_candidate_power_product. ((((exists ff_h_bpcipx_previous_choice_valuation_candidate_power_product_factor. ff_h_bpcipx_previous_choice_valuation_candidate_power_product_factor + S (ff_p_bpcipx_previous_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcipx_previous_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcipx_previous_choice_valuation_candidate_power)) /\ exists ff_q_bpcipx_previous_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcipx_previous_choice_valuation_candidate_power = ff_q_bpcipx_previous_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcipx_previous_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcipx_previous_choice_valuation_candidate_power) + (ff_p_bpcipx_previous_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcipx_previous_choice_valuation_candidate_power_product_partial. ff_h_bpcipx_previous_choice_valuation_candidate_power_product_partial + S (ff_r_bpcipx_previous_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcipx_previous_choice_valuation_candidate_power_product)) * ff_v_bpcipx_previous_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_previous_choice_valuation_candidate_power_product_partial. ff_u_bpcipx_previous_choice_valuation_candidate_power_product = ff_q_bpcipx_previous_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcipx_previous_choice_valuation_candidate_power_product)) * ff_v_bpcipx_previous_choice_valuation_candidate_power_product) + (ff_r_bpcipx_previous_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcipx_previous_choice_valuation_candidate_power_product_successor. ff_h_bpcipx_previous_choice_valuation_candidate_power_product_successor + S (ff_s_bpcipx_previous_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcipx_previous_choice_valuation_candidate_power_product)) * ff_v_bpcipx_previous_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_previous_choice_valuation_candidate_power_product_successor. ff_u_bpcipx_previous_choice_valuation_candidate_power_product = ff_q_bpcipx_previous_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcipx_previous_choice_valuation_candidate_power_product)) * ff_v_bpcipx_previous_choice_valuation_candidate_power_product) + (ff_s_bpcipx_previous_choice_valuation_candidate_power_product))) /\ ff_s_bpcipx_previous_choice_valuation_candidate_power_product = ff_r_bpcipx_previous_choice_valuation_candidate_power_product * ff_p_bpcipx_previous_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcipx_previous_choice_valuation_candidate_divides. n = (bpr_power_value_bpcipx_previous_choice_valuation_candidate) * bpr_divides_quotient_bpcipx_previous_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcipx_previous_choice_valuation_candidate_below. bpr_le_gap_bpcipx_previous_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcipx_previous_choice_valuation) = (bpr_choice_exponent_bpcipx_previous_choice))) /\ (exists bpr_power_code_bpcipx_previous_choice_power bpr_power_scale_bpcipx_previous_choice_power. ((forall bpr_power_index_bpcipx_previous_choice_power. (exists bpr_gap_bpcipx_previous_choice_power_repeat_bound. bpr_gap_bpcipx_previous_choice_power_repeat_bound + S (bpr_power_index_bpcipx_previous_choice_power) = bpr_choice_exponent_bpcipx_previous_choice) -> (((exists bpr_height_bpcipx_previous_choice_power_repeat_entry. bpr_height_bpcipx_previous_choice_power_repeat_entry + S (S (a + bpr_index_bpcipx_previous)) = S ((S (bpr_power_index_bpcipx_previous_choice_power)) * bpr_power_scale_bpcipx_previous_choice_power)) /\ exists bpr_quotient_bpcipx_previous_choice_power_repeat_entry. bpr_power_code_bpcipx_previous_choice_power = bpr_quotient_bpcipx_previous_choice_power_repeat_entry * S ((S (bpr_power_index_bpcipx_previous_choice_power)) * bpr_power_scale_bpcipx_previous_choice_power) + (S (a + bpr_index_bpcipx_previous))))) /\ (exists ff_u_bpcipx_previous_choice_power_product ff_v_bpcipx_previous_choice_power_product. ((((exists ff_h_bpcipx_previous_choice_power_product_start. ff_h_bpcipx_previous_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_previous_choice_power_product)) /\ exists ff_q_bpcipx_previous_choice_power_product_start. ff_u_bpcipx_previous_choice_power_product = ff_q_bpcipx_previous_choice_power_product_start * S ((S (0)) * ff_v_bpcipx_previous_choice_power_product) + (1))) /\ ((((exists ff_h_bpcipx_previous_choice_power_product_terminal. ff_h_bpcipx_previous_choice_power_product_terminal + S (bpr_value_bpcipx_previous) = S ((S (bpr_choice_exponent_bpcipx_previous_choice)) * ff_v_bpcipx_previous_choice_power_product)) /\ exists ff_q_bpcipx_previous_choice_power_product_terminal. ff_u_bpcipx_previous_choice_power_product = ff_q_bpcipx_previous_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcipx_previous_choice)) * ff_v_bpcipx_previous_choice_power_product) + (bpr_value_bpcipx_previous))) /\ forall ff_i_bpcipx_previous_choice_power_product. (exists ff_lt_bpcipx_previous_choice_power_product_bound. ff_lt_bpcipx_previous_choice_power_product_bound + S ff_i_bpcipx_previous_choice_power_product = bpr_choice_exponent_bpcipx_previous_choice) -> exists ff_p_bpcipx_previous_choice_power_product ff_r_bpcipx_previous_choice_power_product ff_s_bpcipx_previous_choice_power_product. ((((exists ff_h_bpcipx_previous_choice_power_product_factor. ff_h_bpcipx_previous_choice_power_product_factor + S (ff_p_bpcipx_previous_choice_power_product) = S ((S (ff_i_bpcipx_previous_choice_power_product)) * bpr_power_scale_bpcipx_previous_choice_power)) /\ exists ff_q_bpcipx_previous_choice_power_product_factor. bpr_power_code_bpcipx_previous_choice_power = ff_q_bpcipx_previous_choice_power_product_factor * S ((S (ff_i_bpcipx_previous_choice_power_product)) * bpr_power_scale_bpcipx_previous_choice_power) + (ff_p_bpcipx_previous_choice_power_product))) /\ ((((exists ff_h_bpcipx_previous_choice_power_product_partial. ff_h_bpcipx_previous_choice_power_product_partial + S (ff_r_bpcipx_previous_choice_power_product) = S ((S (ff_i_bpcipx_previous_choice_power_product)) * ff_v_bpcipx_previous_choice_power_product)) /\ exists ff_q_bpcipx_previous_choice_power_product_partial. ff_u_bpcipx_previous_choice_power_product = ff_q_bpcipx_previous_choice_power_product_partial * S ((S (ff_i_bpcipx_previous_choice_power_product)) * ff_v_bpcipx_previous_choice_power_product) + (ff_r_bpcipx_previous_choice_power_product))) /\ ((((exists ff_h_bpcipx_previous_choice_power_product_successor. ff_h_bpcipx_previous_choice_power_product_successor + S (ff_s_bpcipx_previous_choice_power_product) = S ((S (S ff_i_bpcipx_previous_choice_power_product)) * ff_v_bpcipx_previous_choice_power_product)) /\ exists ff_q_bpcipx_previous_choice_power_product_successor. ff_u_bpcipx_previous_choice_power_product = ff_q_bpcipx_previous_choice_power_product_successor * S ((S (S ff_i_bpcipx_previous_choice_power_product)) * ff_v_bpcipx_previous_choice_power_product) + (ff_s_bpcipx_previous_choice_power_product))) /\ ff_s_bpcipx_previous_choice_power_product = ff_r_bpcipx_previous_choice_power_product * ff_p_bpcipx_previous_choice_power_product)))))))))) \/ (~((~(S (a + bpr_index_bpcipx_previous) = 1) /\ forall bpr_left_bpcipx_previous_choice_prime bpr_right_bpcipx_previous_choice_prime. S (a + bpr_index_bpcipx_previous) = bpr_left_bpcipx_previous_choice_prime * bpr_right_bpcipx_previous_choice_prime -> bpr_left_bpcipx_previous_choice_prime = 1 \/ bpr_right_bpcipx_previous_choice_prime = 1)) /\ bpr_value_bpcipx_previous = 1))))) - 0016
exact IH - 0017
cases hprevious - 0018
cases hprevious_witness - 0019
have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S l) → ∃ y. BetaAt(b,c,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)Exact native replay line
have hnext : exists b c. (forall bpr_index_bpcipx_successor. (exists bpr_gap_bpcipx_successor_bound. bpr_gap_bpcipx_successor_bound + S (bpr_index_bpcipx_successor) = S l) -> exists bpr_value_bpcipx_successor. ((((exists bpr_height_bpcipx_successor_decoded. bpr_height_bpcipx_successor_decoded + S (bpr_value_bpcipx_successor) = S ((S (bpr_index_bpcipx_successor)) * c)) /\ exists bpr_quotient_bpcipx_successor_decoded. b = bpr_quotient_bpcipx_successor_decoded * S ((S (bpr_index_bpcipx_successor)) * c) + (bpr_value_bpcipx_successor))) /\ (((((~(S (a + bpr_index_bpcipx_successor) = 1) /\ forall bpr_left_bpcipx_successor_choice_prime bpr_right_bpcipx_successor_choice_prime. S (a + bpr_index_bpcipx_successor) = bpr_left_bpcipx_successor_choice_prime * bpr_right_bpcipx_successor_choice_prime -> bpr_left_bpcipx_successor_choice_prime = 1 \/ bpr_right_bpcipx_successor_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcipx_successor_choice. ((((exists bpr_le_gap_bpcipx_successor_choice_valuation_selected_bound. bpr_le_gap_bpcipx_successor_choice_valuation_selected_bound + (bpr_choice_exponent_bpcipx_successor_choice) = (n)) /\ (exists bpr_power_value_bpcipx_successor_choice_valuation_selected. ((exists bpr_power_code_bpcipx_successor_choice_valuation_selected_power bpr_power_scale_bpcipx_successor_choice_valuation_selected_power. ((forall bpr_power_index_bpcipx_successor_choice_valuation_selected_power. (exists bpr_gap_bpcipx_successor_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcipx_successor_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcipx_successor_choice_valuation_selected_power) = bpr_choice_exponent_bpcipx_successor_choice) -> (((exists bpr_height_bpcipx_successor_choice_valuation_selected_power_repeat_entry. bpr_height_bpcipx_successor_choice_valuation_selected_power_repeat_entry + S (S (a + bpr_index_bpcipx_successor)) = S ((S (bpr_power_index_bpcipx_successor_choice_valuation_selected_power)) * bpr_power_scale_bpcipx_successor_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcipx_successor_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcipx_successor_choice_valuation_selected_power = bpr_quotient_bpcipx_successor_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcipx_successor_choice_valuation_selected_power)) * bpr_power_scale_bpcipx_successor_choice_valuation_selected_power) + (S (a + bpr_index_bpcipx_successor))))) /\ (exists ff_u_bpcipx_successor_choice_valuation_selected_power_product ff_v_bpcipx_successor_choice_valuation_selected_power_product. ((((exists ff_h_bpcipx_successor_choice_valuation_selected_power_product_start. ff_h_bpcipx_successor_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_successor_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_successor_choice_valuation_selected_power_product_start. ff_u_bpcipx_successor_choice_valuation_selected_power_product = ff_q_bpcipx_successor_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcipx_successor_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcipx_successor_choice_valuation_selected_power_product_terminal. ff_h_bpcipx_successor_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcipx_successor_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcipx_successor_choice)) * ff_v_bpcipx_successor_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_successor_choice_valuation_selected_power_product_terminal. ff_u_bpcipx_successor_choice_valuation_selected_power_product = ff_q_bpcipx_successor_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcipx_successor_choice)) * ff_v_bpcipx_successor_choice_valuation_selected_power_product) + (bpr_power_value_bpcipx_successor_choice_valuation_selected))) /\ forall ff_i_bpcipx_successor_choice_valuation_selected_power_product. (exists ff_lt_bpcipx_successor_choice_valuation_selected_power_product_bound. ff_lt_bpcipx_successor_choice_valuation_selected_power_product_bound + S ff_i_bpcipx_successor_choice_valuation_selected_power_product = bpr_choice_exponent_bpcipx_successor_choice) -> exists ff_p_bpcipx_successor_choice_valuation_selected_power_product ff_r_bpcipx_successor_choice_valuation_selected_power_product ff_s_bpcipx_successor_choice_valuation_selected_power_product. ((((exists ff_h_bpcipx_successor_choice_valuation_selected_power_product_factor. ff_h_bpcipx_successor_choice_valuation_selected_power_product_factor + S (ff_p_bpcipx_successor_choice_valuation_selected_power_product) = S ((S (ff_i_bpcipx_successor_choice_valuation_selected_power_product)) * bpr_power_scale_bpcipx_successor_choice_valuation_selected_power)) /\ exists ff_q_bpcipx_successor_choice_valuation_selected_power_product_factor. bpr_power_code_bpcipx_successor_choice_valuation_selected_power = ff_q_bpcipx_successor_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcipx_successor_choice_valuation_selected_power_product)) * bpr_power_scale_bpcipx_successor_choice_valuation_selected_power) + (ff_p_bpcipx_successor_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcipx_successor_choice_valuation_selected_power_product_partial. ff_h_bpcipx_successor_choice_valuation_selected_power_product_partial + S (ff_r_bpcipx_successor_choice_valuation_selected_power_product) = S ((S (ff_i_bpcipx_successor_choice_valuation_selected_power_product)) * ff_v_bpcipx_successor_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_successor_choice_valuation_selected_power_product_partial. ff_u_bpcipx_successor_choice_valuation_selected_power_product = ff_q_bpcipx_successor_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcipx_successor_choice_valuation_selected_power_product)) * ff_v_bpcipx_successor_choice_valuation_selected_power_product) + (ff_r_bpcipx_successor_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcipx_successor_choice_valuation_selected_power_product_successor. ff_h_bpcipx_successor_choice_valuation_selected_power_product_successor + S (ff_s_bpcipx_successor_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcipx_successor_choice_valuation_selected_power_product)) * ff_v_bpcipx_successor_choice_valuation_selected_power_product)) /\ exists ff_q_bpcipx_successor_choice_valuation_selected_power_product_successor. ff_u_bpcipx_successor_choice_valuation_selected_power_product = ff_q_bpcipx_successor_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcipx_successor_choice_valuation_selected_power_product)) * ff_v_bpcipx_successor_choice_valuation_selected_power_product) + (ff_s_bpcipx_successor_choice_valuation_selected_power_product))) /\ ff_s_bpcipx_successor_choice_valuation_selected_power_product = ff_r_bpcipx_successor_choice_valuation_selected_power_product * ff_p_bpcipx_successor_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcipx_successor_choice_valuation_selected_divides. n = (bpr_power_value_bpcipx_successor_choice_valuation_selected) * bpr_divides_quotient_bpcipx_successor_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcipx_successor_choice_valuation. (exists bpr_le_gap_bpcipx_successor_choice_valuation_candidate_bound. bpr_le_gap_bpcipx_successor_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcipx_successor_choice_valuation) = (n)) -> (exists bpr_power_value_bpcipx_successor_choice_valuation_candidate. ((exists bpr_power_code_bpcipx_successor_choice_valuation_candidate_power bpr_power_scale_bpcipx_successor_choice_valuation_candidate_power. ((forall bpr_power_index_bpcipx_successor_choice_valuation_candidate_power. (exists bpr_gap_bpcipx_successor_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcipx_successor_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcipx_successor_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcipx_successor_choice_valuation) -> (((exists bpr_height_bpcipx_successor_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcipx_successor_choice_valuation_candidate_power_repeat_entry + S (S (a + bpr_index_bpcipx_successor)) = S ((S (bpr_power_index_bpcipx_successor_choice_valuation_candidate_power)) * bpr_power_scale_bpcipx_successor_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcipx_successor_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcipx_successor_choice_valuation_candidate_power = bpr_quotient_bpcipx_successor_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcipx_successor_choice_valuation_candidate_power)) * bpr_power_scale_bpcipx_successor_choice_valuation_candidate_power) + (S (a + bpr_index_bpcipx_successor))))) /\ (exists ff_u_bpcipx_successor_choice_valuation_candidate_power_product ff_v_bpcipx_successor_choice_valuation_candidate_power_product. ((((exists ff_h_bpcipx_successor_choice_valuation_candidate_power_product_start. ff_h_bpcipx_successor_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_successor_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_successor_choice_valuation_candidate_power_product_start. ff_u_bpcipx_successor_choice_valuation_candidate_power_product = ff_q_bpcipx_successor_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcipx_successor_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcipx_successor_choice_valuation_candidate_power_product_terminal. ff_h_bpcipx_successor_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcipx_successor_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcipx_successor_choice_valuation)) * ff_v_bpcipx_successor_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_successor_choice_valuation_candidate_power_product_terminal. ff_u_bpcipx_successor_choice_valuation_candidate_power_product = ff_q_bpcipx_successor_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcipx_successor_choice_valuation)) * ff_v_bpcipx_successor_choice_valuation_candidate_power_product) + (bpr_power_value_bpcipx_successor_choice_valuation_candidate))) /\ forall ff_i_bpcipx_successor_choice_valuation_candidate_power_product. (exists ff_lt_bpcipx_successor_choice_valuation_candidate_power_product_bound. ff_lt_bpcipx_successor_choice_valuation_candidate_power_product_bound + S ff_i_bpcipx_successor_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcipx_successor_choice_valuation) -> exists ff_p_bpcipx_successor_choice_valuation_candidate_power_product ff_r_bpcipx_successor_choice_valuation_candidate_power_product ff_s_bpcipx_successor_choice_valuation_candidate_power_product. ((((exists ff_h_bpcipx_successor_choice_valuation_candidate_power_product_factor. ff_h_bpcipx_successor_choice_valuation_candidate_power_product_factor + S (ff_p_bpcipx_successor_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcipx_successor_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcipx_successor_choice_valuation_candidate_power)) /\ exists ff_q_bpcipx_successor_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcipx_successor_choice_valuation_candidate_power = ff_q_bpcipx_successor_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcipx_successor_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcipx_successor_choice_valuation_candidate_power) + (ff_p_bpcipx_successor_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcipx_successor_choice_valuation_candidate_power_product_partial. ff_h_bpcipx_successor_choice_valuation_candidate_power_product_partial + S (ff_r_bpcipx_successor_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcipx_successor_choice_valuation_candidate_power_product)) * ff_v_bpcipx_successor_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_successor_choice_valuation_candidate_power_product_partial. ff_u_bpcipx_successor_choice_valuation_candidate_power_product = ff_q_bpcipx_successor_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcipx_successor_choice_valuation_candidate_power_product)) * ff_v_bpcipx_successor_choice_valuation_candidate_power_product) + (ff_r_bpcipx_successor_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcipx_successor_choice_valuation_candidate_power_product_successor. ff_h_bpcipx_successor_choice_valuation_candidate_power_product_successor + S (ff_s_bpcipx_successor_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcipx_successor_choice_valuation_candidate_power_product)) * ff_v_bpcipx_successor_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcipx_successor_choice_valuation_candidate_power_product_successor. ff_u_bpcipx_successor_choice_valuation_candidate_power_product = ff_q_bpcipx_successor_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcipx_successor_choice_valuation_candidate_power_product)) * ff_v_bpcipx_successor_choice_valuation_candidate_power_product) + (ff_s_bpcipx_successor_choice_valuation_candidate_power_product))) /\ ff_s_bpcipx_successor_choice_valuation_candidate_power_product = ff_r_bpcipx_successor_choice_valuation_candidate_power_product * ff_p_bpcipx_successor_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcipx_successor_choice_valuation_candidate_divides. n = (bpr_power_value_bpcipx_successor_choice_valuation_candidate) * bpr_divides_quotient_bpcipx_successor_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcipx_successor_choice_valuation_candidate_below. bpr_le_gap_bpcipx_successor_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcipx_successor_choice_valuation) = (bpr_choice_exponent_bpcipx_successor_choice))) /\ (exists bpr_power_code_bpcipx_successor_choice_power bpr_power_scale_bpcipx_successor_choice_power. ((forall bpr_power_index_bpcipx_successor_choice_power. (exists bpr_gap_bpcipx_successor_choice_power_repeat_bound. bpr_gap_bpcipx_successor_choice_power_repeat_bound + S (bpr_power_index_bpcipx_successor_choice_power) = bpr_choice_exponent_bpcipx_successor_choice) -> (((exists bpr_height_bpcipx_successor_choice_power_repeat_entry. bpr_height_bpcipx_successor_choice_power_repeat_entry + S (S (a + bpr_index_bpcipx_successor)) = S ((S (bpr_power_index_bpcipx_successor_choice_power)) * bpr_power_scale_bpcipx_successor_choice_power)) /\ exists bpr_quotient_bpcipx_successor_choice_power_repeat_entry. bpr_power_code_bpcipx_successor_choice_power = bpr_quotient_bpcipx_successor_choice_power_repeat_entry * S ((S (bpr_power_index_bpcipx_successor_choice_power)) * bpr_power_scale_bpcipx_successor_choice_power) + (S (a + bpr_index_bpcipx_successor))))) /\ (exists ff_u_bpcipx_successor_choice_power_product ff_v_bpcipx_successor_choice_power_product. ((((exists ff_h_bpcipx_successor_choice_power_product_start. ff_h_bpcipx_successor_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcipx_successor_choice_power_product)) /\ exists ff_q_bpcipx_successor_choice_power_product_start. ff_u_bpcipx_successor_choice_power_product = ff_q_bpcipx_successor_choice_power_product_start * S ((S (0)) * ff_v_bpcipx_successor_choice_power_product) + (1))) /\ ((((exists ff_h_bpcipx_successor_choice_power_product_terminal. ff_h_bpcipx_successor_choice_power_product_terminal + S (bpr_value_bpcipx_successor) = S ((S (bpr_choice_exponent_bpcipx_successor_choice)) * ff_v_bpcipx_successor_choice_power_product)) /\ exists ff_q_bpcipx_successor_choice_power_product_terminal. ff_u_bpcipx_successor_choice_power_product = ff_q_bpcipx_successor_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcipx_successor_choice)) * ff_v_bpcipx_successor_choice_power_product) + (bpr_value_bpcipx_successor))) /\ forall ff_i_bpcipx_successor_choice_power_product. (exists ff_lt_bpcipx_successor_choice_power_product_bound. ff_lt_bpcipx_successor_choice_power_product_bound + S ff_i_bpcipx_successor_choice_power_product = bpr_choice_exponent_bpcipx_successor_choice) -> exists ff_p_bpcipx_successor_choice_power_product ff_r_bpcipx_successor_choice_power_product ff_s_bpcipx_successor_choice_power_product. ((((exists ff_h_bpcipx_successor_choice_power_product_factor. ff_h_bpcipx_successor_choice_power_product_factor + S (ff_p_bpcipx_successor_choice_power_product) = S ((S (ff_i_bpcipx_successor_choice_power_product)) * bpr_power_scale_bpcipx_successor_choice_power)) /\ exists ff_q_bpcipx_successor_choice_power_product_factor. bpr_power_code_bpcipx_successor_choice_power = ff_q_bpcipx_successor_choice_power_product_factor * S ((S (ff_i_bpcipx_successor_choice_power_product)) * bpr_power_scale_bpcipx_successor_choice_power) + (ff_p_bpcipx_successor_choice_power_product))) /\ ((((exists ff_h_bpcipx_successor_choice_power_product_partial. ff_h_bpcipx_successor_choice_power_product_partial + S (ff_r_bpcipx_successor_choice_power_product) = S ((S (ff_i_bpcipx_successor_choice_power_product)) * ff_v_bpcipx_successor_choice_power_product)) /\ exists ff_q_bpcipx_successor_choice_power_product_partial. ff_u_bpcipx_successor_choice_power_product = ff_q_bpcipx_successor_choice_power_product_partial * S ((S (ff_i_bpcipx_successor_choice_power_product)) * ff_v_bpcipx_successor_choice_power_product) + (ff_r_bpcipx_successor_choice_power_product))) /\ ((((exists ff_h_bpcipx_successor_choice_power_product_successor. ff_h_bpcipx_successor_choice_power_product_successor + S (ff_s_bpcipx_successor_choice_power_product) = S ((S (S ff_i_bpcipx_successor_choice_power_product)) * ff_v_bpcipx_successor_choice_power_product)) /\ exists ff_q_bpcipx_successor_choice_power_product_successor. ff_u_bpcipx_successor_choice_power_product = ff_q_bpcipx_successor_choice_power_product_successor * S ((S (S ff_i_bpcipx_successor_choice_power_product)) * ff_v_bpcipx_successor_choice_power_product) + (ff_s_bpcipx_successor_choice_power_product))) /\ ff_s_bpcipx_successor_choice_power_product = ff_r_bpcipx_successor_choice_power_product * ff_p_bpcipx_successor_choice_power_product)))))))))) \/ (~((~(S (a + bpr_index_bpcipx_successor) = 1) /\ forall bpr_left_bpcipx_successor_choice_prime bpr_right_bpcipx_successor_choice_prime. S (a + bpr_index_bpcipx_successor) = bpr_left_bpcipx_successor_choice_prime * bpr_right_bpcipx_successor_choice_prime -> bpr_left_bpcipx_successor_choice_prime = 1 \/ bpr_right_bpcipx_successor_choice_prime = 1)) /\ bpr_value_bpcipx_successor = 1))))) - 0020
apply prime_contribution_interval_prefix_extend - 0021
exact hprevious_witness_witness - 0022
exact hnext