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. ∀ m. ∃ b. ∃ c. ∀ x. Lt(x,m) → ∃ 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)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 m. exists b c. (forall bpr_prefix_index_bpcpx_result. (exists bpr_gap_bpcpx_result_bound. bpr_gap_bpcpx_result_bound + S (bpr_prefix_index_bpcpx_result) = m) -> exists bpr_prefix_value_bpcpx_result. ((((exists bpr_height_bpcpx_result_decoded. bpr_height_bpcpx_result_decoded + S (bpr_prefix_value_bpcpx_result) = S ((S (bpr_prefix_index_bpcpx_result)) * c)) /\ exists bpr_quotient_bpcpx_result_decoded. b = bpr_quotient_bpcpx_result_decoded * S ((S (bpr_prefix_index_bpcpx_result)) * c) + (bpr_prefix_value_bpcpx_result))) /\ (((((~(S (bpr_prefix_index_bpcpx_result) = 1) /\ forall bpr_left_bpcpx_result_choice_prime bpr_right_bpcpx_result_choice_prime. S (bpr_prefix_index_bpcpx_result) = bpr_left_bpcpx_result_choice_prime * bpr_right_bpcpx_result_choice_prime -> bpr_left_bpcpx_result_choice_prime = 1 \/ bpr_right_bpcpx_result_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpx_result_choice. ((((exists bpr_le_gap_bpcpx_result_choice_valuation_selected_bound. bpr_le_gap_bpcpx_result_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpx_result_choice) = (n)) /\ (exists bpr_power_value_bpcpx_result_choice_valuation_selected. ((exists bpr_power_code_bpcpx_result_choice_valuation_selected_power bpr_power_scale_bpcpx_result_choice_valuation_selected_power. ((forall bpr_power_index_bpcpx_result_choice_valuation_selected_power. (exists bpr_gap_bpcpx_result_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpx_result_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpx_result_choice_valuation_selected_power) = bpr_choice_exponent_bpcpx_result_choice) -> (((exists bpr_height_bpcpx_result_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpx_result_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_result)) = S ((S (bpr_power_index_bpcpx_result_choice_valuation_selected_power)) * bpr_power_scale_bpcpx_result_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpx_result_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpx_result_choice_valuation_selected_power = bpr_quotient_bpcpx_result_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpx_result_choice_valuation_selected_power)) * bpr_power_scale_bpcpx_result_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpx_result))))) /\ (exists ff_u_bpcpx_result_choice_valuation_selected_power_product ff_v_bpcpx_result_choice_valuation_selected_power_product. ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_start. ff_h_bpcpx_result_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_start. ff_u_bpcpx_result_choice_valuation_selected_power_product = ff_q_bpcpx_result_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpx_result_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_terminal. ff_h_bpcpx_result_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpx_result_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpx_result_choice)) * ff_v_bpcpx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_terminal. ff_u_bpcpx_result_choice_valuation_selected_power_product = ff_q_bpcpx_result_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpx_result_choice)) * ff_v_bpcpx_result_choice_valuation_selected_power_product) + (bpr_power_value_bpcpx_result_choice_valuation_selected))) /\ forall ff_i_bpcpx_result_choice_valuation_selected_power_product. (exists ff_lt_bpcpx_result_choice_valuation_selected_power_product_bound. ff_lt_bpcpx_result_choice_valuation_selected_power_product_bound + S ff_i_bpcpx_result_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpx_result_choice) -> exists ff_p_bpcpx_result_choice_valuation_selected_power_product ff_r_bpcpx_result_choice_valuation_selected_power_product ff_s_bpcpx_result_choice_valuation_selected_power_product. ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_factor. ff_h_bpcpx_result_choice_valuation_selected_power_product_factor + S (ff_p_bpcpx_result_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpx_result_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpx_result_choice_valuation_selected_power)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpx_result_choice_valuation_selected_power = ff_q_bpcpx_result_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpx_result_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpx_result_choice_valuation_selected_power) + (ff_p_bpcpx_result_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_partial. ff_h_bpcpx_result_choice_valuation_selected_power_product_partial + S (ff_r_bpcpx_result_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpx_result_choice_valuation_selected_power_product)) * ff_v_bpcpx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_partial. ff_u_bpcpx_result_choice_valuation_selected_power_product = ff_q_bpcpx_result_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpx_result_choice_valuation_selected_power_product)) * ff_v_bpcpx_result_choice_valuation_selected_power_product) + (ff_r_bpcpx_result_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_selected_power_product_successor. ff_h_bpcpx_result_choice_valuation_selected_power_product_successor + S (ff_s_bpcpx_result_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpx_result_choice_valuation_selected_power_product)) * ff_v_bpcpx_result_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_selected_power_product_successor. ff_u_bpcpx_result_choice_valuation_selected_power_product = ff_q_bpcpx_result_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpx_result_choice_valuation_selected_power_product)) * ff_v_bpcpx_result_choice_valuation_selected_power_product) + (ff_s_bpcpx_result_choice_valuation_selected_power_product))) /\ ff_s_bpcpx_result_choice_valuation_selected_power_product = ff_r_bpcpx_result_choice_valuation_selected_power_product * ff_p_bpcpx_result_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpx_result_choice_valuation_selected_divides. n = (bpr_power_value_bpcpx_result_choice_valuation_selected) * bpr_divides_quotient_bpcpx_result_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpx_result_choice_valuation. (exists bpr_le_gap_bpcpx_result_choice_valuation_candidate_bound. bpr_le_gap_bpcpx_result_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpx_result_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpx_result_choice_valuation_candidate. ((exists bpr_power_code_bpcpx_result_choice_valuation_candidate_power bpr_power_scale_bpcpx_result_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpx_result_choice_valuation_candidate_power. (exists bpr_gap_bpcpx_result_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpx_result_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpx_result_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpx_result_choice_valuation) -> (((exists bpr_height_bpcpx_result_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpx_result_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_result)) = S ((S (bpr_power_index_bpcpx_result_choice_valuation_candidate_power)) * bpr_power_scale_bpcpx_result_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpx_result_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpx_result_choice_valuation_candidate_power = bpr_quotient_bpcpx_result_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpx_result_choice_valuation_candidate_power)) * bpr_power_scale_bpcpx_result_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpx_result))))) /\ (exists ff_u_bpcpx_result_choice_valuation_candidate_power_product ff_v_bpcpx_result_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_start. ff_h_bpcpx_result_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_start. ff_u_bpcpx_result_choice_valuation_candidate_power_product = ff_q_bpcpx_result_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_terminal. ff_h_bpcpx_result_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpx_result_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpx_result_choice_valuation)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_terminal. ff_u_bpcpx_result_choice_valuation_candidate_power_product = ff_q_bpcpx_result_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpx_result_choice_valuation)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpx_result_choice_valuation_candidate))) /\ forall ff_i_bpcpx_result_choice_valuation_candidate_power_product. (exists ff_lt_bpcpx_result_choice_valuation_candidate_power_product_bound. ff_lt_bpcpx_result_choice_valuation_candidate_power_product_bound + S ff_i_bpcpx_result_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpx_result_choice_valuation) -> exists ff_p_bpcpx_result_choice_valuation_candidate_power_product ff_r_bpcpx_result_choice_valuation_candidate_power_product ff_s_bpcpx_result_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_factor. ff_h_bpcpx_result_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpx_result_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpx_result_choice_valuation_candidate_power)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpx_result_choice_valuation_candidate_power = ff_q_bpcpx_result_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpx_result_choice_valuation_candidate_power) + (ff_p_bpcpx_result_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_partial. ff_h_bpcpx_result_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpx_result_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_partial. ff_u_bpcpx_result_choice_valuation_candidate_power_product = ff_q_bpcpx_result_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product) + (ff_r_bpcpx_result_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_valuation_candidate_power_product_successor. ff_h_bpcpx_result_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpx_result_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_result_choice_valuation_candidate_power_product_successor. ff_u_bpcpx_result_choice_valuation_candidate_power_product = ff_q_bpcpx_result_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpx_result_choice_valuation_candidate_power_product)) * ff_v_bpcpx_result_choice_valuation_candidate_power_product) + (ff_s_bpcpx_result_choice_valuation_candidate_power_product))) /\ ff_s_bpcpx_result_choice_valuation_candidate_power_product = ff_r_bpcpx_result_choice_valuation_candidate_power_product * ff_p_bpcpx_result_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpx_result_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpx_result_choice_valuation_candidate) * bpr_divides_quotient_bpcpx_result_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpx_result_choice_valuation_candidate_below. bpr_le_gap_bpcpx_result_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpx_result_choice_valuation) = (bpr_choice_exponent_bpcpx_result_choice))) /\ (exists bpr_power_code_bpcpx_result_choice_power bpr_power_scale_bpcpx_result_choice_power. ((forall bpr_power_index_bpcpx_result_choice_power. (exists bpr_gap_bpcpx_result_choice_power_repeat_bound. bpr_gap_bpcpx_result_choice_power_repeat_bound + S (bpr_power_index_bpcpx_result_choice_power) = bpr_choice_exponent_bpcpx_result_choice) -> (((exists bpr_height_bpcpx_result_choice_power_repeat_entry. bpr_height_bpcpx_result_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_result)) = S ((S (bpr_power_index_bpcpx_result_choice_power)) * bpr_power_scale_bpcpx_result_choice_power)) /\ exists bpr_quotient_bpcpx_result_choice_power_repeat_entry. bpr_power_code_bpcpx_result_choice_power = bpr_quotient_bpcpx_result_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpx_result_choice_power)) * bpr_power_scale_bpcpx_result_choice_power) + (S (bpr_prefix_index_bpcpx_result))))) /\ (exists ff_u_bpcpx_result_choice_power_product ff_v_bpcpx_result_choice_power_product. ((((exists ff_h_bpcpx_result_choice_power_product_start. ff_h_bpcpx_result_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_result_choice_power_product)) /\ exists ff_q_bpcpx_result_choice_power_product_start. ff_u_bpcpx_result_choice_power_product = ff_q_bpcpx_result_choice_power_product_start * S ((S (0)) * ff_v_bpcpx_result_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpx_result_choice_power_product_terminal. ff_h_bpcpx_result_choice_power_product_terminal + S (bpr_prefix_value_bpcpx_result) = S ((S (bpr_choice_exponent_bpcpx_result_choice)) * ff_v_bpcpx_result_choice_power_product)) /\ exists ff_q_bpcpx_result_choice_power_product_terminal. ff_u_bpcpx_result_choice_power_product = ff_q_bpcpx_result_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpx_result_choice)) * ff_v_bpcpx_result_choice_power_product) + (bpr_prefix_value_bpcpx_result))) /\ forall ff_i_bpcpx_result_choice_power_product. (exists ff_lt_bpcpx_result_choice_power_product_bound. ff_lt_bpcpx_result_choice_power_product_bound + S ff_i_bpcpx_result_choice_power_product = bpr_choice_exponent_bpcpx_result_choice) -> exists ff_p_bpcpx_result_choice_power_product ff_r_bpcpx_result_choice_power_product ff_s_bpcpx_result_choice_power_product. ((((exists ff_h_bpcpx_result_choice_power_product_factor. ff_h_bpcpx_result_choice_power_product_factor + S (ff_p_bpcpx_result_choice_power_product) = S ((S (ff_i_bpcpx_result_choice_power_product)) * bpr_power_scale_bpcpx_result_choice_power)) /\ exists ff_q_bpcpx_result_choice_power_product_factor. bpr_power_code_bpcpx_result_choice_power = ff_q_bpcpx_result_choice_power_product_factor * S ((S (ff_i_bpcpx_result_choice_power_product)) * bpr_power_scale_bpcpx_result_choice_power) + (ff_p_bpcpx_result_choice_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_power_product_partial. ff_h_bpcpx_result_choice_power_product_partial + S (ff_r_bpcpx_result_choice_power_product) = S ((S (ff_i_bpcpx_result_choice_power_product)) * ff_v_bpcpx_result_choice_power_product)) /\ exists ff_q_bpcpx_result_choice_power_product_partial. ff_u_bpcpx_result_choice_power_product = ff_q_bpcpx_result_choice_power_product_partial * S ((S (ff_i_bpcpx_result_choice_power_product)) * ff_v_bpcpx_result_choice_power_product) + (ff_r_bpcpx_result_choice_power_product))) /\ ((((exists ff_h_bpcpx_result_choice_power_product_successor. ff_h_bpcpx_result_choice_power_product_successor + S (ff_s_bpcpx_result_choice_power_product) = S ((S (S ff_i_bpcpx_result_choice_power_product)) * ff_v_bpcpx_result_choice_power_product)) /\ exists ff_q_bpcpx_result_choice_power_product_successor. ff_u_bpcpx_result_choice_power_product = ff_q_bpcpx_result_choice_power_product_successor * S ((S (S ff_i_bpcpx_result_choice_power_product)) * ff_v_bpcpx_result_choice_power_product) + (ff_s_bpcpx_result_choice_power_product))) /\ ff_s_bpcpx_result_choice_power_product = ff_r_bpcpx_result_choice_power_product * ff_p_bpcpx_result_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpx_result) = 1) /\ forall bpr_left_bpcpx_result_choice_prime bpr_right_bpcpx_result_choice_prime. S (bpr_prefix_index_bpcpx_result) = bpr_left_bpcpx_result_choice_prime * bpr_right_bpcpx_result_choice_prime -> bpr_left_bpcpx_result_choice_prime = 1 \/ bpr_right_bpcpx_result_choice_prime = 1)) /\ bpr_prefix_value_bpcpx_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–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro n
02Induction on mL2–2
Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.
- L2
induction m
03Construct an explicit witnessL3–4
04Fix variables and assumptionsL5–6
05Separate the logical casesL7–8
06Establish hsiL9–13
07Establish hpreviousL14–15
Establish this local claim before using it. It is not an additional assumption.
- L14
have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,m) → ∃ 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)Definitions: Lt(x,m)BetaAt(b,c,x,y)Prime(S x)PowerValuation(S x,n,z)Pow(S x,z,y)Original native command in the exact edition - L15
exact IH
08Separate the logical casesL16–17
09Establish hnextL18–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution prefix extend.
- L18
have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S m) → ∃ 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)Definitions: Lt(x,S m)BetaAt(b,c,x,y)Prime(S x)PowerValuation(S x,n,z)Pow(S x,z,y)Original native command in the exact edition - L19
apply prime_contribution_prefix_extend - L20
exact hprevious_witness_witness - L21
exact hnext
Original defined command ledger · 21 lines
- 0001
intro n - 0002
induction m - 0003
exists 0 - 0004
exists 0 - 0005
intro i - 0006
intro hi - 0007
exfalso - 0008
cases hi - 0009
have hsi : S i = 0 - 0010
apply add_eq_zero_right - 0011
exact hi_witness - 0012
apply succ_ne_zero - 0013
exact hsi - 0014
have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,m) → ∃ 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)Exact native replay line
have hprevious : exists b c. (forall bpr_prefix_index_bpcpx_previous. (exists bpr_gap_bpcpx_previous_bound. bpr_gap_bpcpx_previous_bound + S (bpr_prefix_index_bpcpx_previous) = m) -> exists bpr_prefix_value_bpcpx_previous. ((((exists bpr_height_bpcpx_previous_decoded. bpr_height_bpcpx_previous_decoded + S (bpr_prefix_value_bpcpx_previous) = S ((S (bpr_prefix_index_bpcpx_previous)) * c)) /\ exists bpr_quotient_bpcpx_previous_decoded. b = bpr_quotient_bpcpx_previous_decoded * S ((S (bpr_prefix_index_bpcpx_previous)) * c) + (bpr_prefix_value_bpcpx_previous))) /\ (((((~(S (bpr_prefix_index_bpcpx_previous) = 1) /\ forall bpr_left_bpcpx_previous_choice_prime bpr_right_bpcpx_previous_choice_prime. S (bpr_prefix_index_bpcpx_previous) = bpr_left_bpcpx_previous_choice_prime * bpr_right_bpcpx_previous_choice_prime -> bpr_left_bpcpx_previous_choice_prime = 1 \/ bpr_right_bpcpx_previous_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpx_previous_choice. ((((exists bpr_le_gap_bpcpx_previous_choice_valuation_selected_bound. bpr_le_gap_bpcpx_previous_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpx_previous_choice) = (n)) /\ (exists bpr_power_value_bpcpx_previous_choice_valuation_selected. ((exists bpr_power_code_bpcpx_previous_choice_valuation_selected_power bpr_power_scale_bpcpx_previous_choice_valuation_selected_power. ((forall bpr_power_index_bpcpx_previous_choice_valuation_selected_power. (exists bpr_gap_bpcpx_previous_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpx_previous_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpx_previous_choice_valuation_selected_power) = bpr_choice_exponent_bpcpx_previous_choice) -> (((exists bpr_height_bpcpx_previous_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpx_previous_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_previous)) = S ((S (bpr_power_index_bpcpx_previous_choice_valuation_selected_power)) * bpr_power_scale_bpcpx_previous_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpx_previous_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpx_previous_choice_valuation_selected_power = bpr_quotient_bpcpx_previous_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpx_previous_choice_valuation_selected_power)) * bpr_power_scale_bpcpx_previous_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpx_previous))))) /\ (exists ff_u_bpcpx_previous_choice_valuation_selected_power_product ff_v_bpcpx_previous_choice_valuation_selected_power_product. ((((exists ff_h_bpcpx_previous_choice_valuation_selected_power_product_start. ff_h_bpcpx_previous_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_previous_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_previous_choice_valuation_selected_power_product_start. ff_u_bpcpx_previous_choice_valuation_selected_power_product = ff_q_bpcpx_previous_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpx_previous_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpx_previous_choice_valuation_selected_power_product_terminal. ff_h_bpcpx_previous_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpx_previous_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpx_previous_choice)) * ff_v_bpcpx_previous_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_previous_choice_valuation_selected_power_product_terminal. ff_u_bpcpx_previous_choice_valuation_selected_power_product = ff_q_bpcpx_previous_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpx_previous_choice)) * ff_v_bpcpx_previous_choice_valuation_selected_power_product) + (bpr_power_value_bpcpx_previous_choice_valuation_selected))) /\ forall ff_i_bpcpx_previous_choice_valuation_selected_power_product. (exists ff_lt_bpcpx_previous_choice_valuation_selected_power_product_bound. ff_lt_bpcpx_previous_choice_valuation_selected_power_product_bound + S ff_i_bpcpx_previous_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpx_previous_choice) -> exists ff_p_bpcpx_previous_choice_valuation_selected_power_product ff_r_bpcpx_previous_choice_valuation_selected_power_product ff_s_bpcpx_previous_choice_valuation_selected_power_product. ((((exists ff_h_bpcpx_previous_choice_valuation_selected_power_product_factor. ff_h_bpcpx_previous_choice_valuation_selected_power_product_factor + S (ff_p_bpcpx_previous_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpx_previous_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpx_previous_choice_valuation_selected_power)) /\ exists ff_q_bpcpx_previous_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpx_previous_choice_valuation_selected_power = ff_q_bpcpx_previous_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpx_previous_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpx_previous_choice_valuation_selected_power) + (ff_p_bpcpx_previous_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpx_previous_choice_valuation_selected_power_product_partial. ff_h_bpcpx_previous_choice_valuation_selected_power_product_partial + S (ff_r_bpcpx_previous_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpx_previous_choice_valuation_selected_power_product)) * ff_v_bpcpx_previous_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_previous_choice_valuation_selected_power_product_partial. ff_u_bpcpx_previous_choice_valuation_selected_power_product = ff_q_bpcpx_previous_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpx_previous_choice_valuation_selected_power_product)) * ff_v_bpcpx_previous_choice_valuation_selected_power_product) + (ff_r_bpcpx_previous_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpx_previous_choice_valuation_selected_power_product_successor. ff_h_bpcpx_previous_choice_valuation_selected_power_product_successor + S (ff_s_bpcpx_previous_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpx_previous_choice_valuation_selected_power_product)) * ff_v_bpcpx_previous_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_previous_choice_valuation_selected_power_product_successor. ff_u_bpcpx_previous_choice_valuation_selected_power_product = ff_q_bpcpx_previous_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpx_previous_choice_valuation_selected_power_product)) * ff_v_bpcpx_previous_choice_valuation_selected_power_product) + (ff_s_bpcpx_previous_choice_valuation_selected_power_product))) /\ ff_s_bpcpx_previous_choice_valuation_selected_power_product = ff_r_bpcpx_previous_choice_valuation_selected_power_product * ff_p_bpcpx_previous_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpx_previous_choice_valuation_selected_divides. n = (bpr_power_value_bpcpx_previous_choice_valuation_selected) * bpr_divides_quotient_bpcpx_previous_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpx_previous_choice_valuation. (exists bpr_le_gap_bpcpx_previous_choice_valuation_candidate_bound. bpr_le_gap_bpcpx_previous_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpx_previous_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpx_previous_choice_valuation_candidate. ((exists bpr_power_code_bpcpx_previous_choice_valuation_candidate_power bpr_power_scale_bpcpx_previous_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpx_previous_choice_valuation_candidate_power. (exists bpr_gap_bpcpx_previous_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpx_previous_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpx_previous_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpx_previous_choice_valuation) -> (((exists bpr_height_bpcpx_previous_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpx_previous_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_previous)) = S ((S (bpr_power_index_bpcpx_previous_choice_valuation_candidate_power)) * bpr_power_scale_bpcpx_previous_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpx_previous_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpx_previous_choice_valuation_candidate_power = bpr_quotient_bpcpx_previous_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpx_previous_choice_valuation_candidate_power)) * bpr_power_scale_bpcpx_previous_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpx_previous))))) /\ (exists ff_u_bpcpx_previous_choice_valuation_candidate_power_product ff_v_bpcpx_previous_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpx_previous_choice_valuation_candidate_power_product_start. ff_h_bpcpx_previous_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_previous_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_previous_choice_valuation_candidate_power_product_start. ff_u_bpcpx_previous_choice_valuation_candidate_power_product = ff_q_bpcpx_previous_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpx_previous_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpx_previous_choice_valuation_candidate_power_product_terminal. ff_h_bpcpx_previous_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpx_previous_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpx_previous_choice_valuation)) * ff_v_bpcpx_previous_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_previous_choice_valuation_candidate_power_product_terminal. ff_u_bpcpx_previous_choice_valuation_candidate_power_product = ff_q_bpcpx_previous_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpx_previous_choice_valuation)) * ff_v_bpcpx_previous_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpx_previous_choice_valuation_candidate))) /\ forall ff_i_bpcpx_previous_choice_valuation_candidate_power_product. (exists ff_lt_bpcpx_previous_choice_valuation_candidate_power_product_bound. ff_lt_bpcpx_previous_choice_valuation_candidate_power_product_bound + S ff_i_bpcpx_previous_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpx_previous_choice_valuation) -> exists ff_p_bpcpx_previous_choice_valuation_candidate_power_product ff_r_bpcpx_previous_choice_valuation_candidate_power_product ff_s_bpcpx_previous_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpx_previous_choice_valuation_candidate_power_product_factor. ff_h_bpcpx_previous_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpx_previous_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpx_previous_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpx_previous_choice_valuation_candidate_power)) /\ exists ff_q_bpcpx_previous_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpx_previous_choice_valuation_candidate_power = ff_q_bpcpx_previous_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpx_previous_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpx_previous_choice_valuation_candidate_power) + (ff_p_bpcpx_previous_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpx_previous_choice_valuation_candidate_power_product_partial. ff_h_bpcpx_previous_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpx_previous_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpx_previous_choice_valuation_candidate_power_product)) * ff_v_bpcpx_previous_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_previous_choice_valuation_candidate_power_product_partial. ff_u_bpcpx_previous_choice_valuation_candidate_power_product = ff_q_bpcpx_previous_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpx_previous_choice_valuation_candidate_power_product)) * ff_v_bpcpx_previous_choice_valuation_candidate_power_product) + (ff_r_bpcpx_previous_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpx_previous_choice_valuation_candidate_power_product_successor. ff_h_bpcpx_previous_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpx_previous_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpx_previous_choice_valuation_candidate_power_product)) * ff_v_bpcpx_previous_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_previous_choice_valuation_candidate_power_product_successor. ff_u_bpcpx_previous_choice_valuation_candidate_power_product = ff_q_bpcpx_previous_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpx_previous_choice_valuation_candidate_power_product)) * ff_v_bpcpx_previous_choice_valuation_candidate_power_product) + (ff_s_bpcpx_previous_choice_valuation_candidate_power_product))) /\ ff_s_bpcpx_previous_choice_valuation_candidate_power_product = ff_r_bpcpx_previous_choice_valuation_candidate_power_product * ff_p_bpcpx_previous_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpx_previous_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpx_previous_choice_valuation_candidate) * bpr_divides_quotient_bpcpx_previous_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpx_previous_choice_valuation_candidate_below. bpr_le_gap_bpcpx_previous_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpx_previous_choice_valuation) = (bpr_choice_exponent_bpcpx_previous_choice))) /\ (exists bpr_power_code_bpcpx_previous_choice_power bpr_power_scale_bpcpx_previous_choice_power. ((forall bpr_power_index_bpcpx_previous_choice_power. (exists bpr_gap_bpcpx_previous_choice_power_repeat_bound. bpr_gap_bpcpx_previous_choice_power_repeat_bound + S (bpr_power_index_bpcpx_previous_choice_power) = bpr_choice_exponent_bpcpx_previous_choice) -> (((exists bpr_height_bpcpx_previous_choice_power_repeat_entry. bpr_height_bpcpx_previous_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_previous)) = S ((S (bpr_power_index_bpcpx_previous_choice_power)) * bpr_power_scale_bpcpx_previous_choice_power)) /\ exists bpr_quotient_bpcpx_previous_choice_power_repeat_entry. bpr_power_code_bpcpx_previous_choice_power = bpr_quotient_bpcpx_previous_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpx_previous_choice_power)) * bpr_power_scale_bpcpx_previous_choice_power) + (S (bpr_prefix_index_bpcpx_previous))))) /\ (exists ff_u_bpcpx_previous_choice_power_product ff_v_bpcpx_previous_choice_power_product. ((((exists ff_h_bpcpx_previous_choice_power_product_start. ff_h_bpcpx_previous_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_previous_choice_power_product)) /\ exists ff_q_bpcpx_previous_choice_power_product_start. ff_u_bpcpx_previous_choice_power_product = ff_q_bpcpx_previous_choice_power_product_start * S ((S (0)) * ff_v_bpcpx_previous_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpx_previous_choice_power_product_terminal. ff_h_bpcpx_previous_choice_power_product_terminal + S (bpr_prefix_value_bpcpx_previous) = S ((S (bpr_choice_exponent_bpcpx_previous_choice)) * ff_v_bpcpx_previous_choice_power_product)) /\ exists ff_q_bpcpx_previous_choice_power_product_terminal. ff_u_bpcpx_previous_choice_power_product = ff_q_bpcpx_previous_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpx_previous_choice)) * ff_v_bpcpx_previous_choice_power_product) + (bpr_prefix_value_bpcpx_previous))) /\ forall ff_i_bpcpx_previous_choice_power_product. (exists ff_lt_bpcpx_previous_choice_power_product_bound. ff_lt_bpcpx_previous_choice_power_product_bound + S ff_i_bpcpx_previous_choice_power_product = bpr_choice_exponent_bpcpx_previous_choice) -> exists ff_p_bpcpx_previous_choice_power_product ff_r_bpcpx_previous_choice_power_product ff_s_bpcpx_previous_choice_power_product. ((((exists ff_h_bpcpx_previous_choice_power_product_factor. ff_h_bpcpx_previous_choice_power_product_factor + S (ff_p_bpcpx_previous_choice_power_product) = S ((S (ff_i_bpcpx_previous_choice_power_product)) * bpr_power_scale_bpcpx_previous_choice_power)) /\ exists ff_q_bpcpx_previous_choice_power_product_factor. bpr_power_code_bpcpx_previous_choice_power = ff_q_bpcpx_previous_choice_power_product_factor * S ((S (ff_i_bpcpx_previous_choice_power_product)) * bpr_power_scale_bpcpx_previous_choice_power) + (ff_p_bpcpx_previous_choice_power_product))) /\ ((((exists ff_h_bpcpx_previous_choice_power_product_partial. ff_h_bpcpx_previous_choice_power_product_partial + S (ff_r_bpcpx_previous_choice_power_product) = S ((S (ff_i_bpcpx_previous_choice_power_product)) * ff_v_bpcpx_previous_choice_power_product)) /\ exists ff_q_bpcpx_previous_choice_power_product_partial. ff_u_bpcpx_previous_choice_power_product = ff_q_bpcpx_previous_choice_power_product_partial * S ((S (ff_i_bpcpx_previous_choice_power_product)) * ff_v_bpcpx_previous_choice_power_product) + (ff_r_bpcpx_previous_choice_power_product))) /\ ((((exists ff_h_bpcpx_previous_choice_power_product_successor. ff_h_bpcpx_previous_choice_power_product_successor + S (ff_s_bpcpx_previous_choice_power_product) = S ((S (S ff_i_bpcpx_previous_choice_power_product)) * ff_v_bpcpx_previous_choice_power_product)) /\ exists ff_q_bpcpx_previous_choice_power_product_successor. ff_u_bpcpx_previous_choice_power_product = ff_q_bpcpx_previous_choice_power_product_successor * S ((S (S ff_i_bpcpx_previous_choice_power_product)) * ff_v_bpcpx_previous_choice_power_product) + (ff_s_bpcpx_previous_choice_power_product))) /\ ff_s_bpcpx_previous_choice_power_product = ff_r_bpcpx_previous_choice_power_product * ff_p_bpcpx_previous_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpx_previous) = 1) /\ forall bpr_left_bpcpx_previous_choice_prime bpr_right_bpcpx_previous_choice_prime. S (bpr_prefix_index_bpcpx_previous) = bpr_left_bpcpx_previous_choice_prime * bpr_right_bpcpx_previous_choice_prime -> bpr_left_bpcpx_previous_choice_prime = 1 \/ bpr_right_bpcpx_previous_choice_prime = 1)) /\ bpr_prefix_value_bpcpx_previous = 1))))) - 0015
exact IH - 0016
cases hprevious - 0017
cases hprevious_witness - 0018
have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S m) → ∃ 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)Exact native replay line
have hnext : exists b c. (forall bpr_prefix_index_bpcpx_successor. (exists bpr_gap_bpcpx_successor_bound. bpr_gap_bpcpx_successor_bound + S (bpr_prefix_index_bpcpx_successor) = S m) -> exists bpr_prefix_value_bpcpx_successor. ((((exists bpr_height_bpcpx_successor_decoded. bpr_height_bpcpx_successor_decoded + S (bpr_prefix_value_bpcpx_successor) = S ((S (bpr_prefix_index_bpcpx_successor)) * c)) /\ exists bpr_quotient_bpcpx_successor_decoded. b = bpr_quotient_bpcpx_successor_decoded * S ((S (bpr_prefix_index_bpcpx_successor)) * c) + (bpr_prefix_value_bpcpx_successor))) /\ (((((~(S (bpr_prefix_index_bpcpx_successor) = 1) /\ forall bpr_left_bpcpx_successor_choice_prime bpr_right_bpcpx_successor_choice_prime. S (bpr_prefix_index_bpcpx_successor) = bpr_left_bpcpx_successor_choice_prime * bpr_right_bpcpx_successor_choice_prime -> bpr_left_bpcpx_successor_choice_prime = 1 \/ bpr_right_bpcpx_successor_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpx_successor_choice. ((((exists bpr_le_gap_bpcpx_successor_choice_valuation_selected_bound. bpr_le_gap_bpcpx_successor_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpx_successor_choice) = (n)) /\ (exists bpr_power_value_bpcpx_successor_choice_valuation_selected. ((exists bpr_power_code_bpcpx_successor_choice_valuation_selected_power bpr_power_scale_bpcpx_successor_choice_valuation_selected_power. ((forall bpr_power_index_bpcpx_successor_choice_valuation_selected_power. (exists bpr_gap_bpcpx_successor_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpx_successor_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpx_successor_choice_valuation_selected_power) = bpr_choice_exponent_bpcpx_successor_choice) -> (((exists bpr_height_bpcpx_successor_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpx_successor_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_successor)) = S ((S (bpr_power_index_bpcpx_successor_choice_valuation_selected_power)) * bpr_power_scale_bpcpx_successor_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpx_successor_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpx_successor_choice_valuation_selected_power = bpr_quotient_bpcpx_successor_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpx_successor_choice_valuation_selected_power)) * bpr_power_scale_bpcpx_successor_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpx_successor))))) /\ (exists ff_u_bpcpx_successor_choice_valuation_selected_power_product ff_v_bpcpx_successor_choice_valuation_selected_power_product. ((((exists ff_h_bpcpx_successor_choice_valuation_selected_power_product_start. ff_h_bpcpx_successor_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_successor_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_successor_choice_valuation_selected_power_product_start. ff_u_bpcpx_successor_choice_valuation_selected_power_product = ff_q_bpcpx_successor_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpx_successor_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpx_successor_choice_valuation_selected_power_product_terminal. ff_h_bpcpx_successor_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpx_successor_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpx_successor_choice)) * ff_v_bpcpx_successor_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_successor_choice_valuation_selected_power_product_terminal. ff_u_bpcpx_successor_choice_valuation_selected_power_product = ff_q_bpcpx_successor_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpx_successor_choice)) * ff_v_bpcpx_successor_choice_valuation_selected_power_product) + (bpr_power_value_bpcpx_successor_choice_valuation_selected))) /\ forall ff_i_bpcpx_successor_choice_valuation_selected_power_product. (exists ff_lt_bpcpx_successor_choice_valuation_selected_power_product_bound. ff_lt_bpcpx_successor_choice_valuation_selected_power_product_bound + S ff_i_bpcpx_successor_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpx_successor_choice) -> exists ff_p_bpcpx_successor_choice_valuation_selected_power_product ff_r_bpcpx_successor_choice_valuation_selected_power_product ff_s_bpcpx_successor_choice_valuation_selected_power_product. ((((exists ff_h_bpcpx_successor_choice_valuation_selected_power_product_factor. ff_h_bpcpx_successor_choice_valuation_selected_power_product_factor + S (ff_p_bpcpx_successor_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpx_successor_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpx_successor_choice_valuation_selected_power)) /\ exists ff_q_bpcpx_successor_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpx_successor_choice_valuation_selected_power = ff_q_bpcpx_successor_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpx_successor_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpx_successor_choice_valuation_selected_power) + (ff_p_bpcpx_successor_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpx_successor_choice_valuation_selected_power_product_partial. ff_h_bpcpx_successor_choice_valuation_selected_power_product_partial + S (ff_r_bpcpx_successor_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpx_successor_choice_valuation_selected_power_product)) * ff_v_bpcpx_successor_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_successor_choice_valuation_selected_power_product_partial. ff_u_bpcpx_successor_choice_valuation_selected_power_product = ff_q_bpcpx_successor_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpx_successor_choice_valuation_selected_power_product)) * ff_v_bpcpx_successor_choice_valuation_selected_power_product) + (ff_r_bpcpx_successor_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpx_successor_choice_valuation_selected_power_product_successor. ff_h_bpcpx_successor_choice_valuation_selected_power_product_successor + S (ff_s_bpcpx_successor_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpx_successor_choice_valuation_selected_power_product)) * ff_v_bpcpx_successor_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpx_successor_choice_valuation_selected_power_product_successor. ff_u_bpcpx_successor_choice_valuation_selected_power_product = ff_q_bpcpx_successor_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpx_successor_choice_valuation_selected_power_product)) * ff_v_bpcpx_successor_choice_valuation_selected_power_product) + (ff_s_bpcpx_successor_choice_valuation_selected_power_product))) /\ ff_s_bpcpx_successor_choice_valuation_selected_power_product = ff_r_bpcpx_successor_choice_valuation_selected_power_product * ff_p_bpcpx_successor_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpx_successor_choice_valuation_selected_divides. n = (bpr_power_value_bpcpx_successor_choice_valuation_selected) * bpr_divides_quotient_bpcpx_successor_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpx_successor_choice_valuation. (exists bpr_le_gap_bpcpx_successor_choice_valuation_candidate_bound. bpr_le_gap_bpcpx_successor_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpx_successor_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpx_successor_choice_valuation_candidate. ((exists bpr_power_code_bpcpx_successor_choice_valuation_candidate_power bpr_power_scale_bpcpx_successor_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpx_successor_choice_valuation_candidate_power. (exists bpr_gap_bpcpx_successor_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpx_successor_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpx_successor_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpx_successor_choice_valuation) -> (((exists bpr_height_bpcpx_successor_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpx_successor_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_successor)) = S ((S (bpr_power_index_bpcpx_successor_choice_valuation_candidate_power)) * bpr_power_scale_bpcpx_successor_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpx_successor_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpx_successor_choice_valuation_candidate_power = bpr_quotient_bpcpx_successor_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpx_successor_choice_valuation_candidate_power)) * bpr_power_scale_bpcpx_successor_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpx_successor))))) /\ (exists ff_u_bpcpx_successor_choice_valuation_candidate_power_product ff_v_bpcpx_successor_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpx_successor_choice_valuation_candidate_power_product_start. ff_h_bpcpx_successor_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_successor_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_successor_choice_valuation_candidate_power_product_start. ff_u_bpcpx_successor_choice_valuation_candidate_power_product = ff_q_bpcpx_successor_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpx_successor_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpx_successor_choice_valuation_candidate_power_product_terminal. ff_h_bpcpx_successor_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpx_successor_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpx_successor_choice_valuation)) * ff_v_bpcpx_successor_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_successor_choice_valuation_candidate_power_product_terminal. ff_u_bpcpx_successor_choice_valuation_candidate_power_product = ff_q_bpcpx_successor_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpx_successor_choice_valuation)) * ff_v_bpcpx_successor_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpx_successor_choice_valuation_candidate))) /\ forall ff_i_bpcpx_successor_choice_valuation_candidate_power_product. (exists ff_lt_bpcpx_successor_choice_valuation_candidate_power_product_bound. ff_lt_bpcpx_successor_choice_valuation_candidate_power_product_bound + S ff_i_bpcpx_successor_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpx_successor_choice_valuation) -> exists ff_p_bpcpx_successor_choice_valuation_candidate_power_product ff_r_bpcpx_successor_choice_valuation_candidate_power_product ff_s_bpcpx_successor_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpx_successor_choice_valuation_candidate_power_product_factor. ff_h_bpcpx_successor_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpx_successor_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpx_successor_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpx_successor_choice_valuation_candidate_power)) /\ exists ff_q_bpcpx_successor_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpx_successor_choice_valuation_candidate_power = ff_q_bpcpx_successor_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpx_successor_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpx_successor_choice_valuation_candidate_power) + (ff_p_bpcpx_successor_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpx_successor_choice_valuation_candidate_power_product_partial. ff_h_bpcpx_successor_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpx_successor_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpx_successor_choice_valuation_candidate_power_product)) * ff_v_bpcpx_successor_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_successor_choice_valuation_candidate_power_product_partial. ff_u_bpcpx_successor_choice_valuation_candidate_power_product = ff_q_bpcpx_successor_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpx_successor_choice_valuation_candidate_power_product)) * ff_v_bpcpx_successor_choice_valuation_candidate_power_product) + (ff_r_bpcpx_successor_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpx_successor_choice_valuation_candidate_power_product_successor. ff_h_bpcpx_successor_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpx_successor_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpx_successor_choice_valuation_candidate_power_product)) * ff_v_bpcpx_successor_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpx_successor_choice_valuation_candidate_power_product_successor. ff_u_bpcpx_successor_choice_valuation_candidate_power_product = ff_q_bpcpx_successor_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpx_successor_choice_valuation_candidate_power_product)) * ff_v_bpcpx_successor_choice_valuation_candidate_power_product) + (ff_s_bpcpx_successor_choice_valuation_candidate_power_product))) /\ ff_s_bpcpx_successor_choice_valuation_candidate_power_product = ff_r_bpcpx_successor_choice_valuation_candidate_power_product * ff_p_bpcpx_successor_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpx_successor_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpx_successor_choice_valuation_candidate) * bpr_divides_quotient_bpcpx_successor_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpx_successor_choice_valuation_candidate_below. bpr_le_gap_bpcpx_successor_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpx_successor_choice_valuation) = (bpr_choice_exponent_bpcpx_successor_choice))) /\ (exists bpr_power_code_bpcpx_successor_choice_power bpr_power_scale_bpcpx_successor_choice_power. ((forall bpr_power_index_bpcpx_successor_choice_power. (exists bpr_gap_bpcpx_successor_choice_power_repeat_bound. bpr_gap_bpcpx_successor_choice_power_repeat_bound + S (bpr_power_index_bpcpx_successor_choice_power) = bpr_choice_exponent_bpcpx_successor_choice) -> (((exists bpr_height_bpcpx_successor_choice_power_repeat_entry. bpr_height_bpcpx_successor_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpx_successor)) = S ((S (bpr_power_index_bpcpx_successor_choice_power)) * bpr_power_scale_bpcpx_successor_choice_power)) /\ exists bpr_quotient_bpcpx_successor_choice_power_repeat_entry. bpr_power_code_bpcpx_successor_choice_power = bpr_quotient_bpcpx_successor_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpx_successor_choice_power)) * bpr_power_scale_bpcpx_successor_choice_power) + (S (bpr_prefix_index_bpcpx_successor))))) /\ (exists ff_u_bpcpx_successor_choice_power_product ff_v_bpcpx_successor_choice_power_product. ((((exists ff_h_bpcpx_successor_choice_power_product_start. ff_h_bpcpx_successor_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpx_successor_choice_power_product)) /\ exists ff_q_bpcpx_successor_choice_power_product_start. ff_u_bpcpx_successor_choice_power_product = ff_q_bpcpx_successor_choice_power_product_start * S ((S (0)) * ff_v_bpcpx_successor_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpx_successor_choice_power_product_terminal. ff_h_bpcpx_successor_choice_power_product_terminal + S (bpr_prefix_value_bpcpx_successor) = S ((S (bpr_choice_exponent_bpcpx_successor_choice)) * ff_v_bpcpx_successor_choice_power_product)) /\ exists ff_q_bpcpx_successor_choice_power_product_terminal. ff_u_bpcpx_successor_choice_power_product = ff_q_bpcpx_successor_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpx_successor_choice)) * ff_v_bpcpx_successor_choice_power_product) + (bpr_prefix_value_bpcpx_successor))) /\ forall ff_i_bpcpx_successor_choice_power_product. (exists ff_lt_bpcpx_successor_choice_power_product_bound. ff_lt_bpcpx_successor_choice_power_product_bound + S ff_i_bpcpx_successor_choice_power_product = bpr_choice_exponent_bpcpx_successor_choice) -> exists ff_p_bpcpx_successor_choice_power_product ff_r_bpcpx_successor_choice_power_product ff_s_bpcpx_successor_choice_power_product. ((((exists ff_h_bpcpx_successor_choice_power_product_factor. ff_h_bpcpx_successor_choice_power_product_factor + S (ff_p_bpcpx_successor_choice_power_product) = S ((S (ff_i_bpcpx_successor_choice_power_product)) * bpr_power_scale_bpcpx_successor_choice_power)) /\ exists ff_q_bpcpx_successor_choice_power_product_factor. bpr_power_code_bpcpx_successor_choice_power = ff_q_bpcpx_successor_choice_power_product_factor * S ((S (ff_i_bpcpx_successor_choice_power_product)) * bpr_power_scale_bpcpx_successor_choice_power) + (ff_p_bpcpx_successor_choice_power_product))) /\ ((((exists ff_h_bpcpx_successor_choice_power_product_partial. ff_h_bpcpx_successor_choice_power_product_partial + S (ff_r_bpcpx_successor_choice_power_product) = S ((S (ff_i_bpcpx_successor_choice_power_product)) * ff_v_bpcpx_successor_choice_power_product)) /\ exists ff_q_bpcpx_successor_choice_power_product_partial. ff_u_bpcpx_successor_choice_power_product = ff_q_bpcpx_successor_choice_power_product_partial * S ((S (ff_i_bpcpx_successor_choice_power_product)) * ff_v_bpcpx_successor_choice_power_product) + (ff_r_bpcpx_successor_choice_power_product))) /\ ((((exists ff_h_bpcpx_successor_choice_power_product_successor. ff_h_bpcpx_successor_choice_power_product_successor + S (ff_s_bpcpx_successor_choice_power_product) = S ((S (S ff_i_bpcpx_successor_choice_power_product)) * ff_v_bpcpx_successor_choice_power_product)) /\ exists ff_q_bpcpx_successor_choice_power_product_successor. ff_u_bpcpx_successor_choice_power_product = ff_q_bpcpx_successor_choice_power_product_successor * S ((S (S ff_i_bpcpx_successor_choice_power_product)) * ff_v_bpcpx_successor_choice_power_product) + (ff_s_bpcpx_successor_choice_power_product))) /\ ff_s_bpcpx_successor_choice_power_product = ff_r_bpcpx_successor_choice_power_product * ff_p_bpcpx_successor_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpx_successor) = 1) /\ forall bpr_left_bpcpx_successor_choice_prime bpr_right_bpcpx_successor_choice_prime. S (bpr_prefix_index_bpcpx_successor) = bpr_left_bpcpx_successor_choice_prime * bpr_right_bpcpx_successor_choice_prime -> bpr_left_bpcpx_successor_choice_prime = 1 \/ bpr_right_bpcpx_successor_choice_prime = 1)) /\ bpr_prefix_value_bpcpx_successor = 1))))) - 0019
apply prime_contribution_prefix_extend - 0020
exact hprevious_witness_witness - 0021
exact hnext