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. ∀ s. ∀ q. ∀ r. ∀ C. ∀ A. ∀ B. (∀ x. Lt(n,x) ∧ Le(x,n + n) → ¬Prime(x)) → Lt(2,n) → FloorSqrt(n + n,s) → DivRem(n + n,3,q,r) → CentralBinom(n,C) → Pow(n + n,s,A) → Pow(4,q,B) → Le(C,A · B)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
10 occurrences
In local proof propositions
24 occurrences
Exact expanded native-PA statement
forall n s q r C A B. (forall bpr_prime_candidate_b5cblonbp_exclusion. ((exists bpr_gap_b5cblonbp_exclusion_lower. bpr_gap_b5cblonbp_exclusion_lower + S (n) = bpr_prime_candidate_b5cblonbp_exclusion) /\ (exists bpr_le_gap_b5cblonbp_exclusion_upper. bpr_le_gap_b5cblonbp_exclusion_upper + (bpr_prime_candidate_b5cblonbp_exclusion) = (n + n))) -> ~((~(bpr_prime_candidate_b5cblonbp_exclusion = 1) /\ forall bpr_left_b5cblonbp_exclusion_prime bpr_right_b5cblonbp_exclusion_prime. bpr_prime_candidate_b5cblonbp_exclusion = bpr_left_b5cblonbp_exclusion_prime * bpr_right_b5cblonbp_exclusion_prime -> bpr_left_b5cblonbp_exclusion_prime = 1 \/ bpr_right_b5cblonbp_exclusion_prime = 1))) -> (exists bcf_lt_gap_b5cblonbp_positive. bcf_lt_gap_b5cblonbp_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5cblonbp_floor. bcs_sqrt_lower_gap_b5cblonbp_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5cblonbp_floor. bcs_sqrt_upper_gap_b5cblonbp_floor + S (n + n) = S (s) * S (s))) -> (((n + n) = (3) * (q) + (r) /\ (exists bcf_lt_gap_b5cblonbp_division_bound. bcf_lt_gap_b5cblonbp_division_bound + S (r) = 3))) -> (((exists bcf_lt_gap_b5cblonbp_central_out_of_range. bcf_lt_gap_b5cblonbp_central_out_of_range + S (n + n) = n) /\ C = 0) \/ ((exists bcf_le_gap_b5cblonbp_central_in_range. bcf_le_gap_b5cblonbp_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_b5cblonbp_central bcf_row_code_scale_b5cblonbp_central bcf_row_scale_code_b5cblonbp_central bcf_row_scale_scale_b5cblonbp_central bcf_row_code_b5cblonbp_central bcf_row_scale_b5cblonbp_central. ((forall bcf_row_index_b5cblonbp_central_table. (exists bcf_lt_gap_b5cblonbp_central_table_row_bound. bcf_lt_gap_b5cblonbp_central_table_row_bound + S (bcf_row_index_b5cblonbp_central_table) = S (n + n)) -> exists bcf_row_code_b5cblonbp_central_table bcf_row_scale_b5cblonbp_central_table. ((((exists bcf_height_b5cblonbp_central_table_decoded_row_code. bcf_height_b5cblonbp_central_table_decoded_row_code + S (bcf_row_code_b5cblonbp_central_table) = S ((S (bcf_row_index_b5cblonbp_central_table)) * bcf_row_code_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_table_decoded_row_code. bcf_row_code_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_table_decoded_row_code * S ((S (bcf_row_index_b5cblonbp_central_table)) * bcf_row_code_scale_b5cblonbp_central) + (bcf_row_code_b5cblonbp_central_table))) /\ ((((exists bcf_height_b5cblonbp_central_table_decoded_row_scale. bcf_height_b5cblonbp_central_table_decoded_row_scale + S (bcf_row_scale_b5cblonbp_central_table) = S ((S (bcf_row_index_b5cblonbp_central_table)) * bcf_row_scale_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_table_decoded_row_scale. bcf_row_scale_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_table_decoded_row_scale * S ((S (bcf_row_index_b5cblonbp_central_table)) * bcf_row_scale_scale_b5cblonbp_central) + (bcf_row_scale_b5cblonbp_central_table))) /\ ((bcf_row_index_b5cblonbp_central_table = 0 /\ (forall bcf_index_b5cblonbp_central_table_zero_row. (exists bcf_lt_gap_b5cblonbp_central_table_zero_row_bound. bcf_lt_gap_b5cblonbp_central_table_zero_row_bound + S (bcf_index_b5cblonbp_central_table_zero_row) = S (n + n)) -> exists bcf_value_b5cblonbp_central_table_zero_row. ((((exists bcf_height_b5cblonbp_central_table_zero_row_entry. bcf_height_b5cblonbp_central_table_zero_row_entry + S (bcf_value_b5cblonbp_central_table_zero_row) = S ((S (bcf_index_b5cblonbp_central_table_zero_row)) * bcf_row_scale_b5cblonbp_central_table)) /\ exists bcf_quotient_b5cblonbp_central_table_zero_row_entry. bcf_row_code_b5cblonbp_central_table = bcf_quotient_b5cblonbp_central_table_zero_row_entry * S ((S (bcf_index_b5cblonbp_central_table_zero_row)) * bcf_row_scale_b5cblonbp_central_table) + (bcf_value_b5cblonbp_central_table_zero_row))) /\ ((bcf_index_b5cblonbp_central_table_zero_row = 0 /\ bcf_value_b5cblonbp_central_table_zero_row = 1) \/ exists bcf_predecessor_b5cblonbp_central_table_zero_row. bcf_index_b5cblonbp_central_table_zero_row = S bcf_predecessor_b5cblonbp_central_table_zero_row /\ bcf_value_b5cblonbp_central_table_zero_row = 0)))) \/ exists bcf_predecessor_b5cblonbp_central_table bcf_previous_code_b5cblonbp_central_table bcf_previous_scale_b5cblonbp_central_table. bcf_row_index_b5cblonbp_central_table = S bcf_predecessor_b5cblonbp_central_table /\ ((((exists bcf_height_b5cblonbp_central_table_decoded_previous_code. bcf_height_b5cblonbp_central_table_decoded_previous_code + S (bcf_previous_code_b5cblonbp_central_table) = S ((S (bcf_predecessor_b5cblonbp_central_table)) * bcf_row_code_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_table_decoded_previous_code. bcf_row_code_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_table_decoded_previous_code * S ((S (bcf_predecessor_b5cblonbp_central_table)) * bcf_row_code_scale_b5cblonbp_central) + (bcf_previous_code_b5cblonbp_central_table))) /\ ((((exists bcf_height_b5cblonbp_central_table_decoded_previous_scale. bcf_height_b5cblonbp_central_table_decoded_previous_scale + S (bcf_previous_scale_b5cblonbp_central_table) = S ((S (bcf_predecessor_b5cblonbp_central_table)) * bcf_row_scale_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_table_decoded_previous_scale. bcf_row_scale_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_table_decoded_previous_scale * S ((S (bcf_predecessor_b5cblonbp_central_table)) * bcf_row_scale_scale_b5cblonbp_central) + (bcf_previous_scale_b5cblonbp_central_table))) /\ (forall bcf_index_b5cblonbp_central_table_row_step. (exists bcf_lt_gap_b5cblonbp_central_table_row_step_bound. bcf_lt_gap_b5cblonbp_central_table_row_step_bound + S (bcf_index_b5cblonbp_central_table_row_step) = S (n + n)) -> exists bcf_value_b5cblonbp_central_table_row_step. ((((exists bcf_height_b5cblonbp_central_table_row_step_entry. bcf_height_b5cblonbp_central_table_row_step_entry + S (bcf_value_b5cblonbp_central_table_row_step) = S ((S (bcf_index_b5cblonbp_central_table_row_step)) * bcf_row_scale_b5cblonbp_central_table)) /\ exists bcf_quotient_b5cblonbp_central_table_row_step_entry. bcf_row_code_b5cblonbp_central_table = bcf_quotient_b5cblonbp_central_table_row_step_entry * S ((S (bcf_index_b5cblonbp_central_table_row_step)) * bcf_row_scale_b5cblonbp_central_table) + (bcf_value_b5cblonbp_central_table_row_step))) /\ ((bcf_index_b5cblonbp_central_table_row_step = 0 /\ bcf_value_b5cblonbp_central_table_row_step = 1) \/ exists bcf_predecessor_b5cblonbp_central_table_row_step bcf_left_b5cblonbp_central_table_row_step bcf_right_b5cblonbp_central_table_row_step. bcf_index_b5cblonbp_central_table_row_step = S bcf_predecessor_b5cblonbp_central_table_row_step /\ ((((exists bcf_height_b5cblonbp_central_table_row_step_previous_left. bcf_height_b5cblonbp_central_table_row_step_previous_left + S (bcf_left_b5cblonbp_central_table_row_step) = S ((S (bcf_predecessor_b5cblonbp_central_table_row_step)) * bcf_previous_scale_b5cblonbp_central_table)) /\ exists bcf_quotient_b5cblonbp_central_table_row_step_previous_left. bcf_previous_code_b5cblonbp_central_table = bcf_quotient_b5cblonbp_central_table_row_step_previous_left * S ((S (bcf_predecessor_b5cblonbp_central_table_row_step)) * bcf_previous_scale_b5cblonbp_central_table) + (bcf_left_b5cblonbp_central_table_row_step))) /\ ((((exists bcf_height_b5cblonbp_central_table_row_step_previous_right. bcf_height_b5cblonbp_central_table_row_step_previous_right + S (bcf_right_b5cblonbp_central_table_row_step) = S ((S (S (bcf_predecessor_b5cblonbp_central_table_row_step))) * bcf_previous_scale_b5cblonbp_central_table)) /\ exists bcf_quotient_b5cblonbp_central_table_row_step_previous_right. bcf_previous_code_b5cblonbp_central_table = bcf_quotient_b5cblonbp_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_b5cblonbp_central_table_row_step))) * bcf_previous_scale_b5cblonbp_central_table) + (bcf_right_b5cblonbp_central_table_row_step))) /\ bcf_value_b5cblonbp_central_table_row_step = bcf_left_b5cblonbp_central_table_row_step + bcf_right_b5cblonbp_central_table_row_step))))))))))) /\ ((((exists bcf_height_b5cblonbp_central_decoded_row_code. bcf_height_b5cblonbp_central_decoded_row_code + S (bcf_row_code_b5cblonbp_central) = S ((S (n + n)) * bcf_row_code_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_decoded_row_code. bcf_row_code_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_b5cblonbp_central) + (bcf_row_code_b5cblonbp_central))) /\ ((((exists bcf_height_b5cblonbp_central_decoded_row_scale. bcf_height_b5cblonbp_central_decoded_row_scale + S (bcf_row_scale_b5cblonbp_central) = S ((S (n + n)) * bcf_row_scale_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_decoded_row_scale. bcf_row_scale_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_b5cblonbp_central) + (bcf_row_scale_b5cblonbp_central))) /\ (((exists bcf_height_b5cblonbp_central_decoded_value. bcf_height_b5cblonbp_central_decoded_value + S (C) = S ((S (n)) * bcf_row_scale_b5cblonbp_central)) /\ exists bcf_quotient_b5cblonbp_central_decoded_value. bcf_row_code_b5cblonbp_central = bcf_quotient_b5cblonbp_central_decoded_value * S ((S (n)) * bcf_row_scale_b5cblonbp_central) + (C))))))))) -> (exists bpvi_b_b5cblonbp_power_a bpvi_c_b5cblonbp_power_a. ((forall bpvi_i_b5cblonbp_power_a. (exists bpvi_repeat_gap_b5cblonbp_power_a. bpvi_repeat_gap_b5cblonbp_power_a + S bpvi_i_b5cblonbp_power_a = s) -> (((exists bpvi_h_b5cblonbp_power_a_repeat. bpvi_h_b5cblonbp_power_a_repeat + S (n + n) = S ((S (bpvi_i_b5cblonbp_power_a)) * bpvi_c_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_repeat. bpvi_b_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_repeat * S ((S (bpvi_i_b5cblonbp_power_a)) * bpvi_c_b5cblonbp_power_a) + (n + n)))) /\ (exists bpvi_u_b5cblonbp_power_a bpvi_v_b5cblonbp_power_a. ((((exists bpvi_h_b5cblonbp_power_a_start. bpvi_h_b5cblonbp_power_a_start + S (1) = S ((S (0)) * bpvi_v_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_start. bpvi_u_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_start * S ((S (0)) * bpvi_v_b5cblonbp_power_a) + (1))) /\ ((((exists bpvi_h_b5cblonbp_power_a_terminal. bpvi_h_b5cblonbp_power_a_terminal + S (A) = S ((S (s)) * bpvi_v_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_terminal. bpvi_u_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_terminal * S ((S (s)) * bpvi_v_b5cblonbp_power_a) + (A))) /\ forall bpvi_j_b5cblonbp_power_a. (exists bpvi_product_gap_b5cblonbp_power_a. bpvi_product_gap_b5cblonbp_power_a + S bpvi_j_b5cblonbp_power_a = s) -> exists bpvi_factor_b5cblonbp_power_a bpvi_partial_b5cblonbp_power_a bpvi_successor_b5cblonbp_power_a. ((((exists bpvi_h_b5cblonbp_power_a_factor. bpvi_h_b5cblonbp_power_a_factor + S (bpvi_factor_b5cblonbp_power_a) = S ((S (bpvi_j_b5cblonbp_power_a)) * bpvi_c_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_factor. bpvi_b_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_factor * S ((S (bpvi_j_b5cblonbp_power_a)) * bpvi_c_b5cblonbp_power_a) + (bpvi_factor_b5cblonbp_power_a))) /\ ((((exists bpvi_h_b5cblonbp_power_a_partial. bpvi_h_b5cblonbp_power_a_partial + S (bpvi_partial_b5cblonbp_power_a) = S ((S (bpvi_j_b5cblonbp_power_a)) * bpvi_v_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_partial. bpvi_u_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_partial * S ((S (bpvi_j_b5cblonbp_power_a)) * bpvi_v_b5cblonbp_power_a) + (bpvi_partial_b5cblonbp_power_a))) /\ ((((exists bpvi_h_b5cblonbp_power_a_successor. bpvi_h_b5cblonbp_power_a_successor + S (bpvi_successor_b5cblonbp_power_a) = S ((S (S bpvi_j_b5cblonbp_power_a)) * bpvi_v_b5cblonbp_power_a)) /\ exists bpvi_q_b5cblonbp_power_a_successor. bpvi_u_b5cblonbp_power_a = bpvi_q_b5cblonbp_power_a_successor * S ((S (S bpvi_j_b5cblonbp_power_a)) * bpvi_v_b5cblonbp_power_a) + (bpvi_successor_b5cblonbp_power_a))) /\ bpvi_successor_b5cblonbp_power_a = bpvi_partial_b5cblonbp_power_a * bpvi_factor_b5cblonbp_power_a)))))))) -> (exists bpvi_b_b5cblonbp_power_b bpvi_c_b5cblonbp_power_b. ((forall bpvi_i_b5cblonbp_power_b. (exists bpvi_repeat_gap_b5cblonbp_power_b. bpvi_repeat_gap_b5cblonbp_power_b + S bpvi_i_b5cblonbp_power_b = q) -> (((exists bpvi_h_b5cblonbp_power_b_repeat. bpvi_h_b5cblonbp_power_b_repeat + S (4) = S ((S (bpvi_i_b5cblonbp_power_b)) * bpvi_c_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_repeat. bpvi_b_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_repeat * S ((S (bpvi_i_b5cblonbp_power_b)) * bpvi_c_b5cblonbp_power_b) + (4)))) /\ (exists bpvi_u_b5cblonbp_power_b bpvi_v_b5cblonbp_power_b. ((((exists bpvi_h_b5cblonbp_power_b_start. bpvi_h_b5cblonbp_power_b_start + S (1) = S ((S (0)) * bpvi_v_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_start. bpvi_u_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_start * S ((S (0)) * bpvi_v_b5cblonbp_power_b) + (1))) /\ ((((exists bpvi_h_b5cblonbp_power_b_terminal. bpvi_h_b5cblonbp_power_b_terminal + S (B) = S ((S (q)) * bpvi_v_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_terminal. bpvi_u_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_terminal * S ((S (q)) * bpvi_v_b5cblonbp_power_b) + (B))) /\ forall bpvi_j_b5cblonbp_power_b. (exists bpvi_product_gap_b5cblonbp_power_b. bpvi_product_gap_b5cblonbp_power_b + S bpvi_j_b5cblonbp_power_b = q) -> exists bpvi_factor_b5cblonbp_power_b bpvi_partial_b5cblonbp_power_b bpvi_successor_b5cblonbp_power_b. ((((exists bpvi_h_b5cblonbp_power_b_factor. bpvi_h_b5cblonbp_power_b_factor + S (bpvi_factor_b5cblonbp_power_b) = S ((S (bpvi_j_b5cblonbp_power_b)) * bpvi_c_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_factor. bpvi_b_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_factor * S ((S (bpvi_j_b5cblonbp_power_b)) * bpvi_c_b5cblonbp_power_b) + (bpvi_factor_b5cblonbp_power_b))) /\ ((((exists bpvi_h_b5cblonbp_power_b_partial. bpvi_h_b5cblonbp_power_b_partial + S (bpvi_partial_b5cblonbp_power_b) = S ((S (bpvi_j_b5cblonbp_power_b)) * bpvi_v_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_partial. bpvi_u_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_partial * S ((S (bpvi_j_b5cblonbp_power_b)) * bpvi_v_b5cblonbp_power_b) + (bpvi_partial_b5cblonbp_power_b))) /\ ((((exists bpvi_h_b5cblonbp_power_b_successor. bpvi_h_b5cblonbp_power_b_successor + S (bpvi_successor_b5cblonbp_power_b) = S ((S (S bpvi_j_b5cblonbp_power_b)) * bpvi_v_b5cblonbp_power_b)) /\ exists bpvi_q_b5cblonbp_power_b_successor. bpvi_u_b5cblonbp_power_b = bpvi_q_b5cblonbp_power_b_successor * S ((S (S bpvi_j_b5cblonbp_power_b)) * bpvi_v_b5cblonbp_power_b) + (bpvi_successor_b5cblonbp_power_b))) /\ bpvi_successor_b5cblonbp_power_b = bpvi_partial_b5cblonbp_power_b * bpvi_factor_b5cblonbp_power_b)))))))) -> (exists bcf_le_gap_b5cblonbp_result. bcf_le_gap_b5cblonbp_result + (C) = A * B)Proof neighborhood
Direct theorem prerequisites
BT00PV mul_le_mul BT010J floor_third_double_gap_package BT0107 central_binom_prime_contribution_product_exists BT010Y no_bertrand_small_contribution_product_le_power BT0111 no_bertrand_middle_contribution_interval_le_four_pow BT0113 central_binom_factorization_smallDirect 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 (6)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–14
03Establish hgapsL15–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply floor third double gap package.
- L15
have hgaps : exists g h. s + g = q /\ q + h = n + n - L16
specialize floor_third_double_gap_package n - L17
specialize floor_third_double_gap_package s - L18
specialize floor_third_double_gap_package q - L19
specialize floor_third_double_gap_package r - L20
apply floor_third_double_gap_package - L21
exact hpositive - L22
exact hfloor - L23
exact hdivision
04Separate the logical casesL24–26
05Establish hproductL27–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom prime contribution product exists.
- L27
have hproduct : ∃ z. (∃ x. ∃ y. (∀ m. Lt(m,n + n) → ∃ k. BetaAt(x,y,m,k) ∧ (Prime(S m) ∧ (∃ i. PowerValuation(S m,C,i) ∧ Pow(S m,i,k)) ∨ ¬Prime(S m) ∧ k = 1)) ∧ Product(x,y,n + n,z)) ∧ C = zDefinitions: Lt(m,n + n)BetaAt(x,y,m,k)Prime(S m)PowerValuation(S m,C,i)Pow(S m,i,k)Product(x,y,n + n,z)Original native command in the exact edition - L28
specialize central_binom_prime_contribution_product_exists n - L29
specialize central_binom_prime_contribution_product_exists C - L30
apply central_binom_prime_contribution_product_exists - L31
exact hcentral
06Separate the logical casesL32–33
07Establish hfactorizationL34–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom factorization small.
- L34
have hfactorization : ∃ u. ∃ v. (∃ y. ∃ z. (∀ n. Lt(n,s) → ∃ m. BetaAt(y,z,n,m) ∧ (Prime(S n) ∧ (∃ k. PowerValuation(S n,C,k) ∧ Pow(S n,k,m)) ∨ ¬Prime(S n) ∧ m = 1)) ∧ Product(y,z,s,u)) ∧ ((∃ y. ∃ z. (∀ n. Lt(n,x) → ∃ m. BetaAt(y,z,n,m) ∧ (Prime(S (s + n)) ∧ (∃ k. PowerValuation(S (s + n),C,k) ∧ Pow(S (s + n),k,m)) ∨ ¬Prime(S (s + n)) ∧ m = 1)) ∧ Product(y,z,x,v)) ∧ x2 = u · v)Definitions: Lt(n,s)BetaAt(y,z,n,m)Prime(S n)PowerValuation(S n,C,k)Pow(S n,k,m)Product(y,z,s,u)Lt(n,x)Prime(S (s + n))PowerValuation(S (s + n),C,k)Pow(S (s + n),k,m)Product(y,z,x,v)Original native command in the exact edition - L35
specialize central_binom_factorization_small n - L36
specialize central_binom_factorization_small s - L37
specialize central_binom_factorization_small q - L38
specialize central_binom_factorization_small r - L39
specialize central_binom_factorization_small C - L40
specialize central_binom_factorization_small x - L41
specialize central_binom_factorization_small x1 - L42
specialize central_binom_factorization_small x2 - L43
apply central_binom_factorization_small
08Use earlier factsL44–51
09Separate the logical casesL52–55
10Establish hsmallL56–65
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply no bertrand small contribution product le power.
- L56
- L57
specialize no_bertrand_small_contribution_product_le_power n - L58
specialize no_bertrand_small_contribution_product_le_power s - L59
specialize no_bertrand_small_contribution_product_le_power q - L60
specialize no_bertrand_small_contribution_product_le_power r - L61
specialize no_bertrand_small_contribution_product_le_power C - L62
specialize no_bertrand_small_contribution_product_le_power x3 - L63
specialize no_bertrand_small_contribution_product_le_power A - L64
apply no_bertrand_small_contribution_product_le_power - L65
exact hexclusion
11Use earlier factsL66–71
12Establish hmiddleL72–81
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply no bertrand middle contribution interval le four pow.
- L72
- L73
specialize no_bertrand_middle_contribution_interval_le_four_pow n - L74
specialize no_bertrand_middle_contribution_interval_le_four_pow s - L75
specialize no_bertrand_middle_contribution_interval_le_four_pow q - L76
specialize no_bertrand_middle_contribution_interval_le_four_pow r - L77
specialize no_bertrand_middle_contribution_interval_le_four_pow C - L78
specialize no_bertrand_middle_contribution_interval_le_four_pow x - L79
specialize no_bertrand_middle_contribution_interval_le_four_pow x4 - L80
specialize no_bertrand_middle_contribution_interval_le_four_pow B - L81
apply no_bertrand_middle_contribution_interval_le_four_pow
13Use earlier factsL82–89
14Establish hproduct_boundL90–99
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul.
- L90
have hproduct_bound : Le(x3 · x4,A · B)Definitions: Le(x3 · x4,A · B)Original native command in the exact edition - L91
specialize mul_le_mul x3 - L92
specialize mul_le_mul A - L93
specialize mul_le_mul x4 - L94
specialize mul_le_mul B - L95
apply mul_le_mul - L96
exact hsmall - L97
exact hmiddle - L98
rewrite hproduct_witness_right - L99
rewrite hfactorization_witness_witness_right_right
15Use earlier factsL100–100
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L100
exact hproduct_bound
Original defined command ledger · 100 lines
- 0001
intro n - 0002
intro s - 0003
intro q - 0004
intro r - 0005
intro C - 0006
intro A - 0007
intro B - 0008
intro hexclusion - 0009
intro hpositive - 0010
intro hfloor - 0011
intro hdivision - 0012
intro hcentral - 0013
intro hpower_a - 0014
intro hpower_b - 0015
have hgaps : exists g h. s + g = q /\ q + h = n + n - 0016
specialize floor_third_double_gap_package n - 0017
specialize floor_third_double_gap_package s - 0018
specialize floor_third_double_gap_package q - 0019
specialize floor_third_double_gap_package r - 0020
apply floor_third_double_gap_package - 0021
exact hpositive - 0022
exact hfloor - 0023
exact hdivision - 0024
cases hgaps - 0025
cases hgaps_witness - 0026
cases hgaps_witness_witness - 0027
have hproduct : ∃ z. (∃ x. ∃ y. (∀ m. Lt(m,n + n) → ∃ k. BetaAt(x,y,m,k) ∧ (Prime(S m) ∧ (∃ i. PowerValuation(S m,C,i) ∧ Pow(S m,i,k)) ∨ ¬Prime(S m) ∧ k = 1)) ∧ Product(x,y,n + n,z)) ∧ C = zExact native replay line
have hproduct : exists z. (exists bpr_product_code_b5cblonbp_product bpr_product_scale_b5cblonbp_product. ((forall bpr_prefix_index_b5cblonbp_product_prefix. (exists bpr_gap_b5cblonbp_product_prefix_bound. bpr_gap_b5cblonbp_product_prefix_bound + S (bpr_prefix_index_b5cblonbp_product_prefix) = n + n) -> exists bpr_prefix_value_b5cblonbp_product_prefix. ((((exists bpr_height_b5cblonbp_product_prefix_decoded. bpr_height_b5cblonbp_product_prefix_decoded + S (bpr_prefix_value_b5cblonbp_product_prefix) = S ((S (bpr_prefix_index_b5cblonbp_product_prefix)) * bpr_product_scale_b5cblonbp_product)) /\ exists bpr_quotient_b5cblonbp_product_prefix_decoded. bpr_product_code_b5cblonbp_product = bpr_quotient_b5cblonbp_product_prefix_decoded * S ((S (bpr_prefix_index_b5cblonbp_product_prefix)) * bpr_product_scale_b5cblonbp_product) + (bpr_prefix_value_b5cblonbp_product_prefix))) /\ (((((~(S (bpr_prefix_index_b5cblonbp_product_prefix) = 1) /\ forall bpr_left_b5cblonbp_product_prefix_choice_prime bpr_right_b5cblonbp_product_prefix_choice_prime. S (bpr_prefix_index_b5cblonbp_product_prefix) = bpr_left_b5cblonbp_product_prefix_choice_prime * bpr_right_b5cblonbp_product_prefix_choice_prime -> bpr_left_b5cblonbp_product_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_product_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_b5cblonbp_product_prefix_choice. ((((exists bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_selected_bound. bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_b5cblonbp_product_prefix_choice) = (C)) /\ (exists bpr_power_value_b5cblonbp_product_prefix_choice_valuation_selected. ((exists bpr_power_code_b5cblonbp_product_prefix_choice_valuation_selected_power bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power. ((forall bpr_power_index_b5cblonbp_product_prefix_choice_valuation_selected_power. (exists bpr_gap_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_selected_power) = bpr_choice_exponent_b5cblonbp_product_prefix_choice) -> (((exists bpr_height_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_product_prefix)) = S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_b5cblonbp_product_prefix_choice_valuation_selected_power = bpr_quotient_b5cblonbp_product_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_b5cblonbp_product_prefix))))) /\ (exists ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_start. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_start. ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_terminal. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_b5cblonbp_product_prefix_choice)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_terminal. ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_product_prefix_choice)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product) + (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_selected))) /\ forall ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product. (exists ff_lt_b5cblonbp_product_prefix_choice_valuation_selected_power_product_bound. ff_lt_b5cblonbp_product_prefix_choice_valuation_selected_power_product_bound + S ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_b5cblonbp_product_prefix_choice) -> exists ff_p_b5cblonbp_product_prefix_choice_valuation_selected_power_product ff_r_b5cblonbp_product_prefix_choice_valuation_selected_power_product ff_s_b5cblonbp_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_factor. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_factor + S (ff_p_b5cblonbp_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_b5cblonbp_product_prefix_choice_valuation_selected_power = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_selected_power) + (ff_p_b5cblonbp_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_partial. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_partial + S (ff_r_b5cblonbp_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_partial. ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product) + (ff_r_b5cblonbp_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_successor. ff_h_b5cblonbp_product_prefix_choice_valuation_selected_power_product_successor + S (ff_s_b5cblonbp_product_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_successor. ff_u_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_b5cblonbp_product_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_selected_power_product) + (ff_s_b5cblonbp_product_prefix_choice_valuation_selected_power_product))) /\ ff_s_b5cblonbp_product_prefix_choice_valuation_selected_power_product = ff_r_b5cblonbp_product_prefix_choice_valuation_selected_power_product * ff_p_b5cblonbp_product_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_product_prefix_choice_valuation_selected_divides. C = (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_selected) * bpr_divides_quotient_b5cblonbp_product_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation. (exists bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_candidate_bound. bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation) = (C)) -> (exists bpr_power_value_b5cblonbp_product_prefix_choice_valuation_candidate. ((exists bpr_power_code_b5cblonbp_product_prefix_choice_valuation_candidate_power bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_b5cblonbp_product_prefix_choice_valuation_candidate_power. (exists bpr_gap_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation) -> (((exists bpr_height_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_product_prefix)) = S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_b5cblonbp_product_prefix_choice_valuation_candidate_power = bpr_quotient_b5cblonbp_product_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_b5cblonbp_product_prefix))))) /\ (exists ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_start. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_start. ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_terminal. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_terminal. ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_candidate))) /\ forall ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product. (exists ff_lt_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_bound. ff_lt_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_bound + S ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation) -> exists ff_p_b5cblonbp_product_prefix_choice_valuation_candidate_power_product ff_r_b5cblonbp_product_prefix_choice_valuation_candidate_power_product ff_s_b5cblonbp_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_factor. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_b5cblonbp_product_prefix_choice_valuation_candidate_power = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_valuation_candidate_power) + (ff_p_b5cblonbp_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_partial. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_partial. ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) + (ff_r_b5cblonbp_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_successor. ff_h_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_successor. ff_u_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_product_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_product_prefix_choice_valuation_candidate_power_product) + (ff_s_b5cblonbp_product_prefix_choice_valuation_candidate_power_product))) /\ ff_s_b5cblonbp_product_prefix_choice_valuation_candidate_power_product = ff_r_b5cblonbp_product_prefix_choice_valuation_candidate_power_product * ff_p_b5cblonbp_product_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_product_prefix_choice_valuation_candidate_divides. C = (bpr_power_value_b5cblonbp_product_prefix_choice_valuation_candidate) * bpr_divides_quotient_b5cblonbp_product_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_candidate_below. bpr_le_gap_b5cblonbp_product_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_b5cblonbp_product_prefix_choice_valuation) = (bpr_choice_exponent_b5cblonbp_product_prefix_choice))) /\ (exists bpr_power_code_b5cblonbp_product_prefix_choice_power bpr_power_scale_b5cblonbp_product_prefix_choice_power. ((forall bpr_power_index_b5cblonbp_product_prefix_choice_power. (exists bpr_gap_b5cblonbp_product_prefix_choice_power_repeat_bound. bpr_gap_b5cblonbp_product_prefix_choice_power_repeat_bound + S (bpr_power_index_b5cblonbp_product_prefix_choice_power) = bpr_choice_exponent_b5cblonbp_product_prefix_choice) -> (((exists bpr_height_b5cblonbp_product_prefix_choice_power_repeat_entry. bpr_height_b5cblonbp_product_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_product_prefix)) = S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_power)) /\ exists bpr_quotient_b5cblonbp_product_prefix_choice_power_repeat_entry. bpr_power_code_b5cblonbp_product_prefix_choice_power = bpr_quotient_b5cblonbp_product_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_product_prefix_choice_power)) * bpr_power_scale_b5cblonbp_product_prefix_choice_power) + (S (bpr_prefix_index_b5cblonbp_product_prefix))))) /\ (exists ff_u_b5cblonbp_product_prefix_choice_power_product ff_v_b5cblonbp_product_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_start. ff_h_b5cblonbp_product_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_start. ff_u_b5cblonbp_product_prefix_choice_power_product = ff_q_b5cblonbp_product_prefix_choice_power_product_start * S ((S (0)) * ff_v_b5cblonbp_product_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_terminal. ff_h_b5cblonbp_product_prefix_choice_power_product_terminal + S (bpr_prefix_value_b5cblonbp_product_prefix) = S ((S (bpr_choice_exponent_b5cblonbp_product_prefix_choice)) * ff_v_b5cblonbp_product_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_terminal. ff_u_b5cblonbp_product_prefix_choice_power_product = ff_q_b5cblonbp_product_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_product_prefix_choice)) * ff_v_b5cblonbp_product_prefix_choice_power_product) + (bpr_prefix_value_b5cblonbp_product_prefix))) /\ forall ff_i_b5cblonbp_product_prefix_choice_power_product. (exists ff_lt_b5cblonbp_product_prefix_choice_power_product_bound. ff_lt_b5cblonbp_product_prefix_choice_power_product_bound + S ff_i_b5cblonbp_product_prefix_choice_power_product = bpr_choice_exponent_b5cblonbp_product_prefix_choice) -> exists ff_p_b5cblonbp_product_prefix_choice_power_product ff_r_b5cblonbp_product_prefix_choice_power_product ff_s_b5cblonbp_product_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_factor. ff_h_b5cblonbp_product_prefix_choice_power_product_factor + S (ff_p_b5cblonbp_product_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_power)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_factor. bpr_power_code_b5cblonbp_product_prefix_choice_power = ff_q_b5cblonbp_product_prefix_choice_power_product_factor * S ((S (ff_i_b5cblonbp_product_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_product_prefix_choice_power) + (ff_p_b5cblonbp_product_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_partial. ff_h_b5cblonbp_product_prefix_choice_power_product_partial + S (ff_r_b5cblonbp_product_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_product_prefix_choice_power_product)) * ff_v_b5cblonbp_product_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_partial. ff_u_b5cblonbp_product_prefix_choice_power_product = ff_q_b5cblonbp_product_prefix_choice_power_product_partial * S ((S (ff_i_b5cblonbp_product_prefix_choice_power_product)) * ff_v_b5cblonbp_product_prefix_choice_power_product) + (ff_r_b5cblonbp_product_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_product_prefix_choice_power_product_successor. ff_h_b5cblonbp_product_prefix_choice_power_product_successor + S (ff_s_b5cblonbp_product_prefix_choice_power_product) = S ((S (S ff_i_b5cblonbp_product_prefix_choice_power_product)) * ff_v_b5cblonbp_product_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_product_prefix_choice_power_product_successor. ff_u_b5cblonbp_product_prefix_choice_power_product = ff_q_b5cblonbp_product_prefix_choice_power_product_successor * S ((S (S ff_i_b5cblonbp_product_prefix_choice_power_product)) * ff_v_b5cblonbp_product_prefix_choice_power_product) + (ff_s_b5cblonbp_product_prefix_choice_power_product))) /\ ff_s_b5cblonbp_product_prefix_choice_power_product = ff_r_b5cblonbp_product_prefix_choice_power_product * ff_p_b5cblonbp_product_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_b5cblonbp_product_prefix) = 1) /\ forall bpr_left_b5cblonbp_product_prefix_choice_prime bpr_right_b5cblonbp_product_prefix_choice_prime. S (bpr_prefix_index_b5cblonbp_product_prefix) = bpr_left_b5cblonbp_product_prefix_choice_prime * bpr_right_b5cblonbp_product_prefix_choice_prime -> bpr_left_b5cblonbp_product_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_product_prefix_choice_prime = 1)) /\ bpr_prefix_value_b5cblonbp_product_prefix = 1))))) /\ (exists ff_u_b5cblonbp_product_product ff_v_b5cblonbp_product_product. ((((exists ff_h_b5cblonbp_product_product_start. ff_h_b5cblonbp_product_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_product_product)) /\ exists ff_q_b5cblonbp_product_product_start. ff_u_b5cblonbp_product_product = ff_q_b5cblonbp_product_product_start * S ((S (0)) * ff_v_b5cblonbp_product_product) + (1))) /\ ((((exists ff_h_b5cblonbp_product_product_terminal. ff_h_b5cblonbp_product_product_terminal + S (z) = S ((S (n + n)) * ff_v_b5cblonbp_product_product)) /\ exists ff_q_b5cblonbp_product_product_terminal. ff_u_b5cblonbp_product_product = ff_q_b5cblonbp_product_product_terminal * S ((S (n + n)) * ff_v_b5cblonbp_product_product) + (z))) /\ forall ff_i_b5cblonbp_product_product. (exists ff_lt_b5cblonbp_product_product_bound. ff_lt_b5cblonbp_product_product_bound + S ff_i_b5cblonbp_product_product = n + n) -> exists ff_p_b5cblonbp_product_product ff_r_b5cblonbp_product_product ff_s_b5cblonbp_product_product. ((((exists ff_h_b5cblonbp_product_product_factor. ff_h_b5cblonbp_product_product_factor + S (ff_p_b5cblonbp_product_product) = S ((S (ff_i_b5cblonbp_product_product)) * bpr_product_scale_b5cblonbp_product)) /\ exists ff_q_b5cblonbp_product_product_factor. bpr_product_code_b5cblonbp_product = ff_q_b5cblonbp_product_product_factor * S ((S (ff_i_b5cblonbp_product_product)) * bpr_product_scale_b5cblonbp_product) + (ff_p_b5cblonbp_product_product))) /\ ((((exists ff_h_b5cblonbp_product_product_partial. ff_h_b5cblonbp_product_product_partial + S (ff_r_b5cblonbp_product_product) = S ((S (ff_i_b5cblonbp_product_product)) * ff_v_b5cblonbp_product_product)) /\ exists ff_q_b5cblonbp_product_product_partial. ff_u_b5cblonbp_product_product = ff_q_b5cblonbp_product_product_partial * S ((S (ff_i_b5cblonbp_product_product)) * ff_v_b5cblonbp_product_product) + (ff_r_b5cblonbp_product_product))) /\ ((((exists ff_h_b5cblonbp_product_product_successor. ff_h_b5cblonbp_product_product_successor + S (ff_s_b5cblonbp_product_product) = S ((S (S ff_i_b5cblonbp_product_product)) * ff_v_b5cblonbp_product_product)) /\ exists ff_q_b5cblonbp_product_product_successor. ff_u_b5cblonbp_product_product = ff_q_b5cblonbp_product_product_successor * S ((S (S ff_i_b5cblonbp_product_product)) * ff_v_b5cblonbp_product_product) + (ff_s_b5cblonbp_product_product))) /\ ff_s_b5cblonbp_product_product = ff_r_b5cblonbp_product_product * ff_p_b5cblonbp_product_product)))))))) /\ C = z - 0028
specialize central_binom_prime_contribution_product_exists n - 0029
specialize central_binom_prime_contribution_product_exists C - 0030
apply central_binom_prime_contribution_product_exists - 0031
exact hcentral - 0032
cases hproduct - 0033
cases hproduct_witness - 0034
have hfactorization : ∃ u. ∃ v. (∃ y. ∃ z. (∀ n. Lt(n,s) → ∃ m. BetaAt(y,z,n,m) ∧ (Prime(S n) ∧ (∃ k. PowerValuation(S n,C,k) ∧ Pow(S n,k,m)) ∨ ¬Prime(S n) ∧ m = 1)) ∧ Product(y,z,s,u)) ∧ ((∃ y. ∃ z. (∀ n. Lt(n,x) → ∃ m. BetaAt(y,z,n,m) ∧ (Prime(S (s + n)) ∧ (∃ k. PowerValuation(S (s + n),C,k) ∧ Pow(S (s + n),k,m)) ∨ ¬Prime(S (s + n)) ∧ m = 1)) ∧ Product(y,z,x,v)) ∧ x2 = u · v)Exact native replay line
have hfactorization : exists u v. (exists bpr_product_code_b5cblonbp_small bpr_product_scale_b5cblonbp_small. ((forall bpr_prefix_index_b5cblonbp_small_prefix. (exists bpr_gap_b5cblonbp_small_prefix_bound. bpr_gap_b5cblonbp_small_prefix_bound + S (bpr_prefix_index_b5cblonbp_small_prefix) = s) -> exists bpr_prefix_value_b5cblonbp_small_prefix. ((((exists bpr_height_b5cblonbp_small_prefix_decoded. bpr_height_b5cblonbp_small_prefix_decoded + S (bpr_prefix_value_b5cblonbp_small_prefix) = S ((S (bpr_prefix_index_b5cblonbp_small_prefix)) * bpr_product_scale_b5cblonbp_small)) /\ exists bpr_quotient_b5cblonbp_small_prefix_decoded. bpr_product_code_b5cblonbp_small = bpr_quotient_b5cblonbp_small_prefix_decoded * S ((S (bpr_prefix_index_b5cblonbp_small_prefix)) * bpr_product_scale_b5cblonbp_small) + (bpr_prefix_value_b5cblonbp_small_prefix))) /\ (((((~(S (bpr_prefix_index_b5cblonbp_small_prefix) = 1) /\ forall bpr_left_b5cblonbp_small_prefix_choice_prime bpr_right_b5cblonbp_small_prefix_choice_prime. S (bpr_prefix_index_b5cblonbp_small_prefix) = bpr_left_b5cblonbp_small_prefix_choice_prime * bpr_right_b5cblonbp_small_prefix_choice_prime -> bpr_left_b5cblonbp_small_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_small_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_b5cblonbp_small_prefix_choice. ((((exists bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_selected_bound. bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_b5cblonbp_small_prefix_choice) = (C)) /\ (exists bpr_power_value_b5cblonbp_small_prefix_choice_valuation_selected. ((exists bpr_power_code_b5cblonbp_small_prefix_choice_valuation_selected_power bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power. ((forall bpr_power_index_b5cblonbp_small_prefix_choice_valuation_selected_power. (exists bpr_gap_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_selected_power) = bpr_choice_exponent_b5cblonbp_small_prefix_choice) -> (((exists bpr_height_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_small_prefix)) = S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_b5cblonbp_small_prefix_choice_valuation_selected_power = bpr_quotient_b5cblonbp_small_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_b5cblonbp_small_prefix))))) /\ (exists ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_start. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_start. ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_terminal. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_b5cblonbp_small_prefix_choice)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_terminal. ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_small_prefix_choice)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product) + (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_selected))) /\ forall ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product. (exists ff_lt_b5cblonbp_small_prefix_choice_valuation_selected_power_product_bound. ff_lt_b5cblonbp_small_prefix_choice_valuation_selected_power_product_bound + S ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_b5cblonbp_small_prefix_choice) -> exists ff_p_b5cblonbp_small_prefix_choice_valuation_selected_power_product ff_r_b5cblonbp_small_prefix_choice_valuation_selected_power_product ff_s_b5cblonbp_small_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_factor. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_factor + S (ff_p_b5cblonbp_small_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_b5cblonbp_small_prefix_choice_valuation_selected_power = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_selected_power) + (ff_p_b5cblonbp_small_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_partial. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_partial + S (ff_r_b5cblonbp_small_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_partial. ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product) + (ff_r_b5cblonbp_small_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_successor. ff_h_b5cblonbp_small_prefix_choice_valuation_selected_power_product_successor + S (ff_s_b5cblonbp_small_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_successor. ff_u_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_b5cblonbp_small_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_selected_power_product) + (ff_s_b5cblonbp_small_prefix_choice_valuation_selected_power_product))) /\ ff_s_b5cblonbp_small_prefix_choice_valuation_selected_power_product = ff_r_b5cblonbp_small_prefix_choice_valuation_selected_power_product * ff_p_b5cblonbp_small_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_small_prefix_choice_valuation_selected_divides. C = (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_selected) * bpr_divides_quotient_b5cblonbp_small_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation. (exists bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_candidate_bound. bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation) = (C)) -> (exists bpr_power_value_b5cblonbp_small_prefix_choice_valuation_candidate. ((exists bpr_power_code_b5cblonbp_small_prefix_choice_valuation_candidate_power bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_b5cblonbp_small_prefix_choice_valuation_candidate_power. (exists bpr_gap_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation) -> (((exists bpr_height_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_small_prefix)) = S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_b5cblonbp_small_prefix_choice_valuation_candidate_power = bpr_quotient_b5cblonbp_small_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_b5cblonbp_small_prefix))))) /\ (exists ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_start. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_start. ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_terminal. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_terminal. ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_candidate))) /\ forall ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product. (exists ff_lt_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_bound. ff_lt_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_bound + S ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation) -> exists ff_p_b5cblonbp_small_prefix_choice_valuation_candidate_power_product ff_r_b5cblonbp_small_prefix_choice_valuation_candidate_power_product ff_s_b5cblonbp_small_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_factor. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_b5cblonbp_small_prefix_choice_valuation_candidate_power = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_valuation_candidate_power) + (ff_p_b5cblonbp_small_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_partial. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_partial. ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) + (ff_r_b5cblonbp_small_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_successor. ff_h_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_successor. ff_u_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_small_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_small_prefix_choice_valuation_candidate_power_product) + (ff_s_b5cblonbp_small_prefix_choice_valuation_candidate_power_product))) /\ ff_s_b5cblonbp_small_prefix_choice_valuation_candidate_power_product = ff_r_b5cblonbp_small_prefix_choice_valuation_candidate_power_product * ff_p_b5cblonbp_small_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_small_prefix_choice_valuation_candidate_divides. C = (bpr_power_value_b5cblonbp_small_prefix_choice_valuation_candidate) * bpr_divides_quotient_b5cblonbp_small_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_candidate_below. bpr_le_gap_b5cblonbp_small_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_b5cblonbp_small_prefix_choice_valuation) = (bpr_choice_exponent_b5cblonbp_small_prefix_choice))) /\ (exists bpr_power_code_b5cblonbp_small_prefix_choice_power bpr_power_scale_b5cblonbp_small_prefix_choice_power. ((forall bpr_power_index_b5cblonbp_small_prefix_choice_power. (exists bpr_gap_b5cblonbp_small_prefix_choice_power_repeat_bound. bpr_gap_b5cblonbp_small_prefix_choice_power_repeat_bound + S (bpr_power_index_b5cblonbp_small_prefix_choice_power) = bpr_choice_exponent_b5cblonbp_small_prefix_choice) -> (((exists bpr_height_b5cblonbp_small_prefix_choice_power_repeat_entry. bpr_height_b5cblonbp_small_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_b5cblonbp_small_prefix)) = S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_power)) /\ exists bpr_quotient_b5cblonbp_small_prefix_choice_power_repeat_entry. bpr_power_code_b5cblonbp_small_prefix_choice_power = bpr_quotient_b5cblonbp_small_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_small_prefix_choice_power)) * bpr_power_scale_b5cblonbp_small_prefix_choice_power) + (S (bpr_prefix_index_b5cblonbp_small_prefix))))) /\ (exists ff_u_b5cblonbp_small_prefix_choice_power_product ff_v_b5cblonbp_small_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_start. ff_h_b5cblonbp_small_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_start. ff_u_b5cblonbp_small_prefix_choice_power_product = ff_q_b5cblonbp_small_prefix_choice_power_product_start * S ((S (0)) * ff_v_b5cblonbp_small_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_terminal. ff_h_b5cblonbp_small_prefix_choice_power_product_terminal + S (bpr_prefix_value_b5cblonbp_small_prefix) = S ((S (bpr_choice_exponent_b5cblonbp_small_prefix_choice)) * ff_v_b5cblonbp_small_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_terminal. ff_u_b5cblonbp_small_prefix_choice_power_product = ff_q_b5cblonbp_small_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_small_prefix_choice)) * ff_v_b5cblonbp_small_prefix_choice_power_product) + (bpr_prefix_value_b5cblonbp_small_prefix))) /\ forall ff_i_b5cblonbp_small_prefix_choice_power_product. (exists ff_lt_b5cblonbp_small_prefix_choice_power_product_bound. ff_lt_b5cblonbp_small_prefix_choice_power_product_bound + S ff_i_b5cblonbp_small_prefix_choice_power_product = bpr_choice_exponent_b5cblonbp_small_prefix_choice) -> exists ff_p_b5cblonbp_small_prefix_choice_power_product ff_r_b5cblonbp_small_prefix_choice_power_product ff_s_b5cblonbp_small_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_factor. ff_h_b5cblonbp_small_prefix_choice_power_product_factor + S (ff_p_b5cblonbp_small_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_power)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_factor. bpr_power_code_b5cblonbp_small_prefix_choice_power = ff_q_b5cblonbp_small_prefix_choice_power_product_factor * S ((S (ff_i_b5cblonbp_small_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_small_prefix_choice_power) + (ff_p_b5cblonbp_small_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_partial. ff_h_b5cblonbp_small_prefix_choice_power_product_partial + S (ff_r_b5cblonbp_small_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_small_prefix_choice_power_product)) * ff_v_b5cblonbp_small_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_partial. ff_u_b5cblonbp_small_prefix_choice_power_product = ff_q_b5cblonbp_small_prefix_choice_power_product_partial * S ((S (ff_i_b5cblonbp_small_prefix_choice_power_product)) * ff_v_b5cblonbp_small_prefix_choice_power_product) + (ff_r_b5cblonbp_small_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_small_prefix_choice_power_product_successor. ff_h_b5cblonbp_small_prefix_choice_power_product_successor + S (ff_s_b5cblonbp_small_prefix_choice_power_product) = S ((S (S ff_i_b5cblonbp_small_prefix_choice_power_product)) * ff_v_b5cblonbp_small_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_small_prefix_choice_power_product_successor. ff_u_b5cblonbp_small_prefix_choice_power_product = ff_q_b5cblonbp_small_prefix_choice_power_product_successor * S ((S (S ff_i_b5cblonbp_small_prefix_choice_power_product)) * ff_v_b5cblonbp_small_prefix_choice_power_product) + (ff_s_b5cblonbp_small_prefix_choice_power_product))) /\ ff_s_b5cblonbp_small_prefix_choice_power_product = ff_r_b5cblonbp_small_prefix_choice_power_product * ff_p_b5cblonbp_small_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_b5cblonbp_small_prefix) = 1) /\ forall bpr_left_b5cblonbp_small_prefix_choice_prime bpr_right_b5cblonbp_small_prefix_choice_prime. S (bpr_prefix_index_b5cblonbp_small_prefix) = bpr_left_b5cblonbp_small_prefix_choice_prime * bpr_right_b5cblonbp_small_prefix_choice_prime -> bpr_left_b5cblonbp_small_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_small_prefix_choice_prime = 1)) /\ bpr_prefix_value_b5cblonbp_small_prefix = 1))))) /\ (exists ff_u_b5cblonbp_small_product ff_v_b5cblonbp_small_product. ((((exists ff_h_b5cblonbp_small_product_start. ff_h_b5cblonbp_small_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_small_product)) /\ exists ff_q_b5cblonbp_small_product_start. ff_u_b5cblonbp_small_product = ff_q_b5cblonbp_small_product_start * S ((S (0)) * ff_v_b5cblonbp_small_product) + (1))) /\ ((((exists ff_h_b5cblonbp_small_product_terminal. ff_h_b5cblonbp_small_product_terminal + S (u) = S ((S (s)) * ff_v_b5cblonbp_small_product)) /\ exists ff_q_b5cblonbp_small_product_terminal. ff_u_b5cblonbp_small_product = ff_q_b5cblonbp_small_product_terminal * S ((S (s)) * ff_v_b5cblonbp_small_product) + (u))) /\ forall ff_i_b5cblonbp_small_product. (exists ff_lt_b5cblonbp_small_product_bound. ff_lt_b5cblonbp_small_product_bound + S ff_i_b5cblonbp_small_product = s) -> exists ff_p_b5cblonbp_small_product ff_r_b5cblonbp_small_product ff_s_b5cblonbp_small_product. ((((exists ff_h_b5cblonbp_small_product_factor. ff_h_b5cblonbp_small_product_factor + S (ff_p_b5cblonbp_small_product) = S ((S (ff_i_b5cblonbp_small_product)) * bpr_product_scale_b5cblonbp_small)) /\ exists ff_q_b5cblonbp_small_product_factor. bpr_product_code_b5cblonbp_small = ff_q_b5cblonbp_small_product_factor * S ((S (ff_i_b5cblonbp_small_product)) * bpr_product_scale_b5cblonbp_small) + (ff_p_b5cblonbp_small_product))) /\ ((((exists ff_h_b5cblonbp_small_product_partial. ff_h_b5cblonbp_small_product_partial + S (ff_r_b5cblonbp_small_product) = S ((S (ff_i_b5cblonbp_small_product)) * ff_v_b5cblonbp_small_product)) /\ exists ff_q_b5cblonbp_small_product_partial. ff_u_b5cblonbp_small_product = ff_q_b5cblonbp_small_product_partial * S ((S (ff_i_b5cblonbp_small_product)) * ff_v_b5cblonbp_small_product) + (ff_r_b5cblonbp_small_product))) /\ ((((exists ff_h_b5cblonbp_small_product_successor. ff_h_b5cblonbp_small_product_successor + S (ff_s_b5cblonbp_small_product) = S ((S (S ff_i_b5cblonbp_small_product)) * ff_v_b5cblonbp_small_product)) /\ exists ff_q_b5cblonbp_small_product_successor. ff_u_b5cblonbp_small_product = ff_q_b5cblonbp_small_product_successor * S ((S (S ff_i_b5cblonbp_small_product)) * ff_v_b5cblonbp_small_product) + (ff_s_b5cblonbp_small_product))) /\ ff_s_b5cblonbp_small_product = ff_r_b5cblonbp_small_product * ff_p_b5cblonbp_small_product)))))))) /\ ((exists bpr_code_b5cblonbp_middle bpr_scale_b5cblonbp_middle. ((forall bpr_index_b5cblonbp_middle_prefix. (exists bpr_gap_b5cblonbp_middle_prefix_bound. bpr_gap_b5cblonbp_middle_prefix_bound + S (bpr_index_b5cblonbp_middle_prefix) = x) -> exists bpr_value_b5cblonbp_middle_prefix. ((((exists bpr_height_b5cblonbp_middle_prefix_decoded. bpr_height_b5cblonbp_middle_prefix_decoded + S (bpr_value_b5cblonbp_middle_prefix) = S ((S (bpr_index_b5cblonbp_middle_prefix)) * bpr_scale_b5cblonbp_middle)) /\ exists bpr_quotient_b5cblonbp_middle_prefix_decoded. bpr_code_b5cblonbp_middle = bpr_quotient_b5cblonbp_middle_prefix_decoded * S ((S (bpr_index_b5cblonbp_middle_prefix)) * bpr_scale_b5cblonbp_middle) + (bpr_value_b5cblonbp_middle_prefix))) /\ (((((~(S (s + bpr_index_b5cblonbp_middle_prefix) = 1) /\ forall bpr_left_b5cblonbp_middle_prefix_choice_prime bpr_right_b5cblonbp_middle_prefix_choice_prime. S (s + bpr_index_b5cblonbp_middle_prefix) = bpr_left_b5cblonbp_middle_prefix_choice_prime * bpr_right_b5cblonbp_middle_prefix_choice_prime -> bpr_left_b5cblonbp_middle_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_middle_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_b5cblonbp_middle_prefix_choice. ((((exists bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_selected_bound. bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_b5cblonbp_middle_prefix_choice) = (C)) /\ (exists bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_selected. ((exists bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_selected_power bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power. ((forall bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_selected_power. (exists bpr_gap_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_selected_power) = bpr_choice_exponent_b5cblonbp_middle_prefix_choice) -> (((exists bpr_height_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_entry + S (S (s + bpr_index_b5cblonbp_middle_prefix)) = S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_selected_power = bpr_quotient_b5cblonbp_middle_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_selected_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power) + (S (s + bpr_index_b5cblonbp_middle_prefix))))) /\ (exists ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_start. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_start. ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_terminal. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_b5cblonbp_middle_prefix_choice)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_terminal. ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_middle_prefix_choice)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) + (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_selected))) /\ forall ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product. (exists ff_lt_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_bound. ff_lt_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_bound + S ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_b5cblonbp_middle_prefix_choice) -> exists ff_p_b5cblonbp_middle_prefix_choice_valuation_selected_power_product ff_r_b5cblonbp_middle_prefix_choice_valuation_selected_power_product ff_s_b5cblonbp_middle_prefix_choice_valuation_selected_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_factor. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_factor + S (ff_p_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_selected_power = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_selected_power) + (ff_p_b5cblonbp_middle_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_partial. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_partial + S (ff_r_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_partial. ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) + (ff_r_b5cblonbp_middle_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_successor. ff_h_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_successor + S (ff_s_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_successor. ff_u_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_selected_power_product) + (ff_s_b5cblonbp_middle_prefix_choice_valuation_selected_power_product))) /\ ff_s_b5cblonbp_middle_prefix_choice_valuation_selected_power_product = ff_r_b5cblonbp_middle_prefix_choice_valuation_selected_power_product * ff_p_b5cblonbp_middle_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_middle_prefix_choice_valuation_selected_divides. C = (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_selected) * bpr_divides_quotient_b5cblonbp_middle_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation. (exists bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_bound. bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation) = (C)) -> (exists bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_candidate. ((exists bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_candidate_power bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_candidate_power. (exists bpr_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation) -> (((exists bpr_height_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_entry + S (S (s + bpr_index_b5cblonbp_middle_prefix)) = S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_candidate_power = bpr_quotient_b5cblonbp_middle_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_valuation_candidate_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power) + (S (s + bpr_index_b5cblonbp_middle_prefix))))) /\ (exists ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_start. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_start. ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_terminal. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_terminal. ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_candidate))) /\ forall ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product. (exists ff_lt_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_bound. ff_lt_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_bound + S ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation) -> exists ff_p_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product ff_r_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product ff_s_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_factor. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_b5cblonbp_middle_prefix_choice_valuation_candidate_power = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_valuation_candidate_power) + (ff_p_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_partial. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_partial. ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) + (ff_r_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_successor. ff_h_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_successor. ff_u_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_q_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product) + (ff_s_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product))) /\ ff_s_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product = ff_r_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product * ff_p_b5cblonbp_middle_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_b5cblonbp_middle_prefix_choice_valuation_candidate_divides. C = (bpr_power_value_b5cblonbp_middle_prefix_choice_valuation_candidate) * bpr_divides_quotient_b5cblonbp_middle_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_below. bpr_le_gap_b5cblonbp_middle_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_b5cblonbp_middle_prefix_choice_valuation) = (bpr_choice_exponent_b5cblonbp_middle_prefix_choice))) /\ (exists bpr_power_code_b5cblonbp_middle_prefix_choice_power bpr_power_scale_b5cblonbp_middle_prefix_choice_power. ((forall bpr_power_index_b5cblonbp_middle_prefix_choice_power. (exists bpr_gap_b5cblonbp_middle_prefix_choice_power_repeat_bound. bpr_gap_b5cblonbp_middle_prefix_choice_power_repeat_bound + S (bpr_power_index_b5cblonbp_middle_prefix_choice_power) = bpr_choice_exponent_b5cblonbp_middle_prefix_choice) -> (((exists bpr_height_b5cblonbp_middle_prefix_choice_power_repeat_entry. bpr_height_b5cblonbp_middle_prefix_choice_power_repeat_entry + S (S (s + bpr_index_b5cblonbp_middle_prefix)) = S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_power)) /\ exists bpr_quotient_b5cblonbp_middle_prefix_choice_power_repeat_entry. bpr_power_code_b5cblonbp_middle_prefix_choice_power = bpr_quotient_b5cblonbp_middle_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_b5cblonbp_middle_prefix_choice_power)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_power) + (S (s + bpr_index_b5cblonbp_middle_prefix))))) /\ (exists ff_u_b5cblonbp_middle_prefix_choice_power_product ff_v_b5cblonbp_middle_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_start. ff_h_b5cblonbp_middle_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_start. ff_u_b5cblonbp_middle_prefix_choice_power_product = ff_q_b5cblonbp_middle_prefix_choice_power_product_start * S ((S (0)) * ff_v_b5cblonbp_middle_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_terminal. ff_h_b5cblonbp_middle_prefix_choice_power_product_terminal + S (bpr_value_b5cblonbp_middle_prefix) = S ((S (bpr_choice_exponent_b5cblonbp_middle_prefix_choice)) * ff_v_b5cblonbp_middle_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_terminal. ff_u_b5cblonbp_middle_prefix_choice_power_product = ff_q_b5cblonbp_middle_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_b5cblonbp_middle_prefix_choice)) * ff_v_b5cblonbp_middle_prefix_choice_power_product) + (bpr_value_b5cblonbp_middle_prefix))) /\ forall ff_i_b5cblonbp_middle_prefix_choice_power_product. (exists ff_lt_b5cblonbp_middle_prefix_choice_power_product_bound. ff_lt_b5cblonbp_middle_prefix_choice_power_product_bound + S ff_i_b5cblonbp_middle_prefix_choice_power_product = bpr_choice_exponent_b5cblonbp_middle_prefix_choice) -> exists ff_p_b5cblonbp_middle_prefix_choice_power_product ff_r_b5cblonbp_middle_prefix_choice_power_product ff_s_b5cblonbp_middle_prefix_choice_power_product. ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_factor. ff_h_b5cblonbp_middle_prefix_choice_power_product_factor + S (ff_p_b5cblonbp_middle_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_power)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_factor. bpr_power_code_b5cblonbp_middle_prefix_choice_power = ff_q_b5cblonbp_middle_prefix_choice_power_product_factor * S ((S (ff_i_b5cblonbp_middle_prefix_choice_power_product)) * bpr_power_scale_b5cblonbp_middle_prefix_choice_power) + (ff_p_b5cblonbp_middle_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_partial. ff_h_b5cblonbp_middle_prefix_choice_power_product_partial + S (ff_r_b5cblonbp_middle_prefix_choice_power_product) = S ((S (ff_i_b5cblonbp_middle_prefix_choice_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_partial. ff_u_b5cblonbp_middle_prefix_choice_power_product = ff_q_b5cblonbp_middle_prefix_choice_power_product_partial * S ((S (ff_i_b5cblonbp_middle_prefix_choice_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_power_product) + (ff_r_b5cblonbp_middle_prefix_choice_power_product))) /\ ((((exists ff_h_b5cblonbp_middle_prefix_choice_power_product_successor. ff_h_b5cblonbp_middle_prefix_choice_power_product_successor + S (ff_s_b5cblonbp_middle_prefix_choice_power_product) = S ((S (S ff_i_b5cblonbp_middle_prefix_choice_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_power_product)) /\ exists ff_q_b5cblonbp_middle_prefix_choice_power_product_successor. ff_u_b5cblonbp_middle_prefix_choice_power_product = ff_q_b5cblonbp_middle_prefix_choice_power_product_successor * S ((S (S ff_i_b5cblonbp_middle_prefix_choice_power_product)) * ff_v_b5cblonbp_middle_prefix_choice_power_product) + (ff_s_b5cblonbp_middle_prefix_choice_power_product))) /\ ff_s_b5cblonbp_middle_prefix_choice_power_product = ff_r_b5cblonbp_middle_prefix_choice_power_product * ff_p_b5cblonbp_middle_prefix_choice_power_product)))))))))) \/ (~((~(S (s + bpr_index_b5cblonbp_middle_prefix) = 1) /\ forall bpr_left_b5cblonbp_middle_prefix_choice_prime bpr_right_b5cblonbp_middle_prefix_choice_prime. S (s + bpr_index_b5cblonbp_middle_prefix) = bpr_left_b5cblonbp_middle_prefix_choice_prime * bpr_right_b5cblonbp_middle_prefix_choice_prime -> bpr_left_b5cblonbp_middle_prefix_choice_prime = 1 \/ bpr_right_b5cblonbp_middle_prefix_choice_prime = 1)) /\ bpr_value_b5cblonbp_middle_prefix = 1))))) /\ (exists ff_u_b5cblonbp_middle_product ff_v_b5cblonbp_middle_product. ((((exists ff_h_b5cblonbp_middle_product_start. ff_h_b5cblonbp_middle_product_start + S (1) = S ((S (0)) * ff_v_b5cblonbp_middle_product)) /\ exists ff_q_b5cblonbp_middle_product_start. ff_u_b5cblonbp_middle_product = ff_q_b5cblonbp_middle_product_start * S ((S (0)) * ff_v_b5cblonbp_middle_product) + (1))) /\ ((((exists ff_h_b5cblonbp_middle_product_terminal. ff_h_b5cblonbp_middle_product_terminal + S (v) = S ((S (x)) * ff_v_b5cblonbp_middle_product)) /\ exists ff_q_b5cblonbp_middle_product_terminal. ff_u_b5cblonbp_middle_product = ff_q_b5cblonbp_middle_product_terminal * S ((S (x)) * ff_v_b5cblonbp_middle_product) + (v))) /\ forall ff_i_b5cblonbp_middle_product. (exists ff_lt_b5cblonbp_middle_product_bound. ff_lt_b5cblonbp_middle_product_bound + S ff_i_b5cblonbp_middle_product = x) -> exists ff_p_b5cblonbp_middle_product ff_r_b5cblonbp_middle_product ff_s_b5cblonbp_middle_product. ((((exists ff_h_b5cblonbp_middle_product_factor. ff_h_b5cblonbp_middle_product_factor + S (ff_p_b5cblonbp_middle_product) = S ((S (ff_i_b5cblonbp_middle_product)) * bpr_scale_b5cblonbp_middle)) /\ exists ff_q_b5cblonbp_middle_product_factor. bpr_code_b5cblonbp_middle = ff_q_b5cblonbp_middle_product_factor * S ((S (ff_i_b5cblonbp_middle_product)) * bpr_scale_b5cblonbp_middle) + (ff_p_b5cblonbp_middle_product))) /\ ((((exists ff_h_b5cblonbp_middle_product_partial. ff_h_b5cblonbp_middle_product_partial + S (ff_r_b5cblonbp_middle_product) = S ((S (ff_i_b5cblonbp_middle_product)) * ff_v_b5cblonbp_middle_product)) /\ exists ff_q_b5cblonbp_middle_product_partial. ff_u_b5cblonbp_middle_product = ff_q_b5cblonbp_middle_product_partial * S ((S (ff_i_b5cblonbp_middle_product)) * ff_v_b5cblonbp_middle_product) + (ff_r_b5cblonbp_middle_product))) /\ ((((exists ff_h_b5cblonbp_middle_product_successor. ff_h_b5cblonbp_middle_product_successor + S (ff_s_b5cblonbp_middle_product) = S ((S (S ff_i_b5cblonbp_middle_product)) * ff_v_b5cblonbp_middle_product)) /\ exists ff_q_b5cblonbp_middle_product_successor. ff_u_b5cblonbp_middle_product = ff_q_b5cblonbp_middle_product_successor * S ((S (S ff_i_b5cblonbp_middle_product)) * ff_v_b5cblonbp_middle_product) + (ff_s_b5cblonbp_middle_product))) /\ ff_s_b5cblonbp_middle_product = ff_r_b5cblonbp_middle_product * ff_p_b5cblonbp_middle_product)))))))) /\ x2 = u * v) - 0035
specialize central_binom_factorization_small n - 0036
specialize central_binom_factorization_small s - 0037
specialize central_binom_factorization_small q - 0038
specialize central_binom_factorization_small r - 0039
specialize central_binom_factorization_small C - 0040
specialize central_binom_factorization_small x - 0041
specialize central_binom_factorization_small x1 - 0042
specialize central_binom_factorization_small x2 - 0043
apply central_binom_factorization_small - 0044
exact hexclusion - 0045
exact hpositive - 0046
exact hfloor - 0047
exact hdivision - 0048
exact hcentral - 0049
exact hgaps_witness_witness_left - 0050
exact hgaps_witness_witness_right - 0051
exact hproduct_witness_left - 0052
cases hfactorization - 0053
cases hfactorization_witness - 0054
cases hfactorization_witness_witness - 0055
cases hfactorization_witness_witness_right - 0056
have hsmall : Le(x3,A)Exact native replay line
have hsmall : exists bcf_le_gap_b5cblonbp_x_a. bcf_le_gap_b5cblonbp_x_a + (x3) = A - 0057
specialize no_bertrand_small_contribution_product_le_power n - 0058
specialize no_bertrand_small_contribution_product_le_power s - 0059
specialize no_bertrand_small_contribution_product_le_power q - 0060
specialize no_bertrand_small_contribution_product_le_power r - 0061
specialize no_bertrand_small_contribution_product_le_power C - 0062
specialize no_bertrand_small_contribution_product_le_power x3 - 0063
specialize no_bertrand_small_contribution_product_le_power A - 0064
apply no_bertrand_small_contribution_product_le_power - 0065
exact hexclusion - 0066
exact hpositive - 0067
exact hfloor - 0068
exact hdivision - 0069
exact hcentral - 0070
exact hfactorization_witness_witness_left - 0071
exact hpower_a - 0072
have hmiddle : Le(x4,B)Exact native replay line
have hmiddle : exists bcf_le_gap_b5cblonbp_y_b. bcf_le_gap_b5cblonbp_y_b + (x4) = B - 0073
specialize no_bertrand_middle_contribution_interval_le_four_pow n - 0074
specialize no_bertrand_middle_contribution_interval_le_four_pow s - 0075
specialize no_bertrand_middle_contribution_interval_le_four_pow q - 0076
specialize no_bertrand_middle_contribution_interval_le_four_pow r - 0077
specialize no_bertrand_middle_contribution_interval_le_four_pow C - 0078
specialize no_bertrand_middle_contribution_interval_le_four_pow x - 0079
specialize no_bertrand_middle_contribution_interval_le_four_pow x4 - 0080
specialize no_bertrand_middle_contribution_interval_le_four_pow B - 0081
apply no_bertrand_middle_contribution_interval_le_four_pow - 0082
exact hexclusion - 0083
exact hpositive - 0084
exact hfloor - 0085
exact hdivision - 0086
exact hcentral - 0087
exact hgaps_witness_witness_left - 0088
exact hfactorization_witness_witness_right_left - 0089
exact hpower_b - 0090
have hproduct_bound : Le(x3 · x4,A · B)Exact native replay line
have hproduct_bound : exists bcf_le_gap_b5cblonbp_product_bound. bcf_le_gap_b5cblonbp_product_bound + (x3 * x4) = A * B - 0091
specialize mul_le_mul x3 - 0092
specialize mul_le_mul A - 0093
specialize mul_le_mul x4 - 0094
specialize mul_le_mul B - 0095
apply mul_le_mul - 0096
exact hsmall - 0097
exact hmiddle - 0098
rewrite hproduct_witness_right - 0099
rewrite hfactorization_witness_witness_right_right - 0100
exact hproduct_bound