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.
The carry relation contains actual quotient columns and carry bits, not the desired valuation. The theorem includes all finite lists and zero parts. It uses sequential binary-column carries; a separate simultaneous-grid or permutation-invariance theorem is not asserted.
Exact theorem in conservative defined notation
∀ p. ∀ b. ∀ c. ∀ vb. ∀ vc. ∀ l. BetaValuationPrefix(p,b,c,vb,vc,S l) → BetaValuationPrefix(p,b,c,vb,vc,l)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
le_succ · checked external prerequisite
Original expanded first-order statement
forall p b c vb vc l. (forall mkm_index_drop_source. (exists mkm_lt_drop_source_bound. mkm_lt_drop_source_bound + S (mkm_index_drop_source) = (S l)) -> (exists mkm_value_drop_source_point mkm_exponent_drop_source_point. (((exists fs_h_mkm_drop_source_point_source. fs_h_mkm_drop_source_point_source + S (mkm_value_drop_source_point) = S ((S (mkm_index_drop_source)) * c)) /\ exists fs_q_mkm_drop_source_point_source. b = fs_q_mkm_drop_source_point_source * S ((S (mkm_index_drop_source)) * c) + (mkm_value_drop_source_point))) /\ ((((exists fs_h_mkm_drop_source_point_decoded. fs_h_mkm_drop_source_point_decoded + S (mkm_exponent_drop_source_point) = S ((S (mkm_index_drop_source)) * vc)) /\ exists fs_q_mkm_drop_source_point_decoded. vb = fs_q_mkm_drop_source_point_decoded * S ((S (mkm_index_drop_source)) * vc) + (mkm_exponent_drop_source_point))) /\ (((exists bpv_gap_mkm_drop_source_point_valuation_exponent_bound. bpv_gap_mkm_drop_source_point_valuation_exponent_bound + mkm_exponent_drop_source_point = (mkm_value_drop_source_point)) /\ (exists bpv_result_mkm_drop_source_point_valuation_selected. ((exists ff_b_mkm_drop_source_point_valuation_selected_power ff_c_mkm_drop_source_point_valuation_selected_power. ((forall ff_i_mkm_drop_source_point_valuation_selected_power_repeat. (exists ff_lt_mkm_drop_source_point_valuation_selected_power_repeat_bound. ff_lt_mkm_drop_source_point_valuation_selected_power_repeat_bound + S ff_i_mkm_drop_source_point_valuation_selected_power_repeat = mkm_exponent_drop_source_point) -> (((exists ff_h_mkm_drop_source_point_valuation_selected_power_repeat_decoded. ff_h_mkm_drop_source_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_drop_source_point_valuation_selected_power_repeat)) * ff_c_mkm_drop_source_point_valuation_selected_power)) /\ exists ff_q_mkm_drop_source_point_valuation_selected_power_repeat_decoded. ff_b_mkm_drop_source_point_valuation_selected_power = ff_q_mkm_drop_source_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_drop_source_point_valuation_selected_power_repeat)) * ff_c_mkm_drop_source_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_drop_source_point_valuation_selected_power_product ff_v_mkm_drop_source_point_valuation_selected_power_product. ((((exists ff_h_mkm_drop_source_point_valuation_selected_power_product_start. ff_h_mkm_drop_source_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_drop_source_point_valuation_selected_power_product)) /\ exists ff_q_mkm_drop_source_point_valuation_selected_power_product_start. ff_u_mkm_drop_source_point_valuation_selected_power_product = ff_q_mkm_drop_source_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_drop_source_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_drop_source_point_valuation_selected_power_product_terminal. ff_h_mkm_drop_source_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_drop_source_point_valuation_selected) = S ((S (mkm_exponent_drop_source_point)) * ff_v_mkm_drop_source_point_valuation_selected_power_product)) /\ exists ff_q_mkm_drop_source_point_valuation_selected_power_product_terminal. ff_u_mkm_drop_source_point_valuation_selected_power_product = ff_q_mkm_drop_source_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_drop_source_point)) * ff_v_mkm_drop_source_point_valuation_selected_power_product) + (bpv_result_mkm_drop_source_point_valuation_selected))) /\ forall ff_i_mkm_drop_source_point_valuation_selected_power_product. (exists ff_lt_mkm_drop_source_point_valuation_selected_power_product_bound. ff_lt_mkm_drop_source_point_valuation_selected_power_product_bound + S ff_i_mkm_drop_source_point_valuation_selected_power_product = mkm_exponent_drop_source_point) -> exists ff_p_mkm_drop_source_point_valuation_selected_power_product ff_r_mkm_drop_source_point_valuation_selected_power_product ff_s_mkm_drop_source_point_valuation_selected_power_product. ((((exists ff_h_mkm_drop_source_point_valuation_selected_power_product_factor. ff_h_mkm_drop_source_point_valuation_selected_power_product_factor + S (ff_p_mkm_drop_source_point_valuation_selected_power_product) = S ((S (ff_i_mkm_drop_source_point_valuation_selected_power_product)) * ff_c_mkm_drop_source_point_valuation_selected_power)) /\ exists ff_q_mkm_drop_source_point_valuation_selected_power_product_factor. ff_b_mkm_drop_source_point_valuation_selected_power = ff_q_mkm_drop_source_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_drop_source_point_valuation_selected_power_product)) * ff_c_mkm_drop_source_point_valuation_selected_power) + (ff_p_mkm_drop_source_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_drop_source_point_valuation_selected_power_product_partial. ff_h_mkm_drop_source_point_valuation_selected_power_product_partial + S (ff_r_mkm_drop_source_point_valuation_selected_power_product) = S ((S (ff_i_mkm_drop_source_point_valuation_selected_power_product)) * ff_v_mkm_drop_source_point_valuation_selected_power_product)) /\ exists ff_q_mkm_drop_source_point_valuation_selected_power_product_partial. ff_u_mkm_drop_source_point_valuation_selected_power_product = ff_q_mkm_drop_source_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_drop_source_point_valuation_selected_power_product)) * ff_v_mkm_drop_source_point_valuation_selected_power_product) + (ff_r_mkm_drop_source_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_drop_source_point_valuation_selected_power_product_successor. ff_h_mkm_drop_source_point_valuation_selected_power_product_successor + S (ff_s_mkm_drop_source_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_drop_source_point_valuation_selected_power_product)) * ff_v_mkm_drop_source_point_valuation_selected_power_product)) /\ exists ff_q_mkm_drop_source_point_valuation_selected_power_product_successor. ff_u_mkm_drop_source_point_valuation_selected_power_product = ff_q_mkm_drop_source_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_drop_source_point_valuation_selected_power_product)) * ff_v_mkm_drop_source_point_valuation_selected_power_product) + (ff_s_mkm_drop_source_point_valuation_selected_power_product))) /\ ff_s_mkm_drop_source_point_valuation_selected_power_product = ff_r_mkm_drop_source_point_valuation_selected_power_product * ff_p_mkm_drop_source_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_drop_source_point_valuation_selected_divides. (mkm_value_drop_source_point) = bpv_result_mkm_drop_source_point_valuation_selected * bpv_factor_mkm_drop_source_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_drop_source_point_valuation. (exists bpv_gap_mkm_drop_source_point_valuation_candidate_bound. bpv_gap_mkm_drop_source_point_valuation_candidate_bound + bpv_candidate_mkm_drop_source_point_valuation = (mkm_value_drop_source_point)) -> (exists bpv_result_mkm_drop_source_point_valuation_candidate. ((exists ff_b_mkm_drop_source_point_valuation_candidate_power ff_c_mkm_drop_source_point_valuation_candidate_power. ((forall ff_i_mkm_drop_source_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_drop_source_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_drop_source_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_drop_source_point_valuation_candidate_power_repeat = bpv_candidate_mkm_drop_source_point_valuation) -> (((exists ff_h_mkm_drop_source_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_drop_source_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_drop_source_point_valuation_candidate_power_repeat)) * ff_c_mkm_drop_source_point_valuation_candidate_power)) /\ exists ff_q_mkm_drop_source_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_drop_source_point_valuation_candidate_power = ff_q_mkm_drop_source_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_drop_source_point_valuation_candidate_power_repeat)) * ff_c_mkm_drop_source_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_drop_source_point_valuation_candidate_power_product ff_v_mkm_drop_source_point_valuation_candidate_power_product. ((((exists ff_h_mkm_drop_source_point_valuation_candidate_power_product_start. ff_h_mkm_drop_source_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_drop_source_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_drop_source_point_valuation_candidate_power_product_start. ff_u_mkm_drop_source_point_valuation_candidate_power_product = ff_q_mkm_drop_source_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_drop_source_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_drop_source_point_valuation_candidate_power_product_terminal. ff_h_mkm_drop_source_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_drop_source_point_valuation_candidate) = S ((S (bpv_candidate_mkm_drop_source_point_valuation)) * ff_v_mkm_drop_source_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_drop_source_point_valuation_candidate_power_product_terminal. ff_u_mkm_drop_source_point_valuation_candidate_power_product = ff_q_mkm_drop_source_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_drop_source_point_valuation)) * ff_v_mkm_drop_source_point_valuation_candidate_power_product) + (bpv_result_mkm_drop_source_point_valuation_candidate))) /\ forall ff_i_mkm_drop_source_point_valuation_candidate_power_product. (exists ff_lt_mkm_drop_source_point_valuation_candidate_power_product_bound. ff_lt_mkm_drop_source_point_valuation_candidate_power_product_bound + S ff_i_mkm_drop_source_point_valuation_candidate_power_product = bpv_candidate_mkm_drop_source_point_valuation) -> exists ff_p_mkm_drop_source_point_valuation_candidate_power_product ff_r_mkm_drop_source_point_valuation_candidate_power_product ff_s_mkm_drop_source_point_valuation_candidate_power_product. ((((exists ff_h_mkm_drop_source_point_valuation_candidate_power_product_factor. ff_h_mkm_drop_source_point_valuation_candidate_power_product_factor + S (ff_p_mkm_drop_source_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_drop_source_point_valuation_candidate_power_product)) * ff_c_mkm_drop_source_point_valuation_candidate_power)) /\ exists ff_q_mkm_drop_source_point_valuation_candidate_power_product_factor. ff_b_mkm_drop_source_point_valuation_candidate_power = ff_q_mkm_drop_source_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_drop_source_point_valuation_candidate_power_product)) * ff_c_mkm_drop_source_point_valuation_candidate_power) + (ff_p_mkm_drop_source_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_drop_source_point_valuation_candidate_power_product_partial. ff_h_mkm_drop_source_point_valuation_candidate_power_product_partial + S (ff_r_mkm_drop_source_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_drop_source_point_valuation_candidate_power_product)) * ff_v_mkm_drop_source_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_drop_source_point_valuation_candidate_power_product_partial. ff_u_mkm_drop_source_point_valuation_candidate_power_product = ff_q_mkm_drop_source_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_drop_source_point_valuation_candidate_power_product)) * ff_v_mkm_drop_source_point_valuation_candidate_power_product) + (ff_r_mkm_drop_source_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_drop_source_point_valuation_candidate_power_product_successor. ff_h_mkm_drop_source_point_valuation_candidate_power_product_successor + S (ff_s_mkm_drop_source_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_drop_source_point_valuation_candidate_power_product)) * ff_v_mkm_drop_source_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_drop_source_point_valuation_candidate_power_product_successor. ff_u_mkm_drop_source_point_valuation_candidate_power_product = ff_q_mkm_drop_source_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_drop_source_point_valuation_candidate_power_product)) * ff_v_mkm_drop_source_point_valuation_candidate_power_product) + (ff_s_mkm_drop_source_point_valuation_candidate_power_product))) /\ ff_s_mkm_drop_source_point_valuation_candidate_power_product = ff_r_mkm_drop_source_point_valuation_candidate_power_product * ff_p_mkm_drop_source_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_drop_source_point_valuation_candidate_divides. (mkm_value_drop_source_point) = bpv_result_mkm_drop_source_point_valuation_candidate * bpv_factor_mkm_drop_source_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_drop_source_point_valuation_maximal. bpv_gap_mkm_drop_source_point_valuation_maximal + bpv_candidate_mkm_drop_source_point_valuation = mkm_exponent_drop_source_point))))) -> (forall mkm_index_drop_target. (exists mkm_lt_drop_target_bound. mkm_lt_drop_target_bound + S (mkm_index_drop_target) = (l)) -> (exists mkm_value_drop_target_point mkm_exponent_drop_target_point. (((exists fs_h_mkm_drop_target_point_source. fs_h_mkm_drop_target_point_source + S (mkm_value_drop_target_point) = S ((S (mkm_index_drop_target)) * c)) /\ exists fs_q_mkm_drop_target_point_source. b = fs_q_mkm_drop_target_point_source * S ((S (mkm_index_drop_target)) * c) + (mkm_value_drop_target_point))) /\ ((((exists fs_h_mkm_drop_target_point_decoded. fs_h_mkm_drop_target_point_decoded + S (mkm_exponent_drop_target_point) = S ((S (mkm_index_drop_target)) * vc)) /\ exists fs_q_mkm_drop_target_point_decoded. vb = fs_q_mkm_drop_target_point_decoded * S ((S (mkm_index_drop_target)) * vc) + (mkm_exponent_drop_target_point))) /\ (((exists bpv_gap_mkm_drop_target_point_valuation_exponent_bound. bpv_gap_mkm_drop_target_point_valuation_exponent_bound + mkm_exponent_drop_target_point = (mkm_value_drop_target_point)) /\ (exists bpv_result_mkm_drop_target_point_valuation_selected. ((exists ff_b_mkm_drop_target_point_valuation_selected_power ff_c_mkm_drop_target_point_valuation_selected_power. ((forall ff_i_mkm_drop_target_point_valuation_selected_power_repeat. (exists ff_lt_mkm_drop_target_point_valuation_selected_power_repeat_bound. ff_lt_mkm_drop_target_point_valuation_selected_power_repeat_bound + S ff_i_mkm_drop_target_point_valuation_selected_power_repeat = mkm_exponent_drop_target_point) -> (((exists ff_h_mkm_drop_target_point_valuation_selected_power_repeat_decoded. ff_h_mkm_drop_target_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_drop_target_point_valuation_selected_power_repeat)) * ff_c_mkm_drop_target_point_valuation_selected_power)) /\ exists ff_q_mkm_drop_target_point_valuation_selected_power_repeat_decoded. ff_b_mkm_drop_target_point_valuation_selected_power = ff_q_mkm_drop_target_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_drop_target_point_valuation_selected_power_repeat)) * ff_c_mkm_drop_target_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_drop_target_point_valuation_selected_power_product ff_v_mkm_drop_target_point_valuation_selected_power_product. ((((exists ff_h_mkm_drop_target_point_valuation_selected_power_product_start. ff_h_mkm_drop_target_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_drop_target_point_valuation_selected_power_product)) /\ exists ff_q_mkm_drop_target_point_valuation_selected_power_product_start. ff_u_mkm_drop_target_point_valuation_selected_power_product = ff_q_mkm_drop_target_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_drop_target_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_drop_target_point_valuation_selected_power_product_terminal. ff_h_mkm_drop_target_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_drop_target_point_valuation_selected) = S ((S (mkm_exponent_drop_target_point)) * ff_v_mkm_drop_target_point_valuation_selected_power_product)) /\ exists ff_q_mkm_drop_target_point_valuation_selected_power_product_terminal. ff_u_mkm_drop_target_point_valuation_selected_power_product = ff_q_mkm_drop_target_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_drop_target_point)) * ff_v_mkm_drop_target_point_valuation_selected_power_product) + (bpv_result_mkm_drop_target_point_valuation_selected))) /\ forall ff_i_mkm_drop_target_point_valuation_selected_power_product. (exists ff_lt_mkm_drop_target_point_valuation_selected_power_product_bound. ff_lt_mkm_drop_target_point_valuation_selected_power_product_bound + S ff_i_mkm_drop_target_point_valuation_selected_power_product = mkm_exponent_drop_target_point) -> exists ff_p_mkm_drop_target_point_valuation_selected_power_product ff_r_mkm_drop_target_point_valuation_selected_power_product ff_s_mkm_drop_target_point_valuation_selected_power_product. ((((exists ff_h_mkm_drop_target_point_valuation_selected_power_product_factor. ff_h_mkm_drop_target_point_valuation_selected_power_product_factor + S (ff_p_mkm_drop_target_point_valuation_selected_power_product) = S ((S (ff_i_mkm_drop_target_point_valuation_selected_power_product)) * ff_c_mkm_drop_target_point_valuation_selected_power)) /\ exists ff_q_mkm_drop_target_point_valuation_selected_power_product_factor. ff_b_mkm_drop_target_point_valuation_selected_power = ff_q_mkm_drop_target_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_drop_target_point_valuation_selected_power_product)) * ff_c_mkm_drop_target_point_valuation_selected_power) + (ff_p_mkm_drop_target_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_drop_target_point_valuation_selected_power_product_partial. ff_h_mkm_drop_target_point_valuation_selected_power_product_partial + S (ff_r_mkm_drop_target_point_valuation_selected_power_product) = S ((S (ff_i_mkm_drop_target_point_valuation_selected_power_product)) * ff_v_mkm_drop_target_point_valuation_selected_power_product)) /\ exists ff_q_mkm_drop_target_point_valuation_selected_power_product_partial. ff_u_mkm_drop_target_point_valuation_selected_power_product = ff_q_mkm_drop_target_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_drop_target_point_valuation_selected_power_product)) * ff_v_mkm_drop_target_point_valuation_selected_power_product) + (ff_r_mkm_drop_target_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_drop_target_point_valuation_selected_power_product_successor. ff_h_mkm_drop_target_point_valuation_selected_power_product_successor + S (ff_s_mkm_drop_target_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_drop_target_point_valuation_selected_power_product)) * ff_v_mkm_drop_target_point_valuation_selected_power_product)) /\ exists ff_q_mkm_drop_target_point_valuation_selected_power_product_successor. ff_u_mkm_drop_target_point_valuation_selected_power_product = ff_q_mkm_drop_target_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_drop_target_point_valuation_selected_power_product)) * ff_v_mkm_drop_target_point_valuation_selected_power_product) + (ff_s_mkm_drop_target_point_valuation_selected_power_product))) /\ ff_s_mkm_drop_target_point_valuation_selected_power_product = ff_r_mkm_drop_target_point_valuation_selected_power_product * ff_p_mkm_drop_target_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_drop_target_point_valuation_selected_divides. (mkm_value_drop_target_point) = bpv_result_mkm_drop_target_point_valuation_selected * bpv_factor_mkm_drop_target_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_drop_target_point_valuation. (exists bpv_gap_mkm_drop_target_point_valuation_candidate_bound. bpv_gap_mkm_drop_target_point_valuation_candidate_bound + bpv_candidate_mkm_drop_target_point_valuation = (mkm_value_drop_target_point)) -> (exists bpv_result_mkm_drop_target_point_valuation_candidate. ((exists ff_b_mkm_drop_target_point_valuation_candidate_power ff_c_mkm_drop_target_point_valuation_candidate_power. ((forall ff_i_mkm_drop_target_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_drop_target_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_drop_target_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_drop_target_point_valuation_candidate_power_repeat = bpv_candidate_mkm_drop_target_point_valuation) -> (((exists ff_h_mkm_drop_target_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_drop_target_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_drop_target_point_valuation_candidate_power_repeat)) * ff_c_mkm_drop_target_point_valuation_candidate_power)) /\ exists ff_q_mkm_drop_target_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_drop_target_point_valuation_candidate_power = ff_q_mkm_drop_target_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_drop_target_point_valuation_candidate_power_repeat)) * ff_c_mkm_drop_target_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_drop_target_point_valuation_candidate_power_product ff_v_mkm_drop_target_point_valuation_candidate_power_product. ((((exists ff_h_mkm_drop_target_point_valuation_candidate_power_product_start. ff_h_mkm_drop_target_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_drop_target_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_drop_target_point_valuation_candidate_power_product_start. ff_u_mkm_drop_target_point_valuation_candidate_power_product = ff_q_mkm_drop_target_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_drop_target_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_drop_target_point_valuation_candidate_power_product_terminal. ff_h_mkm_drop_target_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_drop_target_point_valuation_candidate) = S ((S (bpv_candidate_mkm_drop_target_point_valuation)) * ff_v_mkm_drop_target_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_drop_target_point_valuation_candidate_power_product_terminal. ff_u_mkm_drop_target_point_valuation_candidate_power_product = ff_q_mkm_drop_target_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_drop_target_point_valuation)) * ff_v_mkm_drop_target_point_valuation_candidate_power_product) + (bpv_result_mkm_drop_target_point_valuation_candidate))) /\ forall ff_i_mkm_drop_target_point_valuation_candidate_power_product. (exists ff_lt_mkm_drop_target_point_valuation_candidate_power_product_bound. ff_lt_mkm_drop_target_point_valuation_candidate_power_product_bound + S ff_i_mkm_drop_target_point_valuation_candidate_power_product = bpv_candidate_mkm_drop_target_point_valuation) -> exists ff_p_mkm_drop_target_point_valuation_candidate_power_product ff_r_mkm_drop_target_point_valuation_candidate_power_product ff_s_mkm_drop_target_point_valuation_candidate_power_product. ((((exists ff_h_mkm_drop_target_point_valuation_candidate_power_product_factor. ff_h_mkm_drop_target_point_valuation_candidate_power_product_factor + S (ff_p_mkm_drop_target_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_drop_target_point_valuation_candidate_power_product)) * ff_c_mkm_drop_target_point_valuation_candidate_power)) /\ exists ff_q_mkm_drop_target_point_valuation_candidate_power_product_factor. ff_b_mkm_drop_target_point_valuation_candidate_power = ff_q_mkm_drop_target_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_drop_target_point_valuation_candidate_power_product)) * ff_c_mkm_drop_target_point_valuation_candidate_power) + (ff_p_mkm_drop_target_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_drop_target_point_valuation_candidate_power_product_partial. ff_h_mkm_drop_target_point_valuation_candidate_power_product_partial + S (ff_r_mkm_drop_target_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_drop_target_point_valuation_candidate_power_product)) * ff_v_mkm_drop_target_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_drop_target_point_valuation_candidate_power_product_partial. ff_u_mkm_drop_target_point_valuation_candidate_power_product = ff_q_mkm_drop_target_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_drop_target_point_valuation_candidate_power_product)) * ff_v_mkm_drop_target_point_valuation_candidate_power_product) + (ff_r_mkm_drop_target_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_drop_target_point_valuation_candidate_power_product_successor. ff_h_mkm_drop_target_point_valuation_candidate_power_product_successor + S (ff_s_mkm_drop_target_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_drop_target_point_valuation_candidate_power_product)) * ff_v_mkm_drop_target_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_drop_target_point_valuation_candidate_power_product_successor. ff_u_mkm_drop_target_point_valuation_candidate_power_product = ff_q_mkm_drop_target_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_drop_target_point_valuation_candidate_power_product)) * ff_v_mkm_drop_target_point_valuation_candidate_power_product) + (ff_s_mkm_drop_target_point_valuation_candidate_power_product))) /\ ff_s_mkm_drop_target_point_valuation_candidate_power_product = ff_r_mkm_drop_target_point_valuation_candidate_power_product * ff_p_mkm_drop_target_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_drop_target_point_valuation_candidate_divides. (mkm_value_drop_target_point) = bpv_result_mkm_drop_target_point_valuation_candidate * bpv_factor_mkm_drop_target_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_drop_target_point_valuation_maximal. bpv_gap_mkm_drop_target_point_valuation_maximal + bpv_candidate_mkm_drop_target_point_valuation = mkm_exponent_drop_target_point)))))Complete tactic proof in conservative notation
All 15 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
15 script commands · 2 reading checkpoints · 0 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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.