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.
This is a shared constructive tool, not an additional major blueprint goal. The list covers every prime divisor, has no repeated primes, and contains actual prime-power values. One uses the empty support; zero is excluded.
Exact theorem in conservative defined notation
∀ p. ∀ n. ∀ e. ∀ f. e = f → BoundedPowerValuation(p,n,n,e) → BoundedPowerValuation(p,n,n,f)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
none
Original expanded first-order statement
forall p n e f. e = f -> (((exists bpd_gap_pvs_transport_source_selected_bound. bpd_gap_pvs_transport_source_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_transport_source_selected. ((exists bpvi_b_pvs_transport_source_selected_power bpvi_c_pvs_transport_source_selected_power. ((forall bpvi_i_pvs_transport_source_selected_power. (exists bpvi_repeat_gap_pvs_transport_source_selected_power. bpvi_repeat_gap_pvs_transport_source_selected_power + S bpvi_i_pvs_transport_source_selected_power = e) -> (((exists bpvi_h_pvs_transport_source_selected_power_repeat. bpvi_h_pvs_transport_source_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_transport_source_selected_power)) * bpvi_c_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_repeat. bpvi_b_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_repeat * S ((S (bpvi_i_pvs_transport_source_selected_power)) * bpvi_c_pvs_transport_source_selected_power) + (p)))) /\ (exists bpvi_u_pvs_transport_source_selected_power bpvi_v_pvs_transport_source_selected_power. ((((exists bpvi_h_pvs_transport_source_selected_power_start. bpvi_h_pvs_transport_source_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_start. bpvi_u_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_start * S ((S (0)) * bpvi_v_pvs_transport_source_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_transport_source_selected_power_terminal. bpvi_h_pvs_transport_source_selected_power_terminal + S (bpvi_result_pvs_transport_source_selected) = S ((S (e)) * bpvi_v_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_terminal. bpvi_u_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_transport_source_selected_power) + (bpvi_result_pvs_transport_source_selected))) /\ forall bpvi_j_pvs_transport_source_selected_power. (exists bpvi_product_gap_pvs_transport_source_selected_power. bpvi_product_gap_pvs_transport_source_selected_power + S bpvi_j_pvs_transport_source_selected_power = e) -> exists bpvi_factor_pvs_transport_source_selected_power bpvi_partial_pvs_transport_source_selected_power bpvi_successor_pvs_transport_source_selected_power. ((((exists bpvi_h_pvs_transport_source_selected_power_factor. bpvi_h_pvs_transport_source_selected_power_factor + S (bpvi_factor_pvs_transport_source_selected_power) = S ((S (bpvi_j_pvs_transport_source_selected_power)) * bpvi_c_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_factor. bpvi_b_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_factor * S ((S (bpvi_j_pvs_transport_source_selected_power)) * bpvi_c_pvs_transport_source_selected_power) + (bpvi_factor_pvs_transport_source_selected_power))) /\ ((((exists bpvi_h_pvs_transport_source_selected_power_partial. bpvi_h_pvs_transport_source_selected_power_partial + S (bpvi_partial_pvs_transport_source_selected_power) = S ((S (bpvi_j_pvs_transport_source_selected_power)) * bpvi_v_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_partial. bpvi_u_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_partial * S ((S (bpvi_j_pvs_transport_source_selected_power)) * bpvi_v_pvs_transport_source_selected_power) + (bpvi_partial_pvs_transport_source_selected_power))) /\ ((((exists bpvi_h_pvs_transport_source_selected_power_successor. bpvi_h_pvs_transport_source_selected_power_successor + S (bpvi_successor_pvs_transport_source_selected_power) = S ((S (S bpvi_j_pvs_transport_source_selected_power)) * bpvi_v_pvs_transport_source_selected_power)) /\ exists bpvi_q_pvs_transport_source_selected_power_successor. bpvi_u_pvs_transport_source_selected_power = bpvi_q_pvs_transport_source_selected_power_successor * S ((S (S bpvi_j_pvs_transport_source_selected_power)) * bpvi_v_pvs_transport_source_selected_power) + (bpvi_successor_pvs_transport_source_selected_power))) /\ bpvi_successor_pvs_transport_source_selected_power = bpvi_partial_pvs_transport_source_selected_power * bpvi_factor_pvs_transport_source_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_transport_source_selected. n = bpvi_result_pvs_transport_source_selected * bpvi_divisor_factor_pvs_transport_source_selected))) /\ forall bpd_candidate_pvs_transport_source. (exists bpd_gap_pvs_transport_source_candidate_bound. bpd_gap_pvs_transport_source_candidate_bound + (bpd_candidate_pvs_transport_source) = (n)) -> (exists bpvi_result_pvs_transport_source_candidate. ((exists bpvi_b_pvs_transport_source_candidate_power bpvi_c_pvs_transport_source_candidate_power. ((forall bpvi_i_pvs_transport_source_candidate_power. (exists bpvi_repeat_gap_pvs_transport_source_candidate_power. bpvi_repeat_gap_pvs_transport_source_candidate_power + S bpvi_i_pvs_transport_source_candidate_power = bpd_candidate_pvs_transport_source) -> (((exists bpvi_h_pvs_transport_source_candidate_power_repeat. bpvi_h_pvs_transport_source_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_transport_source_candidate_power)) * bpvi_c_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_repeat. bpvi_b_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_repeat * S ((S (bpvi_i_pvs_transport_source_candidate_power)) * bpvi_c_pvs_transport_source_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_transport_source_candidate_power bpvi_v_pvs_transport_source_candidate_power. ((((exists bpvi_h_pvs_transport_source_candidate_power_start. bpvi_h_pvs_transport_source_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_start. bpvi_u_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_start * S ((S (0)) * bpvi_v_pvs_transport_source_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_transport_source_candidate_power_terminal. bpvi_h_pvs_transport_source_candidate_power_terminal + S (bpvi_result_pvs_transport_source_candidate) = S ((S (bpd_candidate_pvs_transport_source)) * bpvi_v_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_terminal. bpvi_u_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_terminal * S ((S (bpd_candidate_pvs_transport_source)) * bpvi_v_pvs_transport_source_candidate_power) + (bpvi_result_pvs_transport_source_candidate))) /\ forall bpvi_j_pvs_transport_source_candidate_power. (exists bpvi_product_gap_pvs_transport_source_candidate_power. bpvi_product_gap_pvs_transport_source_candidate_power + S bpvi_j_pvs_transport_source_candidate_power = bpd_candidate_pvs_transport_source) -> exists bpvi_factor_pvs_transport_source_candidate_power bpvi_partial_pvs_transport_source_candidate_power bpvi_successor_pvs_transport_source_candidate_power. ((((exists bpvi_h_pvs_transport_source_candidate_power_factor. bpvi_h_pvs_transport_source_candidate_power_factor + S (bpvi_factor_pvs_transport_source_candidate_power) = S ((S (bpvi_j_pvs_transport_source_candidate_power)) * bpvi_c_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_factor. bpvi_b_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_factor * S ((S (bpvi_j_pvs_transport_source_candidate_power)) * bpvi_c_pvs_transport_source_candidate_power) + (bpvi_factor_pvs_transport_source_candidate_power))) /\ ((((exists bpvi_h_pvs_transport_source_candidate_power_partial. bpvi_h_pvs_transport_source_candidate_power_partial + S (bpvi_partial_pvs_transport_source_candidate_power) = S ((S (bpvi_j_pvs_transport_source_candidate_power)) * bpvi_v_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_partial. bpvi_u_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_partial * S ((S (bpvi_j_pvs_transport_source_candidate_power)) * bpvi_v_pvs_transport_source_candidate_power) + (bpvi_partial_pvs_transport_source_candidate_power))) /\ ((((exists bpvi_h_pvs_transport_source_candidate_power_successor. bpvi_h_pvs_transport_source_candidate_power_successor + S (bpvi_successor_pvs_transport_source_candidate_power) = S ((S (S bpvi_j_pvs_transport_source_candidate_power)) * bpvi_v_pvs_transport_source_candidate_power)) /\ exists bpvi_q_pvs_transport_source_candidate_power_successor. bpvi_u_pvs_transport_source_candidate_power = bpvi_q_pvs_transport_source_candidate_power_successor * S ((S (S bpvi_j_pvs_transport_source_candidate_power)) * bpvi_v_pvs_transport_source_candidate_power) + (bpvi_successor_pvs_transport_source_candidate_power))) /\ bpvi_successor_pvs_transport_source_candidate_power = bpvi_partial_pvs_transport_source_candidate_power * bpvi_factor_pvs_transport_source_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_transport_source_candidate. n = bpvi_result_pvs_transport_source_candidate * bpvi_divisor_factor_pvs_transport_source_candidate)) -> (exists bpd_gap_pvs_transport_source_maximal. bpd_gap_pvs_transport_source_maximal + (bpd_candidate_pvs_transport_source) = (e))) -> (((exists bpd_gap_pvs_transport_target_selected_bound. bpd_gap_pvs_transport_target_selected_bound + (f) = (n)) /\ (exists bpvi_result_pvs_transport_target_selected. ((exists bpvi_b_pvs_transport_target_selected_power bpvi_c_pvs_transport_target_selected_power. ((forall bpvi_i_pvs_transport_target_selected_power. (exists bpvi_repeat_gap_pvs_transport_target_selected_power. bpvi_repeat_gap_pvs_transport_target_selected_power + S bpvi_i_pvs_transport_target_selected_power = f) -> (((exists bpvi_h_pvs_transport_target_selected_power_repeat. bpvi_h_pvs_transport_target_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_transport_target_selected_power)) * bpvi_c_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_repeat. bpvi_b_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_repeat * S ((S (bpvi_i_pvs_transport_target_selected_power)) * bpvi_c_pvs_transport_target_selected_power) + (p)))) /\ (exists bpvi_u_pvs_transport_target_selected_power bpvi_v_pvs_transport_target_selected_power. ((((exists bpvi_h_pvs_transport_target_selected_power_start. bpvi_h_pvs_transport_target_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_start. bpvi_u_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_start * S ((S (0)) * bpvi_v_pvs_transport_target_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_transport_target_selected_power_terminal. bpvi_h_pvs_transport_target_selected_power_terminal + S (bpvi_result_pvs_transport_target_selected) = S ((S (f)) * bpvi_v_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_terminal. bpvi_u_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_terminal * S ((S (f)) * bpvi_v_pvs_transport_target_selected_power) + (bpvi_result_pvs_transport_target_selected))) /\ forall bpvi_j_pvs_transport_target_selected_power. (exists bpvi_product_gap_pvs_transport_target_selected_power. bpvi_product_gap_pvs_transport_target_selected_power + S bpvi_j_pvs_transport_target_selected_power = f) -> exists bpvi_factor_pvs_transport_target_selected_power bpvi_partial_pvs_transport_target_selected_power bpvi_successor_pvs_transport_target_selected_power. ((((exists bpvi_h_pvs_transport_target_selected_power_factor. bpvi_h_pvs_transport_target_selected_power_factor + S (bpvi_factor_pvs_transport_target_selected_power) = S ((S (bpvi_j_pvs_transport_target_selected_power)) * bpvi_c_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_factor. bpvi_b_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_factor * S ((S (bpvi_j_pvs_transport_target_selected_power)) * bpvi_c_pvs_transport_target_selected_power) + (bpvi_factor_pvs_transport_target_selected_power))) /\ ((((exists bpvi_h_pvs_transport_target_selected_power_partial. bpvi_h_pvs_transport_target_selected_power_partial + S (bpvi_partial_pvs_transport_target_selected_power) = S ((S (bpvi_j_pvs_transport_target_selected_power)) * bpvi_v_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_partial. bpvi_u_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_partial * S ((S (bpvi_j_pvs_transport_target_selected_power)) * bpvi_v_pvs_transport_target_selected_power) + (bpvi_partial_pvs_transport_target_selected_power))) /\ ((((exists bpvi_h_pvs_transport_target_selected_power_successor. bpvi_h_pvs_transport_target_selected_power_successor + S (bpvi_successor_pvs_transport_target_selected_power) = S ((S (S bpvi_j_pvs_transport_target_selected_power)) * bpvi_v_pvs_transport_target_selected_power)) /\ exists bpvi_q_pvs_transport_target_selected_power_successor. bpvi_u_pvs_transport_target_selected_power = bpvi_q_pvs_transport_target_selected_power_successor * S ((S (S bpvi_j_pvs_transport_target_selected_power)) * bpvi_v_pvs_transport_target_selected_power) + (bpvi_successor_pvs_transport_target_selected_power))) /\ bpvi_successor_pvs_transport_target_selected_power = bpvi_partial_pvs_transport_target_selected_power * bpvi_factor_pvs_transport_target_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_transport_target_selected. n = bpvi_result_pvs_transport_target_selected * bpvi_divisor_factor_pvs_transport_target_selected))) /\ forall bpd_candidate_pvs_transport_target. (exists bpd_gap_pvs_transport_target_candidate_bound. bpd_gap_pvs_transport_target_candidate_bound + (bpd_candidate_pvs_transport_target) = (n)) -> (exists bpvi_result_pvs_transport_target_candidate. ((exists bpvi_b_pvs_transport_target_candidate_power bpvi_c_pvs_transport_target_candidate_power. ((forall bpvi_i_pvs_transport_target_candidate_power. (exists bpvi_repeat_gap_pvs_transport_target_candidate_power. bpvi_repeat_gap_pvs_transport_target_candidate_power + S bpvi_i_pvs_transport_target_candidate_power = bpd_candidate_pvs_transport_target) -> (((exists bpvi_h_pvs_transport_target_candidate_power_repeat. bpvi_h_pvs_transport_target_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_transport_target_candidate_power)) * bpvi_c_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_repeat. bpvi_b_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_repeat * S ((S (bpvi_i_pvs_transport_target_candidate_power)) * bpvi_c_pvs_transport_target_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_transport_target_candidate_power bpvi_v_pvs_transport_target_candidate_power. ((((exists bpvi_h_pvs_transport_target_candidate_power_start. bpvi_h_pvs_transport_target_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_start. bpvi_u_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_start * S ((S (0)) * bpvi_v_pvs_transport_target_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_transport_target_candidate_power_terminal. bpvi_h_pvs_transport_target_candidate_power_terminal + S (bpvi_result_pvs_transport_target_candidate) = S ((S (bpd_candidate_pvs_transport_target)) * bpvi_v_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_terminal. bpvi_u_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_terminal * S ((S (bpd_candidate_pvs_transport_target)) * bpvi_v_pvs_transport_target_candidate_power) + (bpvi_result_pvs_transport_target_candidate))) /\ forall bpvi_j_pvs_transport_target_candidate_power. (exists bpvi_product_gap_pvs_transport_target_candidate_power. bpvi_product_gap_pvs_transport_target_candidate_power + S bpvi_j_pvs_transport_target_candidate_power = bpd_candidate_pvs_transport_target) -> exists bpvi_factor_pvs_transport_target_candidate_power bpvi_partial_pvs_transport_target_candidate_power bpvi_successor_pvs_transport_target_candidate_power. ((((exists bpvi_h_pvs_transport_target_candidate_power_factor. bpvi_h_pvs_transport_target_candidate_power_factor + S (bpvi_factor_pvs_transport_target_candidate_power) = S ((S (bpvi_j_pvs_transport_target_candidate_power)) * bpvi_c_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_factor. bpvi_b_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_factor * S ((S (bpvi_j_pvs_transport_target_candidate_power)) * bpvi_c_pvs_transport_target_candidate_power) + (bpvi_factor_pvs_transport_target_candidate_power))) /\ ((((exists bpvi_h_pvs_transport_target_candidate_power_partial. bpvi_h_pvs_transport_target_candidate_power_partial + S (bpvi_partial_pvs_transport_target_candidate_power) = S ((S (bpvi_j_pvs_transport_target_candidate_power)) * bpvi_v_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_partial. bpvi_u_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_partial * S ((S (bpvi_j_pvs_transport_target_candidate_power)) * bpvi_v_pvs_transport_target_candidate_power) + (bpvi_partial_pvs_transport_target_candidate_power))) /\ ((((exists bpvi_h_pvs_transport_target_candidate_power_successor. bpvi_h_pvs_transport_target_candidate_power_successor + S (bpvi_successor_pvs_transport_target_candidate_power) = S ((S (S bpvi_j_pvs_transport_target_candidate_power)) * bpvi_v_pvs_transport_target_candidate_power)) /\ exists bpvi_q_pvs_transport_target_candidate_power_successor. bpvi_u_pvs_transport_target_candidate_power = bpvi_q_pvs_transport_target_candidate_power_successor * S ((S (S bpvi_j_pvs_transport_target_candidate_power)) * bpvi_v_pvs_transport_target_candidate_power) + (bpvi_successor_pvs_transport_target_candidate_power))) /\ bpvi_successor_pvs_transport_target_candidate_power = bpvi_partial_pvs_transport_target_candidate_power * bpvi_factor_pvs_transport_target_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_transport_target_candidate. n = bpvi_result_pvs_transport_target_candidate * bpvi_divisor_factor_pvs_transport_target_candidate)) -> (exists bpd_gap_pvs_transport_target_maximal. bpd_gap_pvs_transport_target_maximal + (bpd_candidate_pvs_transport_target) = (f)))Complete tactic proof in conservative notation
All 13 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
13 script commands · 3 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.
01Fix variables and assumptionsL1–6
02Calculate and transport equalitiesL7–12
03Use earlier factsL13–13
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L13
exact hval