Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ n. ∀ a. ∀ l. ∀ z. (∃ x. ∃ y. (∀ m. Lt(m,a + l) → ∃ k. BetaAt(x,y,m,k) ∧ (Prime(S m) ∧ (∃ i. PowerValuation(S m,n,i) ∧ Pow(S m,i,k)) ∨ ¬Prime(S m) ∧ k = 1)) ∧ Product(x,y,a + l,z)) → ∃ x. ∃ y. (∃ m. ∃ k. (∀ i. Lt(i,a) → ∃ j. BetaAt(m,k,i,j) ∧ (Prime(S i) ∧ (∃ u. PowerValuation(S i,n,u) ∧ Pow(S i,u,j)) ∨ ¬Prime(S i) ∧ j = 1)) ∧ Product(m,k,a,x)) ∧ ((∃ m. ∃ k. (∀ i. Lt(i,l) → ∃ j. BetaAt(m,k,i,j) ∧ (Prime(S (a + i)) ∧ (∃ u. PowerValuation(S (a + i),n,u) ∧ Pow(S (a + i),u,j)) ∨ ¬Prime(S (a + i)) ∧ j = 1)) ∧ Product(m,k,l,y)) ∧ z = x · y)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
21 occurrences
In local proof propositions
17 occurrences
Exact expanded native-PA statement
forall n a l z. (exists bpr_product_code_bpcpis_source bpr_product_scale_bpcpis_source. ((forall bpr_prefix_index_bpcpis_source_prefix. (exists bpr_gap_bpcpis_source_prefix_bound. bpr_gap_bpcpis_source_prefix_bound + S (bpr_prefix_index_bpcpis_source_prefix) = a + l) -> exists bpr_prefix_value_bpcpis_source_prefix. ((((exists bpr_height_bpcpis_source_prefix_decoded. bpr_height_bpcpis_source_prefix_decoded + S (bpr_prefix_value_bpcpis_source_prefix) = S ((S (bpr_prefix_index_bpcpis_source_prefix)) * bpr_product_scale_bpcpis_source)) /\ exists bpr_quotient_bpcpis_source_prefix_decoded. bpr_product_code_bpcpis_source = bpr_quotient_bpcpis_source_prefix_decoded * S ((S (bpr_prefix_index_bpcpis_source_prefix)) * bpr_product_scale_bpcpis_source) + (bpr_prefix_value_bpcpis_source_prefix))) /\ (((((~(S (bpr_prefix_index_bpcpis_source_prefix) = 1) /\ forall bpr_left_bpcpis_source_prefix_choice_prime bpr_right_bpcpis_source_prefix_choice_prime. S (bpr_prefix_index_bpcpis_source_prefix) = bpr_left_bpcpis_source_prefix_choice_prime * bpr_right_bpcpis_source_prefix_choice_prime -> bpr_left_bpcpis_source_prefix_choice_prime = 1 \/ bpr_right_bpcpis_source_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpis_source_prefix_choice. ((((exists bpr_le_gap_bpcpis_source_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcpis_source_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpis_source_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcpis_source_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcpis_source_prefix_choice_valuation_selected_power bpr_power_scale_bpcpis_source_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcpis_source_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcpis_source_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpis_source_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpis_source_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcpis_source_prefix_choice) -> (((exists bpr_height_bpcpis_source_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpis_source_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_source_prefix)) = S ((S (bpr_power_index_bpcpis_source_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_source_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpis_source_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpis_source_prefix_choice_valuation_selected_power = bpr_quotient_bpcpis_source_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpis_source_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_source_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpis_source_prefix))))) /\ (exists ff_u_bpcpis_source_prefix_choice_valuation_selected_power_product ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_start. ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_start. ff_u_bpcpis_source_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpis_source_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpis_source_prefix_choice)) * ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcpis_source_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_source_prefix_choice)) * ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcpis_source_prefix_choice_valuation_selected))) /\ forall ff_i_bpcpis_source_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcpis_source_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcpis_source_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcpis_source_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpis_source_prefix_choice) -> exists ff_p_bpcpis_source_prefix_choice_valuation_selected_power_product ff_r_bpcpis_source_prefix_choice_valuation_selected_power_product ff_s_bpcpis_source_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcpis_source_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_source_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_source_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpis_source_prefix_choice_valuation_selected_power = ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpis_source_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_source_prefix_choice_valuation_selected_power) + (ff_p_bpcpis_source_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcpis_source_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_source_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcpis_source_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpis_source_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product) + (ff_r_bpcpis_source_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcpis_source_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcpis_source_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpis_source_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcpis_source_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_source_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpis_source_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_source_prefix_choice_valuation_selected_power_product) + (ff_s_bpcpis_source_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcpis_source_prefix_choice_valuation_selected_power_product = ff_r_bpcpis_source_prefix_choice_valuation_selected_power_product * ff_p_bpcpis_source_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_source_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcpis_source_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcpis_source_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpis_source_prefix_choice_valuation. (exists bpr_le_gap_bpcpis_source_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcpis_source_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpis_source_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpis_source_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcpis_source_prefix_choice_valuation_candidate_power bpr_power_scale_bpcpis_source_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpis_source_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcpis_source_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpis_source_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpis_source_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpis_source_prefix_choice_valuation) -> (((exists bpr_height_bpcpis_source_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpis_source_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_source_prefix)) = S ((S (bpr_power_index_bpcpis_source_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_source_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpis_source_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpis_source_prefix_choice_valuation_candidate_power = bpr_quotient_bpcpis_source_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpis_source_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_source_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpis_source_prefix))))) /\ (exists ff_u_bpcpis_source_prefix_choice_valuation_candidate_power_product ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcpis_source_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpis_source_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpis_source_prefix_choice_valuation)) * ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcpis_source_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpis_source_prefix_choice_valuation)) * ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpis_source_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcpis_source_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcpis_source_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcpis_source_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcpis_source_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpis_source_prefix_choice_valuation) -> exists ff_p_bpcpis_source_prefix_choice_valuation_candidate_power_product ff_r_bpcpis_source_prefix_choice_valuation_candidate_power_product ff_s_bpcpis_source_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpis_source_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_source_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_source_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpis_source_prefix_choice_valuation_candidate_power = ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpis_source_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_source_prefix_choice_valuation_candidate_power) + (ff_p_bpcpis_source_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpis_source_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_source_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcpis_source_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpis_source_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcpis_source_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcpis_source_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpis_source_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpis_source_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcpis_source_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_source_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpis_source_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_source_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcpis_source_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcpis_source_prefix_choice_valuation_candidate_power_product = ff_r_bpcpis_source_prefix_choice_valuation_candidate_power_product * ff_p_bpcpis_source_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_source_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpis_source_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcpis_source_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpis_source_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcpis_source_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpis_source_prefix_choice_valuation) = (bpr_choice_exponent_bpcpis_source_prefix_choice))) /\ (exists bpr_power_code_bpcpis_source_prefix_choice_power bpr_power_scale_bpcpis_source_prefix_choice_power. ((forall bpr_power_index_bpcpis_source_prefix_choice_power. (exists bpr_gap_bpcpis_source_prefix_choice_power_repeat_bound. bpr_gap_bpcpis_source_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcpis_source_prefix_choice_power) = bpr_choice_exponent_bpcpis_source_prefix_choice) -> (((exists bpr_height_bpcpis_source_prefix_choice_power_repeat_entry. bpr_height_bpcpis_source_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_source_prefix)) = S ((S (bpr_power_index_bpcpis_source_prefix_choice_power)) * bpr_power_scale_bpcpis_source_prefix_choice_power)) /\ exists bpr_quotient_bpcpis_source_prefix_choice_power_repeat_entry. bpr_power_code_bpcpis_source_prefix_choice_power = bpr_quotient_bpcpis_source_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpis_source_prefix_choice_power)) * bpr_power_scale_bpcpis_source_prefix_choice_power) + (S (bpr_prefix_index_bpcpis_source_prefix))))) /\ (exists ff_u_bpcpis_source_prefix_choice_power_product ff_v_bpcpis_source_prefix_choice_power_product. ((((exists ff_h_bpcpis_source_prefix_choice_power_product_start. ff_h_bpcpis_source_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_source_prefix_choice_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_power_product_start. ff_u_bpcpis_source_prefix_choice_power_product = ff_q_bpcpis_source_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcpis_source_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_power_product_terminal. ff_h_bpcpis_source_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpcpis_source_prefix) = S ((S (bpr_choice_exponent_bpcpis_source_prefix_choice)) * ff_v_bpcpis_source_prefix_choice_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_power_product_terminal. ff_u_bpcpis_source_prefix_choice_power_product = ff_q_bpcpis_source_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_source_prefix_choice)) * ff_v_bpcpis_source_prefix_choice_power_product) + (bpr_prefix_value_bpcpis_source_prefix))) /\ forall ff_i_bpcpis_source_prefix_choice_power_product. (exists ff_lt_bpcpis_source_prefix_choice_power_product_bound. ff_lt_bpcpis_source_prefix_choice_power_product_bound + S ff_i_bpcpis_source_prefix_choice_power_product = bpr_choice_exponent_bpcpis_source_prefix_choice) -> exists ff_p_bpcpis_source_prefix_choice_power_product ff_r_bpcpis_source_prefix_choice_power_product ff_s_bpcpis_source_prefix_choice_power_product. ((((exists ff_h_bpcpis_source_prefix_choice_power_product_factor. ff_h_bpcpis_source_prefix_choice_power_product_factor + S (ff_p_bpcpis_source_prefix_choice_power_product) = S ((S (ff_i_bpcpis_source_prefix_choice_power_product)) * bpr_power_scale_bpcpis_source_prefix_choice_power)) /\ exists ff_q_bpcpis_source_prefix_choice_power_product_factor. bpr_power_code_bpcpis_source_prefix_choice_power = ff_q_bpcpis_source_prefix_choice_power_product_factor * S ((S (ff_i_bpcpis_source_prefix_choice_power_product)) * bpr_power_scale_bpcpis_source_prefix_choice_power) + (ff_p_bpcpis_source_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_power_product_partial. ff_h_bpcpis_source_prefix_choice_power_product_partial + S (ff_r_bpcpis_source_prefix_choice_power_product) = S ((S (ff_i_bpcpis_source_prefix_choice_power_product)) * ff_v_bpcpis_source_prefix_choice_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_power_product_partial. ff_u_bpcpis_source_prefix_choice_power_product = ff_q_bpcpis_source_prefix_choice_power_product_partial * S ((S (ff_i_bpcpis_source_prefix_choice_power_product)) * ff_v_bpcpis_source_prefix_choice_power_product) + (ff_r_bpcpis_source_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpis_source_prefix_choice_power_product_successor. ff_h_bpcpis_source_prefix_choice_power_product_successor + S (ff_s_bpcpis_source_prefix_choice_power_product) = S ((S (S ff_i_bpcpis_source_prefix_choice_power_product)) * ff_v_bpcpis_source_prefix_choice_power_product)) /\ exists ff_q_bpcpis_source_prefix_choice_power_product_successor. ff_u_bpcpis_source_prefix_choice_power_product = ff_q_bpcpis_source_prefix_choice_power_product_successor * S ((S (S ff_i_bpcpis_source_prefix_choice_power_product)) * ff_v_bpcpis_source_prefix_choice_power_product) + (ff_s_bpcpis_source_prefix_choice_power_product))) /\ ff_s_bpcpis_source_prefix_choice_power_product = ff_r_bpcpis_source_prefix_choice_power_product * ff_p_bpcpis_source_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpis_source_prefix) = 1) /\ forall bpr_left_bpcpis_source_prefix_choice_prime bpr_right_bpcpis_source_prefix_choice_prime. S (bpr_prefix_index_bpcpis_source_prefix) = bpr_left_bpcpis_source_prefix_choice_prime * bpr_right_bpcpis_source_prefix_choice_prime -> bpr_left_bpcpis_source_prefix_choice_prime = 1 \/ bpr_right_bpcpis_source_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpcpis_source_prefix = 1))))) /\ (exists ff_u_bpcpis_source_product ff_v_bpcpis_source_product. ((((exists ff_h_bpcpis_source_product_start. ff_h_bpcpis_source_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_source_product)) /\ exists ff_q_bpcpis_source_product_start. ff_u_bpcpis_source_product = ff_q_bpcpis_source_product_start * S ((S (0)) * ff_v_bpcpis_source_product) + (1))) /\ ((((exists ff_h_bpcpis_source_product_terminal. ff_h_bpcpis_source_product_terminal + S (z) = S ((S (a + l)) * ff_v_bpcpis_source_product)) /\ exists ff_q_bpcpis_source_product_terminal. ff_u_bpcpis_source_product = ff_q_bpcpis_source_product_terminal * S ((S (a + l)) * ff_v_bpcpis_source_product) + (z))) /\ forall ff_i_bpcpis_source_product. (exists ff_lt_bpcpis_source_product_bound. ff_lt_bpcpis_source_product_bound + S ff_i_bpcpis_source_product = a + l) -> exists ff_p_bpcpis_source_product ff_r_bpcpis_source_product ff_s_bpcpis_source_product. ((((exists ff_h_bpcpis_source_product_factor. ff_h_bpcpis_source_product_factor + S (ff_p_bpcpis_source_product) = S ((S (ff_i_bpcpis_source_product)) * bpr_product_scale_bpcpis_source)) /\ exists ff_q_bpcpis_source_product_factor. bpr_product_code_bpcpis_source = ff_q_bpcpis_source_product_factor * S ((S (ff_i_bpcpis_source_product)) * bpr_product_scale_bpcpis_source) + (ff_p_bpcpis_source_product))) /\ ((((exists ff_h_bpcpis_source_product_partial. ff_h_bpcpis_source_product_partial + S (ff_r_bpcpis_source_product) = S ((S (ff_i_bpcpis_source_product)) * ff_v_bpcpis_source_product)) /\ exists ff_q_bpcpis_source_product_partial. ff_u_bpcpis_source_product = ff_q_bpcpis_source_product_partial * S ((S (ff_i_bpcpis_source_product)) * ff_v_bpcpis_source_product) + (ff_r_bpcpis_source_product))) /\ ((((exists ff_h_bpcpis_source_product_successor. ff_h_bpcpis_source_product_successor + S (ff_s_bpcpis_source_product) = S ((S (S ff_i_bpcpis_source_product)) * ff_v_bpcpis_source_product)) /\ exists ff_q_bpcpis_source_product_successor. ff_u_bpcpis_source_product = ff_q_bpcpis_source_product_successor * S ((S (S ff_i_bpcpis_source_product)) * ff_v_bpcpis_source_product) + (ff_s_bpcpis_source_product))) /\ ff_s_bpcpis_source_product = ff_r_bpcpis_source_product * ff_p_bpcpis_source_product)))))))) -> (exists x y. (exists bpr_product_code_bpcpis_prefix bpr_product_scale_bpcpis_prefix. ((forall bpr_prefix_index_bpcpis_prefix_prefix. (exists bpr_gap_bpcpis_prefix_prefix_bound. bpr_gap_bpcpis_prefix_prefix_bound + S (bpr_prefix_index_bpcpis_prefix_prefix) = a) -> exists bpr_prefix_value_bpcpis_prefix_prefix. ((((exists bpr_height_bpcpis_prefix_prefix_decoded. bpr_height_bpcpis_prefix_prefix_decoded + S (bpr_prefix_value_bpcpis_prefix_prefix) = S ((S (bpr_prefix_index_bpcpis_prefix_prefix)) * bpr_product_scale_bpcpis_prefix)) /\ exists bpr_quotient_bpcpis_prefix_prefix_decoded. bpr_product_code_bpcpis_prefix = bpr_quotient_bpcpis_prefix_prefix_decoded * S ((S (bpr_prefix_index_bpcpis_prefix_prefix)) * bpr_product_scale_bpcpis_prefix) + (bpr_prefix_value_bpcpis_prefix_prefix))) /\ (((((~(S (bpr_prefix_index_bpcpis_prefix_prefix) = 1) /\ forall bpr_left_bpcpis_prefix_prefix_choice_prime bpr_right_bpcpis_prefix_prefix_choice_prime. S (bpr_prefix_index_bpcpis_prefix_prefix) = bpr_left_bpcpis_prefix_prefix_choice_prime * bpr_right_bpcpis_prefix_prefix_choice_prime -> bpr_left_bpcpis_prefix_prefix_choice_prime = 1 \/ bpr_right_bpcpis_prefix_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpis_prefix_prefix_choice. ((((exists bpr_le_gap_bpcpis_prefix_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcpis_prefix_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpis_prefix_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcpis_prefix_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcpis_prefix_prefix_choice_valuation_selected_power bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcpis_prefix_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcpis_prefix_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpis_prefix_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpis_prefix_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcpis_prefix_prefix_choice) -> (((exists bpr_height_bpcpis_prefix_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpis_prefix_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_prefix_prefix)) = S ((S (bpr_power_index_bpcpis_prefix_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpis_prefix_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpis_prefix_prefix_choice_valuation_selected_power = bpr_quotient_bpcpis_prefix_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpis_prefix_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpis_prefix_prefix))))) /\ (exists ff_u_bpcpis_prefix_prefix_choice_valuation_selected_power_product ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_start. ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_start. ff_u_bpcpis_prefix_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpis_prefix_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpis_prefix_prefix_choice)) * ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcpis_prefix_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_prefix_prefix_choice)) * ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcpis_prefix_prefix_choice_valuation_selected))) /\ forall ff_i_bpcpis_prefix_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcpis_prefix_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcpis_prefix_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcpis_prefix_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpis_prefix_prefix_choice) -> exists ff_p_bpcpis_prefix_prefix_choice_valuation_selected_power_product ff_r_bpcpis_prefix_prefix_choice_valuation_selected_power_product ff_s_bpcpis_prefix_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcpis_prefix_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpis_prefix_prefix_choice_valuation_selected_power = ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_selected_power) + (ff_p_bpcpis_prefix_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcpis_prefix_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcpis_prefix_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product) + (ff_r_bpcpis_prefix_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcpis_prefix_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcpis_prefix_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcpis_prefix_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_prefix_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpis_prefix_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_prefix_prefix_choice_valuation_selected_power_product) + (ff_s_bpcpis_prefix_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcpis_prefix_prefix_choice_valuation_selected_power_product = ff_r_bpcpis_prefix_prefix_choice_valuation_selected_power_product * ff_p_bpcpis_prefix_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_prefix_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcpis_prefix_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcpis_prefix_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpis_prefix_prefix_choice_valuation. (exists bpr_le_gap_bpcpis_prefix_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcpis_prefix_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpis_prefix_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpis_prefix_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcpis_prefix_prefix_choice_valuation_candidate_power bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpis_prefix_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcpis_prefix_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpis_prefix_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpis_prefix_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpis_prefix_prefix_choice_valuation) -> (((exists bpr_height_bpcpis_prefix_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpis_prefix_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_prefix_prefix)) = S ((S (bpr_power_index_bpcpis_prefix_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpis_prefix_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpis_prefix_prefix_choice_valuation_candidate_power = bpr_quotient_bpcpis_prefix_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpis_prefix_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpis_prefix_prefix))))) /\ (exists ff_u_bpcpis_prefix_prefix_choice_valuation_candidate_power_product ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcpis_prefix_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpis_prefix_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpis_prefix_prefix_choice_valuation)) * ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcpis_prefix_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpis_prefix_prefix_choice_valuation)) * ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpis_prefix_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcpis_prefix_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcpis_prefix_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpis_prefix_prefix_choice_valuation) -> exists ff_p_bpcpis_prefix_prefix_choice_valuation_candidate_power_product ff_r_bpcpis_prefix_prefix_choice_valuation_candidate_power_product ff_s_bpcpis_prefix_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpis_prefix_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpis_prefix_prefix_choice_valuation_candidate_power = ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_prefix_prefix_choice_valuation_candidate_power) + (ff_p_bpcpis_prefix_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpis_prefix_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcpis_prefix_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcpis_prefix_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpis_prefix_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcpis_prefix_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_prefix_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_prefix_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcpis_prefix_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcpis_prefix_prefix_choice_valuation_candidate_power_product = ff_r_bpcpis_prefix_prefix_choice_valuation_candidate_power_product * ff_p_bpcpis_prefix_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_prefix_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpis_prefix_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcpis_prefix_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpis_prefix_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcpis_prefix_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpis_prefix_prefix_choice_valuation) = (bpr_choice_exponent_bpcpis_prefix_prefix_choice))) /\ (exists bpr_power_code_bpcpis_prefix_prefix_choice_power bpr_power_scale_bpcpis_prefix_prefix_choice_power. ((forall bpr_power_index_bpcpis_prefix_prefix_choice_power. (exists bpr_gap_bpcpis_prefix_prefix_choice_power_repeat_bound. bpr_gap_bpcpis_prefix_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcpis_prefix_prefix_choice_power) = bpr_choice_exponent_bpcpis_prefix_prefix_choice) -> (((exists bpr_height_bpcpis_prefix_prefix_choice_power_repeat_entry. bpr_height_bpcpis_prefix_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_prefix_prefix)) = S ((S (bpr_power_index_bpcpis_prefix_prefix_choice_power)) * bpr_power_scale_bpcpis_prefix_prefix_choice_power)) /\ exists bpr_quotient_bpcpis_prefix_prefix_choice_power_repeat_entry. bpr_power_code_bpcpis_prefix_prefix_choice_power = bpr_quotient_bpcpis_prefix_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpis_prefix_prefix_choice_power)) * bpr_power_scale_bpcpis_prefix_prefix_choice_power) + (S (bpr_prefix_index_bpcpis_prefix_prefix))))) /\ (exists ff_u_bpcpis_prefix_prefix_choice_power_product ff_v_bpcpis_prefix_prefix_choice_power_product. ((((exists ff_h_bpcpis_prefix_prefix_choice_power_product_start. ff_h_bpcpis_prefix_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_prefix_prefix_choice_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_power_product_start. ff_u_bpcpis_prefix_prefix_choice_power_product = ff_q_bpcpis_prefix_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcpis_prefix_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_power_product_terminal. ff_h_bpcpis_prefix_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpcpis_prefix_prefix) = S ((S (bpr_choice_exponent_bpcpis_prefix_prefix_choice)) * ff_v_bpcpis_prefix_prefix_choice_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_power_product_terminal. ff_u_bpcpis_prefix_prefix_choice_power_product = ff_q_bpcpis_prefix_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_prefix_prefix_choice)) * ff_v_bpcpis_prefix_prefix_choice_power_product) + (bpr_prefix_value_bpcpis_prefix_prefix))) /\ forall ff_i_bpcpis_prefix_prefix_choice_power_product. (exists ff_lt_bpcpis_prefix_prefix_choice_power_product_bound. ff_lt_bpcpis_prefix_prefix_choice_power_product_bound + S ff_i_bpcpis_prefix_prefix_choice_power_product = bpr_choice_exponent_bpcpis_prefix_prefix_choice) -> exists ff_p_bpcpis_prefix_prefix_choice_power_product ff_r_bpcpis_prefix_prefix_choice_power_product ff_s_bpcpis_prefix_prefix_choice_power_product. ((((exists ff_h_bpcpis_prefix_prefix_choice_power_product_factor. ff_h_bpcpis_prefix_prefix_choice_power_product_factor + S (ff_p_bpcpis_prefix_prefix_choice_power_product) = S ((S (ff_i_bpcpis_prefix_prefix_choice_power_product)) * bpr_power_scale_bpcpis_prefix_prefix_choice_power)) /\ exists ff_q_bpcpis_prefix_prefix_choice_power_product_factor. bpr_power_code_bpcpis_prefix_prefix_choice_power = ff_q_bpcpis_prefix_prefix_choice_power_product_factor * S ((S (ff_i_bpcpis_prefix_prefix_choice_power_product)) * bpr_power_scale_bpcpis_prefix_prefix_choice_power) + (ff_p_bpcpis_prefix_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_power_product_partial. ff_h_bpcpis_prefix_prefix_choice_power_product_partial + S (ff_r_bpcpis_prefix_prefix_choice_power_product) = S ((S (ff_i_bpcpis_prefix_prefix_choice_power_product)) * ff_v_bpcpis_prefix_prefix_choice_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_power_product_partial. ff_u_bpcpis_prefix_prefix_choice_power_product = ff_q_bpcpis_prefix_prefix_choice_power_product_partial * S ((S (ff_i_bpcpis_prefix_prefix_choice_power_product)) * ff_v_bpcpis_prefix_prefix_choice_power_product) + (ff_r_bpcpis_prefix_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpis_prefix_prefix_choice_power_product_successor. ff_h_bpcpis_prefix_prefix_choice_power_product_successor + S (ff_s_bpcpis_prefix_prefix_choice_power_product) = S ((S (S ff_i_bpcpis_prefix_prefix_choice_power_product)) * ff_v_bpcpis_prefix_prefix_choice_power_product)) /\ exists ff_q_bpcpis_prefix_prefix_choice_power_product_successor. ff_u_bpcpis_prefix_prefix_choice_power_product = ff_q_bpcpis_prefix_prefix_choice_power_product_successor * S ((S (S ff_i_bpcpis_prefix_prefix_choice_power_product)) * ff_v_bpcpis_prefix_prefix_choice_power_product) + (ff_s_bpcpis_prefix_prefix_choice_power_product))) /\ ff_s_bpcpis_prefix_prefix_choice_power_product = ff_r_bpcpis_prefix_prefix_choice_power_product * ff_p_bpcpis_prefix_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpis_prefix_prefix) = 1) /\ forall bpr_left_bpcpis_prefix_prefix_choice_prime bpr_right_bpcpis_prefix_prefix_choice_prime. S (bpr_prefix_index_bpcpis_prefix_prefix) = bpr_left_bpcpis_prefix_prefix_choice_prime * bpr_right_bpcpis_prefix_prefix_choice_prime -> bpr_left_bpcpis_prefix_prefix_choice_prime = 1 \/ bpr_right_bpcpis_prefix_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpcpis_prefix_prefix = 1))))) /\ (exists ff_u_bpcpis_prefix_product ff_v_bpcpis_prefix_product. ((((exists ff_h_bpcpis_prefix_product_start. ff_h_bpcpis_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_prefix_product)) /\ exists ff_q_bpcpis_prefix_product_start. ff_u_bpcpis_prefix_product = ff_q_bpcpis_prefix_product_start * S ((S (0)) * ff_v_bpcpis_prefix_product) + (1))) /\ ((((exists ff_h_bpcpis_prefix_product_terminal. ff_h_bpcpis_prefix_product_terminal + S (x) = S ((S (a)) * ff_v_bpcpis_prefix_product)) /\ exists ff_q_bpcpis_prefix_product_terminal. ff_u_bpcpis_prefix_product = ff_q_bpcpis_prefix_product_terminal * S ((S (a)) * ff_v_bpcpis_prefix_product) + (x))) /\ forall ff_i_bpcpis_prefix_product. (exists ff_lt_bpcpis_prefix_product_bound. ff_lt_bpcpis_prefix_product_bound + S ff_i_bpcpis_prefix_product = a) -> exists ff_p_bpcpis_prefix_product ff_r_bpcpis_prefix_product ff_s_bpcpis_prefix_product. ((((exists ff_h_bpcpis_prefix_product_factor. ff_h_bpcpis_prefix_product_factor + S (ff_p_bpcpis_prefix_product) = S ((S (ff_i_bpcpis_prefix_product)) * bpr_product_scale_bpcpis_prefix)) /\ exists ff_q_bpcpis_prefix_product_factor. bpr_product_code_bpcpis_prefix = ff_q_bpcpis_prefix_product_factor * S ((S (ff_i_bpcpis_prefix_product)) * bpr_product_scale_bpcpis_prefix) + (ff_p_bpcpis_prefix_product))) /\ ((((exists ff_h_bpcpis_prefix_product_partial. ff_h_bpcpis_prefix_product_partial + S (ff_r_bpcpis_prefix_product) = S ((S (ff_i_bpcpis_prefix_product)) * ff_v_bpcpis_prefix_product)) /\ exists ff_q_bpcpis_prefix_product_partial. ff_u_bpcpis_prefix_product = ff_q_bpcpis_prefix_product_partial * S ((S (ff_i_bpcpis_prefix_product)) * ff_v_bpcpis_prefix_product) + (ff_r_bpcpis_prefix_product))) /\ ((((exists ff_h_bpcpis_prefix_product_successor. ff_h_bpcpis_prefix_product_successor + S (ff_s_bpcpis_prefix_product) = S ((S (S ff_i_bpcpis_prefix_product)) * ff_v_bpcpis_prefix_product)) /\ exists ff_q_bpcpis_prefix_product_successor. ff_u_bpcpis_prefix_product = ff_q_bpcpis_prefix_product_successor * S ((S (S ff_i_bpcpis_prefix_product)) * ff_v_bpcpis_prefix_product) + (ff_s_bpcpis_prefix_product))) /\ ff_s_bpcpis_prefix_product = ff_r_bpcpis_prefix_product * ff_p_bpcpis_prefix_product)))))))) /\ ((exists bpr_code_bpcpis_interval bpr_scale_bpcpis_interval. ((forall bpr_index_bpcpis_interval_prefix. (exists bpr_gap_bpcpis_interval_prefix_bound. bpr_gap_bpcpis_interval_prefix_bound + S (bpr_index_bpcpis_interval_prefix) = l) -> exists bpr_value_bpcpis_interval_prefix. ((((exists bpr_height_bpcpis_interval_prefix_decoded. bpr_height_bpcpis_interval_prefix_decoded + S (bpr_value_bpcpis_interval_prefix) = S ((S (bpr_index_bpcpis_interval_prefix)) * bpr_scale_bpcpis_interval)) /\ exists bpr_quotient_bpcpis_interval_prefix_decoded. bpr_code_bpcpis_interval = bpr_quotient_bpcpis_interval_prefix_decoded * S ((S (bpr_index_bpcpis_interval_prefix)) * bpr_scale_bpcpis_interval) + (bpr_value_bpcpis_interval_prefix))) /\ (((((~(S (a + bpr_index_bpcpis_interval_prefix) = 1) /\ forall bpr_left_bpcpis_interval_prefix_choice_prime bpr_right_bpcpis_interval_prefix_choice_prime. S (a + bpr_index_bpcpis_interval_prefix) = bpr_left_bpcpis_interval_prefix_choice_prime * bpr_right_bpcpis_interval_prefix_choice_prime -> bpr_left_bpcpis_interval_prefix_choice_prime = 1 \/ bpr_right_bpcpis_interval_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpis_interval_prefix_choice. ((((exists bpr_le_gap_bpcpis_interval_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcpis_interval_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpis_interval_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcpis_interval_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcpis_interval_prefix_choice_valuation_selected_power bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcpis_interval_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcpis_interval_prefix_choice) -> (((exists bpr_height_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_entry + S (S (a + bpr_index_bpcpis_interval_prefix)) = S ((S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpis_interval_prefix_choice_valuation_selected_power = bpr_quotient_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power) + (S (a + bpr_index_bpcpis_interval_prefix))))) /\ (exists ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_start. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_start. ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpis_interval_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpis_interval_prefix_choice)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_interval_prefix_choice)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcpis_interval_prefix_choice_valuation_selected))) /\ forall ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcpis_interval_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcpis_interval_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpis_interval_prefix_choice) -> exists ff_p_bpcpis_interval_prefix_choice_valuation_selected_power_product ff_r_bpcpis_interval_prefix_choice_valuation_selected_power_product ff_s_bpcpis_interval_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcpis_interval_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpis_interval_prefix_choice_valuation_selected_power = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power) + (ff_p_bpcpis_interval_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcpis_interval_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product) + (ff_r_bpcpis_interval_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcpis_interval_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product) + (ff_s_bpcpis_interval_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_r_bpcpis_interval_prefix_choice_valuation_selected_power_product * ff_p_bpcpis_interval_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_interval_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcpis_interval_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcpis_interval_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation. (exists bpr_le_gap_bpcpis_interval_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcpis_interval_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpis_interval_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcpis_interval_prefix_choice_valuation_candidate_power bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpis_interval_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation) -> (((exists bpr_height_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_entry + S (S (a + bpr_index_bpcpis_interval_prefix)) = S ((S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpis_interval_prefix_choice_valuation_candidate_power = bpr_quotient_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power) + (S (a + bpr_index_bpcpis_interval_prefix))))) /\ (exists ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpis_interval_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpis_interval_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcpis_interval_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcpis_interval_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation) -> exists ff_p_bpcpis_interval_prefix_choice_valuation_candidate_power_product ff_r_bpcpis_interval_prefix_choice_valuation_candidate_power_product ff_s_bpcpis_interval_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpis_interval_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpis_interval_prefix_choice_valuation_candidate_power = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power) + (ff_p_bpcpis_interval_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpis_interval_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcpis_interval_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpis_interval_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcpis_interval_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_r_bpcpis_interval_prefix_choice_valuation_candidate_power_product * ff_p_bpcpis_interval_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_interval_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpis_interval_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcpis_interval_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpis_interval_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcpis_interval_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation) = (bpr_choice_exponent_bpcpis_interval_prefix_choice))) /\ (exists bpr_power_code_bpcpis_interval_prefix_choice_power bpr_power_scale_bpcpis_interval_prefix_choice_power. ((forall bpr_power_index_bpcpis_interval_prefix_choice_power. (exists bpr_gap_bpcpis_interval_prefix_choice_power_repeat_bound. bpr_gap_bpcpis_interval_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcpis_interval_prefix_choice_power) = bpr_choice_exponent_bpcpis_interval_prefix_choice) -> (((exists bpr_height_bpcpis_interval_prefix_choice_power_repeat_entry. bpr_height_bpcpis_interval_prefix_choice_power_repeat_entry + S (S (a + bpr_index_bpcpis_interval_prefix)) = S ((S (bpr_power_index_bpcpis_interval_prefix_choice_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_power)) /\ exists bpr_quotient_bpcpis_interval_prefix_choice_power_repeat_entry. bpr_power_code_bpcpis_interval_prefix_choice_power = bpr_quotient_bpcpis_interval_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpis_interval_prefix_choice_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_power) + (S (a + bpr_index_bpcpis_interval_prefix))))) /\ (exists ff_u_bpcpis_interval_prefix_choice_power_product ff_v_bpcpis_interval_prefix_choice_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_start. ff_h_bpcpis_interval_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_start. ff_u_bpcpis_interval_prefix_choice_power_product = ff_q_bpcpis_interval_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_terminal. ff_h_bpcpis_interval_prefix_choice_power_product_terminal + S (bpr_value_bpcpis_interval_prefix) = S ((S (bpr_choice_exponent_bpcpis_interval_prefix_choice)) * ff_v_bpcpis_interval_prefix_choice_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_terminal. ff_u_bpcpis_interval_prefix_choice_power_product = ff_q_bpcpis_interval_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_interval_prefix_choice)) * ff_v_bpcpis_interval_prefix_choice_power_product) + (bpr_value_bpcpis_interval_prefix))) /\ forall ff_i_bpcpis_interval_prefix_choice_power_product. (exists ff_lt_bpcpis_interval_prefix_choice_power_product_bound. ff_lt_bpcpis_interval_prefix_choice_power_product_bound + S ff_i_bpcpis_interval_prefix_choice_power_product = bpr_choice_exponent_bpcpis_interval_prefix_choice) -> exists ff_p_bpcpis_interval_prefix_choice_power_product ff_r_bpcpis_interval_prefix_choice_power_product ff_s_bpcpis_interval_prefix_choice_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_factor. ff_h_bpcpis_interval_prefix_choice_power_product_factor + S (ff_p_bpcpis_interval_prefix_choice_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_power)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_factor. bpr_power_code_bpcpis_interval_prefix_choice_power = ff_q_bpcpis_interval_prefix_choice_power_product_factor * S ((S (ff_i_bpcpis_interval_prefix_choice_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_power) + (ff_p_bpcpis_interval_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_partial. ff_h_bpcpis_interval_prefix_choice_power_product_partial + S (ff_r_bpcpis_interval_prefix_choice_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_power_product)) * ff_v_bpcpis_interval_prefix_choice_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_partial. ff_u_bpcpis_interval_prefix_choice_power_product = ff_q_bpcpis_interval_prefix_choice_power_product_partial * S ((S (ff_i_bpcpis_interval_prefix_choice_power_product)) * ff_v_bpcpis_interval_prefix_choice_power_product) + (ff_r_bpcpis_interval_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_successor. ff_h_bpcpis_interval_prefix_choice_power_product_successor + S (ff_s_bpcpis_interval_prefix_choice_power_product) = S ((S (S ff_i_bpcpis_interval_prefix_choice_power_product)) * ff_v_bpcpis_interval_prefix_choice_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_successor. ff_u_bpcpis_interval_prefix_choice_power_product = ff_q_bpcpis_interval_prefix_choice_power_product_successor * S ((S (S ff_i_bpcpis_interval_prefix_choice_power_product)) * ff_v_bpcpis_interval_prefix_choice_power_product) + (ff_s_bpcpis_interval_prefix_choice_power_product))) /\ ff_s_bpcpis_interval_prefix_choice_power_product = ff_r_bpcpis_interval_prefix_choice_power_product * ff_p_bpcpis_interval_prefix_choice_power_product)))))))))) \/ (~((~(S (a + bpr_index_bpcpis_interval_prefix) = 1) /\ forall bpr_left_bpcpis_interval_prefix_choice_prime bpr_right_bpcpis_interval_prefix_choice_prime. S (a + bpr_index_bpcpis_interval_prefix) = bpr_left_bpcpis_interval_prefix_choice_prime * bpr_right_bpcpis_interval_prefix_choice_prime -> bpr_left_bpcpis_interval_prefix_choice_prime = 1 \/ bpr_right_bpcpis_interval_prefix_choice_prime = 1)) /\ bpr_value_bpcpis_interval_prefix = 1))))) /\ (exists ff_u_bpcpis_interval_product ff_v_bpcpis_interval_product. ((((exists ff_h_bpcpis_interval_product_start. ff_h_bpcpis_interval_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_interval_product)) /\ exists ff_q_bpcpis_interval_product_start. ff_u_bpcpis_interval_product = ff_q_bpcpis_interval_product_start * S ((S (0)) * ff_v_bpcpis_interval_product) + (1))) /\ ((((exists ff_h_bpcpis_interval_product_terminal. ff_h_bpcpis_interval_product_terminal + S (y) = S ((S (l)) * ff_v_bpcpis_interval_product)) /\ exists ff_q_bpcpis_interval_product_terminal. ff_u_bpcpis_interval_product = ff_q_bpcpis_interval_product_terminal * S ((S (l)) * ff_v_bpcpis_interval_product) + (y))) /\ forall ff_i_bpcpis_interval_product. (exists ff_lt_bpcpis_interval_product_bound. ff_lt_bpcpis_interval_product_bound + S ff_i_bpcpis_interval_product = l) -> exists ff_p_bpcpis_interval_product ff_r_bpcpis_interval_product ff_s_bpcpis_interval_product. ((((exists ff_h_bpcpis_interval_product_factor. ff_h_bpcpis_interval_product_factor + S (ff_p_bpcpis_interval_product) = S ((S (ff_i_bpcpis_interval_product)) * bpr_scale_bpcpis_interval)) /\ exists ff_q_bpcpis_interval_product_factor. bpr_code_bpcpis_interval = ff_q_bpcpis_interval_product_factor * S ((S (ff_i_bpcpis_interval_product)) * bpr_scale_bpcpis_interval) + (ff_p_bpcpis_interval_product))) /\ ((((exists ff_h_bpcpis_interval_product_partial. ff_h_bpcpis_interval_product_partial + S (ff_r_bpcpis_interval_product) = S ((S (ff_i_bpcpis_interval_product)) * ff_v_bpcpis_interval_product)) /\ exists ff_q_bpcpis_interval_product_partial. ff_u_bpcpis_interval_product = ff_q_bpcpis_interval_product_partial * S ((S (ff_i_bpcpis_interval_product)) * ff_v_bpcpis_interval_product) + (ff_r_bpcpis_interval_product))) /\ ((((exists ff_h_bpcpis_interval_product_successor. ff_h_bpcpis_interval_product_successor + S (ff_s_bpcpis_interval_product) = S ((S (S ff_i_bpcpis_interval_product)) * ff_v_bpcpis_interval_product)) /\ exists ff_q_bpcpis_interval_product_successor. ff_u_bpcpis_interval_product = ff_q_bpcpis_interval_product_successor * S ((S (S ff_i_bpcpis_interval_product)) * ff_v_bpcpis_interval_product) + (ff_s_bpcpis_interval_product))) /\ ff_s_bpcpis_interval_product = ff_r_bpcpis_interval_product * ff_p_bpcpis_interval_product)))))))) /\ z = x * y))Proof neighborhood
Direct theorem prerequisites
BT00UQ beta_product_prefix_suffix_split BT010L prime_contribution_interval_prefix_exists BT010P prime_contribution_interval_prefix_shift BT010Q prime_contribution_prefix_restrict_addDirect 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 (4)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–8
03Establish hrestrictedL9–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution prefix restrict add.
- L9
have hrestricted : ∀ bpr_prefix_index_bpcpis_restricted. Lt(bpr_prefix_index_bpcpis_restricted,a) → ∃ y. BetaAt(x,x1,bpr_prefix_index_bpcpis_restricted,y) ∧ (Prime(S bpr_prefix_index_bpcpis_restricted) ∧ (∃ z. PowerValuation(S bpr_prefix_index_bpcpis_restricted,n,z) ∧ Pow(S bpr_prefix_index_bpcpis_restricted,z,y)) ∨ ¬Prime(S bpr_prefix_index_bpcpis_restricted) ∧ y = 1)Definitions: Lt(bpr_prefix_index_bpcpis_restricted,a)BetaAt(x,x1,bpr_prefix_index_bpcpis_restricted,y)Prime(S bpr_prefix_index_bpcpis_restricted)PowerValuation(S bpr_prefix_index_bpcpis_restricted,n,z)Pow(S bpr_prefix_index_bpcpis_restricted,z,y)Original native command in the exact edition - L10
apply prime_contribution_prefix_restrict_add - L11
exact hproduct_witness_witness_left
04Establish hintervalL12–13
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution interval prefix exists.
- L12
have hinterval : ∃ d. ∃ e. ∀ x. Lt(x,l) → ∃ y. BetaAt(d,e,x,y) ∧ (Prime(S (a + x)) ∧ (∃ z. PowerValuation(S (a + x),n,z) ∧ Pow(S (a + x),z,y)) ∨ ¬Prime(S (a + x)) ∧ y = 1)Definitions: Lt(x,l)BetaAt(d,e,x,y)Prime(S (a + x))PowerValuation(S (a + x),n,z)Pow(S (a + x),z,y)Original native command in the exact edition - L13
apply prime_contribution_interval_prefix_exists
05Separate the logical casesL14–15
06Establish hshiftL16–25
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution interval prefix shift.
- L16
have hshift : ∀ i. ∀ p. Lt(i,l) → BetaAt(x,x1,a + i,p) → BetaAt(x2,x3,i,p)Definitions: Lt(i,l)BetaAt(x,x1,a + i,p)BetaAt(x2,x3,i,p)Original native command in the exact edition - L17
specialize prime_contribution_interval_prefix_shift n - L18
specialize prime_contribution_interval_prefix_shift a - L19
specialize prime_contribution_interval_prefix_shift x - L20
specialize prime_contribution_interval_prefix_shift x1 - L21
specialize prime_contribution_interval_prefix_shift x2 - L22
specialize prime_contribution_interval_prefix_shift x3 - L23
specialize prime_contribution_interval_prefix_shift l - L24
apply prime_contribution_interval_prefix_shift - L25
exact hproduct_witness_witness_left
07Use earlier factsL26–26
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L26
exact hinterval_witness_witness
08Establish hsplitL27–36
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product prefix suffix split.
- L27
have hsplit : ∃ p. ∃ q. Product(x,x1,a,p) ∧ (Product(x2,x3,l,q) ∧ z = p · q)Definitions: Product(x,x1,a,p)Product(x2,x3,l,q)Original native command in the exact edition - L28
specialize beta_product_prefix_suffix_split x - L29
specialize beta_product_prefix_suffix_split x1 - L30
specialize beta_product_prefix_suffix_split x2 - L31
specialize beta_product_prefix_suffix_split x3 - L32
specialize beta_product_prefix_suffix_split a - L33
specialize beta_product_prefix_suffix_split l - L34
specialize beta_product_prefix_suffix_split z - L35
apply beta_product_prefix_suffix_split - L36
exact hshift
09Use earlier factsL37–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L37
exact hproduct_witness_witness_right
10Separate the logical casesL38–41
11Construct an explicit witnessL42–43
12Separate the logical casesL44–44
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L44
split
13Construct an explicit witnessL45–46
14Separate the logical casesL47–47
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L47
split
15Use earlier factsL48–49
16Separate the logical casesL50–50
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L50
split
17Construct an explicit witnessL51–52
18Separate the logical casesL53–53
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L53
split
Original defined command ledger · 56 lines
- 0001
intro n - 0002
intro a - 0003
intro l - 0004
intro z - 0005
intro hproduct - 0006
cases hproduct - 0007
cases hproduct_witness - 0008
cases hproduct_witness_witness - 0009
have hrestricted : ∀ bpr_prefix_index_bpcpis_restricted. Lt(bpr_prefix_index_bpcpis_restricted,a) → ∃ y. BetaAt(x,x1,bpr_prefix_index_bpcpis_restricted,y) ∧ (Prime(S bpr_prefix_index_bpcpis_restricted) ∧ (∃ z. PowerValuation(S bpr_prefix_index_bpcpis_restricted,n,z) ∧ Pow(S bpr_prefix_index_bpcpis_restricted,z,y)) ∨ ¬Prime(S bpr_prefix_index_bpcpis_restricted) ∧ y = 1)Exact native replay line
have hrestricted : forall bpr_prefix_index_bpcpis_restricted. (exists bpr_gap_bpcpis_restricted_bound. bpr_gap_bpcpis_restricted_bound + S (bpr_prefix_index_bpcpis_restricted) = a) -> exists bpr_prefix_value_bpcpis_restricted. ((((exists bpr_height_bpcpis_restricted_decoded. bpr_height_bpcpis_restricted_decoded + S (bpr_prefix_value_bpcpis_restricted) = S ((S (bpr_prefix_index_bpcpis_restricted)) * x1)) /\ exists bpr_quotient_bpcpis_restricted_decoded. x = bpr_quotient_bpcpis_restricted_decoded * S ((S (bpr_prefix_index_bpcpis_restricted)) * x1) + (bpr_prefix_value_bpcpis_restricted))) /\ (((((~(S (bpr_prefix_index_bpcpis_restricted) = 1) /\ forall bpr_left_bpcpis_restricted_choice_prime bpr_right_bpcpis_restricted_choice_prime. S (bpr_prefix_index_bpcpis_restricted) = bpr_left_bpcpis_restricted_choice_prime * bpr_right_bpcpis_restricted_choice_prime -> bpr_left_bpcpis_restricted_choice_prime = 1 \/ bpr_right_bpcpis_restricted_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpis_restricted_choice. ((((exists bpr_le_gap_bpcpis_restricted_choice_valuation_selected_bound. bpr_le_gap_bpcpis_restricted_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpis_restricted_choice) = (n)) /\ (exists bpr_power_value_bpcpis_restricted_choice_valuation_selected. ((exists bpr_power_code_bpcpis_restricted_choice_valuation_selected_power bpr_power_scale_bpcpis_restricted_choice_valuation_selected_power. ((forall bpr_power_index_bpcpis_restricted_choice_valuation_selected_power. (exists bpr_gap_bpcpis_restricted_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpis_restricted_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpis_restricted_choice_valuation_selected_power) = bpr_choice_exponent_bpcpis_restricted_choice) -> (((exists bpr_height_bpcpis_restricted_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpis_restricted_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_restricted)) = S ((S (bpr_power_index_bpcpis_restricted_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_restricted_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpis_restricted_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpis_restricted_choice_valuation_selected_power = bpr_quotient_bpcpis_restricted_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpis_restricted_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_restricted_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpis_restricted))))) /\ (exists ff_u_bpcpis_restricted_choice_valuation_selected_power_product ff_v_bpcpis_restricted_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_restricted_choice_valuation_selected_power_product_start. ff_h_bpcpis_restricted_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_restricted_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_restricted_choice_valuation_selected_power_product_start. ff_u_bpcpis_restricted_choice_valuation_selected_power_product = ff_q_bpcpis_restricted_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpis_restricted_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpis_restricted_choice_valuation_selected_power_product_terminal. ff_h_bpcpis_restricted_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpis_restricted_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpis_restricted_choice)) * ff_v_bpcpis_restricted_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_restricted_choice_valuation_selected_power_product_terminal. ff_u_bpcpis_restricted_choice_valuation_selected_power_product = ff_q_bpcpis_restricted_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_restricted_choice)) * ff_v_bpcpis_restricted_choice_valuation_selected_power_product) + (bpr_power_value_bpcpis_restricted_choice_valuation_selected))) /\ forall ff_i_bpcpis_restricted_choice_valuation_selected_power_product. (exists ff_lt_bpcpis_restricted_choice_valuation_selected_power_product_bound. ff_lt_bpcpis_restricted_choice_valuation_selected_power_product_bound + S ff_i_bpcpis_restricted_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpis_restricted_choice) -> exists ff_p_bpcpis_restricted_choice_valuation_selected_power_product ff_r_bpcpis_restricted_choice_valuation_selected_power_product ff_s_bpcpis_restricted_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_restricted_choice_valuation_selected_power_product_factor. ff_h_bpcpis_restricted_choice_valuation_selected_power_product_factor + S (ff_p_bpcpis_restricted_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_restricted_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_restricted_choice_valuation_selected_power)) /\ exists ff_q_bpcpis_restricted_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpis_restricted_choice_valuation_selected_power = ff_q_bpcpis_restricted_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpis_restricted_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_restricted_choice_valuation_selected_power) + (ff_p_bpcpis_restricted_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_restricted_choice_valuation_selected_power_product_partial. ff_h_bpcpis_restricted_choice_valuation_selected_power_product_partial + S (ff_r_bpcpis_restricted_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_restricted_choice_valuation_selected_power_product)) * ff_v_bpcpis_restricted_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_restricted_choice_valuation_selected_power_product_partial. ff_u_bpcpis_restricted_choice_valuation_selected_power_product = ff_q_bpcpis_restricted_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpis_restricted_choice_valuation_selected_power_product)) * ff_v_bpcpis_restricted_choice_valuation_selected_power_product) + (ff_r_bpcpis_restricted_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_restricted_choice_valuation_selected_power_product_successor. ff_h_bpcpis_restricted_choice_valuation_selected_power_product_successor + S (ff_s_bpcpis_restricted_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpis_restricted_choice_valuation_selected_power_product)) * ff_v_bpcpis_restricted_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_restricted_choice_valuation_selected_power_product_successor. ff_u_bpcpis_restricted_choice_valuation_selected_power_product = ff_q_bpcpis_restricted_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpis_restricted_choice_valuation_selected_power_product)) * ff_v_bpcpis_restricted_choice_valuation_selected_power_product) + (ff_s_bpcpis_restricted_choice_valuation_selected_power_product))) /\ ff_s_bpcpis_restricted_choice_valuation_selected_power_product = ff_r_bpcpis_restricted_choice_valuation_selected_power_product * ff_p_bpcpis_restricted_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_restricted_choice_valuation_selected_divides. n = (bpr_power_value_bpcpis_restricted_choice_valuation_selected) * bpr_divides_quotient_bpcpis_restricted_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpis_restricted_choice_valuation. (exists bpr_le_gap_bpcpis_restricted_choice_valuation_candidate_bound. bpr_le_gap_bpcpis_restricted_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpis_restricted_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpis_restricted_choice_valuation_candidate. ((exists bpr_power_code_bpcpis_restricted_choice_valuation_candidate_power bpr_power_scale_bpcpis_restricted_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpis_restricted_choice_valuation_candidate_power. (exists bpr_gap_bpcpis_restricted_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpis_restricted_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpis_restricted_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpis_restricted_choice_valuation) -> (((exists bpr_height_bpcpis_restricted_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpis_restricted_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_restricted)) = S ((S (bpr_power_index_bpcpis_restricted_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_restricted_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpis_restricted_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpis_restricted_choice_valuation_candidate_power = bpr_quotient_bpcpis_restricted_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpis_restricted_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_restricted_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpis_restricted))))) /\ (exists ff_u_bpcpis_restricted_choice_valuation_candidate_power_product ff_v_bpcpis_restricted_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_start. ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_restricted_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_start. ff_u_bpcpis_restricted_choice_valuation_candidate_power_product = ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpis_restricted_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_terminal. ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpis_restricted_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpis_restricted_choice_valuation)) * ff_v_bpcpis_restricted_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_terminal. ff_u_bpcpis_restricted_choice_valuation_candidate_power_product = ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpis_restricted_choice_valuation)) * ff_v_bpcpis_restricted_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpis_restricted_choice_valuation_candidate))) /\ forall ff_i_bpcpis_restricted_choice_valuation_candidate_power_product. (exists ff_lt_bpcpis_restricted_choice_valuation_candidate_power_product_bound. ff_lt_bpcpis_restricted_choice_valuation_candidate_power_product_bound + S ff_i_bpcpis_restricted_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpis_restricted_choice_valuation) -> exists ff_p_bpcpis_restricted_choice_valuation_candidate_power_product ff_r_bpcpis_restricted_choice_valuation_candidate_power_product ff_s_bpcpis_restricted_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_factor. ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpis_restricted_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_restricted_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_restricted_choice_valuation_candidate_power)) /\ exists ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpis_restricted_choice_valuation_candidate_power = ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpis_restricted_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_restricted_choice_valuation_candidate_power) + (ff_p_bpcpis_restricted_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_partial. ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpis_restricted_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_restricted_choice_valuation_candidate_power_product)) * ff_v_bpcpis_restricted_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_partial. ff_u_bpcpis_restricted_choice_valuation_candidate_power_product = ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpis_restricted_choice_valuation_candidate_power_product)) * ff_v_bpcpis_restricted_choice_valuation_candidate_power_product) + (ff_r_bpcpis_restricted_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_successor. ff_h_bpcpis_restricted_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpis_restricted_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpis_restricted_choice_valuation_candidate_power_product)) * ff_v_bpcpis_restricted_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_successor. ff_u_bpcpis_restricted_choice_valuation_candidate_power_product = ff_q_bpcpis_restricted_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpis_restricted_choice_valuation_candidate_power_product)) * ff_v_bpcpis_restricted_choice_valuation_candidate_power_product) + (ff_s_bpcpis_restricted_choice_valuation_candidate_power_product))) /\ ff_s_bpcpis_restricted_choice_valuation_candidate_power_product = ff_r_bpcpis_restricted_choice_valuation_candidate_power_product * ff_p_bpcpis_restricted_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_restricted_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpis_restricted_choice_valuation_candidate) * bpr_divides_quotient_bpcpis_restricted_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpis_restricted_choice_valuation_candidate_below. bpr_le_gap_bpcpis_restricted_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpis_restricted_choice_valuation) = (bpr_choice_exponent_bpcpis_restricted_choice))) /\ (exists bpr_power_code_bpcpis_restricted_choice_power bpr_power_scale_bpcpis_restricted_choice_power. ((forall bpr_power_index_bpcpis_restricted_choice_power. (exists bpr_gap_bpcpis_restricted_choice_power_repeat_bound. bpr_gap_bpcpis_restricted_choice_power_repeat_bound + S (bpr_power_index_bpcpis_restricted_choice_power) = bpr_choice_exponent_bpcpis_restricted_choice) -> (((exists bpr_height_bpcpis_restricted_choice_power_repeat_entry. bpr_height_bpcpis_restricted_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpis_restricted)) = S ((S (bpr_power_index_bpcpis_restricted_choice_power)) * bpr_power_scale_bpcpis_restricted_choice_power)) /\ exists bpr_quotient_bpcpis_restricted_choice_power_repeat_entry. bpr_power_code_bpcpis_restricted_choice_power = bpr_quotient_bpcpis_restricted_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpis_restricted_choice_power)) * bpr_power_scale_bpcpis_restricted_choice_power) + (S (bpr_prefix_index_bpcpis_restricted))))) /\ (exists ff_u_bpcpis_restricted_choice_power_product ff_v_bpcpis_restricted_choice_power_product. ((((exists ff_h_bpcpis_restricted_choice_power_product_start. ff_h_bpcpis_restricted_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_restricted_choice_power_product)) /\ exists ff_q_bpcpis_restricted_choice_power_product_start. ff_u_bpcpis_restricted_choice_power_product = ff_q_bpcpis_restricted_choice_power_product_start * S ((S (0)) * ff_v_bpcpis_restricted_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpis_restricted_choice_power_product_terminal. ff_h_bpcpis_restricted_choice_power_product_terminal + S (bpr_prefix_value_bpcpis_restricted) = S ((S (bpr_choice_exponent_bpcpis_restricted_choice)) * ff_v_bpcpis_restricted_choice_power_product)) /\ exists ff_q_bpcpis_restricted_choice_power_product_terminal. ff_u_bpcpis_restricted_choice_power_product = ff_q_bpcpis_restricted_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_restricted_choice)) * ff_v_bpcpis_restricted_choice_power_product) + (bpr_prefix_value_bpcpis_restricted))) /\ forall ff_i_bpcpis_restricted_choice_power_product. (exists ff_lt_bpcpis_restricted_choice_power_product_bound. ff_lt_bpcpis_restricted_choice_power_product_bound + S ff_i_bpcpis_restricted_choice_power_product = bpr_choice_exponent_bpcpis_restricted_choice) -> exists ff_p_bpcpis_restricted_choice_power_product ff_r_bpcpis_restricted_choice_power_product ff_s_bpcpis_restricted_choice_power_product. ((((exists ff_h_bpcpis_restricted_choice_power_product_factor. ff_h_bpcpis_restricted_choice_power_product_factor + S (ff_p_bpcpis_restricted_choice_power_product) = S ((S (ff_i_bpcpis_restricted_choice_power_product)) * bpr_power_scale_bpcpis_restricted_choice_power)) /\ exists ff_q_bpcpis_restricted_choice_power_product_factor. bpr_power_code_bpcpis_restricted_choice_power = ff_q_bpcpis_restricted_choice_power_product_factor * S ((S (ff_i_bpcpis_restricted_choice_power_product)) * bpr_power_scale_bpcpis_restricted_choice_power) + (ff_p_bpcpis_restricted_choice_power_product))) /\ ((((exists ff_h_bpcpis_restricted_choice_power_product_partial. ff_h_bpcpis_restricted_choice_power_product_partial + S (ff_r_bpcpis_restricted_choice_power_product) = S ((S (ff_i_bpcpis_restricted_choice_power_product)) * ff_v_bpcpis_restricted_choice_power_product)) /\ exists ff_q_bpcpis_restricted_choice_power_product_partial. ff_u_bpcpis_restricted_choice_power_product = ff_q_bpcpis_restricted_choice_power_product_partial * S ((S (ff_i_bpcpis_restricted_choice_power_product)) * ff_v_bpcpis_restricted_choice_power_product) + (ff_r_bpcpis_restricted_choice_power_product))) /\ ((((exists ff_h_bpcpis_restricted_choice_power_product_successor. ff_h_bpcpis_restricted_choice_power_product_successor + S (ff_s_bpcpis_restricted_choice_power_product) = S ((S (S ff_i_bpcpis_restricted_choice_power_product)) * ff_v_bpcpis_restricted_choice_power_product)) /\ exists ff_q_bpcpis_restricted_choice_power_product_successor. ff_u_bpcpis_restricted_choice_power_product = ff_q_bpcpis_restricted_choice_power_product_successor * S ((S (S ff_i_bpcpis_restricted_choice_power_product)) * ff_v_bpcpis_restricted_choice_power_product) + (ff_s_bpcpis_restricted_choice_power_product))) /\ ff_s_bpcpis_restricted_choice_power_product = ff_r_bpcpis_restricted_choice_power_product * ff_p_bpcpis_restricted_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpis_restricted) = 1) /\ forall bpr_left_bpcpis_restricted_choice_prime bpr_right_bpcpis_restricted_choice_prime. S (bpr_prefix_index_bpcpis_restricted) = bpr_left_bpcpis_restricted_choice_prime * bpr_right_bpcpis_restricted_choice_prime -> bpr_left_bpcpis_restricted_choice_prime = 1 \/ bpr_right_bpcpis_restricted_choice_prime = 1)) /\ bpr_prefix_value_bpcpis_restricted = 1)))) - 0010
apply prime_contribution_prefix_restrict_add - 0011
exact hproduct_witness_witness_left - 0012
have hinterval : ∃ d. ∃ e. ∀ x. Lt(x,l) → ∃ y. BetaAt(d,e,x,y) ∧ (Prime(S (a + x)) ∧ (∃ z. PowerValuation(S (a + x),n,z) ∧ Pow(S (a + x),z,y)) ∨ ¬Prime(S (a + x)) ∧ y = 1)Exact native replay line
have hinterval : exists d e. (forall bpr_index_bpcpis_interval_prefix. (exists bpr_gap_bpcpis_interval_prefix_bound. bpr_gap_bpcpis_interval_prefix_bound + S (bpr_index_bpcpis_interval_prefix) = l) -> exists bpr_value_bpcpis_interval_prefix. ((((exists bpr_height_bpcpis_interval_prefix_decoded. bpr_height_bpcpis_interval_prefix_decoded + S (bpr_value_bpcpis_interval_prefix) = S ((S (bpr_index_bpcpis_interval_prefix)) * e)) /\ exists bpr_quotient_bpcpis_interval_prefix_decoded. d = bpr_quotient_bpcpis_interval_prefix_decoded * S ((S (bpr_index_bpcpis_interval_prefix)) * e) + (bpr_value_bpcpis_interval_prefix))) /\ (((((~(S (a + bpr_index_bpcpis_interval_prefix) = 1) /\ forall bpr_left_bpcpis_interval_prefix_choice_prime bpr_right_bpcpis_interval_prefix_choice_prime. S (a + bpr_index_bpcpis_interval_prefix) = bpr_left_bpcpis_interval_prefix_choice_prime * bpr_right_bpcpis_interval_prefix_choice_prime -> bpr_left_bpcpis_interval_prefix_choice_prime = 1 \/ bpr_right_bpcpis_interval_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpis_interval_prefix_choice. ((((exists bpr_le_gap_bpcpis_interval_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcpis_interval_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpis_interval_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcpis_interval_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcpis_interval_prefix_choice_valuation_selected_power bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcpis_interval_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcpis_interval_prefix_choice) -> (((exists bpr_height_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_entry + S (S (a + bpr_index_bpcpis_interval_prefix)) = S ((S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpis_interval_prefix_choice_valuation_selected_power = bpr_quotient_bpcpis_interval_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power) + (S (a + bpr_index_bpcpis_interval_prefix))))) /\ (exists ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_start. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_start. ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpis_interval_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpis_interval_prefix_choice)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_interval_prefix_choice)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcpis_interval_prefix_choice_valuation_selected))) /\ forall ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcpis_interval_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcpis_interval_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpis_interval_prefix_choice) -> exists ff_p_bpcpis_interval_prefix_choice_valuation_selected_power_product ff_r_bpcpis_interval_prefix_choice_valuation_selected_power_product ff_s_bpcpis_interval_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcpis_interval_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpis_interval_prefix_choice_valuation_selected_power = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_selected_power) + (ff_p_bpcpis_interval_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcpis_interval_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product) + (ff_r_bpcpis_interval_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcpis_interval_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcpis_interval_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpis_interval_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_selected_power_product) + (ff_s_bpcpis_interval_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcpis_interval_prefix_choice_valuation_selected_power_product = ff_r_bpcpis_interval_prefix_choice_valuation_selected_power_product * ff_p_bpcpis_interval_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_interval_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcpis_interval_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcpis_interval_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation. (exists bpr_le_gap_bpcpis_interval_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcpis_interval_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpis_interval_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcpis_interval_prefix_choice_valuation_candidate_power bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpis_interval_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation) -> (((exists bpr_height_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_entry + S (S (a + bpr_index_bpcpis_interval_prefix)) = S ((S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpis_interval_prefix_choice_valuation_candidate_power = bpr_quotient_bpcpis_interval_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpis_interval_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power) + (S (a + bpr_index_bpcpis_interval_prefix))))) /\ (exists ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpis_interval_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpis_interval_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcpis_interval_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcpis_interval_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation) -> exists ff_p_bpcpis_interval_prefix_choice_valuation_candidate_power_product ff_r_bpcpis_interval_prefix_choice_valuation_candidate_power_product ff_s_bpcpis_interval_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpis_interval_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpis_interval_prefix_choice_valuation_candidate_power = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_valuation_candidate_power) + (ff_p_bpcpis_interval_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpis_interval_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcpis_interval_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcpis_interval_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpis_interval_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_q_bpcpis_interval_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpis_interval_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpis_interval_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcpis_interval_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcpis_interval_prefix_choice_valuation_candidate_power_product = ff_r_bpcpis_interval_prefix_choice_valuation_candidate_power_product * ff_p_bpcpis_interval_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpis_interval_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpis_interval_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcpis_interval_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpis_interval_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcpis_interval_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpis_interval_prefix_choice_valuation) = (bpr_choice_exponent_bpcpis_interval_prefix_choice))) /\ (exists bpr_power_code_bpcpis_interval_prefix_choice_power bpr_power_scale_bpcpis_interval_prefix_choice_power. ((forall bpr_power_index_bpcpis_interval_prefix_choice_power. (exists bpr_gap_bpcpis_interval_prefix_choice_power_repeat_bound. bpr_gap_bpcpis_interval_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcpis_interval_prefix_choice_power) = bpr_choice_exponent_bpcpis_interval_prefix_choice) -> (((exists bpr_height_bpcpis_interval_prefix_choice_power_repeat_entry. bpr_height_bpcpis_interval_prefix_choice_power_repeat_entry + S (S (a + bpr_index_bpcpis_interval_prefix)) = S ((S (bpr_power_index_bpcpis_interval_prefix_choice_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_power)) /\ exists bpr_quotient_bpcpis_interval_prefix_choice_power_repeat_entry. bpr_power_code_bpcpis_interval_prefix_choice_power = bpr_quotient_bpcpis_interval_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpis_interval_prefix_choice_power)) * bpr_power_scale_bpcpis_interval_prefix_choice_power) + (S (a + bpr_index_bpcpis_interval_prefix))))) /\ (exists ff_u_bpcpis_interval_prefix_choice_power_product ff_v_bpcpis_interval_prefix_choice_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_start. ff_h_bpcpis_interval_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_start. ff_u_bpcpis_interval_prefix_choice_power_product = ff_q_bpcpis_interval_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcpis_interval_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_terminal. ff_h_bpcpis_interval_prefix_choice_power_product_terminal + S (bpr_value_bpcpis_interval_prefix) = S ((S (bpr_choice_exponent_bpcpis_interval_prefix_choice)) * ff_v_bpcpis_interval_prefix_choice_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_terminal. ff_u_bpcpis_interval_prefix_choice_power_product = ff_q_bpcpis_interval_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpis_interval_prefix_choice)) * ff_v_bpcpis_interval_prefix_choice_power_product) + (bpr_value_bpcpis_interval_prefix))) /\ forall ff_i_bpcpis_interval_prefix_choice_power_product. (exists ff_lt_bpcpis_interval_prefix_choice_power_product_bound. ff_lt_bpcpis_interval_prefix_choice_power_product_bound + S ff_i_bpcpis_interval_prefix_choice_power_product = bpr_choice_exponent_bpcpis_interval_prefix_choice) -> exists ff_p_bpcpis_interval_prefix_choice_power_product ff_r_bpcpis_interval_prefix_choice_power_product ff_s_bpcpis_interval_prefix_choice_power_product. ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_factor. ff_h_bpcpis_interval_prefix_choice_power_product_factor + S (ff_p_bpcpis_interval_prefix_choice_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_power)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_factor. bpr_power_code_bpcpis_interval_prefix_choice_power = ff_q_bpcpis_interval_prefix_choice_power_product_factor * S ((S (ff_i_bpcpis_interval_prefix_choice_power_product)) * bpr_power_scale_bpcpis_interval_prefix_choice_power) + (ff_p_bpcpis_interval_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_partial. ff_h_bpcpis_interval_prefix_choice_power_product_partial + S (ff_r_bpcpis_interval_prefix_choice_power_product) = S ((S (ff_i_bpcpis_interval_prefix_choice_power_product)) * ff_v_bpcpis_interval_prefix_choice_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_partial. ff_u_bpcpis_interval_prefix_choice_power_product = ff_q_bpcpis_interval_prefix_choice_power_product_partial * S ((S (ff_i_bpcpis_interval_prefix_choice_power_product)) * ff_v_bpcpis_interval_prefix_choice_power_product) + (ff_r_bpcpis_interval_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpis_interval_prefix_choice_power_product_successor. ff_h_bpcpis_interval_prefix_choice_power_product_successor + S (ff_s_bpcpis_interval_prefix_choice_power_product) = S ((S (S ff_i_bpcpis_interval_prefix_choice_power_product)) * ff_v_bpcpis_interval_prefix_choice_power_product)) /\ exists ff_q_bpcpis_interval_prefix_choice_power_product_successor. ff_u_bpcpis_interval_prefix_choice_power_product = ff_q_bpcpis_interval_prefix_choice_power_product_successor * S ((S (S ff_i_bpcpis_interval_prefix_choice_power_product)) * ff_v_bpcpis_interval_prefix_choice_power_product) + (ff_s_bpcpis_interval_prefix_choice_power_product))) /\ ff_s_bpcpis_interval_prefix_choice_power_product = ff_r_bpcpis_interval_prefix_choice_power_product * ff_p_bpcpis_interval_prefix_choice_power_product)))))))))) \/ (~((~(S (a + bpr_index_bpcpis_interval_prefix) = 1) /\ forall bpr_left_bpcpis_interval_prefix_choice_prime bpr_right_bpcpis_interval_prefix_choice_prime. S (a + bpr_index_bpcpis_interval_prefix) = bpr_left_bpcpis_interval_prefix_choice_prime * bpr_right_bpcpis_interval_prefix_choice_prime -> bpr_left_bpcpis_interval_prefix_choice_prime = 1 \/ bpr_right_bpcpis_interval_prefix_choice_prime = 1)) /\ bpr_value_bpcpis_interval_prefix = 1))))) - 0013
apply prime_contribution_interval_prefix_exists - 0014
cases hinterval - 0015
cases hinterval_witness - 0016
have hshift : ∀ i. ∀ p. Lt(i,l) → BetaAt(x,x1,a + i,p) → BetaAt(x2,x3,i,p)Exact native replay line
have hshift : forall i p. (exists bpr_gap_bpcpis_shift_bound. bpr_gap_bpcpis_shift_bound + S (i) = l) -> (((exists bpr_height_bpcpis_shift_source. bpr_height_bpcpis_shift_source + S (p) = S ((S (a + i)) * x1)) /\ exists bpr_quotient_bpcpis_shift_source. x = bpr_quotient_bpcpis_shift_source * S ((S (a + i)) * x1) + (p))) -> (((exists bpr_height_bpcpis_shift_target. bpr_height_bpcpis_shift_target + S (p) = S ((S (i)) * x3)) /\ exists bpr_quotient_bpcpis_shift_target. x2 = bpr_quotient_bpcpis_shift_target * S ((S (i)) * x3) + (p))) - 0017
specialize prime_contribution_interval_prefix_shift n - 0018
specialize prime_contribution_interval_prefix_shift a - 0019
specialize prime_contribution_interval_prefix_shift x - 0020
specialize prime_contribution_interval_prefix_shift x1 - 0021
specialize prime_contribution_interval_prefix_shift x2 - 0022
specialize prime_contribution_interval_prefix_shift x3 - 0023
specialize prime_contribution_interval_prefix_shift l - 0024
apply prime_contribution_interval_prefix_shift - 0025
exact hproduct_witness_witness_left - 0026
exact hinterval_witness_witness - 0027
have hsplit : ∃ p. ∃ q. Product(x,x1,a,p) ∧ (Product(x2,x3,l,q) ∧ z = p · q)Exact native replay line
have hsplit : exists p q. (exists ff_u_bpcpis_prefix_product ff_v_bpcpis_prefix_product. ((((exists ff_h_bpcpis_prefix_product_start. ff_h_bpcpis_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_prefix_product)) /\ exists ff_q_bpcpis_prefix_product_start. ff_u_bpcpis_prefix_product = ff_q_bpcpis_prefix_product_start * S ((S (0)) * ff_v_bpcpis_prefix_product) + (1))) /\ ((((exists ff_h_bpcpis_prefix_product_terminal. ff_h_bpcpis_prefix_product_terminal + S (p) = S ((S (a)) * ff_v_bpcpis_prefix_product)) /\ exists ff_q_bpcpis_prefix_product_terminal. ff_u_bpcpis_prefix_product = ff_q_bpcpis_prefix_product_terminal * S ((S (a)) * ff_v_bpcpis_prefix_product) + (p))) /\ forall ff_i_bpcpis_prefix_product. (exists ff_lt_bpcpis_prefix_product_bound. ff_lt_bpcpis_prefix_product_bound + S ff_i_bpcpis_prefix_product = a) -> exists ff_p_bpcpis_prefix_product ff_r_bpcpis_prefix_product ff_s_bpcpis_prefix_product. ((((exists ff_h_bpcpis_prefix_product_factor. ff_h_bpcpis_prefix_product_factor + S (ff_p_bpcpis_prefix_product) = S ((S (ff_i_bpcpis_prefix_product)) * x1)) /\ exists ff_q_bpcpis_prefix_product_factor. x = ff_q_bpcpis_prefix_product_factor * S ((S (ff_i_bpcpis_prefix_product)) * x1) + (ff_p_bpcpis_prefix_product))) /\ ((((exists ff_h_bpcpis_prefix_product_partial. ff_h_bpcpis_prefix_product_partial + S (ff_r_bpcpis_prefix_product) = S ((S (ff_i_bpcpis_prefix_product)) * ff_v_bpcpis_prefix_product)) /\ exists ff_q_bpcpis_prefix_product_partial. ff_u_bpcpis_prefix_product = ff_q_bpcpis_prefix_product_partial * S ((S (ff_i_bpcpis_prefix_product)) * ff_v_bpcpis_prefix_product) + (ff_r_bpcpis_prefix_product))) /\ ((((exists ff_h_bpcpis_prefix_product_successor. ff_h_bpcpis_prefix_product_successor + S (ff_s_bpcpis_prefix_product) = S ((S (S ff_i_bpcpis_prefix_product)) * ff_v_bpcpis_prefix_product)) /\ exists ff_q_bpcpis_prefix_product_successor. ff_u_bpcpis_prefix_product = ff_q_bpcpis_prefix_product_successor * S ((S (S ff_i_bpcpis_prefix_product)) * ff_v_bpcpis_prefix_product) + (ff_s_bpcpis_prefix_product))) /\ ff_s_bpcpis_prefix_product = ff_r_bpcpis_prefix_product * ff_p_bpcpis_prefix_product)))))) /\ ((exists ff_u_bpcpis_interval_product ff_v_bpcpis_interval_product. ((((exists ff_h_bpcpis_interval_product_start. ff_h_bpcpis_interval_product_start + S (1) = S ((S (0)) * ff_v_bpcpis_interval_product)) /\ exists ff_q_bpcpis_interval_product_start. ff_u_bpcpis_interval_product = ff_q_bpcpis_interval_product_start * S ((S (0)) * ff_v_bpcpis_interval_product) + (1))) /\ ((((exists ff_h_bpcpis_interval_product_terminal. ff_h_bpcpis_interval_product_terminal + S (q) = S ((S (l)) * ff_v_bpcpis_interval_product)) /\ exists ff_q_bpcpis_interval_product_terminal. ff_u_bpcpis_interval_product = ff_q_bpcpis_interval_product_terminal * S ((S (l)) * ff_v_bpcpis_interval_product) + (q))) /\ forall ff_i_bpcpis_interval_product. (exists ff_lt_bpcpis_interval_product_bound. ff_lt_bpcpis_interval_product_bound + S ff_i_bpcpis_interval_product = l) -> exists ff_p_bpcpis_interval_product ff_r_bpcpis_interval_product ff_s_bpcpis_interval_product. ((((exists ff_h_bpcpis_interval_product_factor. ff_h_bpcpis_interval_product_factor + S (ff_p_bpcpis_interval_product) = S ((S (ff_i_bpcpis_interval_product)) * x3)) /\ exists ff_q_bpcpis_interval_product_factor. x2 = ff_q_bpcpis_interval_product_factor * S ((S (ff_i_bpcpis_interval_product)) * x3) + (ff_p_bpcpis_interval_product))) /\ ((((exists ff_h_bpcpis_interval_product_partial. ff_h_bpcpis_interval_product_partial + S (ff_r_bpcpis_interval_product) = S ((S (ff_i_bpcpis_interval_product)) * ff_v_bpcpis_interval_product)) /\ exists ff_q_bpcpis_interval_product_partial. ff_u_bpcpis_interval_product = ff_q_bpcpis_interval_product_partial * S ((S (ff_i_bpcpis_interval_product)) * ff_v_bpcpis_interval_product) + (ff_r_bpcpis_interval_product))) /\ ((((exists ff_h_bpcpis_interval_product_successor. ff_h_bpcpis_interval_product_successor + S (ff_s_bpcpis_interval_product) = S ((S (S ff_i_bpcpis_interval_product)) * ff_v_bpcpis_interval_product)) /\ exists ff_q_bpcpis_interval_product_successor. ff_u_bpcpis_interval_product = ff_q_bpcpis_interval_product_successor * S ((S (S ff_i_bpcpis_interval_product)) * ff_v_bpcpis_interval_product) + (ff_s_bpcpis_interval_product))) /\ ff_s_bpcpis_interval_product = ff_r_bpcpis_interval_product * ff_p_bpcpis_interval_product)))))) /\ z = p * q) - 0028
specialize beta_product_prefix_suffix_split x - 0029
specialize beta_product_prefix_suffix_split x1 - 0030
specialize beta_product_prefix_suffix_split x2 - 0031
specialize beta_product_prefix_suffix_split x3 - 0032
specialize beta_product_prefix_suffix_split a - 0033
specialize beta_product_prefix_suffix_split l - 0034
specialize beta_product_prefix_suffix_split z - 0035
apply beta_product_prefix_suffix_split - 0036
exact hshift - 0037
exact hproduct_witness_witness_right - 0038
cases hsplit - 0039
cases hsplit_witness - 0040
cases hsplit_witness_witness - 0041
cases hsplit_witness_witness_right - 0042
exists x4 - 0043
exists x5 - 0044
split - 0045
exists x - 0046
exists x1 - 0047
split - 0048
exact hrestricted - 0049
exact hsplit_witness_witness_left - 0050
split - 0051
exists x2 - 0052
exists x3 - 0053
split - 0054
exact hinterval_witness_witness - 0055
exact hsplit_witness_witness_right_left - 0056
exact hsplit_witness_witness_right_right