Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ p. ∀ n. ∃ e. FactorialValuation(p,n,e)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
1 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall p n. exists e. (exists bfv_factorial_bfv_total. ((exists ff_b_bfv_total_factorial ff_c_bfv_total_factorial. ((forall ff_i_bfv_total_factorial_range. (exists ff_lt_bfv_total_factorial_range_bound. ff_lt_bfv_total_factorial_range_bound + S ff_i_bfv_total_factorial_range = n) -> (((exists ff_h_bfv_total_factorial_range_decoded. ff_h_bfv_total_factorial_range_decoded + S (1 + ff_i_bfv_total_factorial_range) = S ((S (ff_i_bfv_total_factorial_range)) * ff_c_bfv_total_factorial)) /\ exists ff_q_bfv_total_factorial_range_decoded. ff_b_bfv_total_factorial = ff_q_bfv_total_factorial_range_decoded * S ((S (ff_i_bfv_total_factorial_range)) * ff_c_bfv_total_factorial) + (1 + ff_i_bfv_total_factorial_range)))) /\ (exists ff_u_bfv_total_factorial_product ff_v_bfv_total_factorial_product. ((((exists ff_h_bfv_total_factorial_product_start. ff_h_bfv_total_factorial_product_start + S (1) = S ((S (0)) * ff_v_bfv_total_factorial_product)) /\ exists ff_q_bfv_total_factorial_product_start. ff_u_bfv_total_factorial_product = ff_q_bfv_total_factorial_product_start * S ((S (0)) * ff_v_bfv_total_factorial_product) + (1))) /\ ((((exists ff_h_bfv_total_factorial_product_terminal. ff_h_bfv_total_factorial_product_terminal + S (bfv_factorial_bfv_total) = S ((S (n)) * ff_v_bfv_total_factorial_product)) /\ exists ff_q_bfv_total_factorial_product_terminal. ff_u_bfv_total_factorial_product = ff_q_bfv_total_factorial_product_terminal * S ((S (n)) * ff_v_bfv_total_factorial_product) + (bfv_factorial_bfv_total))) /\ forall ff_i_bfv_total_factorial_product. (exists ff_lt_bfv_total_factorial_product_bound. ff_lt_bfv_total_factorial_product_bound + S ff_i_bfv_total_factorial_product = n) -> exists ff_p_bfv_total_factorial_product ff_r_bfv_total_factorial_product ff_s_bfv_total_factorial_product. ((((exists ff_h_bfv_total_factorial_product_factor. ff_h_bfv_total_factorial_product_factor + S (ff_p_bfv_total_factorial_product) = S ((S (ff_i_bfv_total_factorial_product)) * ff_c_bfv_total_factorial)) /\ exists ff_q_bfv_total_factorial_product_factor. ff_b_bfv_total_factorial = ff_q_bfv_total_factorial_product_factor * S ((S (ff_i_bfv_total_factorial_product)) * ff_c_bfv_total_factorial) + (ff_p_bfv_total_factorial_product))) /\ ((((exists ff_h_bfv_total_factorial_product_partial. ff_h_bfv_total_factorial_product_partial + S (ff_r_bfv_total_factorial_product) = S ((S (ff_i_bfv_total_factorial_product)) * ff_v_bfv_total_factorial_product)) /\ exists ff_q_bfv_total_factorial_product_partial. ff_u_bfv_total_factorial_product = ff_q_bfv_total_factorial_product_partial * S ((S (ff_i_bfv_total_factorial_product)) * ff_v_bfv_total_factorial_product) + (ff_r_bfv_total_factorial_product))) /\ ((((exists ff_h_bfv_total_factorial_product_successor. ff_h_bfv_total_factorial_product_successor + S (ff_s_bfv_total_factorial_product) = S ((S (S ff_i_bfv_total_factorial_product)) * ff_v_bfv_total_factorial_product)) /\ exists ff_q_bfv_total_factorial_product_successor. ff_u_bfv_total_factorial_product = ff_q_bfv_total_factorial_product_successor * S ((S (S ff_i_bfv_total_factorial_product)) * ff_v_bfv_total_factorial_product) + (ff_s_bfv_total_factorial_product))) /\ ff_s_bfv_total_factorial_product = ff_r_bfv_total_factorial_product * ff_p_bfv_total_factorial_product)))))))) /\ (((exists bpv_gap_bfv_total_valuation_exponent_bound. bpv_gap_bfv_total_valuation_exponent_bound + e = bfv_factorial_bfv_total) /\ (exists bpv_result_bfv_total_valuation_selected. ((exists ff_b_bfv_total_valuation_selected_power ff_c_bfv_total_valuation_selected_power. ((forall ff_i_bfv_total_valuation_selected_power_repeat. (exists ff_lt_bfv_total_valuation_selected_power_repeat_bound. ff_lt_bfv_total_valuation_selected_power_repeat_bound + S ff_i_bfv_total_valuation_selected_power_repeat = e) -> (((exists ff_h_bfv_total_valuation_selected_power_repeat_decoded. ff_h_bfv_total_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_total_valuation_selected_power_repeat)) * ff_c_bfv_total_valuation_selected_power)) /\ exists ff_q_bfv_total_valuation_selected_power_repeat_decoded. ff_b_bfv_total_valuation_selected_power = ff_q_bfv_total_valuation_selected_power_repeat_decoded * S ((S (ff_i_bfv_total_valuation_selected_power_repeat)) * ff_c_bfv_total_valuation_selected_power) + (p)))) /\ (exists ff_u_bfv_total_valuation_selected_power_product ff_v_bfv_total_valuation_selected_power_product. ((((exists ff_h_bfv_total_valuation_selected_power_product_start. ff_h_bfv_total_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_total_valuation_selected_power_product)) /\ exists ff_q_bfv_total_valuation_selected_power_product_start. ff_u_bfv_total_valuation_selected_power_product = ff_q_bfv_total_valuation_selected_power_product_start * S ((S (0)) * ff_v_bfv_total_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_total_valuation_selected_power_product_terminal. ff_h_bfv_total_valuation_selected_power_product_terminal + S (bpv_result_bfv_total_valuation_selected) = S ((S (e)) * ff_v_bfv_total_valuation_selected_power_product)) /\ exists ff_q_bfv_total_valuation_selected_power_product_terminal. ff_u_bfv_total_valuation_selected_power_product = ff_q_bfv_total_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_bfv_total_valuation_selected_power_product) + (bpv_result_bfv_total_valuation_selected))) /\ forall ff_i_bfv_total_valuation_selected_power_product. (exists ff_lt_bfv_total_valuation_selected_power_product_bound. ff_lt_bfv_total_valuation_selected_power_product_bound + S ff_i_bfv_total_valuation_selected_power_product = e) -> exists ff_p_bfv_total_valuation_selected_power_product ff_r_bfv_total_valuation_selected_power_product ff_s_bfv_total_valuation_selected_power_product. ((((exists ff_h_bfv_total_valuation_selected_power_product_factor. ff_h_bfv_total_valuation_selected_power_product_factor + S (ff_p_bfv_total_valuation_selected_power_product) = S ((S (ff_i_bfv_total_valuation_selected_power_product)) * ff_c_bfv_total_valuation_selected_power)) /\ exists ff_q_bfv_total_valuation_selected_power_product_factor. ff_b_bfv_total_valuation_selected_power = ff_q_bfv_total_valuation_selected_power_product_factor * S ((S (ff_i_bfv_total_valuation_selected_power_product)) * ff_c_bfv_total_valuation_selected_power) + (ff_p_bfv_total_valuation_selected_power_product))) /\ ((((exists ff_h_bfv_total_valuation_selected_power_product_partial. ff_h_bfv_total_valuation_selected_power_product_partial + S (ff_r_bfv_total_valuation_selected_power_product) = S ((S (ff_i_bfv_total_valuation_selected_power_product)) * ff_v_bfv_total_valuation_selected_power_product)) /\ exists ff_q_bfv_total_valuation_selected_power_product_partial. ff_u_bfv_total_valuation_selected_power_product = ff_q_bfv_total_valuation_selected_power_product_partial * S ((S (ff_i_bfv_total_valuation_selected_power_product)) * ff_v_bfv_total_valuation_selected_power_product) + (ff_r_bfv_total_valuation_selected_power_product))) /\ ((((exists ff_h_bfv_total_valuation_selected_power_product_successor. ff_h_bfv_total_valuation_selected_power_product_successor + S (ff_s_bfv_total_valuation_selected_power_product) = S ((S (S ff_i_bfv_total_valuation_selected_power_product)) * ff_v_bfv_total_valuation_selected_power_product)) /\ exists ff_q_bfv_total_valuation_selected_power_product_successor. ff_u_bfv_total_valuation_selected_power_product = ff_q_bfv_total_valuation_selected_power_product_successor * S ((S (S ff_i_bfv_total_valuation_selected_power_product)) * ff_v_bfv_total_valuation_selected_power_product) + (ff_s_bfv_total_valuation_selected_power_product))) /\ ff_s_bfv_total_valuation_selected_power_product = ff_r_bfv_total_valuation_selected_power_product * ff_p_bfv_total_valuation_selected_power_product)))))))) /\ (exists bpv_factor_bfv_total_valuation_selected_divides. bfv_factorial_bfv_total = bpv_result_bfv_total_valuation_selected * bpv_factor_bfv_total_valuation_selected_divides)))) /\ forall bpv_candidate_bfv_total_valuation. (exists bpv_gap_bfv_total_valuation_candidate_bound. bpv_gap_bfv_total_valuation_candidate_bound + bpv_candidate_bfv_total_valuation = bfv_factorial_bfv_total) -> (exists bpv_result_bfv_total_valuation_candidate. ((exists ff_b_bfv_total_valuation_candidate_power ff_c_bfv_total_valuation_candidate_power. ((forall ff_i_bfv_total_valuation_candidate_power_repeat. (exists ff_lt_bfv_total_valuation_candidate_power_repeat_bound. ff_lt_bfv_total_valuation_candidate_power_repeat_bound + S ff_i_bfv_total_valuation_candidate_power_repeat = bpv_candidate_bfv_total_valuation) -> (((exists ff_h_bfv_total_valuation_candidate_power_repeat_decoded. ff_h_bfv_total_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_total_valuation_candidate_power_repeat)) * ff_c_bfv_total_valuation_candidate_power)) /\ exists ff_q_bfv_total_valuation_candidate_power_repeat_decoded. ff_b_bfv_total_valuation_candidate_power = ff_q_bfv_total_valuation_candidate_power_repeat_decoded * S ((S (ff_i_bfv_total_valuation_candidate_power_repeat)) * ff_c_bfv_total_valuation_candidate_power) + (p)))) /\ (exists ff_u_bfv_total_valuation_candidate_power_product ff_v_bfv_total_valuation_candidate_power_product. ((((exists ff_h_bfv_total_valuation_candidate_power_product_start. ff_h_bfv_total_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_total_valuation_candidate_power_product)) /\ exists ff_q_bfv_total_valuation_candidate_power_product_start. ff_u_bfv_total_valuation_candidate_power_product = ff_q_bfv_total_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bfv_total_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bfv_total_valuation_candidate_power_product_terminal. ff_h_bfv_total_valuation_candidate_power_product_terminal + S (bpv_result_bfv_total_valuation_candidate) = S ((S (bpv_candidate_bfv_total_valuation)) * ff_v_bfv_total_valuation_candidate_power_product)) /\ exists ff_q_bfv_total_valuation_candidate_power_product_terminal. ff_u_bfv_total_valuation_candidate_power_product = ff_q_bfv_total_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_bfv_total_valuation)) * ff_v_bfv_total_valuation_candidate_power_product) + (bpv_result_bfv_total_valuation_candidate))) /\ forall ff_i_bfv_total_valuation_candidate_power_product. (exists ff_lt_bfv_total_valuation_candidate_power_product_bound. ff_lt_bfv_total_valuation_candidate_power_product_bound + S ff_i_bfv_total_valuation_candidate_power_product = bpv_candidate_bfv_total_valuation) -> exists ff_p_bfv_total_valuation_candidate_power_product ff_r_bfv_total_valuation_candidate_power_product ff_s_bfv_total_valuation_candidate_power_product. ((((exists ff_h_bfv_total_valuation_candidate_power_product_factor. ff_h_bfv_total_valuation_candidate_power_product_factor + S (ff_p_bfv_total_valuation_candidate_power_product) = S ((S (ff_i_bfv_total_valuation_candidate_power_product)) * ff_c_bfv_total_valuation_candidate_power)) /\ exists ff_q_bfv_total_valuation_candidate_power_product_factor. ff_b_bfv_total_valuation_candidate_power = ff_q_bfv_total_valuation_candidate_power_product_factor * S ((S (ff_i_bfv_total_valuation_candidate_power_product)) * ff_c_bfv_total_valuation_candidate_power) + (ff_p_bfv_total_valuation_candidate_power_product))) /\ ((((exists ff_h_bfv_total_valuation_candidate_power_product_partial. ff_h_bfv_total_valuation_candidate_power_product_partial + S (ff_r_bfv_total_valuation_candidate_power_product) = S ((S (ff_i_bfv_total_valuation_candidate_power_product)) * ff_v_bfv_total_valuation_candidate_power_product)) /\ exists ff_q_bfv_total_valuation_candidate_power_product_partial. ff_u_bfv_total_valuation_candidate_power_product = ff_q_bfv_total_valuation_candidate_power_product_partial * S ((S (ff_i_bfv_total_valuation_candidate_power_product)) * ff_v_bfv_total_valuation_candidate_power_product) + (ff_r_bfv_total_valuation_candidate_power_product))) /\ ((((exists ff_h_bfv_total_valuation_candidate_power_product_successor. ff_h_bfv_total_valuation_candidate_power_product_successor + S (ff_s_bfv_total_valuation_candidate_power_product) = S ((S (S ff_i_bfv_total_valuation_candidate_power_product)) * ff_v_bfv_total_valuation_candidate_power_product)) /\ exists ff_q_bfv_total_valuation_candidate_power_product_successor. ff_u_bfv_total_valuation_candidate_power_product = ff_q_bfv_total_valuation_candidate_power_product_successor * S ((S (S ff_i_bfv_total_valuation_candidate_power_product)) * ff_v_bfv_total_valuation_candidate_power_product) + (ff_s_bfv_total_valuation_candidate_power_product))) /\ ff_s_bfv_total_valuation_candidate_power_product = ff_r_bfv_total_valuation_candidate_power_product * ff_p_bfv_total_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_bfv_total_valuation_candidate_divides. bfv_factorial_bfv_total = bpv_result_bfv_total_valuation_candidate * bpv_factor_bfv_total_valuation_candidate_divides))) -> (exists bpv_gap_bfv_total_valuation_maximal. bpv_gap_bfv_total_valuation_maximal + bpv_candidate_bfv_total_valuation = e))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–2
02Establish hfactorialL3–5
Establish this local claim before using it. It is not an additional assumption.
- L3
have hfactorial : ∃ F. Factorial(n,F)Definitions: Factorial(n,F)Original native command in the exact edition - L4
specialize factorial_exists n - L5
exact factorial_exists
03Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
cases hfactorial
04Establish hvaluationL7–10
Establish this local claim before using it. It is not an additional assumption.
- L7
have hvaluation : ∃ e. PowerValuation(p,x,e)Definitions: PowerValuation(p,x,e)Original native command in the exact edition - L8
specialize power_valuation_exists p - L9
specialize power_valuation_exists x - L10
exact power_valuation_exists
05Separate the logical casesL11–11
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L11
cases hvaluation
06Construct an explicit witnessL12–13
07Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
split
Original defined command ledger · 16 lines
- 0001
intro p - 0002
intro n - 0003
have hfactorial : ∃ F. Factorial(n,F)Exact native replay line
have hfactorial : exists F. (exists ff_b_bfv_total_witness ff_c_bfv_total_witness. ((forall ff_i_bfv_total_witness_range. (exists ff_lt_bfv_total_witness_range_bound. ff_lt_bfv_total_witness_range_bound + S ff_i_bfv_total_witness_range = n) -> (((exists ff_h_bfv_total_witness_range_decoded. ff_h_bfv_total_witness_range_decoded + S (1 + ff_i_bfv_total_witness_range) = S ((S (ff_i_bfv_total_witness_range)) * ff_c_bfv_total_witness)) /\ exists ff_q_bfv_total_witness_range_decoded. ff_b_bfv_total_witness = ff_q_bfv_total_witness_range_decoded * S ((S (ff_i_bfv_total_witness_range)) * ff_c_bfv_total_witness) + (1 + ff_i_bfv_total_witness_range)))) /\ (exists ff_u_bfv_total_witness_product ff_v_bfv_total_witness_product. ((((exists ff_h_bfv_total_witness_product_start. ff_h_bfv_total_witness_product_start + S (1) = S ((S (0)) * ff_v_bfv_total_witness_product)) /\ exists ff_q_bfv_total_witness_product_start. ff_u_bfv_total_witness_product = ff_q_bfv_total_witness_product_start * S ((S (0)) * ff_v_bfv_total_witness_product) + (1))) /\ ((((exists ff_h_bfv_total_witness_product_terminal. ff_h_bfv_total_witness_product_terminal + S (F) = S ((S (n)) * ff_v_bfv_total_witness_product)) /\ exists ff_q_bfv_total_witness_product_terminal. ff_u_bfv_total_witness_product = ff_q_bfv_total_witness_product_terminal * S ((S (n)) * ff_v_bfv_total_witness_product) + (F))) /\ forall ff_i_bfv_total_witness_product. (exists ff_lt_bfv_total_witness_product_bound. ff_lt_bfv_total_witness_product_bound + S ff_i_bfv_total_witness_product = n) -> exists ff_p_bfv_total_witness_product ff_r_bfv_total_witness_product ff_s_bfv_total_witness_product. ((((exists ff_h_bfv_total_witness_product_factor. ff_h_bfv_total_witness_product_factor + S (ff_p_bfv_total_witness_product) = S ((S (ff_i_bfv_total_witness_product)) * ff_c_bfv_total_witness)) /\ exists ff_q_bfv_total_witness_product_factor. ff_b_bfv_total_witness = ff_q_bfv_total_witness_product_factor * S ((S (ff_i_bfv_total_witness_product)) * ff_c_bfv_total_witness) + (ff_p_bfv_total_witness_product))) /\ ((((exists ff_h_bfv_total_witness_product_partial. ff_h_bfv_total_witness_product_partial + S (ff_r_bfv_total_witness_product) = S ((S (ff_i_bfv_total_witness_product)) * ff_v_bfv_total_witness_product)) /\ exists ff_q_bfv_total_witness_product_partial. ff_u_bfv_total_witness_product = ff_q_bfv_total_witness_product_partial * S ((S (ff_i_bfv_total_witness_product)) * ff_v_bfv_total_witness_product) + (ff_r_bfv_total_witness_product))) /\ ((((exists ff_h_bfv_total_witness_product_successor. ff_h_bfv_total_witness_product_successor + S (ff_s_bfv_total_witness_product) = S ((S (S ff_i_bfv_total_witness_product)) * ff_v_bfv_total_witness_product)) /\ exists ff_q_bfv_total_witness_product_successor. ff_u_bfv_total_witness_product = ff_q_bfv_total_witness_product_successor * S ((S (S ff_i_bfv_total_witness_product)) * ff_v_bfv_total_witness_product) + (ff_s_bfv_total_witness_product))) /\ ff_s_bfv_total_witness_product = ff_r_bfv_total_witness_product * ff_p_bfv_total_witness_product)))))))) - 0004
specialize factorial_exists n - 0005
exact factorial_exists - 0006
cases hfactorial - 0007
have hvaluation : ∃ e. PowerValuation(p,x,e)Exact native replay line
have hvaluation : exists e. (((exists bpv_gap_bfv_total_graph_exponent_bound. bpv_gap_bfv_total_graph_exponent_bound + e = x) /\ (exists bpv_result_bfv_total_graph_selected. ((exists ff_b_bfv_total_graph_selected_power ff_c_bfv_total_graph_selected_power. ((forall ff_i_bfv_total_graph_selected_power_repeat. (exists ff_lt_bfv_total_graph_selected_power_repeat_bound. ff_lt_bfv_total_graph_selected_power_repeat_bound + S ff_i_bfv_total_graph_selected_power_repeat = e) -> (((exists ff_h_bfv_total_graph_selected_power_repeat_decoded. ff_h_bfv_total_graph_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_total_graph_selected_power_repeat)) * ff_c_bfv_total_graph_selected_power)) /\ exists ff_q_bfv_total_graph_selected_power_repeat_decoded. ff_b_bfv_total_graph_selected_power = ff_q_bfv_total_graph_selected_power_repeat_decoded * S ((S (ff_i_bfv_total_graph_selected_power_repeat)) * ff_c_bfv_total_graph_selected_power) + (p)))) /\ (exists ff_u_bfv_total_graph_selected_power_product ff_v_bfv_total_graph_selected_power_product. ((((exists ff_h_bfv_total_graph_selected_power_product_start. ff_h_bfv_total_graph_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_total_graph_selected_power_product)) /\ exists ff_q_bfv_total_graph_selected_power_product_start. ff_u_bfv_total_graph_selected_power_product = ff_q_bfv_total_graph_selected_power_product_start * S ((S (0)) * ff_v_bfv_total_graph_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_total_graph_selected_power_product_terminal. ff_h_bfv_total_graph_selected_power_product_terminal + S (bpv_result_bfv_total_graph_selected) = S ((S (e)) * ff_v_bfv_total_graph_selected_power_product)) /\ exists ff_q_bfv_total_graph_selected_power_product_terminal. ff_u_bfv_total_graph_selected_power_product = ff_q_bfv_total_graph_selected_power_product_terminal * S ((S (e)) * ff_v_bfv_total_graph_selected_power_product) + (bpv_result_bfv_total_graph_selected))) /\ forall ff_i_bfv_total_graph_selected_power_product. (exists ff_lt_bfv_total_graph_selected_power_product_bound. ff_lt_bfv_total_graph_selected_power_product_bound + S ff_i_bfv_total_graph_selected_power_product = e) -> exists ff_p_bfv_total_graph_selected_power_product ff_r_bfv_total_graph_selected_power_product ff_s_bfv_total_graph_selected_power_product. ((((exists ff_h_bfv_total_graph_selected_power_product_factor. ff_h_bfv_total_graph_selected_power_product_factor + S (ff_p_bfv_total_graph_selected_power_product) = S ((S (ff_i_bfv_total_graph_selected_power_product)) * ff_c_bfv_total_graph_selected_power)) /\ exists ff_q_bfv_total_graph_selected_power_product_factor. ff_b_bfv_total_graph_selected_power = ff_q_bfv_total_graph_selected_power_product_factor * S ((S (ff_i_bfv_total_graph_selected_power_product)) * ff_c_bfv_total_graph_selected_power) + (ff_p_bfv_total_graph_selected_power_product))) /\ ((((exists ff_h_bfv_total_graph_selected_power_product_partial. ff_h_bfv_total_graph_selected_power_product_partial + S (ff_r_bfv_total_graph_selected_power_product) = S ((S (ff_i_bfv_total_graph_selected_power_product)) * ff_v_bfv_total_graph_selected_power_product)) /\ exists ff_q_bfv_total_graph_selected_power_product_partial. ff_u_bfv_total_graph_selected_power_product = ff_q_bfv_total_graph_selected_power_product_partial * S ((S (ff_i_bfv_total_graph_selected_power_product)) * ff_v_bfv_total_graph_selected_power_product) + (ff_r_bfv_total_graph_selected_power_product))) /\ ((((exists ff_h_bfv_total_graph_selected_power_product_successor. ff_h_bfv_total_graph_selected_power_product_successor + S (ff_s_bfv_total_graph_selected_power_product) = S ((S (S ff_i_bfv_total_graph_selected_power_product)) * ff_v_bfv_total_graph_selected_power_product)) /\ exists ff_q_bfv_total_graph_selected_power_product_successor. ff_u_bfv_total_graph_selected_power_product = ff_q_bfv_total_graph_selected_power_product_successor * S ((S (S ff_i_bfv_total_graph_selected_power_product)) * ff_v_bfv_total_graph_selected_power_product) + (ff_s_bfv_total_graph_selected_power_product))) /\ ff_s_bfv_total_graph_selected_power_product = ff_r_bfv_total_graph_selected_power_product * ff_p_bfv_total_graph_selected_power_product)))))))) /\ (exists bpv_factor_bfv_total_graph_selected_divides. x = bpv_result_bfv_total_graph_selected * bpv_factor_bfv_total_graph_selected_divides)))) /\ forall bpv_candidate_bfv_total_graph. (exists bpv_gap_bfv_total_graph_candidate_bound. bpv_gap_bfv_total_graph_candidate_bound + bpv_candidate_bfv_total_graph = x) -> (exists bpv_result_bfv_total_graph_candidate. ((exists ff_b_bfv_total_graph_candidate_power ff_c_bfv_total_graph_candidate_power. ((forall ff_i_bfv_total_graph_candidate_power_repeat. (exists ff_lt_bfv_total_graph_candidate_power_repeat_bound. ff_lt_bfv_total_graph_candidate_power_repeat_bound + S ff_i_bfv_total_graph_candidate_power_repeat = bpv_candidate_bfv_total_graph) -> (((exists ff_h_bfv_total_graph_candidate_power_repeat_decoded. ff_h_bfv_total_graph_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_total_graph_candidate_power_repeat)) * ff_c_bfv_total_graph_candidate_power)) /\ exists ff_q_bfv_total_graph_candidate_power_repeat_decoded. ff_b_bfv_total_graph_candidate_power = ff_q_bfv_total_graph_candidate_power_repeat_decoded * S ((S (ff_i_bfv_total_graph_candidate_power_repeat)) * ff_c_bfv_total_graph_candidate_power) + (p)))) /\ (exists ff_u_bfv_total_graph_candidate_power_product ff_v_bfv_total_graph_candidate_power_product. ((((exists ff_h_bfv_total_graph_candidate_power_product_start. ff_h_bfv_total_graph_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_total_graph_candidate_power_product)) /\ exists ff_q_bfv_total_graph_candidate_power_product_start. ff_u_bfv_total_graph_candidate_power_product = ff_q_bfv_total_graph_candidate_power_product_start * S ((S (0)) * ff_v_bfv_total_graph_candidate_power_product) + (1))) /\ ((((exists ff_h_bfv_total_graph_candidate_power_product_terminal. ff_h_bfv_total_graph_candidate_power_product_terminal + S (bpv_result_bfv_total_graph_candidate) = S ((S (bpv_candidate_bfv_total_graph)) * ff_v_bfv_total_graph_candidate_power_product)) /\ exists ff_q_bfv_total_graph_candidate_power_product_terminal. ff_u_bfv_total_graph_candidate_power_product = ff_q_bfv_total_graph_candidate_power_product_terminal * S ((S (bpv_candidate_bfv_total_graph)) * ff_v_bfv_total_graph_candidate_power_product) + (bpv_result_bfv_total_graph_candidate))) /\ forall ff_i_bfv_total_graph_candidate_power_product. (exists ff_lt_bfv_total_graph_candidate_power_product_bound. ff_lt_bfv_total_graph_candidate_power_product_bound + S ff_i_bfv_total_graph_candidate_power_product = bpv_candidate_bfv_total_graph) -> exists ff_p_bfv_total_graph_candidate_power_product ff_r_bfv_total_graph_candidate_power_product ff_s_bfv_total_graph_candidate_power_product. ((((exists ff_h_bfv_total_graph_candidate_power_product_factor. ff_h_bfv_total_graph_candidate_power_product_factor + S (ff_p_bfv_total_graph_candidate_power_product) = S ((S (ff_i_bfv_total_graph_candidate_power_product)) * ff_c_bfv_total_graph_candidate_power)) /\ exists ff_q_bfv_total_graph_candidate_power_product_factor. ff_b_bfv_total_graph_candidate_power = ff_q_bfv_total_graph_candidate_power_product_factor * S ((S (ff_i_bfv_total_graph_candidate_power_product)) * ff_c_bfv_total_graph_candidate_power) + (ff_p_bfv_total_graph_candidate_power_product))) /\ ((((exists ff_h_bfv_total_graph_candidate_power_product_partial. ff_h_bfv_total_graph_candidate_power_product_partial + S (ff_r_bfv_total_graph_candidate_power_product) = S ((S (ff_i_bfv_total_graph_candidate_power_product)) * ff_v_bfv_total_graph_candidate_power_product)) /\ exists ff_q_bfv_total_graph_candidate_power_product_partial. ff_u_bfv_total_graph_candidate_power_product = ff_q_bfv_total_graph_candidate_power_product_partial * S ((S (ff_i_bfv_total_graph_candidate_power_product)) * ff_v_bfv_total_graph_candidate_power_product) + (ff_r_bfv_total_graph_candidate_power_product))) /\ ((((exists ff_h_bfv_total_graph_candidate_power_product_successor. ff_h_bfv_total_graph_candidate_power_product_successor + S (ff_s_bfv_total_graph_candidate_power_product) = S ((S (S ff_i_bfv_total_graph_candidate_power_product)) * ff_v_bfv_total_graph_candidate_power_product)) /\ exists ff_q_bfv_total_graph_candidate_power_product_successor. ff_u_bfv_total_graph_candidate_power_product = ff_q_bfv_total_graph_candidate_power_product_successor * S ((S (S ff_i_bfv_total_graph_candidate_power_product)) * ff_v_bfv_total_graph_candidate_power_product) + (ff_s_bfv_total_graph_candidate_power_product))) /\ ff_s_bfv_total_graph_candidate_power_product = ff_r_bfv_total_graph_candidate_power_product * ff_p_bfv_total_graph_candidate_power_product)))))))) /\ (exists bpv_factor_bfv_total_graph_candidate_divides. x = bpv_result_bfv_total_graph_candidate * bpv_factor_bfv_total_graph_candidate_divides))) -> (exists bpv_gap_bfv_total_graph_maximal. bpv_gap_bfv_total_graph_maximal + bpv_candidate_bfv_total_graph = e)) - 0008
specialize power_valuation_exists p - 0009
specialize power_valuation_exists x - 0010
exact power_valuation_exists - 0011
cases hvaluation - 0012
exists x1 - 0013
exists x - 0014
split - 0015
exact hfactorial_witness - 0016
exact hvaluation_witness