BT00YP

prime_contribution_prefix_extend

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Append one contribution while preserving the old prefix.

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.

Exact expanded PA statement

forall n b c m. (forall bpr_prefix_index_bpcpe_before. (exists bpr_gap_bpcpe_before_bound. bpr_gap_bpcpe_before_bound + S (bpr_prefix_index_bpcpe_before) = m) -> exists bpr_prefix_value_bpcpe_before. ((((exists bpr_height_bpcpe_before_decoded. bpr_height_bpcpe_before_decoded + S (bpr_prefix_value_bpcpe_before) = S ((S (bpr_prefix_index_bpcpe_before)) * c)) /\ exists bpr_quotient_bpcpe_before_decoded. b = bpr_quotient_bpcpe_before_decoded * S ((S (bpr_prefix_index_bpcpe_before)) * c) + (bpr_prefix_value_bpcpe_before))) /\ (((((~(S (bpr_prefix_index_bpcpe_before) = 1) /\ forall bpr_left_bpcpe_before_choice_prime bpr_right_bpcpe_before_choice_prime. S (bpr_prefix_index_bpcpe_before) = bpr_left_bpcpe_before_choice_prime * bpr_right_bpcpe_before_choice_prime -> bpr_left_bpcpe_before_choice_prime = 1 \/ bpr_right_bpcpe_before_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpe_before_choice. ((((exists bpr_le_gap_bpcpe_before_choice_valuation_selected_bound. bpr_le_gap_bpcpe_before_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpe_before_choice) = (n)) /\ (exists bpr_power_value_bpcpe_before_choice_valuation_selected. ((exists bpr_power_code_bpcpe_before_choice_valuation_selected_power bpr_power_scale_bpcpe_before_choice_valuation_selected_power. ((forall bpr_power_index_bpcpe_before_choice_valuation_selected_power. (exists bpr_gap_bpcpe_before_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpe_before_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpe_before_choice_valuation_selected_power) = bpr_choice_exponent_bpcpe_before_choice) -> (((exists bpr_height_bpcpe_before_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpe_before_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpe_before)) = S ((S (bpr_power_index_bpcpe_before_choice_valuation_selected_power)) * bpr_power_scale_bpcpe_before_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpe_before_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpe_before_choice_valuation_selected_power = bpr_quotient_bpcpe_before_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpe_before_choice_valuation_selected_power)) * bpr_power_scale_bpcpe_before_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpe_before))))) /\ (exists ff_u_bpcpe_before_choice_valuation_selected_power_product ff_v_bpcpe_before_choice_valuation_selected_power_product. ((((exists ff_h_bpcpe_before_choice_valuation_selected_power_product_start. ff_h_bpcpe_before_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_before_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_before_choice_valuation_selected_power_product_start. ff_u_bpcpe_before_choice_valuation_selected_power_product = ff_q_bpcpe_before_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpe_before_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpe_before_choice_valuation_selected_power_product_terminal. ff_h_bpcpe_before_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpe_before_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpe_before_choice)) * ff_v_bpcpe_before_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_before_choice_valuation_selected_power_product_terminal. ff_u_bpcpe_before_choice_valuation_selected_power_product = ff_q_bpcpe_before_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpe_before_choice)) * ff_v_bpcpe_before_choice_valuation_selected_power_product) + (bpr_power_value_bpcpe_before_choice_valuation_selected))) /\ forall ff_i_bpcpe_before_choice_valuation_selected_power_product. (exists ff_lt_bpcpe_before_choice_valuation_selected_power_product_bound. ff_lt_bpcpe_before_choice_valuation_selected_power_product_bound + S ff_i_bpcpe_before_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpe_before_choice) -> exists ff_p_bpcpe_before_choice_valuation_selected_power_product ff_r_bpcpe_before_choice_valuation_selected_power_product ff_s_bpcpe_before_choice_valuation_selected_power_product. ((((exists ff_h_bpcpe_before_choice_valuation_selected_power_product_factor. ff_h_bpcpe_before_choice_valuation_selected_power_product_factor + S (ff_p_bpcpe_before_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpe_before_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpe_before_choice_valuation_selected_power)) /\ exists ff_q_bpcpe_before_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpe_before_choice_valuation_selected_power = ff_q_bpcpe_before_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpe_before_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpe_before_choice_valuation_selected_power) + (ff_p_bpcpe_before_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpe_before_choice_valuation_selected_power_product_partial. ff_h_bpcpe_before_choice_valuation_selected_power_product_partial + S (ff_r_bpcpe_before_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpe_before_choice_valuation_selected_power_product)) * ff_v_bpcpe_before_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_before_choice_valuation_selected_power_product_partial. ff_u_bpcpe_before_choice_valuation_selected_power_product = ff_q_bpcpe_before_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpe_before_choice_valuation_selected_power_product)) * ff_v_bpcpe_before_choice_valuation_selected_power_product) + (ff_r_bpcpe_before_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpe_before_choice_valuation_selected_power_product_successor. ff_h_bpcpe_before_choice_valuation_selected_power_product_successor + S (ff_s_bpcpe_before_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpe_before_choice_valuation_selected_power_product)) * ff_v_bpcpe_before_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_before_choice_valuation_selected_power_product_successor. ff_u_bpcpe_before_choice_valuation_selected_power_product = ff_q_bpcpe_before_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpe_before_choice_valuation_selected_power_product)) * ff_v_bpcpe_before_choice_valuation_selected_power_product) + (ff_s_bpcpe_before_choice_valuation_selected_power_product))) /\ ff_s_bpcpe_before_choice_valuation_selected_power_product = ff_r_bpcpe_before_choice_valuation_selected_power_product * ff_p_bpcpe_before_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpe_before_choice_valuation_selected_divides. n = (bpr_power_value_bpcpe_before_choice_valuation_selected) * bpr_divides_quotient_bpcpe_before_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpe_before_choice_valuation. (exists bpr_le_gap_bpcpe_before_choice_valuation_candidate_bound. bpr_le_gap_bpcpe_before_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpe_before_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpe_before_choice_valuation_candidate. ((exists bpr_power_code_bpcpe_before_choice_valuation_candidate_power bpr_power_scale_bpcpe_before_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpe_before_choice_valuation_candidate_power. (exists bpr_gap_bpcpe_before_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpe_before_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpe_before_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpe_before_choice_valuation) -> (((exists bpr_height_bpcpe_before_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpe_before_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpe_before)) = S ((S (bpr_power_index_bpcpe_before_choice_valuation_candidate_power)) * bpr_power_scale_bpcpe_before_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpe_before_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpe_before_choice_valuation_candidate_power = bpr_quotient_bpcpe_before_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpe_before_choice_valuation_candidate_power)) * bpr_power_scale_bpcpe_before_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpe_before))))) /\ (exists ff_u_bpcpe_before_choice_valuation_candidate_power_product ff_v_bpcpe_before_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpe_before_choice_valuation_candidate_power_product_start. ff_h_bpcpe_before_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_before_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_before_choice_valuation_candidate_power_product_start. ff_u_bpcpe_before_choice_valuation_candidate_power_product = ff_q_bpcpe_before_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpe_before_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpe_before_choice_valuation_candidate_power_product_terminal. ff_h_bpcpe_before_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpe_before_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpe_before_choice_valuation)) * ff_v_bpcpe_before_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_before_choice_valuation_candidate_power_product_terminal. ff_u_bpcpe_before_choice_valuation_candidate_power_product = ff_q_bpcpe_before_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpe_before_choice_valuation)) * ff_v_bpcpe_before_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpe_before_choice_valuation_candidate))) /\ forall ff_i_bpcpe_before_choice_valuation_candidate_power_product. (exists ff_lt_bpcpe_before_choice_valuation_candidate_power_product_bound. ff_lt_bpcpe_before_choice_valuation_candidate_power_product_bound + S ff_i_bpcpe_before_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpe_before_choice_valuation) -> exists ff_p_bpcpe_before_choice_valuation_candidate_power_product ff_r_bpcpe_before_choice_valuation_candidate_power_product ff_s_bpcpe_before_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpe_before_choice_valuation_candidate_power_product_factor. ff_h_bpcpe_before_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpe_before_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpe_before_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpe_before_choice_valuation_candidate_power)) /\ exists ff_q_bpcpe_before_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpe_before_choice_valuation_candidate_power = ff_q_bpcpe_before_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpe_before_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpe_before_choice_valuation_candidate_power) + (ff_p_bpcpe_before_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpe_before_choice_valuation_candidate_power_product_partial. ff_h_bpcpe_before_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpe_before_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpe_before_choice_valuation_candidate_power_product)) * ff_v_bpcpe_before_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_before_choice_valuation_candidate_power_product_partial. ff_u_bpcpe_before_choice_valuation_candidate_power_product = ff_q_bpcpe_before_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpe_before_choice_valuation_candidate_power_product)) * ff_v_bpcpe_before_choice_valuation_candidate_power_product) + (ff_r_bpcpe_before_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpe_before_choice_valuation_candidate_power_product_successor. ff_h_bpcpe_before_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpe_before_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpe_before_choice_valuation_candidate_power_product)) * ff_v_bpcpe_before_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_before_choice_valuation_candidate_power_product_successor. ff_u_bpcpe_before_choice_valuation_candidate_power_product = ff_q_bpcpe_before_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpe_before_choice_valuation_candidate_power_product)) * ff_v_bpcpe_before_choice_valuation_candidate_power_product) + (ff_s_bpcpe_before_choice_valuation_candidate_power_product))) /\ ff_s_bpcpe_before_choice_valuation_candidate_power_product = ff_r_bpcpe_before_choice_valuation_candidate_power_product * ff_p_bpcpe_before_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpe_before_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpe_before_choice_valuation_candidate) * bpr_divides_quotient_bpcpe_before_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpe_before_choice_valuation_candidate_below. bpr_le_gap_bpcpe_before_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpe_before_choice_valuation) = (bpr_choice_exponent_bpcpe_before_choice))) /\ (exists bpr_power_code_bpcpe_before_choice_power bpr_power_scale_bpcpe_before_choice_power. ((forall bpr_power_index_bpcpe_before_choice_power. (exists bpr_gap_bpcpe_before_choice_power_repeat_bound. bpr_gap_bpcpe_before_choice_power_repeat_bound + S (bpr_power_index_bpcpe_before_choice_power) = bpr_choice_exponent_bpcpe_before_choice) -> (((exists bpr_height_bpcpe_before_choice_power_repeat_entry. bpr_height_bpcpe_before_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpe_before)) = S ((S (bpr_power_index_bpcpe_before_choice_power)) * bpr_power_scale_bpcpe_before_choice_power)) /\ exists bpr_quotient_bpcpe_before_choice_power_repeat_entry. bpr_power_code_bpcpe_before_choice_power = bpr_quotient_bpcpe_before_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpe_before_choice_power)) * bpr_power_scale_bpcpe_before_choice_power) + (S (bpr_prefix_index_bpcpe_before))))) /\ (exists ff_u_bpcpe_before_choice_power_product ff_v_bpcpe_before_choice_power_product. ((((exists ff_h_bpcpe_before_choice_power_product_start. ff_h_bpcpe_before_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_before_choice_power_product)) /\ exists ff_q_bpcpe_before_choice_power_product_start. ff_u_bpcpe_before_choice_power_product = ff_q_bpcpe_before_choice_power_product_start * S ((S (0)) * ff_v_bpcpe_before_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpe_before_choice_power_product_terminal. ff_h_bpcpe_before_choice_power_product_terminal + S (bpr_prefix_value_bpcpe_before) = S ((S (bpr_choice_exponent_bpcpe_before_choice)) * ff_v_bpcpe_before_choice_power_product)) /\ exists ff_q_bpcpe_before_choice_power_product_terminal. ff_u_bpcpe_before_choice_power_product = ff_q_bpcpe_before_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpe_before_choice)) * ff_v_bpcpe_before_choice_power_product) + (bpr_prefix_value_bpcpe_before))) /\ forall ff_i_bpcpe_before_choice_power_product. (exists ff_lt_bpcpe_before_choice_power_product_bound. ff_lt_bpcpe_before_choice_power_product_bound + S ff_i_bpcpe_before_choice_power_product = bpr_choice_exponent_bpcpe_before_choice) -> exists ff_p_bpcpe_before_choice_power_product ff_r_bpcpe_before_choice_power_product ff_s_bpcpe_before_choice_power_product. ((((exists ff_h_bpcpe_before_choice_power_product_factor. ff_h_bpcpe_before_choice_power_product_factor + S (ff_p_bpcpe_before_choice_power_product) = S ((S (ff_i_bpcpe_before_choice_power_product)) * bpr_power_scale_bpcpe_before_choice_power)) /\ exists ff_q_bpcpe_before_choice_power_product_factor. bpr_power_code_bpcpe_before_choice_power = ff_q_bpcpe_before_choice_power_product_factor * S ((S (ff_i_bpcpe_before_choice_power_product)) * bpr_power_scale_bpcpe_before_choice_power) + (ff_p_bpcpe_before_choice_power_product))) /\ ((((exists ff_h_bpcpe_before_choice_power_product_partial. ff_h_bpcpe_before_choice_power_product_partial + S (ff_r_bpcpe_before_choice_power_product) = S ((S (ff_i_bpcpe_before_choice_power_product)) * ff_v_bpcpe_before_choice_power_product)) /\ exists ff_q_bpcpe_before_choice_power_product_partial. ff_u_bpcpe_before_choice_power_product = ff_q_bpcpe_before_choice_power_product_partial * S ((S (ff_i_bpcpe_before_choice_power_product)) * ff_v_bpcpe_before_choice_power_product) + (ff_r_bpcpe_before_choice_power_product))) /\ ((((exists ff_h_bpcpe_before_choice_power_product_successor. ff_h_bpcpe_before_choice_power_product_successor + S (ff_s_bpcpe_before_choice_power_product) = S ((S (S ff_i_bpcpe_before_choice_power_product)) * ff_v_bpcpe_before_choice_power_product)) /\ exists ff_q_bpcpe_before_choice_power_product_successor. ff_u_bpcpe_before_choice_power_product = ff_q_bpcpe_before_choice_power_product_successor * S ((S (S ff_i_bpcpe_before_choice_power_product)) * ff_v_bpcpe_before_choice_power_product) + (ff_s_bpcpe_before_choice_power_product))) /\ ff_s_bpcpe_before_choice_power_product = ff_r_bpcpe_before_choice_power_product * ff_p_bpcpe_before_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpe_before) = 1) /\ forall bpr_left_bpcpe_before_choice_prime bpr_right_bpcpe_before_choice_prime. S (bpr_prefix_index_bpcpe_before) = bpr_left_bpcpe_before_choice_prime * bpr_right_bpcpe_before_choice_prime -> bpr_left_bpcpe_before_choice_prime = 1 \/ bpr_right_bpcpe_before_choice_prime = 1)) /\ bpr_prefix_value_bpcpe_before = 1))))) -> exists d e. (forall bpr_prefix_index_bpcpe_after. (exists bpr_gap_bpcpe_after_bound. bpr_gap_bpcpe_after_bound + S (bpr_prefix_index_bpcpe_after) = S m) -> exists bpr_prefix_value_bpcpe_after. ((((exists bpr_height_bpcpe_after_decoded. bpr_height_bpcpe_after_decoded + S (bpr_prefix_value_bpcpe_after) = S ((S (bpr_prefix_index_bpcpe_after)) * e)) /\ exists bpr_quotient_bpcpe_after_decoded. d = bpr_quotient_bpcpe_after_decoded * S ((S (bpr_prefix_index_bpcpe_after)) * e) + (bpr_prefix_value_bpcpe_after))) /\ (((((~(S (bpr_prefix_index_bpcpe_after) = 1) /\ forall bpr_left_bpcpe_after_choice_prime bpr_right_bpcpe_after_choice_prime. S (bpr_prefix_index_bpcpe_after) = bpr_left_bpcpe_after_choice_prime * bpr_right_bpcpe_after_choice_prime -> bpr_left_bpcpe_after_choice_prime = 1 \/ bpr_right_bpcpe_after_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpe_after_choice. ((((exists bpr_le_gap_bpcpe_after_choice_valuation_selected_bound. bpr_le_gap_bpcpe_after_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpe_after_choice) = (n)) /\ (exists bpr_power_value_bpcpe_after_choice_valuation_selected. ((exists bpr_power_code_bpcpe_after_choice_valuation_selected_power bpr_power_scale_bpcpe_after_choice_valuation_selected_power. ((forall bpr_power_index_bpcpe_after_choice_valuation_selected_power. (exists bpr_gap_bpcpe_after_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpe_after_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpe_after_choice_valuation_selected_power) = bpr_choice_exponent_bpcpe_after_choice) -> (((exists bpr_height_bpcpe_after_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpe_after_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpe_after)) = S ((S (bpr_power_index_bpcpe_after_choice_valuation_selected_power)) * bpr_power_scale_bpcpe_after_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpe_after_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpe_after_choice_valuation_selected_power = bpr_quotient_bpcpe_after_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpe_after_choice_valuation_selected_power)) * bpr_power_scale_bpcpe_after_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpe_after))))) /\ (exists ff_u_bpcpe_after_choice_valuation_selected_power_product ff_v_bpcpe_after_choice_valuation_selected_power_product. ((((exists ff_h_bpcpe_after_choice_valuation_selected_power_product_start. ff_h_bpcpe_after_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_after_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_after_choice_valuation_selected_power_product_start. ff_u_bpcpe_after_choice_valuation_selected_power_product = ff_q_bpcpe_after_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpe_after_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpe_after_choice_valuation_selected_power_product_terminal. ff_h_bpcpe_after_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpe_after_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpe_after_choice)) * ff_v_bpcpe_after_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_after_choice_valuation_selected_power_product_terminal. ff_u_bpcpe_after_choice_valuation_selected_power_product = ff_q_bpcpe_after_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpe_after_choice)) * ff_v_bpcpe_after_choice_valuation_selected_power_product) + (bpr_power_value_bpcpe_after_choice_valuation_selected))) /\ forall ff_i_bpcpe_after_choice_valuation_selected_power_product. (exists ff_lt_bpcpe_after_choice_valuation_selected_power_product_bound. ff_lt_bpcpe_after_choice_valuation_selected_power_product_bound + S ff_i_bpcpe_after_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpe_after_choice) -> exists ff_p_bpcpe_after_choice_valuation_selected_power_product ff_r_bpcpe_after_choice_valuation_selected_power_product ff_s_bpcpe_after_choice_valuation_selected_power_product. ((((exists ff_h_bpcpe_after_choice_valuation_selected_power_product_factor. ff_h_bpcpe_after_choice_valuation_selected_power_product_factor + S (ff_p_bpcpe_after_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpe_after_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpe_after_choice_valuation_selected_power)) /\ exists ff_q_bpcpe_after_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpe_after_choice_valuation_selected_power = ff_q_bpcpe_after_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpe_after_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpe_after_choice_valuation_selected_power) + (ff_p_bpcpe_after_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpe_after_choice_valuation_selected_power_product_partial. ff_h_bpcpe_after_choice_valuation_selected_power_product_partial + S (ff_r_bpcpe_after_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpe_after_choice_valuation_selected_power_product)) * ff_v_bpcpe_after_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_after_choice_valuation_selected_power_product_partial. ff_u_bpcpe_after_choice_valuation_selected_power_product = ff_q_bpcpe_after_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpe_after_choice_valuation_selected_power_product)) * ff_v_bpcpe_after_choice_valuation_selected_power_product) + (ff_r_bpcpe_after_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpe_after_choice_valuation_selected_power_product_successor. ff_h_bpcpe_after_choice_valuation_selected_power_product_successor + S (ff_s_bpcpe_after_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpe_after_choice_valuation_selected_power_product)) * ff_v_bpcpe_after_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_after_choice_valuation_selected_power_product_successor. ff_u_bpcpe_after_choice_valuation_selected_power_product = ff_q_bpcpe_after_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpe_after_choice_valuation_selected_power_product)) * ff_v_bpcpe_after_choice_valuation_selected_power_product) + (ff_s_bpcpe_after_choice_valuation_selected_power_product))) /\ ff_s_bpcpe_after_choice_valuation_selected_power_product = ff_r_bpcpe_after_choice_valuation_selected_power_product * ff_p_bpcpe_after_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpe_after_choice_valuation_selected_divides. n = (bpr_power_value_bpcpe_after_choice_valuation_selected) * bpr_divides_quotient_bpcpe_after_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpe_after_choice_valuation. (exists bpr_le_gap_bpcpe_after_choice_valuation_candidate_bound. bpr_le_gap_bpcpe_after_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpe_after_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpe_after_choice_valuation_candidate. ((exists bpr_power_code_bpcpe_after_choice_valuation_candidate_power bpr_power_scale_bpcpe_after_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpe_after_choice_valuation_candidate_power. (exists bpr_gap_bpcpe_after_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpe_after_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpe_after_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpe_after_choice_valuation) -> (((exists bpr_height_bpcpe_after_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpe_after_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpe_after)) = S ((S (bpr_power_index_bpcpe_after_choice_valuation_candidate_power)) * bpr_power_scale_bpcpe_after_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpe_after_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpe_after_choice_valuation_candidate_power = bpr_quotient_bpcpe_after_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpe_after_choice_valuation_candidate_power)) * bpr_power_scale_bpcpe_after_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpe_after))))) /\ (exists ff_u_bpcpe_after_choice_valuation_candidate_power_product ff_v_bpcpe_after_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpe_after_choice_valuation_candidate_power_product_start. ff_h_bpcpe_after_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_after_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_after_choice_valuation_candidate_power_product_start. ff_u_bpcpe_after_choice_valuation_candidate_power_product = ff_q_bpcpe_after_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpe_after_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpe_after_choice_valuation_candidate_power_product_terminal. ff_h_bpcpe_after_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpe_after_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpe_after_choice_valuation)) * ff_v_bpcpe_after_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_after_choice_valuation_candidate_power_product_terminal. ff_u_bpcpe_after_choice_valuation_candidate_power_product = ff_q_bpcpe_after_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpe_after_choice_valuation)) * ff_v_bpcpe_after_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpe_after_choice_valuation_candidate))) /\ forall ff_i_bpcpe_after_choice_valuation_candidate_power_product. (exists ff_lt_bpcpe_after_choice_valuation_candidate_power_product_bound. ff_lt_bpcpe_after_choice_valuation_candidate_power_product_bound + S ff_i_bpcpe_after_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpe_after_choice_valuation) -> exists ff_p_bpcpe_after_choice_valuation_candidate_power_product ff_r_bpcpe_after_choice_valuation_candidate_power_product ff_s_bpcpe_after_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpe_after_choice_valuation_candidate_power_product_factor. ff_h_bpcpe_after_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpe_after_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpe_after_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpe_after_choice_valuation_candidate_power)) /\ exists ff_q_bpcpe_after_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpe_after_choice_valuation_candidate_power = ff_q_bpcpe_after_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpe_after_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpe_after_choice_valuation_candidate_power) + (ff_p_bpcpe_after_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpe_after_choice_valuation_candidate_power_product_partial. ff_h_bpcpe_after_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpe_after_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpe_after_choice_valuation_candidate_power_product)) * ff_v_bpcpe_after_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_after_choice_valuation_candidate_power_product_partial. ff_u_bpcpe_after_choice_valuation_candidate_power_product = ff_q_bpcpe_after_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpe_after_choice_valuation_candidate_power_product)) * ff_v_bpcpe_after_choice_valuation_candidate_power_product) + (ff_r_bpcpe_after_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpe_after_choice_valuation_candidate_power_product_successor. ff_h_bpcpe_after_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpe_after_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpe_after_choice_valuation_candidate_power_product)) * ff_v_bpcpe_after_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_after_choice_valuation_candidate_power_product_successor. ff_u_bpcpe_after_choice_valuation_candidate_power_product = ff_q_bpcpe_after_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpe_after_choice_valuation_candidate_power_product)) * ff_v_bpcpe_after_choice_valuation_candidate_power_product) + (ff_s_bpcpe_after_choice_valuation_candidate_power_product))) /\ ff_s_bpcpe_after_choice_valuation_candidate_power_product = ff_r_bpcpe_after_choice_valuation_candidate_power_product * ff_p_bpcpe_after_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpe_after_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpe_after_choice_valuation_candidate) * bpr_divides_quotient_bpcpe_after_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpe_after_choice_valuation_candidate_below. bpr_le_gap_bpcpe_after_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpe_after_choice_valuation) = (bpr_choice_exponent_bpcpe_after_choice))) /\ (exists bpr_power_code_bpcpe_after_choice_power bpr_power_scale_bpcpe_after_choice_power. ((forall bpr_power_index_bpcpe_after_choice_power. (exists bpr_gap_bpcpe_after_choice_power_repeat_bound. bpr_gap_bpcpe_after_choice_power_repeat_bound + S (bpr_power_index_bpcpe_after_choice_power) = bpr_choice_exponent_bpcpe_after_choice) -> (((exists bpr_height_bpcpe_after_choice_power_repeat_entry. bpr_height_bpcpe_after_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpe_after)) = S ((S (bpr_power_index_bpcpe_after_choice_power)) * bpr_power_scale_bpcpe_after_choice_power)) /\ exists bpr_quotient_bpcpe_after_choice_power_repeat_entry. bpr_power_code_bpcpe_after_choice_power = bpr_quotient_bpcpe_after_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpe_after_choice_power)) * bpr_power_scale_bpcpe_after_choice_power) + (S (bpr_prefix_index_bpcpe_after))))) /\ (exists ff_u_bpcpe_after_choice_power_product ff_v_bpcpe_after_choice_power_product. ((((exists ff_h_bpcpe_after_choice_power_product_start. ff_h_bpcpe_after_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_after_choice_power_product)) /\ exists ff_q_bpcpe_after_choice_power_product_start. ff_u_bpcpe_after_choice_power_product = ff_q_bpcpe_after_choice_power_product_start * S ((S (0)) * ff_v_bpcpe_after_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpe_after_choice_power_product_terminal. ff_h_bpcpe_after_choice_power_product_terminal + S (bpr_prefix_value_bpcpe_after) = S ((S (bpr_choice_exponent_bpcpe_after_choice)) * ff_v_bpcpe_after_choice_power_product)) /\ exists ff_q_bpcpe_after_choice_power_product_terminal. ff_u_bpcpe_after_choice_power_product = ff_q_bpcpe_after_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpe_after_choice)) * ff_v_bpcpe_after_choice_power_product) + (bpr_prefix_value_bpcpe_after))) /\ forall ff_i_bpcpe_after_choice_power_product. (exists ff_lt_bpcpe_after_choice_power_product_bound. ff_lt_bpcpe_after_choice_power_product_bound + S ff_i_bpcpe_after_choice_power_product = bpr_choice_exponent_bpcpe_after_choice) -> exists ff_p_bpcpe_after_choice_power_product ff_r_bpcpe_after_choice_power_product ff_s_bpcpe_after_choice_power_product. ((((exists ff_h_bpcpe_after_choice_power_product_factor. ff_h_bpcpe_after_choice_power_product_factor + S (ff_p_bpcpe_after_choice_power_product) = S ((S (ff_i_bpcpe_after_choice_power_product)) * bpr_power_scale_bpcpe_after_choice_power)) /\ exists ff_q_bpcpe_after_choice_power_product_factor. bpr_power_code_bpcpe_after_choice_power = ff_q_bpcpe_after_choice_power_product_factor * S ((S (ff_i_bpcpe_after_choice_power_product)) * bpr_power_scale_bpcpe_after_choice_power) + (ff_p_bpcpe_after_choice_power_product))) /\ ((((exists ff_h_bpcpe_after_choice_power_product_partial. ff_h_bpcpe_after_choice_power_product_partial + S (ff_r_bpcpe_after_choice_power_product) = S ((S (ff_i_bpcpe_after_choice_power_product)) * ff_v_bpcpe_after_choice_power_product)) /\ exists ff_q_bpcpe_after_choice_power_product_partial. ff_u_bpcpe_after_choice_power_product = ff_q_bpcpe_after_choice_power_product_partial * S ((S (ff_i_bpcpe_after_choice_power_product)) * ff_v_bpcpe_after_choice_power_product) + (ff_r_bpcpe_after_choice_power_product))) /\ ((((exists ff_h_bpcpe_after_choice_power_product_successor. ff_h_bpcpe_after_choice_power_product_successor + S (ff_s_bpcpe_after_choice_power_product) = S ((S (S ff_i_bpcpe_after_choice_power_product)) * ff_v_bpcpe_after_choice_power_product)) /\ exists ff_q_bpcpe_after_choice_power_product_successor. ff_u_bpcpe_after_choice_power_product = ff_q_bpcpe_after_choice_power_product_successor * S ((S (S ff_i_bpcpe_after_choice_power_product)) * ff_v_bpcpe_after_choice_power_product) + (ff_s_bpcpe_after_choice_power_product))) /\ ff_s_bpcpe_after_choice_power_product = ff_r_bpcpe_after_choice_power_product * ff_p_bpcpe_after_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpe_after) = 1) /\ forall bpr_left_bpcpe_after_choice_prime bpr_right_bpcpe_after_choice_prime. S (bpr_prefix_index_bpcpe_after) = bpr_left_bpcpe_after_choice_prime * bpr_right_bpcpe_after_choice_prime -> bpr_left_bpcpe_after_choice_prime = 1 \/ bpr_right_bpcpe_after_choice_prime = 1)) /\ bpr_prefix_value_bpcpe_after = 1)))))

Structural proof guide

Append one contribution while preserving the old prefix.

Direct prerequisites: prime_contribution_choice_exists, beta_prefix_extend, finite_lt_succ_eq_or_lt. The authored body proceeds by case analysis (7), intermediate claims (4), equality transport (12).

Proof neighborhood

Direct dependencies

BT00YN prime_contribution_choice_exists BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct dependents

BT00YQ prime_contribution_prefix_exists

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

48 script commands · 19 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (3)
prime contribution choice existsbeta prefix extendfinite lt succ eq or lt

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro m
  5. L5
    intro hprefix
02Establish hchoiceL6–7

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution choice exists.

  1. L6
    have hchoice : ∃ x. Prime(S m) ∧ (∃ y. BoundedPowerValuation(S m,n,n,y) ∧ Pow(S m,y,x)) ∨ ¬Prime(S m) ∧ x = 1Definitions: PrimePowBoundedPowerValuation
  2. L7
    apply prime_contribution_choice_exists
03Separate the logical casesL8–8

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L8
    cases hchoice
04Establish hextL9–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix extend.

  1. L9
    have hext : ∃ d. ∃ e. BetaAt(d,e,m,x) ∧ (∀ y. ∀ z. Lt(y,m) → BetaAt(b,c,y,z) → BetaAt(d,e,y,z))Definitions: LtBetaAt
  2. L10
    apply beta_prefix_extend
05Separate the logical casesL11–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L11
    cases hext
  2. L12
    cases hext_witness
  3. L13
    cases hext_witness_witness
06Construct an explicit witnessL14–15

Supply the displayed value, then prove that it has the required property.

  1. L14
    exists x1
  2. L15
    exists x2
07Fix variables and assumptionsL16–17

Work with arbitrary variables or the premises of the current implication.

  1. L16
    intro i
  2. L17
    intro hi
08Establish hsplitL18–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L18
    have hsplit : i = m \/ exists gap. gap + S i = m
  2. L19
    apply finite_lt_succ_eq_or_lt
  3. L20
    exact hi
09Separate the logical casesL21–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L21
    cases hsplit
10Calculate and transport equalitiesL22–31

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L22
    rewrite hsplit_left
  2. L23
    rewrite hsplit_left
  3. L24
    rewrite hsplit_left
  4. L25
    rewrite hsplit_left
  5. L26
    rewrite hsplit_left
  6. L27
    rewrite hsplit_left
  7. L28
    rewrite hsplit_left
  8. L29
    rewrite hsplit_left
  9. L30
    rewrite hsplit_left
  10. L31
    rewrite hsplit_left
11Calculate and transport equalitiesL32–33

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite hsplit_left
  2. L33
    rewrite hsplit_left
12Construct an explicit witnessL34–34

Supply the displayed value, then prove that it has the required property.

  1. L34
    exists x
13Separate the logical casesL35–35

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L35
    split
14Use earlier factsL36–37

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L36
    exact hext_witness_witness_left
  2. L37
    exact hchoice_witness
15Establish holdL38–40

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.

  1. L38
    have hold : ∃ a. BetaAt(b,c,i,a) ∧ (Prime(S i) ∧ (∃ x. BoundedPowerValuation(S i,n,n,x) ∧ Pow(S i,x,a)) ∨ ¬Prime(S i) ∧ a = 1)Definitions: PrimeBetaAtPowBoundedPowerValuation
  2. L39
    apply hprefix
  3. L40
    exact hsplit_right
16Separate the logical casesL41–42

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L41
    cases hold
  2. L42
    cases hold_witness
17Construct an explicit witnessL43–43

Supply the displayed value, then prove that it has the required property.

  1. L43
    exists x3
18Separate the logical casesL44–44

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L44
    split
19Use earlier factsL45–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L45
    apply hext_witness_witness_right
  2. L46
    exact hsplit_right
  3. L47
    exact hold_witness_left
  4. L48
    exact hold_witness_right

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro m
  5. 0005intro hprefix
  6. 0006have hchoice : exists x. (((((~(S (m) = 1) /\ forall bpr_left_bpcpe_choice_prime bpr_right_bpcpe_choice_prime. S (m) = bpr_left_bpcpe_choice_prime * bpr_right_bpcpe_choice_prime -> bpr_left_bpcpe_choice_prime = 1 \/ bpr_right_bpcpe_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpe_choice. ((((exists bpr_le_gap_bpcpe_choice_valuation_selected_bound. bpr_le_gap_bpcpe_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpe_choice) = (n)) /\ (exists bpr_power_value_bpcpe_choice_valuation_selected. ((exists bpr_power_code_bpcpe_choice_valuation_selected_power bpr_power_scale_bpcpe_choice_valuation_selected_power. ((forall bpr_power_index_bpcpe_choice_valuation_selected_power. (exists bpr_gap_bpcpe_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpe_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpe_choice_valuation_selected_power) = bpr_choice_exponent_bpcpe_choice) -> (((exists bpr_height_bpcpe_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpe_choice_valuation_selected_power_repeat_entry + S (S (m)) = S ((S (bpr_power_index_bpcpe_choice_valuation_selected_power)) * bpr_power_scale_bpcpe_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpe_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpe_choice_valuation_selected_power = bpr_quotient_bpcpe_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpe_choice_valuation_selected_power)) * bpr_power_scale_bpcpe_choice_valuation_selected_power) + (S (m))))) /\ (exists ff_u_bpcpe_choice_valuation_selected_power_product ff_v_bpcpe_choice_valuation_selected_power_product. ((((exists ff_h_bpcpe_choice_valuation_selected_power_product_start. ff_h_bpcpe_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_choice_valuation_selected_power_product_start. ff_u_bpcpe_choice_valuation_selected_power_product = ff_q_bpcpe_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpe_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpe_choice_valuation_selected_power_product_terminal. ff_h_bpcpe_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpe_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpe_choice)) * ff_v_bpcpe_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_choice_valuation_selected_power_product_terminal. ff_u_bpcpe_choice_valuation_selected_power_product = ff_q_bpcpe_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpe_choice)) * ff_v_bpcpe_choice_valuation_selected_power_product) + (bpr_power_value_bpcpe_choice_valuation_selected))) /\ forall ff_i_bpcpe_choice_valuation_selected_power_product. (exists ff_lt_bpcpe_choice_valuation_selected_power_product_bound. ff_lt_bpcpe_choice_valuation_selected_power_product_bound + S ff_i_bpcpe_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpe_choice) -> exists ff_p_bpcpe_choice_valuation_selected_power_product ff_r_bpcpe_choice_valuation_selected_power_product ff_s_bpcpe_choice_valuation_selected_power_product. ((((exists ff_h_bpcpe_choice_valuation_selected_power_product_factor. ff_h_bpcpe_choice_valuation_selected_power_product_factor + S (ff_p_bpcpe_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpe_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpe_choice_valuation_selected_power)) /\ exists ff_q_bpcpe_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpe_choice_valuation_selected_power = ff_q_bpcpe_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpe_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpe_choice_valuation_selected_power) + (ff_p_bpcpe_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpe_choice_valuation_selected_power_product_partial. ff_h_bpcpe_choice_valuation_selected_power_product_partial + S (ff_r_bpcpe_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpe_choice_valuation_selected_power_product)) * ff_v_bpcpe_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_choice_valuation_selected_power_product_partial. ff_u_bpcpe_choice_valuation_selected_power_product = ff_q_bpcpe_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpe_choice_valuation_selected_power_product)) * ff_v_bpcpe_choice_valuation_selected_power_product) + (ff_r_bpcpe_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpe_choice_valuation_selected_power_product_successor. ff_h_bpcpe_choice_valuation_selected_power_product_successor + S (ff_s_bpcpe_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpe_choice_valuation_selected_power_product)) * ff_v_bpcpe_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_choice_valuation_selected_power_product_successor. ff_u_bpcpe_choice_valuation_selected_power_product = ff_q_bpcpe_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpe_choice_valuation_selected_power_product)) * ff_v_bpcpe_choice_valuation_selected_power_product) + (ff_s_bpcpe_choice_valuation_selected_power_product))) /\ ff_s_bpcpe_choice_valuation_selected_power_product = ff_r_bpcpe_choice_valuation_selected_power_product * ff_p_bpcpe_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpe_choice_valuation_selected_divides. n = (bpr_power_value_bpcpe_choice_valuation_selected) * bpr_divides_quotient_bpcpe_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpe_choice_valuation. (exists bpr_le_gap_bpcpe_choice_valuation_candidate_bound. bpr_le_gap_bpcpe_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpe_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpe_choice_valuation_candidate. ((exists bpr_power_code_bpcpe_choice_valuation_candidate_power bpr_power_scale_bpcpe_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpe_choice_valuation_candidate_power. (exists bpr_gap_bpcpe_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpe_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpe_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpe_choice_valuation) -> (((exists bpr_height_bpcpe_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpe_choice_valuation_candidate_power_repeat_entry + S (S (m)) = S ((S (bpr_power_index_bpcpe_choice_valuation_candidate_power)) * bpr_power_scale_bpcpe_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpe_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpe_choice_valuation_candidate_power = bpr_quotient_bpcpe_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpe_choice_valuation_candidate_power)) * bpr_power_scale_bpcpe_choice_valuation_candidate_power) + (S (m))))) /\ (exists ff_u_bpcpe_choice_valuation_candidate_power_product ff_v_bpcpe_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpe_choice_valuation_candidate_power_product_start. ff_h_bpcpe_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_choice_valuation_candidate_power_product_start. ff_u_bpcpe_choice_valuation_candidate_power_product = ff_q_bpcpe_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpe_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpe_choice_valuation_candidate_power_product_terminal. ff_h_bpcpe_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpe_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpe_choice_valuation)) * ff_v_bpcpe_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_choice_valuation_candidate_power_product_terminal. ff_u_bpcpe_choice_valuation_candidate_power_product = ff_q_bpcpe_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpe_choice_valuation)) * ff_v_bpcpe_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpe_choice_valuation_candidate))) /\ forall ff_i_bpcpe_choice_valuation_candidate_power_product. (exists ff_lt_bpcpe_choice_valuation_candidate_power_product_bound. ff_lt_bpcpe_choice_valuation_candidate_power_product_bound + S ff_i_bpcpe_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpe_choice_valuation) -> exists ff_p_bpcpe_choice_valuation_candidate_power_product ff_r_bpcpe_choice_valuation_candidate_power_product ff_s_bpcpe_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpe_choice_valuation_candidate_power_product_factor. ff_h_bpcpe_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpe_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpe_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpe_choice_valuation_candidate_power)) /\ exists ff_q_bpcpe_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpe_choice_valuation_candidate_power = ff_q_bpcpe_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpe_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpe_choice_valuation_candidate_power) + (ff_p_bpcpe_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpe_choice_valuation_candidate_power_product_partial. ff_h_bpcpe_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpe_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpe_choice_valuation_candidate_power_product)) * ff_v_bpcpe_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_choice_valuation_candidate_power_product_partial. ff_u_bpcpe_choice_valuation_candidate_power_product = ff_q_bpcpe_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpe_choice_valuation_candidate_power_product)) * ff_v_bpcpe_choice_valuation_candidate_power_product) + (ff_r_bpcpe_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpe_choice_valuation_candidate_power_product_successor. ff_h_bpcpe_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpe_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpe_choice_valuation_candidate_power_product)) * ff_v_bpcpe_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_choice_valuation_candidate_power_product_successor. ff_u_bpcpe_choice_valuation_candidate_power_product = ff_q_bpcpe_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpe_choice_valuation_candidate_power_product)) * ff_v_bpcpe_choice_valuation_candidate_power_product) + (ff_s_bpcpe_choice_valuation_candidate_power_product))) /\ ff_s_bpcpe_choice_valuation_candidate_power_product = ff_r_bpcpe_choice_valuation_candidate_power_product * ff_p_bpcpe_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpe_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpe_choice_valuation_candidate) * bpr_divides_quotient_bpcpe_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpe_choice_valuation_candidate_below. bpr_le_gap_bpcpe_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpe_choice_valuation) = (bpr_choice_exponent_bpcpe_choice))) /\ (exists bpr_power_code_bpcpe_choice_power bpr_power_scale_bpcpe_choice_power. ((forall bpr_power_index_bpcpe_choice_power. (exists bpr_gap_bpcpe_choice_power_repeat_bound. bpr_gap_bpcpe_choice_power_repeat_bound + S (bpr_power_index_bpcpe_choice_power) = bpr_choice_exponent_bpcpe_choice) -> (((exists bpr_height_bpcpe_choice_power_repeat_entry. bpr_height_bpcpe_choice_power_repeat_entry + S (S (m)) = S ((S (bpr_power_index_bpcpe_choice_power)) * bpr_power_scale_bpcpe_choice_power)) /\ exists bpr_quotient_bpcpe_choice_power_repeat_entry. bpr_power_code_bpcpe_choice_power = bpr_quotient_bpcpe_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpe_choice_power)) * bpr_power_scale_bpcpe_choice_power) + (S (m))))) /\ (exists ff_u_bpcpe_choice_power_product ff_v_bpcpe_choice_power_product. ((((exists ff_h_bpcpe_choice_power_product_start. ff_h_bpcpe_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_choice_power_product)) /\ exists ff_q_bpcpe_choice_power_product_start. ff_u_bpcpe_choice_power_product = ff_q_bpcpe_choice_power_product_start * S ((S (0)) * ff_v_bpcpe_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpe_choice_power_product_terminal. ff_h_bpcpe_choice_power_product_terminal + S (x) = S ((S (bpr_choice_exponent_bpcpe_choice)) * ff_v_bpcpe_choice_power_product)) /\ exists ff_q_bpcpe_choice_power_product_terminal. ff_u_bpcpe_choice_power_product = ff_q_bpcpe_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpe_choice)) * ff_v_bpcpe_choice_power_product) + (x))) /\ forall ff_i_bpcpe_choice_power_product. (exists ff_lt_bpcpe_choice_power_product_bound. ff_lt_bpcpe_choice_power_product_bound + S ff_i_bpcpe_choice_power_product = bpr_choice_exponent_bpcpe_choice) -> exists ff_p_bpcpe_choice_power_product ff_r_bpcpe_choice_power_product ff_s_bpcpe_choice_power_product. ((((exists ff_h_bpcpe_choice_power_product_factor. ff_h_bpcpe_choice_power_product_factor + S (ff_p_bpcpe_choice_power_product) = S ((S (ff_i_bpcpe_choice_power_product)) * bpr_power_scale_bpcpe_choice_power)) /\ exists ff_q_bpcpe_choice_power_product_factor. bpr_power_code_bpcpe_choice_power = ff_q_bpcpe_choice_power_product_factor * S ((S (ff_i_bpcpe_choice_power_product)) * bpr_power_scale_bpcpe_choice_power) + (ff_p_bpcpe_choice_power_product))) /\ ((((exists ff_h_bpcpe_choice_power_product_partial. ff_h_bpcpe_choice_power_product_partial + S (ff_r_bpcpe_choice_power_product) = S ((S (ff_i_bpcpe_choice_power_product)) * ff_v_bpcpe_choice_power_product)) /\ exists ff_q_bpcpe_choice_power_product_partial. ff_u_bpcpe_choice_power_product = ff_q_bpcpe_choice_power_product_partial * S ((S (ff_i_bpcpe_choice_power_product)) * ff_v_bpcpe_choice_power_product) + (ff_r_bpcpe_choice_power_product))) /\ ((((exists ff_h_bpcpe_choice_power_product_successor. ff_h_bpcpe_choice_power_product_successor + S (ff_s_bpcpe_choice_power_product) = S ((S (S ff_i_bpcpe_choice_power_product)) * ff_v_bpcpe_choice_power_product)) /\ exists ff_q_bpcpe_choice_power_product_successor. ff_u_bpcpe_choice_power_product = ff_q_bpcpe_choice_power_product_successor * S ((S (S ff_i_bpcpe_choice_power_product)) * ff_v_bpcpe_choice_power_product) + (ff_s_bpcpe_choice_power_product))) /\ ff_s_bpcpe_choice_power_product = ff_r_bpcpe_choice_power_product * ff_p_bpcpe_choice_power_product)))))))))) \/ (~((~(S (m) = 1) /\ forall bpr_left_bpcpe_choice_prime bpr_right_bpcpe_choice_prime. S (m) = bpr_left_bpcpe_choice_prime * bpr_right_bpcpe_choice_prime -> bpr_left_bpcpe_choice_prime = 1 \/ bpr_right_bpcpe_choice_prime = 1)) /\ x = 1)))
  7. 0007apply prime_contribution_choice_exists
  8. 0008cases hchoice
  9. 0009have hext : exists d e. ((exists bpr_height_bpcpe_new_entry. bpr_height_bpcpe_new_entry + S (x) = S ((S (m)) * e)) /\ exists bpr_quotient_bpcpe_new_entry. d = bpr_quotient_bpcpe_new_entry * S ((S (m)) * e) + (x)) /\ forall i a. (exists bpr_gap_bpcpe_old_bound. bpr_gap_bpcpe_old_bound + S (i) = m) -> (((exists bpr_height_bpcpe_old_source. bpr_height_bpcpe_old_source + S (a) = S ((S (i)) * c)) /\ exists bpr_quotient_bpcpe_old_source. b = bpr_quotient_bpcpe_old_source * S ((S (i)) * c) + (a))) -> (((exists bpr_height_bpcpe_old_target. bpr_height_bpcpe_old_target + S (a) = S ((S (i)) * e)) /\ exists bpr_quotient_bpcpe_old_target. d = bpr_quotient_bpcpe_old_target * S ((S (i)) * e) + (a)))
  10. 0010apply beta_prefix_extend
  11. 0011cases hext
  12. 0012cases hext_witness
  13. 0013cases hext_witness_witness
  14. 0014exists x1
  15. 0015exists x2
  16. 0016intro i
  17. 0017intro hi
  18. 0018have hsplit : i = m \/ exists gap. gap + S i = m
  19. 0019apply finite_lt_succ_eq_or_lt
  20. 0020exact hi
  21. 0021cases hsplit
  22. 0022rewrite hsplit_left
  23. 0023rewrite hsplit_left
  24. 0024rewrite hsplit_left
  25. 0025rewrite hsplit_left
  26. 0026rewrite hsplit_left
  27. 0027rewrite hsplit_left
  28. 0028rewrite hsplit_left
  29. 0029rewrite hsplit_left
  30. 0030rewrite hsplit_left
  31. 0031rewrite hsplit_left
  32. 0032rewrite hsplit_left
  33. 0033rewrite hsplit_left
  34. 0034exists x
  35. 0035split
  36. 0036exact hext_witness_witness_left
  37. 0037exact hchoice_witness
  38. 0038have hold : exists a. (((exists bpr_height_bpcpe_old_entry. bpr_height_bpcpe_old_entry + S (a) = S ((S (i)) * c)) /\ exists bpr_quotient_bpcpe_old_entry. b = bpr_quotient_bpcpe_old_entry * S ((S (i)) * c) + (a))) /\ (((((~(S (i) = 1) /\ forall bpr_left_bpcpe_old_choice_prime bpr_right_bpcpe_old_choice_prime. S (i) = bpr_left_bpcpe_old_choice_prime * bpr_right_bpcpe_old_choice_prime -> bpr_left_bpcpe_old_choice_prime = 1 \/ bpr_right_bpcpe_old_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpe_old_choice. ((((exists bpr_le_gap_bpcpe_old_choice_valuation_selected_bound. bpr_le_gap_bpcpe_old_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpe_old_choice) = (n)) /\ (exists bpr_power_value_bpcpe_old_choice_valuation_selected. ((exists bpr_power_code_bpcpe_old_choice_valuation_selected_power bpr_power_scale_bpcpe_old_choice_valuation_selected_power. ((forall bpr_power_index_bpcpe_old_choice_valuation_selected_power. (exists bpr_gap_bpcpe_old_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpe_old_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpe_old_choice_valuation_selected_power) = bpr_choice_exponent_bpcpe_old_choice) -> (((exists bpr_height_bpcpe_old_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpe_old_choice_valuation_selected_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcpe_old_choice_valuation_selected_power)) * bpr_power_scale_bpcpe_old_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpe_old_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpe_old_choice_valuation_selected_power = bpr_quotient_bpcpe_old_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpe_old_choice_valuation_selected_power)) * bpr_power_scale_bpcpe_old_choice_valuation_selected_power) + (S (i))))) /\ (exists ff_u_bpcpe_old_choice_valuation_selected_power_product ff_v_bpcpe_old_choice_valuation_selected_power_product. ((((exists ff_h_bpcpe_old_choice_valuation_selected_power_product_start. ff_h_bpcpe_old_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_old_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_old_choice_valuation_selected_power_product_start. ff_u_bpcpe_old_choice_valuation_selected_power_product = ff_q_bpcpe_old_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpe_old_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpe_old_choice_valuation_selected_power_product_terminal. ff_h_bpcpe_old_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpe_old_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpe_old_choice)) * ff_v_bpcpe_old_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_old_choice_valuation_selected_power_product_terminal. ff_u_bpcpe_old_choice_valuation_selected_power_product = ff_q_bpcpe_old_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpe_old_choice)) * ff_v_bpcpe_old_choice_valuation_selected_power_product) + (bpr_power_value_bpcpe_old_choice_valuation_selected))) /\ forall ff_i_bpcpe_old_choice_valuation_selected_power_product. (exists ff_lt_bpcpe_old_choice_valuation_selected_power_product_bound. ff_lt_bpcpe_old_choice_valuation_selected_power_product_bound + S ff_i_bpcpe_old_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpe_old_choice) -> exists ff_p_bpcpe_old_choice_valuation_selected_power_product ff_r_bpcpe_old_choice_valuation_selected_power_product ff_s_bpcpe_old_choice_valuation_selected_power_product. ((((exists ff_h_bpcpe_old_choice_valuation_selected_power_product_factor. ff_h_bpcpe_old_choice_valuation_selected_power_product_factor + S (ff_p_bpcpe_old_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpe_old_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpe_old_choice_valuation_selected_power)) /\ exists ff_q_bpcpe_old_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpe_old_choice_valuation_selected_power = ff_q_bpcpe_old_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpe_old_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpe_old_choice_valuation_selected_power) + (ff_p_bpcpe_old_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpe_old_choice_valuation_selected_power_product_partial. ff_h_bpcpe_old_choice_valuation_selected_power_product_partial + S (ff_r_bpcpe_old_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpe_old_choice_valuation_selected_power_product)) * ff_v_bpcpe_old_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_old_choice_valuation_selected_power_product_partial. ff_u_bpcpe_old_choice_valuation_selected_power_product = ff_q_bpcpe_old_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpe_old_choice_valuation_selected_power_product)) * ff_v_bpcpe_old_choice_valuation_selected_power_product) + (ff_r_bpcpe_old_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpe_old_choice_valuation_selected_power_product_successor. ff_h_bpcpe_old_choice_valuation_selected_power_product_successor + S (ff_s_bpcpe_old_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpe_old_choice_valuation_selected_power_product)) * ff_v_bpcpe_old_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpe_old_choice_valuation_selected_power_product_successor. ff_u_bpcpe_old_choice_valuation_selected_power_product = ff_q_bpcpe_old_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpe_old_choice_valuation_selected_power_product)) * ff_v_bpcpe_old_choice_valuation_selected_power_product) + (ff_s_bpcpe_old_choice_valuation_selected_power_product))) /\ ff_s_bpcpe_old_choice_valuation_selected_power_product = ff_r_bpcpe_old_choice_valuation_selected_power_product * ff_p_bpcpe_old_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpe_old_choice_valuation_selected_divides. n = (bpr_power_value_bpcpe_old_choice_valuation_selected) * bpr_divides_quotient_bpcpe_old_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpe_old_choice_valuation. (exists bpr_le_gap_bpcpe_old_choice_valuation_candidate_bound. bpr_le_gap_bpcpe_old_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpe_old_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpe_old_choice_valuation_candidate. ((exists bpr_power_code_bpcpe_old_choice_valuation_candidate_power bpr_power_scale_bpcpe_old_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpe_old_choice_valuation_candidate_power. (exists bpr_gap_bpcpe_old_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpe_old_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpe_old_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpe_old_choice_valuation) -> (((exists bpr_height_bpcpe_old_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpe_old_choice_valuation_candidate_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcpe_old_choice_valuation_candidate_power)) * bpr_power_scale_bpcpe_old_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpe_old_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpe_old_choice_valuation_candidate_power = bpr_quotient_bpcpe_old_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpe_old_choice_valuation_candidate_power)) * bpr_power_scale_bpcpe_old_choice_valuation_candidate_power) + (S (i))))) /\ (exists ff_u_bpcpe_old_choice_valuation_candidate_power_product ff_v_bpcpe_old_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpe_old_choice_valuation_candidate_power_product_start. ff_h_bpcpe_old_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_old_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_old_choice_valuation_candidate_power_product_start. ff_u_bpcpe_old_choice_valuation_candidate_power_product = ff_q_bpcpe_old_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpe_old_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpe_old_choice_valuation_candidate_power_product_terminal. ff_h_bpcpe_old_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpe_old_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpe_old_choice_valuation)) * ff_v_bpcpe_old_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_old_choice_valuation_candidate_power_product_terminal. ff_u_bpcpe_old_choice_valuation_candidate_power_product = ff_q_bpcpe_old_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpe_old_choice_valuation)) * ff_v_bpcpe_old_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpe_old_choice_valuation_candidate))) /\ forall ff_i_bpcpe_old_choice_valuation_candidate_power_product. (exists ff_lt_bpcpe_old_choice_valuation_candidate_power_product_bound. ff_lt_bpcpe_old_choice_valuation_candidate_power_product_bound + S ff_i_bpcpe_old_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpe_old_choice_valuation) -> exists ff_p_bpcpe_old_choice_valuation_candidate_power_product ff_r_bpcpe_old_choice_valuation_candidate_power_product ff_s_bpcpe_old_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpe_old_choice_valuation_candidate_power_product_factor. ff_h_bpcpe_old_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpe_old_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpe_old_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpe_old_choice_valuation_candidate_power)) /\ exists ff_q_bpcpe_old_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpe_old_choice_valuation_candidate_power = ff_q_bpcpe_old_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpe_old_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpe_old_choice_valuation_candidate_power) + (ff_p_bpcpe_old_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpe_old_choice_valuation_candidate_power_product_partial. ff_h_bpcpe_old_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpe_old_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpe_old_choice_valuation_candidate_power_product)) * ff_v_bpcpe_old_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_old_choice_valuation_candidate_power_product_partial. ff_u_bpcpe_old_choice_valuation_candidate_power_product = ff_q_bpcpe_old_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpe_old_choice_valuation_candidate_power_product)) * ff_v_bpcpe_old_choice_valuation_candidate_power_product) + (ff_r_bpcpe_old_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpe_old_choice_valuation_candidate_power_product_successor. ff_h_bpcpe_old_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpe_old_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpe_old_choice_valuation_candidate_power_product)) * ff_v_bpcpe_old_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpe_old_choice_valuation_candidate_power_product_successor. ff_u_bpcpe_old_choice_valuation_candidate_power_product = ff_q_bpcpe_old_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpe_old_choice_valuation_candidate_power_product)) * ff_v_bpcpe_old_choice_valuation_candidate_power_product) + (ff_s_bpcpe_old_choice_valuation_candidate_power_product))) /\ ff_s_bpcpe_old_choice_valuation_candidate_power_product = ff_r_bpcpe_old_choice_valuation_candidate_power_product * ff_p_bpcpe_old_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpe_old_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpe_old_choice_valuation_candidate) * bpr_divides_quotient_bpcpe_old_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpe_old_choice_valuation_candidate_below. bpr_le_gap_bpcpe_old_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpe_old_choice_valuation) = (bpr_choice_exponent_bpcpe_old_choice))) /\ (exists bpr_power_code_bpcpe_old_choice_power bpr_power_scale_bpcpe_old_choice_power. ((forall bpr_power_index_bpcpe_old_choice_power. (exists bpr_gap_bpcpe_old_choice_power_repeat_bound. bpr_gap_bpcpe_old_choice_power_repeat_bound + S (bpr_power_index_bpcpe_old_choice_power) = bpr_choice_exponent_bpcpe_old_choice) -> (((exists bpr_height_bpcpe_old_choice_power_repeat_entry. bpr_height_bpcpe_old_choice_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcpe_old_choice_power)) * bpr_power_scale_bpcpe_old_choice_power)) /\ exists bpr_quotient_bpcpe_old_choice_power_repeat_entry. bpr_power_code_bpcpe_old_choice_power = bpr_quotient_bpcpe_old_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpe_old_choice_power)) * bpr_power_scale_bpcpe_old_choice_power) + (S (i))))) /\ (exists ff_u_bpcpe_old_choice_power_product ff_v_bpcpe_old_choice_power_product. ((((exists ff_h_bpcpe_old_choice_power_product_start. ff_h_bpcpe_old_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpe_old_choice_power_product)) /\ exists ff_q_bpcpe_old_choice_power_product_start. ff_u_bpcpe_old_choice_power_product = ff_q_bpcpe_old_choice_power_product_start * S ((S (0)) * ff_v_bpcpe_old_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpe_old_choice_power_product_terminal. ff_h_bpcpe_old_choice_power_product_terminal + S (a) = S ((S (bpr_choice_exponent_bpcpe_old_choice)) * ff_v_bpcpe_old_choice_power_product)) /\ exists ff_q_bpcpe_old_choice_power_product_terminal. ff_u_bpcpe_old_choice_power_product = ff_q_bpcpe_old_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpe_old_choice)) * ff_v_bpcpe_old_choice_power_product) + (a))) /\ forall ff_i_bpcpe_old_choice_power_product. (exists ff_lt_bpcpe_old_choice_power_product_bound. ff_lt_bpcpe_old_choice_power_product_bound + S ff_i_bpcpe_old_choice_power_product = bpr_choice_exponent_bpcpe_old_choice) -> exists ff_p_bpcpe_old_choice_power_product ff_r_bpcpe_old_choice_power_product ff_s_bpcpe_old_choice_power_product. ((((exists ff_h_bpcpe_old_choice_power_product_factor. ff_h_bpcpe_old_choice_power_product_factor + S (ff_p_bpcpe_old_choice_power_product) = S ((S (ff_i_bpcpe_old_choice_power_product)) * bpr_power_scale_bpcpe_old_choice_power)) /\ exists ff_q_bpcpe_old_choice_power_product_factor. bpr_power_code_bpcpe_old_choice_power = ff_q_bpcpe_old_choice_power_product_factor * S ((S (ff_i_bpcpe_old_choice_power_product)) * bpr_power_scale_bpcpe_old_choice_power) + (ff_p_bpcpe_old_choice_power_product))) /\ ((((exists ff_h_bpcpe_old_choice_power_product_partial. ff_h_bpcpe_old_choice_power_product_partial + S (ff_r_bpcpe_old_choice_power_product) = S ((S (ff_i_bpcpe_old_choice_power_product)) * ff_v_bpcpe_old_choice_power_product)) /\ exists ff_q_bpcpe_old_choice_power_product_partial. ff_u_bpcpe_old_choice_power_product = ff_q_bpcpe_old_choice_power_product_partial * S ((S (ff_i_bpcpe_old_choice_power_product)) * ff_v_bpcpe_old_choice_power_product) + (ff_r_bpcpe_old_choice_power_product))) /\ ((((exists ff_h_bpcpe_old_choice_power_product_successor. ff_h_bpcpe_old_choice_power_product_successor + S (ff_s_bpcpe_old_choice_power_product) = S ((S (S ff_i_bpcpe_old_choice_power_product)) * ff_v_bpcpe_old_choice_power_product)) /\ exists ff_q_bpcpe_old_choice_power_product_successor. ff_u_bpcpe_old_choice_power_product = ff_q_bpcpe_old_choice_power_product_successor * S ((S (S ff_i_bpcpe_old_choice_power_product)) * ff_v_bpcpe_old_choice_power_product) + (ff_s_bpcpe_old_choice_power_product))) /\ ff_s_bpcpe_old_choice_power_product = ff_r_bpcpe_old_choice_power_product * ff_p_bpcpe_old_choice_power_product)))))))))) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpcpe_old_choice_prime bpr_right_bpcpe_old_choice_prime. S (i) = bpr_left_bpcpe_old_choice_prime * bpr_right_bpcpe_old_choice_prime -> bpr_left_bpcpe_old_choice_prime = 1 \/ bpr_right_bpcpe_old_choice_prime = 1)) /\ a = 1)))
  39. 0039apply hprefix
  40. 0040exact hsplit_right
  41. 0041cases hold
  42. 0042cases hold_witness
  43. 0043exists x3
  44. 0044split
  45. 0045apply hext_witness_witness_right
  46. 0046exact hsplit_right
  47. 0047exact hold_witness_left
  48. 0048exact hold_witness_right