Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ n. ∀ a. ∀ b. ∀ c. ∀ l. (∀ 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)) → ∃ x. ∃ y. ∀ z. Lt(z,S l) → ∃ m. BetaAt(x,y,z,m) ∧ (Prime(S (a + z)) ∧ (∃ k. PowerValuation(S (a + z),n,k) ∧ Pow(S (a + z),k,m)) ∨ ¬Prime(S (a + z)) ∧ m = 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
12 occurrences
In local proof propositions
14 occurrences
Exact expanded native-PA statement
forall n a b c l. (forall bpr_index_bpcifpe_before. (exists bpr_gap_bpcifpe_before_bound. bpr_gap_bpcifpe_before_bound + S (bpr_index_bpcifpe_before) = l) -> exists bpr_value_bpcifpe_before. ((((exists bpr_height_bpcifpe_before_decoded. bpr_height_bpcifpe_before_decoded + S (bpr_value_bpcifpe_before) = S ((S (bpr_index_bpcifpe_before)) * c)) /\ exists bpr_quotient_bpcifpe_before_decoded. b = bpr_quotient_bpcifpe_before_decoded * S ((S (bpr_index_bpcifpe_before)) * c) + (bpr_value_bpcifpe_before))) /\ (((((~(S (a + bpr_index_bpcifpe_before) = 1) /\ forall bpr_left_bpcifpe_before_choice_prime bpr_right_bpcifpe_before_choice_prime. S (a + bpr_index_bpcifpe_before) = bpr_left_bpcifpe_before_choice_prime * bpr_right_bpcifpe_before_choice_prime -> bpr_left_bpcifpe_before_choice_prime = 1 \/ bpr_right_bpcifpe_before_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcifpe_before_choice. ((((exists bpr_le_gap_bpcifpe_before_choice_valuation_selected_bound. bpr_le_gap_bpcifpe_before_choice_valuation_selected_bound + (bpr_choice_exponent_bpcifpe_before_choice) = (n)) /\ (exists bpr_power_value_bpcifpe_before_choice_valuation_selected. ((exists bpr_power_code_bpcifpe_before_choice_valuation_selected_power bpr_power_scale_bpcifpe_before_choice_valuation_selected_power. ((forall bpr_power_index_bpcifpe_before_choice_valuation_selected_power. (exists bpr_gap_bpcifpe_before_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcifpe_before_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcifpe_before_choice_valuation_selected_power) = bpr_choice_exponent_bpcifpe_before_choice) -> (((exists bpr_height_bpcifpe_before_choice_valuation_selected_power_repeat_entry. bpr_height_bpcifpe_before_choice_valuation_selected_power_repeat_entry + S (S (a + bpr_index_bpcifpe_before)) = S ((S (bpr_power_index_bpcifpe_before_choice_valuation_selected_power)) * bpr_power_scale_bpcifpe_before_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcifpe_before_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcifpe_before_choice_valuation_selected_power = bpr_quotient_bpcifpe_before_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_before_choice_valuation_selected_power)) * bpr_power_scale_bpcifpe_before_choice_valuation_selected_power) + (S (a + bpr_index_bpcifpe_before))))) /\ (exists ff_u_bpcifpe_before_choice_valuation_selected_power_product ff_v_bpcifpe_before_choice_valuation_selected_power_product. ((((exists ff_h_bpcifpe_before_choice_valuation_selected_power_product_start. ff_h_bpcifpe_before_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_before_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_before_choice_valuation_selected_power_product_start. ff_u_bpcifpe_before_choice_valuation_selected_power_product = ff_q_bpcifpe_before_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcifpe_before_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_before_choice_valuation_selected_power_product_terminal. ff_h_bpcifpe_before_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcifpe_before_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcifpe_before_choice)) * ff_v_bpcifpe_before_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_before_choice_valuation_selected_power_product_terminal. ff_u_bpcifpe_before_choice_valuation_selected_power_product = ff_q_bpcifpe_before_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcifpe_before_choice)) * ff_v_bpcifpe_before_choice_valuation_selected_power_product) + (bpr_power_value_bpcifpe_before_choice_valuation_selected))) /\ forall ff_i_bpcifpe_before_choice_valuation_selected_power_product. (exists ff_lt_bpcifpe_before_choice_valuation_selected_power_product_bound. ff_lt_bpcifpe_before_choice_valuation_selected_power_product_bound + S ff_i_bpcifpe_before_choice_valuation_selected_power_product = bpr_choice_exponent_bpcifpe_before_choice) -> exists ff_p_bpcifpe_before_choice_valuation_selected_power_product ff_r_bpcifpe_before_choice_valuation_selected_power_product ff_s_bpcifpe_before_choice_valuation_selected_power_product. ((((exists ff_h_bpcifpe_before_choice_valuation_selected_power_product_factor. ff_h_bpcifpe_before_choice_valuation_selected_power_product_factor + S (ff_p_bpcifpe_before_choice_valuation_selected_power_product) = S ((S (ff_i_bpcifpe_before_choice_valuation_selected_power_product)) * bpr_power_scale_bpcifpe_before_choice_valuation_selected_power)) /\ exists ff_q_bpcifpe_before_choice_valuation_selected_power_product_factor. bpr_power_code_bpcifpe_before_choice_valuation_selected_power = ff_q_bpcifpe_before_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcifpe_before_choice_valuation_selected_power_product)) * bpr_power_scale_bpcifpe_before_choice_valuation_selected_power) + (ff_p_bpcifpe_before_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcifpe_before_choice_valuation_selected_power_product_partial. ff_h_bpcifpe_before_choice_valuation_selected_power_product_partial + S (ff_r_bpcifpe_before_choice_valuation_selected_power_product) = S ((S (ff_i_bpcifpe_before_choice_valuation_selected_power_product)) * ff_v_bpcifpe_before_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_before_choice_valuation_selected_power_product_partial. ff_u_bpcifpe_before_choice_valuation_selected_power_product = ff_q_bpcifpe_before_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcifpe_before_choice_valuation_selected_power_product)) * ff_v_bpcifpe_before_choice_valuation_selected_power_product) + (ff_r_bpcifpe_before_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcifpe_before_choice_valuation_selected_power_product_successor. ff_h_bpcifpe_before_choice_valuation_selected_power_product_successor + S (ff_s_bpcifpe_before_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcifpe_before_choice_valuation_selected_power_product)) * ff_v_bpcifpe_before_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_before_choice_valuation_selected_power_product_successor. ff_u_bpcifpe_before_choice_valuation_selected_power_product = ff_q_bpcifpe_before_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcifpe_before_choice_valuation_selected_power_product)) * ff_v_bpcifpe_before_choice_valuation_selected_power_product) + (ff_s_bpcifpe_before_choice_valuation_selected_power_product))) /\ ff_s_bpcifpe_before_choice_valuation_selected_power_product = ff_r_bpcifpe_before_choice_valuation_selected_power_product * ff_p_bpcifpe_before_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcifpe_before_choice_valuation_selected_divides. n = (bpr_power_value_bpcifpe_before_choice_valuation_selected) * bpr_divides_quotient_bpcifpe_before_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcifpe_before_choice_valuation. (exists bpr_le_gap_bpcifpe_before_choice_valuation_candidate_bound. bpr_le_gap_bpcifpe_before_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcifpe_before_choice_valuation) = (n)) -> (exists bpr_power_value_bpcifpe_before_choice_valuation_candidate. ((exists bpr_power_code_bpcifpe_before_choice_valuation_candidate_power bpr_power_scale_bpcifpe_before_choice_valuation_candidate_power. ((forall bpr_power_index_bpcifpe_before_choice_valuation_candidate_power. (exists bpr_gap_bpcifpe_before_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcifpe_before_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcifpe_before_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcifpe_before_choice_valuation) -> (((exists bpr_height_bpcifpe_before_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcifpe_before_choice_valuation_candidate_power_repeat_entry + S (S (a + bpr_index_bpcifpe_before)) = S ((S (bpr_power_index_bpcifpe_before_choice_valuation_candidate_power)) * bpr_power_scale_bpcifpe_before_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcifpe_before_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcifpe_before_choice_valuation_candidate_power = bpr_quotient_bpcifpe_before_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_before_choice_valuation_candidate_power)) * bpr_power_scale_bpcifpe_before_choice_valuation_candidate_power) + (S (a + bpr_index_bpcifpe_before))))) /\ (exists ff_u_bpcifpe_before_choice_valuation_candidate_power_product ff_v_bpcifpe_before_choice_valuation_candidate_power_product. ((((exists ff_h_bpcifpe_before_choice_valuation_candidate_power_product_start. ff_h_bpcifpe_before_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_before_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_before_choice_valuation_candidate_power_product_start. ff_u_bpcifpe_before_choice_valuation_candidate_power_product = ff_q_bpcifpe_before_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcifpe_before_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_before_choice_valuation_candidate_power_product_terminal. ff_h_bpcifpe_before_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcifpe_before_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcifpe_before_choice_valuation)) * ff_v_bpcifpe_before_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_before_choice_valuation_candidate_power_product_terminal. ff_u_bpcifpe_before_choice_valuation_candidate_power_product = ff_q_bpcifpe_before_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcifpe_before_choice_valuation)) * ff_v_bpcifpe_before_choice_valuation_candidate_power_product) + (bpr_power_value_bpcifpe_before_choice_valuation_candidate))) /\ forall ff_i_bpcifpe_before_choice_valuation_candidate_power_product. (exists ff_lt_bpcifpe_before_choice_valuation_candidate_power_product_bound. ff_lt_bpcifpe_before_choice_valuation_candidate_power_product_bound + S ff_i_bpcifpe_before_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcifpe_before_choice_valuation) -> exists ff_p_bpcifpe_before_choice_valuation_candidate_power_product ff_r_bpcifpe_before_choice_valuation_candidate_power_product ff_s_bpcifpe_before_choice_valuation_candidate_power_product. ((((exists ff_h_bpcifpe_before_choice_valuation_candidate_power_product_factor. ff_h_bpcifpe_before_choice_valuation_candidate_power_product_factor + S (ff_p_bpcifpe_before_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcifpe_before_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcifpe_before_choice_valuation_candidate_power)) /\ exists ff_q_bpcifpe_before_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcifpe_before_choice_valuation_candidate_power = ff_q_bpcifpe_before_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcifpe_before_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcifpe_before_choice_valuation_candidate_power) + (ff_p_bpcifpe_before_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcifpe_before_choice_valuation_candidate_power_product_partial. ff_h_bpcifpe_before_choice_valuation_candidate_power_product_partial + S (ff_r_bpcifpe_before_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcifpe_before_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_before_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_before_choice_valuation_candidate_power_product_partial. ff_u_bpcifpe_before_choice_valuation_candidate_power_product = ff_q_bpcifpe_before_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcifpe_before_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_before_choice_valuation_candidate_power_product) + (ff_r_bpcifpe_before_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcifpe_before_choice_valuation_candidate_power_product_successor. ff_h_bpcifpe_before_choice_valuation_candidate_power_product_successor + S (ff_s_bpcifpe_before_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcifpe_before_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_before_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_before_choice_valuation_candidate_power_product_successor. ff_u_bpcifpe_before_choice_valuation_candidate_power_product = ff_q_bpcifpe_before_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcifpe_before_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_before_choice_valuation_candidate_power_product) + (ff_s_bpcifpe_before_choice_valuation_candidate_power_product))) /\ ff_s_bpcifpe_before_choice_valuation_candidate_power_product = ff_r_bpcifpe_before_choice_valuation_candidate_power_product * ff_p_bpcifpe_before_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcifpe_before_choice_valuation_candidate_divides. n = (bpr_power_value_bpcifpe_before_choice_valuation_candidate) * bpr_divides_quotient_bpcifpe_before_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcifpe_before_choice_valuation_candidate_below. bpr_le_gap_bpcifpe_before_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcifpe_before_choice_valuation) = (bpr_choice_exponent_bpcifpe_before_choice))) /\ (exists bpr_power_code_bpcifpe_before_choice_power bpr_power_scale_bpcifpe_before_choice_power. ((forall bpr_power_index_bpcifpe_before_choice_power. (exists bpr_gap_bpcifpe_before_choice_power_repeat_bound. bpr_gap_bpcifpe_before_choice_power_repeat_bound + S (bpr_power_index_bpcifpe_before_choice_power) = bpr_choice_exponent_bpcifpe_before_choice) -> (((exists bpr_height_bpcifpe_before_choice_power_repeat_entry. bpr_height_bpcifpe_before_choice_power_repeat_entry + S (S (a + bpr_index_bpcifpe_before)) = S ((S (bpr_power_index_bpcifpe_before_choice_power)) * bpr_power_scale_bpcifpe_before_choice_power)) /\ exists bpr_quotient_bpcifpe_before_choice_power_repeat_entry. bpr_power_code_bpcifpe_before_choice_power = bpr_quotient_bpcifpe_before_choice_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_before_choice_power)) * bpr_power_scale_bpcifpe_before_choice_power) + (S (a + bpr_index_bpcifpe_before))))) /\ (exists ff_u_bpcifpe_before_choice_power_product ff_v_bpcifpe_before_choice_power_product. ((((exists ff_h_bpcifpe_before_choice_power_product_start. ff_h_bpcifpe_before_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_before_choice_power_product)) /\ exists ff_q_bpcifpe_before_choice_power_product_start. ff_u_bpcifpe_before_choice_power_product = ff_q_bpcifpe_before_choice_power_product_start * S ((S (0)) * ff_v_bpcifpe_before_choice_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_before_choice_power_product_terminal. ff_h_bpcifpe_before_choice_power_product_terminal + S (bpr_value_bpcifpe_before) = S ((S (bpr_choice_exponent_bpcifpe_before_choice)) * ff_v_bpcifpe_before_choice_power_product)) /\ exists ff_q_bpcifpe_before_choice_power_product_terminal. ff_u_bpcifpe_before_choice_power_product = ff_q_bpcifpe_before_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcifpe_before_choice)) * ff_v_bpcifpe_before_choice_power_product) + (bpr_value_bpcifpe_before))) /\ forall ff_i_bpcifpe_before_choice_power_product. (exists ff_lt_bpcifpe_before_choice_power_product_bound. ff_lt_bpcifpe_before_choice_power_product_bound + S ff_i_bpcifpe_before_choice_power_product = bpr_choice_exponent_bpcifpe_before_choice) -> exists ff_p_bpcifpe_before_choice_power_product ff_r_bpcifpe_before_choice_power_product ff_s_bpcifpe_before_choice_power_product. ((((exists ff_h_bpcifpe_before_choice_power_product_factor. ff_h_bpcifpe_before_choice_power_product_factor + S (ff_p_bpcifpe_before_choice_power_product) = S ((S (ff_i_bpcifpe_before_choice_power_product)) * bpr_power_scale_bpcifpe_before_choice_power)) /\ exists ff_q_bpcifpe_before_choice_power_product_factor. bpr_power_code_bpcifpe_before_choice_power = ff_q_bpcifpe_before_choice_power_product_factor * S ((S (ff_i_bpcifpe_before_choice_power_product)) * bpr_power_scale_bpcifpe_before_choice_power) + (ff_p_bpcifpe_before_choice_power_product))) /\ ((((exists ff_h_bpcifpe_before_choice_power_product_partial. ff_h_bpcifpe_before_choice_power_product_partial + S (ff_r_bpcifpe_before_choice_power_product) = S ((S (ff_i_bpcifpe_before_choice_power_product)) * ff_v_bpcifpe_before_choice_power_product)) /\ exists ff_q_bpcifpe_before_choice_power_product_partial. ff_u_bpcifpe_before_choice_power_product = ff_q_bpcifpe_before_choice_power_product_partial * S ((S (ff_i_bpcifpe_before_choice_power_product)) * ff_v_bpcifpe_before_choice_power_product) + (ff_r_bpcifpe_before_choice_power_product))) /\ ((((exists ff_h_bpcifpe_before_choice_power_product_successor. ff_h_bpcifpe_before_choice_power_product_successor + S (ff_s_bpcifpe_before_choice_power_product) = S ((S (S ff_i_bpcifpe_before_choice_power_product)) * ff_v_bpcifpe_before_choice_power_product)) /\ exists ff_q_bpcifpe_before_choice_power_product_successor. ff_u_bpcifpe_before_choice_power_product = ff_q_bpcifpe_before_choice_power_product_successor * S ((S (S ff_i_bpcifpe_before_choice_power_product)) * ff_v_bpcifpe_before_choice_power_product) + (ff_s_bpcifpe_before_choice_power_product))) /\ ff_s_bpcifpe_before_choice_power_product = ff_r_bpcifpe_before_choice_power_product * ff_p_bpcifpe_before_choice_power_product)))))))))) \/ (~((~(S (a + bpr_index_bpcifpe_before) = 1) /\ forall bpr_left_bpcifpe_before_choice_prime bpr_right_bpcifpe_before_choice_prime. S (a + bpr_index_bpcifpe_before) = bpr_left_bpcifpe_before_choice_prime * bpr_right_bpcifpe_before_choice_prime -> bpr_left_bpcifpe_before_choice_prime = 1 \/ bpr_right_bpcifpe_before_choice_prime = 1)) /\ bpr_value_bpcifpe_before = 1))))) -> exists d e. (forall bpr_index_bpcifpe_after. (exists bpr_gap_bpcifpe_after_bound. bpr_gap_bpcifpe_after_bound + S (bpr_index_bpcifpe_after) = S l) -> exists bpr_value_bpcifpe_after. ((((exists bpr_height_bpcifpe_after_decoded. bpr_height_bpcifpe_after_decoded + S (bpr_value_bpcifpe_after) = S ((S (bpr_index_bpcifpe_after)) * e)) /\ exists bpr_quotient_bpcifpe_after_decoded. d = bpr_quotient_bpcifpe_after_decoded * S ((S (bpr_index_bpcifpe_after)) * e) + (bpr_value_bpcifpe_after))) /\ (((((~(S (a + bpr_index_bpcifpe_after) = 1) /\ forall bpr_left_bpcifpe_after_choice_prime bpr_right_bpcifpe_after_choice_prime. S (a + bpr_index_bpcifpe_after) = bpr_left_bpcifpe_after_choice_prime * bpr_right_bpcifpe_after_choice_prime -> bpr_left_bpcifpe_after_choice_prime = 1 \/ bpr_right_bpcifpe_after_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcifpe_after_choice. ((((exists bpr_le_gap_bpcifpe_after_choice_valuation_selected_bound. bpr_le_gap_bpcifpe_after_choice_valuation_selected_bound + (bpr_choice_exponent_bpcifpe_after_choice) = (n)) /\ (exists bpr_power_value_bpcifpe_after_choice_valuation_selected. ((exists bpr_power_code_bpcifpe_after_choice_valuation_selected_power bpr_power_scale_bpcifpe_after_choice_valuation_selected_power. ((forall bpr_power_index_bpcifpe_after_choice_valuation_selected_power. (exists bpr_gap_bpcifpe_after_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcifpe_after_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcifpe_after_choice_valuation_selected_power) = bpr_choice_exponent_bpcifpe_after_choice) -> (((exists bpr_height_bpcifpe_after_choice_valuation_selected_power_repeat_entry. bpr_height_bpcifpe_after_choice_valuation_selected_power_repeat_entry + S (S (a + bpr_index_bpcifpe_after)) = S ((S (bpr_power_index_bpcifpe_after_choice_valuation_selected_power)) * bpr_power_scale_bpcifpe_after_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcifpe_after_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcifpe_after_choice_valuation_selected_power = bpr_quotient_bpcifpe_after_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_after_choice_valuation_selected_power)) * bpr_power_scale_bpcifpe_after_choice_valuation_selected_power) + (S (a + bpr_index_bpcifpe_after))))) /\ (exists ff_u_bpcifpe_after_choice_valuation_selected_power_product ff_v_bpcifpe_after_choice_valuation_selected_power_product. ((((exists ff_h_bpcifpe_after_choice_valuation_selected_power_product_start. ff_h_bpcifpe_after_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_after_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_after_choice_valuation_selected_power_product_start. ff_u_bpcifpe_after_choice_valuation_selected_power_product = ff_q_bpcifpe_after_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcifpe_after_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_after_choice_valuation_selected_power_product_terminal. ff_h_bpcifpe_after_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcifpe_after_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcifpe_after_choice)) * ff_v_bpcifpe_after_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_after_choice_valuation_selected_power_product_terminal. ff_u_bpcifpe_after_choice_valuation_selected_power_product = ff_q_bpcifpe_after_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcifpe_after_choice)) * ff_v_bpcifpe_after_choice_valuation_selected_power_product) + (bpr_power_value_bpcifpe_after_choice_valuation_selected))) /\ forall ff_i_bpcifpe_after_choice_valuation_selected_power_product. (exists ff_lt_bpcifpe_after_choice_valuation_selected_power_product_bound. ff_lt_bpcifpe_after_choice_valuation_selected_power_product_bound + S ff_i_bpcifpe_after_choice_valuation_selected_power_product = bpr_choice_exponent_bpcifpe_after_choice) -> exists ff_p_bpcifpe_after_choice_valuation_selected_power_product ff_r_bpcifpe_after_choice_valuation_selected_power_product ff_s_bpcifpe_after_choice_valuation_selected_power_product. ((((exists ff_h_bpcifpe_after_choice_valuation_selected_power_product_factor. ff_h_bpcifpe_after_choice_valuation_selected_power_product_factor + S (ff_p_bpcifpe_after_choice_valuation_selected_power_product) = S ((S (ff_i_bpcifpe_after_choice_valuation_selected_power_product)) * bpr_power_scale_bpcifpe_after_choice_valuation_selected_power)) /\ exists ff_q_bpcifpe_after_choice_valuation_selected_power_product_factor. bpr_power_code_bpcifpe_after_choice_valuation_selected_power = ff_q_bpcifpe_after_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcifpe_after_choice_valuation_selected_power_product)) * bpr_power_scale_bpcifpe_after_choice_valuation_selected_power) + (ff_p_bpcifpe_after_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcifpe_after_choice_valuation_selected_power_product_partial. ff_h_bpcifpe_after_choice_valuation_selected_power_product_partial + S (ff_r_bpcifpe_after_choice_valuation_selected_power_product) = S ((S (ff_i_bpcifpe_after_choice_valuation_selected_power_product)) * ff_v_bpcifpe_after_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_after_choice_valuation_selected_power_product_partial. ff_u_bpcifpe_after_choice_valuation_selected_power_product = ff_q_bpcifpe_after_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcifpe_after_choice_valuation_selected_power_product)) * ff_v_bpcifpe_after_choice_valuation_selected_power_product) + (ff_r_bpcifpe_after_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcifpe_after_choice_valuation_selected_power_product_successor. ff_h_bpcifpe_after_choice_valuation_selected_power_product_successor + S (ff_s_bpcifpe_after_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcifpe_after_choice_valuation_selected_power_product)) * ff_v_bpcifpe_after_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_after_choice_valuation_selected_power_product_successor. ff_u_bpcifpe_after_choice_valuation_selected_power_product = ff_q_bpcifpe_after_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcifpe_after_choice_valuation_selected_power_product)) * ff_v_bpcifpe_after_choice_valuation_selected_power_product) + (ff_s_bpcifpe_after_choice_valuation_selected_power_product))) /\ ff_s_bpcifpe_after_choice_valuation_selected_power_product = ff_r_bpcifpe_after_choice_valuation_selected_power_product * ff_p_bpcifpe_after_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcifpe_after_choice_valuation_selected_divides. n = (bpr_power_value_bpcifpe_after_choice_valuation_selected) * bpr_divides_quotient_bpcifpe_after_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcifpe_after_choice_valuation. (exists bpr_le_gap_bpcifpe_after_choice_valuation_candidate_bound. bpr_le_gap_bpcifpe_after_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcifpe_after_choice_valuation) = (n)) -> (exists bpr_power_value_bpcifpe_after_choice_valuation_candidate. ((exists bpr_power_code_bpcifpe_after_choice_valuation_candidate_power bpr_power_scale_bpcifpe_after_choice_valuation_candidate_power. ((forall bpr_power_index_bpcifpe_after_choice_valuation_candidate_power. (exists bpr_gap_bpcifpe_after_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcifpe_after_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcifpe_after_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcifpe_after_choice_valuation) -> (((exists bpr_height_bpcifpe_after_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcifpe_after_choice_valuation_candidate_power_repeat_entry + S (S (a + bpr_index_bpcifpe_after)) = S ((S (bpr_power_index_bpcifpe_after_choice_valuation_candidate_power)) * bpr_power_scale_bpcifpe_after_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcifpe_after_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcifpe_after_choice_valuation_candidate_power = bpr_quotient_bpcifpe_after_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_after_choice_valuation_candidate_power)) * bpr_power_scale_bpcifpe_after_choice_valuation_candidate_power) + (S (a + bpr_index_bpcifpe_after))))) /\ (exists ff_u_bpcifpe_after_choice_valuation_candidate_power_product ff_v_bpcifpe_after_choice_valuation_candidate_power_product. ((((exists ff_h_bpcifpe_after_choice_valuation_candidate_power_product_start. ff_h_bpcifpe_after_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_after_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_after_choice_valuation_candidate_power_product_start. ff_u_bpcifpe_after_choice_valuation_candidate_power_product = ff_q_bpcifpe_after_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcifpe_after_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_after_choice_valuation_candidate_power_product_terminal. ff_h_bpcifpe_after_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcifpe_after_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcifpe_after_choice_valuation)) * ff_v_bpcifpe_after_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_after_choice_valuation_candidate_power_product_terminal. ff_u_bpcifpe_after_choice_valuation_candidate_power_product = ff_q_bpcifpe_after_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcifpe_after_choice_valuation)) * ff_v_bpcifpe_after_choice_valuation_candidate_power_product) + (bpr_power_value_bpcifpe_after_choice_valuation_candidate))) /\ forall ff_i_bpcifpe_after_choice_valuation_candidate_power_product. (exists ff_lt_bpcifpe_after_choice_valuation_candidate_power_product_bound. ff_lt_bpcifpe_after_choice_valuation_candidate_power_product_bound + S ff_i_bpcifpe_after_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcifpe_after_choice_valuation) -> exists ff_p_bpcifpe_after_choice_valuation_candidate_power_product ff_r_bpcifpe_after_choice_valuation_candidate_power_product ff_s_bpcifpe_after_choice_valuation_candidate_power_product. ((((exists ff_h_bpcifpe_after_choice_valuation_candidate_power_product_factor. ff_h_bpcifpe_after_choice_valuation_candidate_power_product_factor + S (ff_p_bpcifpe_after_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcifpe_after_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcifpe_after_choice_valuation_candidate_power)) /\ exists ff_q_bpcifpe_after_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcifpe_after_choice_valuation_candidate_power = ff_q_bpcifpe_after_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcifpe_after_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcifpe_after_choice_valuation_candidate_power) + (ff_p_bpcifpe_after_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcifpe_after_choice_valuation_candidate_power_product_partial. ff_h_bpcifpe_after_choice_valuation_candidate_power_product_partial + S (ff_r_bpcifpe_after_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcifpe_after_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_after_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_after_choice_valuation_candidate_power_product_partial. ff_u_bpcifpe_after_choice_valuation_candidate_power_product = ff_q_bpcifpe_after_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcifpe_after_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_after_choice_valuation_candidate_power_product) + (ff_r_bpcifpe_after_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcifpe_after_choice_valuation_candidate_power_product_successor. ff_h_bpcifpe_after_choice_valuation_candidate_power_product_successor + S (ff_s_bpcifpe_after_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcifpe_after_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_after_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_after_choice_valuation_candidate_power_product_successor. ff_u_bpcifpe_after_choice_valuation_candidate_power_product = ff_q_bpcifpe_after_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcifpe_after_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_after_choice_valuation_candidate_power_product) + (ff_s_bpcifpe_after_choice_valuation_candidate_power_product))) /\ ff_s_bpcifpe_after_choice_valuation_candidate_power_product = ff_r_bpcifpe_after_choice_valuation_candidate_power_product * ff_p_bpcifpe_after_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcifpe_after_choice_valuation_candidate_divides. n = (bpr_power_value_bpcifpe_after_choice_valuation_candidate) * bpr_divides_quotient_bpcifpe_after_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcifpe_after_choice_valuation_candidate_below. bpr_le_gap_bpcifpe_after_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcifpe_after_choice_valuation) = (bpr_choice_exponent_bpcifpe_after_choice))) /\ (exists bpr_power_code_bpcifpe_after_choice_power bpr_power_scale_bpcifpe_after_choice_power. ((forall bpr_power_index_bpcifpe_after_choice_power. (exists bpr_gap_bpcifpe_after_choice_power_repeat_bound. bpr_gap_bpcifpe_after_choice_power_repeat_bound + S (bpr_power_index_bpcifpe_after_choice_power) = bpr_choice_exponent_bpcifpe_after_choice) -> (((exists bpr_height_bpcifpe_after_choice_power_repeat_entry. bpr_height_bpcifpe_after_choice_power_repeat_entry + S (S (a + bpr_index_bpcifpe_after)) = S ((S (bpr_power_index_bpcifpe_after_choice_power)) * bpr_power_scale_bpcifpe_after_choice_power)) /\ exists bpr_quotient_bpcifpe_after_choice_power_repeat_entry. bpr_power_code_bpcifpe_after_choice_power = bpr_quotient_bpcifpe_after_choice_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_after_choice_power)) * bpr_power_scale_bpcifpe_after_choice_power) + (S (a + bpr_index_bpcifpe_after))))) /\ (exists ff_u_bpcifpe_after_choice_power_product ff_v_bpcifpe_after_choice_power_product. ((((exists ff_h_bpcifpe_after_choice_power_product_start. ff_h_bpcifpe_after_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_after_choice_power_product)) /\ exists ff_q_bpcifpe_after_choice_power_product_start. ff_u_bpcifpe_after_choice_power_product = ff_q_bpcifpe_after_choice_power_product_start * S ((S (0)) * ff_v_bpcifpe_after_choice_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_after_choice_power_product_terminal. ff_h_bpcifpe_after_choice_power_product_terminal + S (bpr_value_bpcifpe_after) = S ((S (bpr_choice_exponent_bpcifpe_after_choice)) * ff_v_bpcifpe_after_choice_power_product)) /\ exists ff_q_bpcifpe_after_choice_power_product_terminal. ff_u_bpcifpe_after_choice_power_product = ff_q_bpcifpe_after_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcifpe_after_choice)) * ff_v_bpcifpe_after_choice_power_product) + (bpr_value_bpcifpe_after))) /\ forall ff_i_bpcifpe_after_choice_power_product. (exists ff_lt_bpcifpe_after_choice_power_product_bound. ff_lt_bpcifpe_after_choice_power_product_bound + S ff_i_bpcifpe_after_choice_power_product = bpr_choice_exponent_bpcifpe_after_choice) -> exists ff_p_bpcifpe_after_choice_power_product ff_r_bpcifpe_after_choice_power_product ff_s_bpcifpe_after_choice_power_product. ((((exists ff_h_bpcifpe_after_choice_power_product_factor. ff_h_bpcifpe_after_choice_power_product_factor + S (ff_p_bpcifpe_after_choice_power_product) = S ((S (ff_i_bpcifpe_after_choice_power_product)) * bpr_power_scale_bpcifpe_after_choice_power)) /\ exists ff_q_bpcifpe_after_choice_power_product_factor. bpr_power_code_bpcifpe_after_choice_power = ff_q_bpcifpe_after_choice_power_product_factor * S ((S (ff_i_bpcifpe_after_choice_power_product)) * bpr_power_scale_bpcifpe_after_choice_power) + (ff_p_bpcifpe_after_choice_power_product))) /\ ((((exists ff_h_bpcifpe_after_choice_power_product_partial. ff_h_bpcifpe_after_choice_power_product_partial + S (ff_r_bpcifpe_after_choice_power_product) = S ((S (ff_i_bpcifpe_after_choice_power_product)) * ff_v_bpcifpe_after_choice_power_product)) /\ exists ff_q_bpcifpe_after_choice_power_product_partial. ff_u_bpcifpe_after_choice_power_product = ff_q_bpcifpe_after_choice_power_product_partial * S ((S (ff_i_bpcifpe_after_choice_power_product)) * ff_v_bpcifpe_after_choice_power_product) + (ff_r_bpcifpe_after_choice_power_product))) /\ ((((exists ff_h_bpcifpe_after_choice_power_product_successor. ff_h_bpcifpe_after_choice_power_product_successor + S (ff_s_bpcifpe_after_choice_power_product) = S ((S (S ff_i_bpcifpe_after_choice_power_product)) * ff_v_bpcifpe_after_choice_power_product)) /\ exists ff_q_bpcifpe_after_choice_power_product_successor. ff_u_bpcifpe_after_choice_power_product = ff_q_bpcifpe_after_choice_power_product_successor * S ((S (S ff_i_bpcifpe_after_choice_power_product)) * ff_v_bpcifpe_after_choice_power_product) + (ff_s_bpcifpe_after_choice_power_product))) /\ ff_s_bpcifpe_after_choice_power_product = ff_r_bpcifpe_after_choice_power_product * ff_p_bpcifpe_after_choice_power_product)))))))))) \/ (~((~(S (a + bpr_index_bpcifpe_after) = 1) /\ forall bpr_left_bpcifpe_after_choice_prime bpr_right_bpcifpe_after_choice_prime. S (a + bpr_index_bpcifpe_after) = bpr_left_bpcifpe_after_choice_prime * bpr_right_bpcifpe_after_choice_prime -> bpr_left_bpcifpe_after_choice_prime = 1 \/ bpr_right_bpcifpe_after_choice_prime = 1)) /\ bpr_value_bpcifpe_after = 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–6
02Establish hchoiceL7–10
Establish this local claim before using it. It is not an additional assumption.
- L7
have hchoice : ∃ x. Prime(S (a + l)) ∧ (∃ y. PowerValuation(S (a + l),n,y) ∧ Pow(S (a + l),y,x)) ∨ ¬Prime(S (a + l)) ∧ x = 1Definitions: Prime(S (a + l))PowerValuation(S (a + l),n,y)Pow(S (a + l),y,x)Original native command in the exact edition - L8
specialize prime_contribution_choice_exists n - L9
specialize prime_contribution_choice_exists (a + l) - L10
exact prime_contribution_choice_exists
03Separate the logical casesL11–11
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L11
cases hchoice
04Establish hextL12–13
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix extend.
- L12
have hext : ∃ d. ∃ e. BetaAt(d,e,l,x) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(b,c,y,z) → BetaAt(d,e,y,z))Definitions: BetaAt(d,e,l,x)Lt(y,l)BetaAt(b,c,y,z)BetaAt(d,e,y,z)Original native command in the exact edition - L13
apply beta_prefix_extend
05Separate the logical casesL14–16
06Construct an explicit witnessL17–18
07Fix variables and assumptionsL19–20
08Establish hsplitL21–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
09Separate the logical casesL24–24
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L24
cases hsplit
10Calculate and transport equalitiesL25–34
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
11Calculate and transport equalitiesL35–36
12Construct an explicit witnessL37–37
Supply the displayed value, then prove that it has the required property.
- L37
exists x
13Separate the logical casesL38–38
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L38
split
14Use earlier factsL39–40
15Establish holdL41–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
- L41
have hold : ∃ p. BetaAt(b,c,i,p) ∧ (Prime(S (a + i)) ∧ (∃ x. PowerValuation(S (a + i),n,x) ∧ Pow(S (a + i),x,p)) ∨ ¬Prime(S (a + i)) ∧ p = 1)Definitions: BetaAt(b,c,i,p)Prime(S (a + i))PowerValuation(S (a + i),n,x)Pow(S (a + i),x,p)Original native command in the exact edition - L42
apply hprefix - L43
exact hsplit_right
16Separate the logical casesL44–45
17Construct an explicit witnessL46–46
Supply the displayed value, then prove that it has the required property.
- L46
exists x3
18Separate the logical casesL47–47
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L47
split
Original defined command ledger · 51 lines
- 0001
intro n - 0002
intro a - 0003
intro b - 0004
intro c - 0005
intro l - 0006
intro hprefix - 0007
have hchoice : ∃ x. Prime(S (a + l)) ∧ (∃ y. PowerValuation(S (a + l),n,y) ∧ Pow(S (a + l),y,x)) ∨ ¬Prime(S (a + l)) ∧ x = 1Exact native replay line
have hchoice : exists x. (((((~(S (a + l) = 1) /\ forall bpr_left_bpcifpe_last_choice_prime bpr_right_bpcifpe_last_choice_prime. S (a + l) = bpr_left_bpcifpe_last_choice_prime * bpr_right_bpcifpe_last_choice_prime -> bpr_left_bpcifpe_last_choice_prime = 1 \/ bpr_right_bpcifpe_last_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcifpe_last_choice. ((((exists bpr_le_gap_bpcifpe_last_choice_valuation_selected_bound. bpr_le_gap_bpcifpe_last_choice_valuation_selected_bound + (bpr_choice_exponent_bpcifpe_last_choice) = (n)) /\ (exists bpr_power_value_bpcifpe_last_choice_valuation_selected. ((exists bpr_power_code_bpcifpe_last_choice_valuation_selected_power bpr_power_scale_bpcifpe_last_choice_valuation_selected_power. ((forall bpr_power_index_bpcifpe_last_choice_valuation_selected_power. (exists bpr_gap_bpcifpe_last_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcifpe_last_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcifpe_last_choice_valuation_selected_power) = bpr_choice_exponent_bpcifpe_last_choice) -> (((exists bpr_height_bpcifpe_last_choice_valuation_selected_power_repeat_entry. bpr_height_bpcifpe_last_choice_valuation_selected_power_repeat_entry + S (S (a + l)) = S ((S (bpr_power_index_bpcifpe_last_choice_valuation_selected_power)) * bpr_power_scale_bpcifpe_last_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcifpe_last_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcifpe_last_choice_valuation_selected_power = bpr_quotient_bpcifpe_last_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_last_choice_valuation_selected_power)) * bpr_power_scale_bpcifpe_last_choice_valuation_selected_power) + (S (a + l))))) /\ (exists ff_u_bpcifpe_last_choice_valuation_selected_power_product ff_v_bpcifpe_last_choice_valuation_selected_power_product. ((((exists ff_h_bpcifpe_last_choice_valuation_selected_power_product_start. ff_h_bpcifpe_last_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_last_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_last_choice_valuation_selected_power_product_start. ff_u_bpcifpe_last_choice_valuation_selected_power_product = ff_q_bpcifpe_last_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcifpe_last_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_last_choice_valuation_selected_power_product_terminal. ff_h_bpcifpe_last_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcifpe_last_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcifpe_last_choice)) * ff_v_bpcifpe_last_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_last_choice_valuation_selected_power_product_terminal. ff_u_bpcifpe_last_choice_valuation_selected_power_product = ff_q_bpcifpe_last_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcifpe_last_choice)) * ff_v_bpcifpe_last_choice_valuation_selected_power_product) + (bpr_power_value_bpcifpe_last_choice_valuation_selected))) /\ forall ff_i_bpcifpe_last_choice_valuation_selected_power_product. (exists ff_lt_bpcifpe_last_choice_valuation_selected_power_product_bound. ff_lt_bpcifpe_last_choice_valuation_selected_power_product_bound + S ff_i_bpcifpe_last_choice_valuation_selected_power_product = bpr_choice_exponent_bpcifpe_last_choice) -> exists ff_p_bpcifpe_last_choice_valuation_selected_power_product ff_r_bpcifpe_last_choice_valuation_selected_power_product ff_s_bpcifpe_last_choice_valuation_selected_power_product. ((((exists ff_h_bpcifpe_last_choice_valuation_selected_power_product_factor. ff_h_bpcifpe_last_choice_valuation_selected_power_product_factor + S (ff_p_bpcifpe_last_choice_valuation_selected_power_product) = S ((S (ff_i_bpcifpe_last_choice_valuation_selected_power_product)) * bpr_power_scale_bpcifpe_last_choice_valuation_selected_power)) /\ exists ff_q_bpcifpe_last_choice_valuation_selected_power_product_factor. bpr_power_code_bpcifpe_last_choice_valuation_selected_power = ff_q_bpcifpe_last_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcifpe_last_choice_valuation_selected_power_product)) * bpr_power_scale_bpcifpe_last_choice_valuation_selected_power) + (ff_p_bpcifpe_last_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcifpe_last_choice_valuation_selected_power_product_partial. ff_h_bpcifpe_last_choice_valuation_selected_power_product_partial + S (ff_r_bpcifpe_last_choice_valuation_selected_power_product) = S ((S (ff_i_bpcifpe_last_choice_valuation_selected_power_product)) * ff_v_bpcifpe_last_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_last_choice_valuation_selected_power_product_partial. ff_u_bpcifpe_last_choice_valuation_selected_power_product = ff_q_bpcifpe_last_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcifpe_last_choice_valuation_selected_power_product)) * ff_v_bpcifpe_last_choice_valuation_selected_power_product) + (ff_r_bpcifpe_last_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcifpe_last_choice_valuation_selected_power_product_successor. ff_h_bpcifpe_last_choice_valuation_selected_power_product_successor + S (ff_s_bpcifpe_last_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcifpe_last_choice_valuation_selected_power_product)) * ff_v_bpcifpe_last_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_last_choice_valuation_selected_power_product_successor. ff_u_bpcifpe_last_choice_valuation_selected_power_product = ff_q_bpcifpe_last_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcifpe_last_choice_valuation_selected_power_product)) * ff_v_bpcifpe_last_choice_valuation_selected_power_product) + (ff_s_bpcifpe_last_choice_valuation_selected_power_product))) /\ ff_s_bpcifpe_last_choice_valuation_selected_power_product = ff_r_bpcifpe_last_choice_valuation_selected_power_product * ff_p_bpcifpe_last_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcifpe_last_choice_valuation_selected_divides. n = (bpr_power_value_bpcifpe_last_choice_valuation_selected) * bpr_divides_quotient_bpcifpe_last_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcifpe_last_choice_valuation. (exists bpr_le_gap_bpcifpe_last_choice_valuation_candidate_bound. bpr_le_gap_bpcifpe_last_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcifpe_last_choice_valuation) = (n)) -> (exists bpr_power_value_bpcifpe_last_choice_valuation_candidate. ((exists bpr_power_code_bpcifpe_last_choice_valuation_candidate_power bpr_power_scale_bpcifpe_last_choice_valuation_candidate_power. ((forall bpr_power_index_bpcifpe_last_choice_valuation_candidate_power. (exists bpr_gap_bpcifpe_last_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcifpe_last_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcifpe_last_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcifpe_last_choice_valuation) -> (((exists bpr_height_bpcifpe_last_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcifpe_last_choice_valuation_candidate_power_repeat_entry + S (S (a + l)) = S ((S (bpr_power_index_bpcifpe_last_choice_valuation_candidate_power)) * bpr_power_scale_bpcifpe_last_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcifpe_last_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcifpe_last_choice_valuation_candidate_power = bpr_quotient_bpcifpe_last_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_last_choice_valuation_candidate_power)) * bpr_power_scale_bpcifpe_last_choice_valuation_candidate_power) + (S (a + l))))) /\ (exists ff_u_bpcifpe_last_choice_valuation_candidate_power_product ff_v_bpcifpe_last_choice_valuation_candidate_power_product. ((((exists ff_h_bpcifpe_last_choice_valuation_candidate_power_product_start. ff_h_bpcifpe_last_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_last_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_last_choice_valuation_candidate_power_product_start. ff_u_bpcifpe_last_choice_valuation_candidate_power_product = ff_q_bpcifpe_last_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcifpe_last_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_last_choice_valuation_candidate_power_product_terminal. ff_h_bpcifpe_last_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcifpe_last_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcifpe_last_choice_valuation)) * ff_v_bpcifpe_last_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_last_choice_valuation_candidate_power_product_terminal. ff_u_bpcifpe_last_choice_valuation_candidate_power_product = ff_q_bpcifpe_last_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcifpe_last_choice_valuation)) * ff_v_bpcifpe_last_choice_valuation_candidate_power_product) + (bpr_power_value_bpcifpe_last_choice_valuation_candidate))) /\ forall ff_i_bpcifpe_last_choice_valuation_candidate_power_product. (exists ff_lt_bpcifpe_last_choice_valuation_candidate_power_product_bound. ff_lt_bpcifpe_last_choice_valuation_candidate_power_product_bound + S ff_i_bpcifpe_last_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcifpe_last_choice_valuation) -> exists ff_p_bpcifpe_last_choice_valuation_candidate_power_product ff_r_bpcifpe_last_choice_valuation_candidate_power_product ff_s_bpcifpe_last_choice_valuation_candidate_power_product. ((((exists ff_h_bpcifpe_last_choice_valuation_candidate_power_product_factor. ff_h_bpcifpe_last_choice_valuation_candidate_power_product_factor + S (ff_p_bpcifpe_last_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcifpe_last_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcifpe_last_choice_valuation_candidate_power)) /\ exists ff_q_bpcifpe_last_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcifpe_last_choice_valuation_candidate_power = ff_q_bpcifpe_last_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcifpe_last_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcifpe_last_choice_valuation_candidate_power) + (ff_p_bpcifpe_last_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcifpe_last_choice_valuation_candidate_power_product_partial. ff_h_bpcifpe_last_choice_valuation_candidate_power_product_partial + S (ff_r_bpcifpe_last_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcifpe_last_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_last_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_last_choice_valuation_candidate_power_product_partial. ff_u_bpcifpe_last_choice_valuation_candidate_power_product = ff_q_bpcifpe_last_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcifpe_last_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_last_choice_valuation_candidate_power_product) + (ff_r_bpcifpe_last_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcifpe_last_choice_valuation_candidate_power_product_successor. ff_h_bpcifpe_last_choice_valuation_candidate_power_product_successor + S (ff_s_bpcifpe_last_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcifpe_last_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_last_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_last_choice_valuation_candidate_power_product_successor. ff_u_bpcifpe_last_choice_valuation_candidate_power_product = ff_q_bpcifpe_last_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcifpe_last_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_last_choice_valuation_candidate_power_product) + (ff_s_bpcifpe_last_choice_valuation_candidate_power_product))) /\ ff_s_bpcifpe_last_choice_valuation_candidate_power_product = ff_r_bpcifpe_last_choice_valuation_candidate_power_product * ff_p_bpcifpe_last_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcifpe_last_choice_valuation_candidate_divides. n = (bpr_power_value_bpcifpe_last_choice_valuation_candidate) * bpr_divides_quotient_bpcifpe_last_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcifpe_last_choice_valuation_candidate_below. bpr_le_gap_bpcifpe_last_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcifpe_last_choice_valuation) = (bpr_choice_exponent_bpcifpe_last_choice))) /\ (exists bpr_power_code_bpcifpe_last_choice_power bpr_power_scale_bpcifpe_last_choice_power. ((forall bpr_power_index_bpcifpe_last_choice_power. (exists bpr_gap_bpcifpe_last_choice_power_repeat_bound. bpr_gap_bpcifpe_last_choice_power_repeat_bound + S (bpr_power_index_bpcifpe_last_choice_power) = bpr_choice_exponent_bpcifpe_last_choice) -> (((exists bpr_height_bpcifpe_last_choice_power_repeat_entry. bpr_height_bpcifpe_last_choice_power_repeat_entry + S (S (a + l)) = S ((S (bpr_power_index_bpcifpe_last_choice_power)) * bpr_power_scale_bpcifpe_last_choice_power)) /\ exists bpr_quotient_bpcifpe_last_choice_power_repeat_entry. bpr_power_code_bpcifpe_last_choice_power = bpr_quotient_bpcifpe_last_choice_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_last_choice_power)) * bpr_power_scale_bpcifpe_last_choice_power) + (S (a + l))))) /\ (exists ff_u_bpcifpe_last_choice_power_product ff_v_bpcifpe_last_choice_power_product. ((((exists ff_h_bpcifpe_last_choice_power_product_start. ff_h_bpcifpe_last_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_last_choice_power_product)) /\ exists ff_q_bpcifpe_last_choice_power_product_start. ff_u_bpcifpe_last_choice_power_product = ff_q_bpcifpe_last_choice_power_product_start * S ((S (0)) * ff_v_bpcifpe_last_choice_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_last_choice_power_product_terminal. ff_h_bpcifpe_last_choice_power_product_terminal + S (x) = S ((S (bpr_choice_exponent_bpcifpe_last_choice)) * ff_v_bpcifpe_last_choice_power_product)) /\ exists ff_q_bpcifpe_last_choice_power_product_terminal. ff_u_bpcifpe_last_choice_power_product = ff_q_bpcifpe_last_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcifpe_last_choice)) * ff_v_bpcifpe_last_choice_power_product) + (x))) /\ forall ff_i_bpcifpe_last_choice_power_product. (exists ff_lt_bpcifpe_last_choice_power_product_bound. ff_lt_bpcifpe_last_choice_power_product_bound + S ff_i_bpcifpe_last_choice_power_product = bpr_choice_exponent_bpcifpe_last_choice) -> exists ff_p_bpcifpe_last_choice_power_product ff_r_bpcifpe_last_choice_power_product ff_s_bpcifpe_last_choice_power_product. ((((exists ff_h_bpcifpe_last_choice_power_product_factor. ff_h_bpcifpe_last_choice_power_product_factor + S (ff_p_bpcifpe_last_choice_power_product) = S ((S (ff_i_bpcifpe_last_choice_power_product)) * bpr_power_scale_bpcifpe_last_choice_power)) /\ exists ff_q_bpcifpe_last_choice_power_product_factor. bpr_power_code_bpcifpe_last_choice_power = ff_q_bpcifpe_last_choice_power_product_factor * S ((S (ff_i_bpcifpe_last_choice_power_product)) * bpr_power_scale_bpcifpe_last_choice_power) + (ff_p_bpcifpe_last_choice_power_product))) /\ ((((exists ff_h_bpcifpe_last_choice_power_product_partial. ff_h_bpcifpe_last_choice_power_product_partial + S (ff_r_bpcifpe_last_choice_power_product) = S ((S (ff_i_bpcifpe_last_choice_power_product)) * ff_v_bpcifpe_last_choice_power_product)) /\ exists ff_q_bpcifpe_last_choice_power_product_partial. ff_u_bpcifpe_last_choice_power_product = ff_q_bpcifpe_last_choice_power_product_partial * S ((S (ff_i_bpcifpe_last_choice_power_product)) * ff_v_bpcifpe_last_choice_power_product) + (ff_r_bpcifpe_last_choice_power_product))) /\ ((((exists ff_h_bpcifpe_last_choice_power_product_successor. ff_h_bpcifpe_last_choice_power_product_successor + S (ff_s_bpcifpe_last_choice_power_product) = S ((S (S ff_i_bpcifpe_last_choice_power_product)) * ff_v_bpcifpe_last_choice_power_product)) /\ exists ff_q_bpcifpe_last_choice_power_product_successor. ff_u_bpcifpe_last_choice_power_product = ff_q_bpcifpe_last_choice_power_product_successor * S ((S (S ff_i_bpcifpe_last_choice_power_product)) * ff_v_bpcifpe_last_choice_power_product) + (ff_s_bpcifpe_last_choice_power_product))) /\ ff_s_bpcifpe_last_choice_power_product = ff_r_bpcifpe_last_choice_power_product * ff_p_bpcifpe_last_choice_power_product)))))))))) \/ (~((~(S (a + l) = 1) /\ forall bpr_left_bpcifpe_last_choice_prime bpr_right_bpcifpe_last_choice_prime. S (a + l) = bpr_left_bpcifpe_last_choice_prime * bpr_right_bpcifpe_last_choice_prime -> bpr_left_bpcifpe_last_choice_prime = 1 \/ bpr_right_bpcifpe_last_choice_prime = 1)) /\ x = 1))) - 0008
specialize prime_contribution_choice_exists n - 0009
specialize prime_contribution_choice_exists (a + l) - 0010
exact prime_contribution_choice_exists - 0011
cases hchoice - 0012
have hext : ∃ d. ∃ e. BetaAt(d,e,l,x) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(b,c,y,z) → BetaAt(d,e,y,z))Exact native replay line
have hext : exists d e. ((((exists bpr_height_bpcifpe_append. bpr_height_bpcifpe_append + S (x) = S ((S (l)) * e)) /\ exists bpr_quotient_bpcifpe_append. d = bpr_quotient_bpcifpe_append * S ((S (l)) * e) + (x))) /\ forall i p. (exists bpr_gap_bpcifpe_old_bound. bpr_gap_bpcifpe_old_bound + S (i) = l) -> (((exists bpr_height_bpcifpe_old. bpr_height_bpcifpe_old + S (p) = S ((S (i)) * c)) /\ exists bpr_quotient_bpcifpe_old. b = bpr_quotient_bpcifpe_old * S ((S (i)) * c) + (p))) -> (((exists bpr_height_bpcifpe_new. bpr_height_bpcifpe_new + S (p) = S ((S (i)) * e)) /\ exists bpr_quotient_bpcifpe_new. d = bpr_quotient_bpcifpe_new * S ((S (i)) * e) + (p)))) - 0013
apply beta_prefix_extend - 0014
cases hext - 0015
cases hext_witness - 0016
cases hext_witness_witness - 0017
exists x1 - 0018
exists x2 - 0019
intro i - 0020
intro hi - 0021
have hsplit : i = l ∨ Lt(i,l)Exact native replay line
have hsplit : i = l \/ exists gap. gap + S i = l - 0022
apply finite_lt_succ_eq_or_lt - 0023
exact hi - 0024
cases hsplit - 0025
rewrite hsplit_left - 0026
rewrite hsplit_left - 0027
rewrite hsplit_left - 0028
rewrite hsplit_left - 0029
rewrite hsplit_left - 0030
rewrite hsplit_left - 0031
rewrite hsplit_left - 0032
rewrite hsplit_left - 0033
rewrite hsplit_left - 0034
rewrite hsplit_left - 0035
rewrite hsplit_left - 0036
rewrite hsplit_left - 0037
exists x - 0038
split - 0039
exact hext_witness_witness_left - 0040
exact hchoice_witness - 0041
have hold : ∃ p. BetaAt(b,c,i,p) ∧ (Prime(S (a + i)) ∧ (∃ x. PowerValuation(S (a + i),n,x) ∧ Pow(S (a + i),x,p)) ∨ ¬Prime(S (a + i)) ∧ p = 1)Exact native replay line
have hold : exists p. ((((exists bpr_height_bpcifpe_hold_decoded. bpr_height_bpcifpe_hold_decoded + S (p) = S ((S (i)) * c)) /\ exists bpr_quotient_bpcifpe_hold_decoded. b = bpr_quotient_bpcifpe_hold_decoded * S ((S (i)) * c) + (p))) /\ (((((~(S (a + i) = 1) /\ forall bpr_left_bpcifpe_hold_choice_prime bpr_right_bpcifpe_hold_choice_prime. S (a + i) = bpr_left_bpcifpe_hold_choice_prime * bpr_right_bpcifpe_hold_choice_prime -> bpr_left_bpcifpe_hold_choice_prime = 1 \/ bpr_right_bpcifpe_hold_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcifpe_hold_choice. ((((exists bpr_le_gap_bpcifpe_hold_choice_valuation_selected_bound. bpr_le_gap_bpcifpe_hold_choice_valuation_selected_bound + (bpr_choice_exponent_bpcifpe_hold_choice) = (n)) /\ (exists bpr_power_value_bpcifpe_hold_choice_valuation_selected. ((exists bpr_power_code_bpcifpe_hold_choice_valuation_selected_power bpr_power_scale_bpcifpe_hold_choice_valuation_selected_power. ((forall bpr_power_index_bpcifpe_hold_choice_valuation_selected_power. (exists bpr_gap_bpcifpe_hold_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcifpe_hold_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcifpe_hold_choice_valuation_selected_power) = bpr_choice_exponent_bpcifpe_hold_choice) -> (((exists bpr_height_bpcifpe_hold_choice_valuation_selected_power_repeat_entry. bpr_height_bpcifpe_hold_choice_valuation_selected_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcifpe_hold_choice_valuation_selected_power)) * bpr_power_scale_bpcifpe_hold_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcifpe_hold_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcifpe_hold_choice_valuation_selected_power = bpr_quotient_bpcifpe_hold_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_hold_choice_valuation_selected_power)) * bpr_power_scale_bpcifpe_hold_choice_valuation_selected_power) + (S (a + i))))) /\ (exists ff_u_bpcifpe_hold_choice_valuation_selected_power_product ff_v_bpcifpe_hold_choice_valuation_selected_power_product. ((((exists ff_h_bpcifpe_hold_choice_valuation_selected_power_product_start. ff_h_bpcifpe_hold_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_hold_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_hold_choice_valuation_selected_power_product_start. ff_u_bpcifpe_hold_choice_valuation_selected_power_product = ff_q_bpcifpe_hold_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcifpe_hold_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_hold_choice_valuation_selected_power_product_terminal. ff_h_bpcifpe_hold_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcifpe_hold_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcifpe_hold_choice)) * ff_v_bpcifpe_hold_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_hold_choice_valuation_selected_power_product_terminal. ff_u_bpcifpe_hold_choice_valuation_selected_power_product = ff_q_bpcifpe_hold_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcifpe_hold_choice)) * ff_v_bpcifpe_hold_choice_valuation_selected_power_product) + (bpr_power_value_bpcifpe_hold_choice_valuation_selected))) /\ forall ff_i_bpcifpe_hold_choice_valuation_selected_power_product. (exists ff_lt_bpcifpe_hold_choice_valuation_selected_power_product_bound. ff_lt_bpcifpe_hold_choice_valuation_selected_power_product_bound + S ff_i_bpcifpe_hold_choice_valuation_selected_power_product = bpr_choice_exponent_bpcifpe_hold_choice) -> exists ff_p_bpcifpe_hold_choice_valuation_selected_power_product ff_r_bpcifpe_hold_choice_valuation_selected_power_product ff_s_bpcifpe_hold_choice_valuation_selected_power_product. ((((exists ff_h_bpcifpe_hold_choice_valuation_selected_power_product_factor. ff_h_bpcifpe_hold_choice_valuation_selected_power_product_factor + S (ff_p_bpcifpe_hold_choice_valuation_selected_power_product) = S ((S (ff_i_bpcifpe_hold_choice_valuation_selected_power_product)) * bpr_power_scale_bpcifpe_hold_choice_valuation_selected_power)) /\ exists ff_q_bpcifpe_hold_choice_valuation_selected_power_product_factor. bpr_power_code_bpcifpe_hold_choice_valuation_selected_power = ff_q_bpcifpe_hold_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcifpe_hold_choice_valuation_selected_power_product)) * bpr_power_scale_bpcifpe_hold_choice_valuation_selected_power) + (ff_p_bpcifpe_hold_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcifpe_hold_choice_valuation_selected_power_product_partial. ff_h_bpcifpe_hold_choice_valuation_selected_power_product_partial + S (ff_r_bpcifpe_hold_choice_valuation_selected_power_product) = S ((S (ff_i_bpcifpe_hold_choice_valuation_selected_power_product)) * ff_v_bpcifpe_hold_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_hold_choice_valuation_selected_power_product_partial. ff_u_bpcifpe_hold_choice_valuation_selected_power_product = ff_q_bpcifpe_hold_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcifpe_hold_choice_valuation_selected_power_product)) * ff_v_bpcifpe_hold_choice_valuation_selected_power_product) + (ff_r_bpcifpe_hold_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcifpe_hold_choice_valuation_selected_power_product_successor. ff_h_bpcifpe_hold_choice_valuation_selected_power_product_successor + S (ff_s_bpcifpe_hold_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcifpe_hold_choice_valuation_selected_power_product)) * ff_v_bpcifpe_hold_choice_valuation_selected_power_product)) /\ exists ff_q_bpcifpe_hold_choice_valuation_selected_power_product_successor. ff_u_bpcifpe_hold_choice_valuation_selected_power_product = ff_q_bpcifpe_hold_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcifpe_hold_choice_valuation_selected_power_product)) * ff_v_bpcifpe_hold_choice_valuation_selected_power_product) + (ff_s_bpcifpe_hold_choice_valuation_selected_power_product))) /\ ff_s_bpcifpe_hold_choice_valuation_selected_power_product = ff_r_bpcifpe_hold_choice_valuation_selected_power_product * ff_p_bpcifpe_hold_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcifpe_hold_choice_valuation_selected_divides. n = (bpr_power_value_bpcifpe_hold_choice_valuation_selected) * bpr_divides_quotient_bpcifpe_hold_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcifpe_hold_choice_valuation. (exists bpr_le_gap_bpcifpe_hold_choice_valuation_candidate_bound. bpr_le_gap_bpcifpe_hold_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcifpe_hold_choice_valuation) = (n)) -> (exists bpr_power_value_bpcifpe_hold_choice_valuation_candidate. ((exists bpr_power_code_bpcifpe_hold_choice_valuation_candidate_power bpr_power_scale_bpcifpe_hold_choice_valuation_candidate_power. ((forall bpr_power_index_bpcifpe_hold_choice_valuation_candidate_power. (exists bpr_gap_bpcifpe_hold_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcifpe_hold_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcifpe_hold_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcifpe_hold_choice_valuation) -> (((exists bpr_height_bpcifpe_hold_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcifpe_hold_choice_valuation_candidate_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcifpe_hold_choice_valuation_candidate_power)) * bpr_power_scale_bpcifpe_hold_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcifpe_hold_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcifpe_hold_choice_valuation_candidate_power = bpr_quotient_bpcifpe_hold_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_hold_choice_valuation_candidate_power)) * bpr_power_scale_bpcifpe_hold_choice_valuation_candidate_power) + (S (a + i))))) /\ (exists ff_u_bpcifpe_hold_choice_valuation_candidate_power_product ff_v_bpcifpe_hold_choice_valuation_candidate_power_product. ((((exists ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_start. ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_hold_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_start. ff_u_bpcifpe_hold_choice_valuation_candidate_power_product = ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcifpe_hold_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_terminal. ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcifpe_hold_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcifpe_hold_choice_valuation)) * ff_v_bpcifpe_hold_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_terminal. ff_u_bpcifpe_hold_choice_valuation_candidate_power_product = ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcifpe_hold_choice_valuation)) * ff_v_bpcifpe_hold_choice_valuation_candidate_power_product) + (bpr_power_value_bpcifpe_hold_choice_valuation_candidate))) /\ forall ff_i_bpcifpe_hold_choice_valuation_candidate_power_product. (exists ff_lt_bpcifpe_hold_choice_valuation_candidate_power_product_bound. ff_lt_bpcifpe_hold_choice_valuation_candidate_power_product_bound + S ff_i_bpcifpe_hold_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcifpe_hold_choice_valuation) -> exists ff_p_bpcifpe_hold_choice_valuation_candidate_power_product ff_r_bpcifpe_hold_choice_valuation_candidate_power_product ff_s_bpcifpe_hold_choice_valuation_candidate_power_product. ((((exists ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_factor. ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_factor + S (ff_p_bpcifpe_hold_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcifpe_hold_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcifpe_hold_choice_valuation_candidate_power)) /\ exists ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcifpe_hold_choice_valuation_candidate_power = ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcifpe_hold_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcifpe_hold_choice_valuation_candidate_power) + (ff_p_bpcifpe_hold_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_partial. ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_partial + S (ff_r_bpcifpe_hold_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcifpe_hold_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_hold_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_partial. ff_u_bpcifpe_hold_choice_valuation_candidate_power_product = ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcifpe_hold_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_hold_choice_valuation_candidate_power_product) + (ff_r_bpcifpe_hold_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_successor. ff_h_bpcifpe_hold_choice_valuation_candidate_power_product_successor + S (ff_s_bpcifpe_hold_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcifpe_hold_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_hold_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_successor. ff_u_bpcifpe_hold_choice_valuation_candidate_power_product = ff_q_bpcifpe_hold_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcifpe_hold_choice_valuation_candidate_power_product)) * ff_v_bpcifpe_hold_choice_valuation_candidate_power_product) + (ff_s_bpcifpe_hold_choice_valuation_candidate_power_product))) /\ ff_s_bpcifpe_hold_choice_valuation_candidate_power_product = ff_r_bpcifpe_hold_choice_valuation_candidate_power_product * ff_p_bpcifpe_hold_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcifpe_hold_choice_valuation_candidate_divides. n = (bpr_power_value_bpcifpe_hold_choice_valuation_candidate) * bpr_divides_quotient_bpcifpe_hold_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcifpe_hold_choice_valuation_candidate_below. bpr_le_gap_bpcifpe_hold_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcifpe_hold_choice_valuation) = (bpr_choice_exponent_bpcifpe_hold_choice))) /\ (exists bpr_power_code_bpcifpe_hold_choice_power bpr_power_scale_bpcifpe_hold_choice_power. ((forall bpr_power_index_bpcifpe_hold_choice_power. (exists bpr_gap_bpcifpe_hold_choice_power_repeat_bound. bpr_gap_bpcifpe_hold_choice_power_repeat_bound + S (bpr_power_index_bpcifpe_hold_choice_power) = bpr_choice_exponent_bpcifpe_hold_choice) -> (((exists bpr_height_bpcifpe_hold_choice_power_repeat_entry. bpr_height_bpcifpe_hold_choice_power_repeat_entry + S (S (a + i)) = S ((S (bpr_power_index_bpcifpe_hold_choice_power)) * bpr_power_scale_bpcifpe_hold_choice_power)) /\ exists bpr_quotient_bpcifpe_hold_choice_power_repeat_entry. bpr_power_code_bpcifpe_hold_choice_power = bpr_quotient_bpcifpe_hold_choice_power_repeat_entry * S ((S (bpr_power_index_bpcifpe_hold_choice_power)) * bpr_power_scale_bpcifpe_hold_choice_power) + (S (a + i))))) /\ (exists ff_u_bpcifpe_hold_choice_power_product ff_v_bpcifpe_hold_choice_power_product. ((((exists ff_h_bpcifpe_hold_choice_power_product_start. ff_h_bpcifpe_hold_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcifpe_hold_choice_power_product)) /\ exists ff_q_bpcifpe_hold_choice_power_product_start. ff_u_bpcifpe_hold_choice_power_product = ff_q_bpcifpe_hold_choice_power_product_start * S ((S (0)) * ff_v_bpcifpe_hold_choice_power_product) + (1))) /\ ((((exists ff_h_bpcifpe_hold_choice_power_product_terminal. ff_h_bpcifpe_hold_choice_power_product_terminal + S (p) = S ((S (bpr_choice_exponent_bpcifpe_hold_choice)) * ff_v_bpcifpe_hold_choice_power_product)) /\ exists ff_q_bpcifpe_hold_choice_power_product_terminal. ff_u_bpcifpe_hold_choice_power_product = ff_q_bpcifpe_hold_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcifpe_hold_choice)) * ff_v_bpcifpe_hold_choice_power_product) + (p))) /\ forall ff_i_bpcifpe_hold_choice_power_product. (exists ff_lt_bpcifpe_hold_choice_power_product_bound. ff_lt_bpcifpe_hold_choice_power_product_bound + S ff_i_bpcifpe_hold_choice_power_product = bpr_choice_exponent_bpcifpe_hold_choice) -> exists ff_p_bpcifpe_hold_choice_power_product ff_r_bpcifpe_hold_choice_power_product ff_s_bpcifpe_hold_choice_power_product. ((((exists ff_h_bpcifpe_hold_choice_power_product_factor. ff_h_bpcifpe_hold_choice_power_product_factor + S (ff_p_bpcifpe_hold_choice_power_product) = S ((S (ff_i_bpcifpe_hold_choice_power_product)) * bpr_power_scale_bpcifpe_hold_choice_power)) /\ exists ff_q_bpcifpe_hold_choice_power_product_factor. bpr_power_code_bpcifpe_hold_choice_power = ff_q_bpcifpe_hold_choice_power_product_factor * S ((S (ff_i_bpcifpe_hold_choice_power_product)) * bpr_power_scale_bpcifpe_hold_choice_power) + (ff_p_bpcifpe_hold_choice_power_product))) /\ ((((exists ff_h_bpcifpe_hold_choice_power_product_partial. ff_h_bpcifpe_hold_choice_power_product_partial + S (ff_r_bpcifpe_hold_choice_power_product) = S ((S (ff_i_bpcifpe_hold_choice_power_product)) * ff_v_bpcifpe_hold_choice_power_product)) /\ exists ff_q_bpcifpe_hold_choice_power_product_partial. ff_u_bpcifpe_hold_choice_power_product = ff_q_bpcifpe_hold_choice_power_product_partial * S ((S (ff_i_bpcifpe_hold_choice_power_product)) * ff_v_bpcifpe_hold_choice_power_product) + (ff_r_bpcifpe_hold_choice_power_product))) /\ ((((exists ff_h_bpcifpe_hold_choice_power_product_successor. ff_h_bpcifpe_hold_choice_power_product_successor + S (ff_s_bpcifpe_hold_choice_power_product) = S ((S (S ff_i_bpcifpe_hold_choice_power_product)) * ff_v_bpcifpe_hold_choice_power_product)) /\ exists ff_q_bpcifpe_hold_choice_power_product_successor. ff_u_bpcifpe_hold_choice_power_product = ff_q_bpcifpe_hold_choice_power_product_successor * S ((S (S ff_i_bpcifpe_hold_choice_power_product)) * ff_v_bpcifpe_hold_choice_power_product) + (ff_s_bpcifpe_hold_choice_power_product))) /\ ff_s_bpcifpe_hold_choice_power_product = ff_r_bpcifpe_hold_choice_power_product * ff_p_bpcifpe_hold_choice_power_product)))))))))) \/ (~((~(S (a + i) = 1) /\ forall bpr_left_bpcifpe_hold_choice_prime bpr_right_bpcifpe_hold_choice_prime. S (a + i) = bpr_left_bpcifpe_hold_choice_prime * bpr_right_bpcifpe_hold_choice_prime -> bpr_left_bpcifpe_hold_choice_prime = 1 \/ bpr_right_bpcifpe_hold_choice_prime = 1)) /\ p = 1)))) - 0042
apply hprefix - 0043
exact hsplit_right - 0044
cases hold - 0045
cases hold_witness - 0046
exists x3 - 0047
split - 0048
apply hext_witness_witness_right - 0049
exact hsplit_right - 0050
exact hold_witness_left - 0051
exact hold_witness_right