SK002C

perfect_power_root_table_prefix_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Finite induction constructs an actual beta table from the already proved pointwise root theorem, without any finite-choice axiom.

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 first-order arithmetic statement

forall L n g. (forall ppf_degree_table_prefix_available. ~(ppf_degree_table_prefix_available = 0) -> (exists pvs_factor_table_prefix_availabledivisor. (g) = (ppf_degree_table_prefix_available) * pvs_factor_table_prefix_availabledivisor) -> exists ppf_root_table_prefix_available. (exists pa_b_pvs_table_prefix_availablepower pa_c_pvs_table_prefix_availablepower. ((forall pa_i_pvs_table_prefix_availablepower_repeat. (exists pa_lt_pvs_table_prefix_availablepower_repeat_bound. pa_lt_pvs_table_prefix_availablepower_repeat_bound + S pa_i_pvs_table_prefix_availablepower_repeat = ppf_degree_table_prefix_available) -> (((exists pa_h_pvs_table_prefix_availablepower_repeat_decoded. pa_h_pvs_table_prefix_availablepower_repeat_decoded + S (ppf_root_table_prefix_available) = S ((S (pa_i_pvs_table_prefix_availablepower_repeat)) * pa_c_pvs_table_prefix_availablepower)) /\ exists pa_q_pvs_table_prefix_availablepower_repeat_decoded. pa_b_pvs_table_prefix_availablepower = pa_q_pvs_table_prefix_availablepower_repeat_decoded * S ((S (pa_i_pvs_table_prefix_availablepower_repeat)) * pa_c_pvs_table_prefix_availablepower) + (ppf_root_table_prefix_available)))) /\ (exists pa_u_pvs_table_prefix_availablepower_product pa_v_pvs_table_prefix_availablepower_product. ((((exists pa_h_pvs_table_prefix_availablepower_product_start. pa_h_pvs_table_prefix_availablepower_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_prefix_availablepower_product)) /\ exists pa_q_pvs_table_prefix_availablepower_product_start. pa_u_pvs_table_prefix_availablepower_product = pa_q_pvs_table_prefix_availablepower_product_start * S ((S (0)) * pa_v_pvs_table_prefix_availablepower_product) + (1))) /\ ((((exists pa_h_pvs_table_prefix_availablepower_product_terminal. pa_h_pvs_table_prefix_availablepower_product_terminal + S (n) = S ((S (ppf_degree_table_prefix_available)) * pa_v_pvs_table_prefix_availablepower_product)) /\ exists pa_q_pvs_table_prefix_availablepower_product_terminal. pa_u_pvs_table_prefix_availablepower_product = pa_q_pvs_table_prefix_availablepower_product_terminal * S ((S (ppf_degree_table_prefix_available)) * pa_v_pvs_table_prefix_availablepower_product) + (n))) /\ forall pa_i_pvs_table_prefix_availablepower_product. (exists pa_lt_pvs_table_prefix_availablepower_product_bound. pa_lt_pvs_table_prefix_availablepower_product_bound + S pa_i_pvs_table_prefix_availablepower_product = ppf_degree_table_prefix_available) -> exists pa_p_pvs_table_prefix_availablepower_product pa_r_pvs_table_prefix_availablepower_product pa_s_pvs_table_prefix_availablepower_product. ((((exists pa_h_pvs_table_prefix_availablepower_product_factor. pa_h_pvs_table_prefix_availablepower_product_factor + S (pa_p_pvs_table_prefix_availablepower_product) = S ((S (pa_i_pvs_table_prefix_availablepower_product)) * pa_c_pvs_table_prefix_availablepower)) /\ exists pa_q_pvs_table_prefix_availablepower_product_factor. pa_b_pvs_table_prefix_availablepower = pa_q_pvs_table_prefix_availablepower_product_factor * S ((S (pa_i_pvs_table_prefix_availablepower_product)) * pa_c_pvs_table_prefix_availablepower) + (pa_p_pvs_table_prefix_availablepower_product))) /\ ((((exists pa_h_pvs_table_prefix_availablepower_product_partial. pa_h_pvs_table_prefix_availablepower_product_partial + S (pa_r_pvs_table_prefix_availablepower_product) = S ((S (pa_i_pvs_table_prefix_availablepower_product)) * pa_v_pvs_table_prefix_availablepower_product)) /\ exists pa_q_pvs_table_prefix_availablepower_product_partial. pa_u_pvs_table_prefix_availablepower_product = pa_q_pvs_table_prefix_availablepower_product_partial * S ((S (pa_i_pvs_table_prefix_availablepower_product)) * pa_v_pvs_table_prefix_availablepower_product) + (pa_r_pvs_table_prefix_availablepower_product))) /\ ((((exists pa_h_pvs_table_prefix_availablepower_product_successor. pa_h_pvs_table_prefix_availablepower_product_successor + S (pa_s_pvs_table_prefix_availablepower_product) = S ((S (S pa_i_pvs_table_prefix_availablepower_product)) * pa_v_pvs_table_prefix_availablepower_product)) /\ exists pa_q_pvs_table_prefix_availablepower_product_successor. pa_u_pvs_table_prefix_availablepower_product = pa_q_pvs_table_prefix_availablepower_product_successor * S ((S (S pa_i_pvs_table_prefix_availablepower_product)) * pa_v_pvs_table_prefix_availablepower_product) + (pa_s_pvs_table_prefix_availablepower_product))) /\ pa_s_pvs_table_prefix_availablepower_product = pa_r_pvs_table_prefix_availablepower_product * pa_p_pvs_table_prefix_availablepower_product))))))))) -> exists b c. (forall ppf_table_degree_table_prefix_constructed. (exists pvs_gap_table_prefix_constructedbound. pvs_gap_table_prefix_constructedbound + S (ppf_table_degree_table_prefix_constructed) = (L)) -> ~(ppf_table_degree_table_prefix_constructed = 0) -> (exists pvs_factor_table_prefix_constructeddivisor. (g) = (ppf_table_degree_table_prefix_constructed) * pvs_factor_table_prefix_constructeddivisor) -> exists ppf_table_root_table_prefix_constructed. (((exists ff_h_pvs_table_prefix_constructedentry. ff_h_pvs_table_prefix_constructedentry + S (ppf_table_root_table_prefix_constructed) = S ((S (ppf_table_degree_table_prefix_constructed)) * c)) /\ exists ff_q_pvs_table_prefix_constructedentry. b = ff_q_pvs_table_prefix_constructedentry * S ((S (ppf_table_degree_table_prefix_constructed)) * c) + (ppf_table_root_table_prefix_constructed))) /\ (exists pa_b_pvs_table_prefix_constructedpower pa_c_pvs_table_prefix_constructedpower. ((forall pa_i_pvs_table_prefix_constructedpower_repeat. (exists pa_lt_pvs_table_prefix_constructedpower_repeat_bound. pa_lt_pvs_table_prefix_constructedpower_repeat_bound + S pa_i_pvs_table_prefix_constructedpower_repeat = ppf_table_degree_table_prefix_constructed) -> (((exists pa_h_pvs_table_prefix_constructedpower_repeat_decoded. pa_h_pvs_table_prefix_constructedpower_repeat_decoded + S (ppf_table_root_table_prefix_constructed) = S ((S (pa_i_pvs_table_prefix_constructedpower_repeat)) * pa_c_pvs_table_prefix_constructedpower)) /\ exists pa_q_pvs_table_prefix_constructedpower_repeat_decoded. pa_b_pvs_table_prefix_constructedpower = pa_q_pvs_table_prefix_constructedpower_repeat_decoded * S ((S (pa_i_pvs_table_prefix_constructedpower_repeat)) * pa_c_pvs_table_prefix_constructedpower) + (ppf_table_root_table_prefix_constructed)))) /\ (exists pa_u_pvs_table_prefix_constructedpower_product pa_v_pvs_table_prefix_constructedpower_product. ((((exists pa_h_pvs_table_prefix_constructedpower_product_start. pa_h_pvs_table_prefix_constructedpower_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_prefix_constructedpower_product)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_start. pa_u_pvs_table_prefix_constructedpower_product = pa_q_pvs_table_prefix_constructedpower_product_start * S ((S (0)) * pa_v_pvs_table_prefix_constructedpower_product) + (1))) /\ ((((exists pa_h_pvs_table_prefix_constructedpower_product_terminal. pa_h_pvs_table_prefix_constructedpower_product_terminal + S (n) = S ((S (ppf_table_degree_table_prefix_constructed)) * pa_v_pvs_table_prefix_constructedpower_product)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_terminal. pa_u_pvs_table_prefix_constructedpower_product = pa_q_pvs_table_prefix_constructedpower_product_terminal * S ((S (ppf_table_degree_table_prefix_constructed)) * pa_v_pvs_table_prefix_constructedpower_product) + (n))) /\ forall pa_i_pvs_table_prefix_constructedpower_product. (exists pa_lt_pvs_table_prefix_constructedpower_product_bound. pa_lt_pvs_table_prefix_constructedpower_product_bound + S pa_i_pvs_table_prefix_constructedpower_product = ppf_table_degree_table_prefix_constructed) -> exists pa_p_pvs_table_prefix_constructedpower_product pa_r_pvs_table_prefix_constructedpower_product pa_s_pvs_table_prefix_constructedpower_product. ((((exists pa_h_pvs_table_prefix_constructedpower_product_factor. pa_h_pvs_table_prefix_constructedpower_product_factor + S (pa_p_pvs_table_prefix_constructedpower_product) = S ((S (pa_i_pvs_table_prefix_constructedpower_product)) * pa_c_pvs_table_prefix_constructedpower)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_factor. pa_b_pvs_table_prefix_constructedpower = pa_q_pvs_table_prefix_constructedpower_product_factor * S ((S (pa_i_pvs_table_prefix_constructedpower_product)) * pa_c_pvs_table_prefix_constructedpower) + (pa_p_pvs_table_prefix_constructedpower_product))) /\ ((((exists pa_h_pvs_table_prefix_constructedpower_product_partial. pa_h_pvs_table_prefix_constructedpower_product_partial + S (pa_r_pvs_table_prefix_constructedpower_product) = S ((S (pa_i_pvs_table_prefix_constructedpower_product)) * pa_v_pvs_table_prefix_constructedpower_product)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_partial. pa_u_pvs_table_prefix_constructedpower_product = pa_q_pvs_table_prefix_constructedpower_product_partial * S ((S (pa_i_pvs_table_prefix_constructedpower_product)) * pa_v_pvs_table_prefix_constructedpower_product) + (pa_r_pvs_table_prefix_constructedpower_product))) /\ ((((exists pa_h_pvs_table_prefix_constructedpower_product_successor. pa_h_pvs_table_prefix_constructedpower_product_successor + S (pa_s_pvs_table_prefix_constructedpower_product) = S ((S (S pa_i_pvs_table_prefix_constructedpower_product)) * pa_v_pvs_table_prefix_constructedpower_product)) /\ exists pa_q_pvs_table_prefix_constructedpower_product_successor. pa_u_pvs_table_prefix_constructedpower_product = pa_q_pvs_table_prefix_constructedpower_product_successor * S ((S (S pa_i_pvs_table_prefix_constructedpower_product)) * pa_v_pvs_table_prefix_constructedpower_product) + (pa_s_pvs_table_prefix_constructedpower_product))) /\ pa_s_pvs_table_prefix_constructedpower_product = pa_r_pvs_table_prefix_constructedpower_product * pa_p_pvs_table_prefix_constructedpower_product)))))))))

Constructive proof overview

Generated structural guide

Finite induction constructs an actual beta table from the already proved pointwise root theorem, without any finite-choice axiom.

The unchanged tactic script uses 4 declared prerequisites and contains 56 exact native proof lines.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

factor_permutation_below_zero_impossible Alpha theorem; checked-use authorized SK002B perfect_power_root_table_conditional_entry beta_prefix_extend Stable theorem; checked-use authorized SK002A perfect_power_root_table_prefix_append

Direct dependents

SK002D perfect_power_root_table_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

56 script commands · 16 reading checkpoints · 3 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 (2)
perfect power root table conditional entryperfect power root table prefix append

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–1

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

  1. L1
    intro L
02Induction on LL2–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction L
  2. L3
    intro n
  3. L4
    intro g
  4. L5
    intro havailable
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–11

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

  1. L8
    intro k
  2. L9
    intro hbound
  3. L10
    intro hk
  4. L11
    intro hdiv
05Separate the logical casesL12–12

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

  1. L12
    exfalso
06Use earlier factsL13–15

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

  1. L13
    specialize factor_permutation_below_zero_impossible (k)
  2. L14
    apply factor_permutation_below_zero_impossible
  3. L15
    exact hbound
07Fix variables and assumptionsL16–18

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

  1. L16
    intro n
  2. L17
    intro g
  3. L18
    intro havailable
08Establish hrootL19–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply perfect power root table conditional entry.

  1. L19
    have hroot : ∃ R. ¬L = 0 → Dvd(L,g) → Pow(R,L,n)Definitions: DvdPow
  2. L20
    specialize perfect_power_root_table_conditional_entry (n)
  3. L21
    specialize perfect_power_root_table_conditional_entry (g)
  4. L22
    specialize perfect_power_root_table_conditional_entry (L)
  5. L23
    apply perfect_power_root_table_conditional_entry
  6. L24
    exact havailable
09Separate the logical casesL25–25

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

  1. L25
    cases hroot
10Establish hpreviousL26–30

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

  1. L26
    have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,L) → ¬x = 0 → Dvd(x,g) → ∃ y. BetaAt(b,c,x,y) ∧ Pow(y,x,n)Definitions: LtDvdBetaAtPow
  2. L27
    specialize IH (n)
  3. L28
    specialize IH (g)
  4. L29
    apply IH
  5. L30
    exact havailable
11Separate the logical casesL31–32

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

  1. L31
    cases hprevious
  2. L32
    cases hprevious_witness
12Establish hextendL33–38

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

  1. L33
    have hextend : ∃ b. ∃ c. BetaAt(b,c,L,x) ∧ (∀ y. ∀ z. Lt(y,L) → BetaAt(x1,x2,y,z) → BetaAt(b,c,y,z))Definitions: LtBetaAt
  2. L34
    specialize beta_prefix_extend (L)
  3. L35
    specialize beta_prefix_extend (x1)
  4. L36
    specialize beta_prefix_extend (x2)
  5. L37
    specialize beta_prefix_extend (x)
  6. L38
    apply beta_prefix_extend
13Separate the logical casesL39–41

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

  1. L39
    cases hextend
  2. L40
    cases hextend_witness
  3. L41
    cases hextend_witness_witness
14Construct an explicit witnessL42–43

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

  1. L42
    exists x3
  2. L43
    exists x4
15Use earlier factsL44–53

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

  1. L44
    specialize perfect_power_root_table_prefix_append (n)
  2. L45
    specialize perfect_power_root_table_prefix_append (g)
  3. L46
    specialize perfect_power_root_table_prefix_append (x1)
  4. L47
    specialize perfect_power_root_table_prefix_append (x2)
  5. L48
    specialize perfect_power_root_table_prefix_append (x3)
  6. L49
    specialize perfect_power_root_table_prefix_append (x4)
  7. L50
    specialize perfect_power_root_table_prefix_append (L)
  8. L51
    specialize perfect_power_root_table_prefix_append (x)
  9. L52
    apply perfect_power_root_table_prefix_append
  10. L53
    exact hprevious_witness_witness
16Use earlier factsL54–56

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

  1. L54
    exact hextend_witness_witness_right
  2. L55
    exact hextend_witness_witness_left
  3. L56
    exact hroot_witness

Library-wide reading audit

Original exact command ledger · 56 lines
  1. 0001intro L
  2. 0002induction L
  3. 0003intro n
  4. 0004intro g
  5. 0005intro havailable
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro k
  9. 0009intro hbound
  10. 0010intro hk
  11. 0011intro hdiv
  12. 0012exfalso
  13. 0013specialize factor_permutation_below_zero_impossible (k)
  14. 0014apply factor_permutation_below_zero_impossible
  15. 0015exact hbound
  16. 0016intro n
  17. 0017intro g
  18. 0018intro havailable
  19. 0019have hroot : exists R. ~(L = 0) -> (exists pvs_factor_prefix_conditional_divisor. (g) = (L) * pvs_factor_prefix_conditional_divisor) -> (exists pa_b_pvs_prefix_conditional_power pa_c_pvs_prefix_conditional_power. ((forall pa_i_pvs_prefix_conditional_power_repeat. (exists pa_lt_pvs_prefix_conditional_power_repeat_bound. pa_lt_pvs_prefix_conditional_power_repeat_bound + S pa_i_pvs_prefix_conditional_power_repeat = L) -> (((exists pa_h_pvs_prefix_conditional_power_repeat_decoded. pa_h_pvs_prefix_conditional_power_repeat_decoded + S (R) = S ((S (pa_i_pvs_prefix_conditional_power_repeat)) * pa_c_pvs_prefix_conditional_power)) /\ exists pa_q_pvs_prefix_conditional_power_repeat_decoded. pa_b_pvs_prefix_conditional_power = pa_q_pvs_prefix_conditional_power_repeat_decoded * S ((S (pa_i_pvs_prefix_conditional_power_repeat)) * pa_c_pvs_prefix_conditional_power) + (R)))) /\ (exists pa_u_pvs_prefix_conditional_power_product pa_v_pvs_prefix_conditional_power_product. ((((exists pa_h_pvs_prefix_conditional_power_product_start. pa_h_pvs_prefix_conditional_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_prefix_conditional_power_product)) /\ exists pa_q_pvs_prefix_conditional_power_product_start. pa_u_pvs_prefix_conditional_power_product = pa_q_pvs_prefix_conditional_power_product_start * S ((S (0)) * pa_v_pvs_prefix_conditional_power_product) + (1))) /\ ((((exists pa_h_pvs_prefix_conditional_power_product_terminal. pa_h_pvs_prefix_conditional_power_product_terminal + S (n) = S ((S (L)) * pa_v_pvs_prefix_conditional_power_product)) /\ exists pa_q_pvs_prefix_conditional_power_product_terminal. pa_u_pvs_prefix_conditional_power_product = pa_q_pvs_prefix_conditional_power_product_terminal * S ((S (L)) * pa_v_pvs_prefix_conditional_power_product) + (n))) /\ forall pa_i_pvs_prefix_conditional_power_product. (exists pa_lt_pvs_prefix_conditional_power_product_bound. pa_lt_pvs_prefix_conditional_power_product_bound + S pa_i_pvs_prefix_conditional_power_product = L) -> exists pa_p_pvs_prefix_conditional_power_product pa_r_pvs_prefix_conditional_power_product pa_s_pvs_prefix_conditional_power_product. ((((exists pa_h_pvs_prefix_conditional_power_product_factor. pa_h_pvs_prefix_conditional_power_product_factor + S (pa_p_pvs_prefix_conditional_power_product) = S ((S (pa_i_pvs_prefix_conditional_power_product)) * pa_c_pvs_prefix_conditional_power)) /\ exists pa_q_pvs_prefix_conditional_power_product_factor. pa_b_pvs_prefix_conditional_power = pa_q_pvs_prefix_conditional_power_product_factor * S ((S (pa_i_pvs_prefix_conditional_power_product)) * pa_c_pvs_prefix_conditional_power) + (pa_p_pvs_prefix_conditional_power_product))) /\ ((((exists pa_h_pvs_prefix_conditional_power_product_partial. pa_h_pvs_prefix_conditional_power_product_partial + S (pa_r_pvs_prefix_conditional_power_product) = S ((S (pa_i_pvs_prefix_conditional_power_product)) * pa_v_pvs_prefix_conditional_power_product)) /\ exists pa_q_pvs_prefix_conditional_power_product_partial. pa_u_pvs_prefix_conditional_power_product = pa_q_pvs_prefix_conditional_power_product_partial * S ((S (pa_i_pvs_prefix_conditional_power_product)) * pa_v_pvs_prefix_conditional_power_product) + (pa_r_pvs_prefix_conditional_power_product))) /\ ((((exists pa_h_pvs_prefix_conditional_power_product_successor. pa_h_pvs_prefix_conditional_power_product_successor + S (pa_s_pvs_prefix_conditional_power_product) = S ((S (S pa_i_pvs_prefix_conditional_power_product)) * pa_v_pvs_prefix_conditional_power_product)) /\ exists pa_q_pvs_prefix_conditional_power_product_successor. pa_u_pvs_prefix_conditional_power_product = pa_q_pvs_prefix_conditional_power_product_successor * S ((S (S pa_i_pvs_prefix_conditional_power_product)) * pa_v_pvs_prefix_conditional_power_product) + (pa_s_pvs_prefix_conditional_power_product))) /\ pa_s_pvs_prefix_conditional_power_product = pa_r_pvs_prefix_conditional_power_product * pa_p_pvs_prefix_conditional_power_product))))))))
  20. 0020specialize perfect_power_root_table_conditional_entry (n)
  21. 0021specialize perfect_power_root_table_conditional_entry (g)
  22. 0022specialize perfect_power_root_table_conditional_entry (L)
  23. 0023apply perfect_power_root_table_conditional_entry
  24. 0024exact havailable
  25. 0025cases hroot
  26. 0026have hprevious : exists b c. (forall ppf_table_degree_table_prefix_previous. (exists pvs_gap_table_prefix_previousbound. pvs_gap_table_prefix_previousbound + S (ppf_table_degree_table_prefix_previous) = (L)) -> ~(ppf_table_degree_table_prefix_previous = 0) -> (exists pvs_factor_table_prefix_previousdivisor. (g) = (ppf_table_degree_table_prefix_previous) * pvs_factor_table_prefix_previousdivisor) -> exists ppf_table_root_table_prefix_previous. (((exists ff_h_pvs_table_prefix_previousentry. ff_h_pvs_table_prefix_previousentry + S (ppf_table_root_table_prefix_previous) = S ((S (ppf_table_degree_table_prefix_previous)) * c)) /\ exists ff_q_pvs_table_prefix_previousentry. b = ff_q_pvs_table_prefix_previousentry * S ((S (ppf_table_degree_table_prefix_previous)) * c) + (ppf_table_root_table_prefix_previous))) /\ (exists pa_b_pvs_table_prefix_previouspower pa_c_pvs_table_prefix_previouspower. ((forall pa_i_pvs_table_prefix_previouspower_repeat. (exists pa_lt_pvs_table_prefix_previouspower_repeat_bound. pa_lt_pvs_table_prefix_previouspower_repeat_bound + S pa_i_pvs_table_prefix_previouspower_repeat = ppf_table_degree_table_prefix_previous) -> (((exists pa_h_pvs_table_prefix_previouspower_repeat_decoded. pa_h_pvs_table_prefix_previouspower_repeat_decoded + S (ppf_table_root_table_prefix_previous) = S ((S (pa_i_pvs_table_prefix_previouspower_repeat)) * pa_c_pvs_table_prefix_previouspower)) /\ exists pa_q_pvs_table_prefix_previouspower_repeat_decoded. pa_b_pvs_table_prefix_previouspower = pa_q_pvs_table_prefix_previouspower_repeat_decoded * S ((S (pa_i_pvs_table_prefix_previouspower_repeat)) * pa_c_pvs_table_prefix_previouspower) + (ppf_table_root_table_prefix_previous)))) /\ (exists pa_u_pvs_table_prefix_previouspower_product pa_v_pvs_table_prefix_previouspower_product. ((((exists pa_h_pvs_table_prefix_previouspower_product_start. pa_h_pvs_table_prefix_previouspower_product_start + S (1) = S ((S (0)) * pa_v_pvs_table_prefix_previouspower_product)) /\ exists pa_q_pvs_table_prefix_previouspower_product_start. pa_u_pvs_table_prefix_previouspower_product = pa_q_pvs_table_prefix_previouspower_product_start * S ((S (0)) * pa_v_pvs_table_prefix_previouspower_product) + (1))) /\ ((((exists pa_h_pvs_table_prefix_previouspower_product_terminal. pa_h_pvs_table_prefix_previouspower_product_terminal + S (n) = S ((S (ppf_table_degree_table_prefix_previous)) * pa_v_pvs_table_prefix_previouspower_product)) /\ exists pa_q_pvs_table_prefix_previouspower_product_terminal. pa_u_pvs_table_prefix_previouspower_product = pa_q_pvs_table_prefix_previouspower_product_terminal * S ((S (ppf_table_degree_table_prefix_previous)) * pa_v_pvs_table_prefix_previouspower_product) + (n))) /\ forall pa_i_pvs_table_prefix_previouspower_product. (exists pa_lt_pvs_table_prefix_previouspower_product_bound. pa_lt_pvs_table_prefix_previouspower_product_bound + S pa_i_pvs_table_prefix_previouspower_product = ppf_table_degree_table_prefix_previous) -> exists pa_p_pvs_table_prefix_previouspower_product pa_r_pvs_table_prefix_previouspower_product pa_s_pvs_table_prefix_previouspower_product. ((((exists pa_h_pvs_table_prefix_previouspower_product_factor. pa_h_pvs_table_prefix_previouspower_product_factor + S (pa_p_pvs_table_prefix_previouspower_product) = S ((S (pa_i_pvs_table_prefix_previouspower_product)) * pa_c_pvs_table_prefix_previouspower)) /\ exists pa_q_pvs_table_prefix_previouspower_product_factor. pa_b_pvs_table_prefix_previouspower = pa_q_pvs_table_prefix_previouspower_product_factor * S ((S (pa_i_pvs_table_prefix_previouspower_product)) * pa_c_pvs_table_prefix_previouspower) + (pa_p_pvs_table_prefix_previouspower_product))) /\ ((((exists pa_h_pvs_table_prefix_previouspower_product_partial. pa_h_pvs_table_prefix_previouspower_product_partial + S (pa_r_pvs_table_prefix_previouspower_product) = S ((S (pa_i_pvs_table_prefix_previouspower_product)) * pa_v_pvs_table_prefix_previouspower_product)) /\ exists pa_q_pvs_table_prefix_previouspower_product_partial. pa_u_pvs_table_prefix_previouspower_product = pa_q_pvs_table_prefix_previouspower_product_partial * S ((S (pa_i_pvs_table_prefix_previouspower_product)) * pa_v_pvs_table_prefix_previouspower_product) + (pa_r_pvs_table_prefix_previouspower_product))) /\ ((((exists pa_h_pvs_table_prefix_previouspower_product_successor. pa_h_pvs_table_prefix_previouspower_product_successor + S (pa_s_pvs_table_prefix_previouspower_product) = S ((S (S pa_i_pvs_table_prefix_previouspower_product)) * pa_v_pvs_table_prefix_previouspower_product)) /\ exists pa_q_pvs_table_prefix_previouspower_product_successor. pa_u_pvs_table_prefix_previouspower_product = pa_q_pvs_table_prefix_previouspower_product_successor * S ((S (S pa_i_pvs_table_prefix_previouspower_product)) * pa_v_pvs_table_prefix_previouspower_product) + (pa_s_pvs_table_prefix_previouspower_product))) /\ pa_s_pvs_table_prefix_previouspower_product = pa_r_pvs_table_prefix_previouspower_product * pa_p_pvs_table_prefix_previouspower_product)))))))))
  27. 0027specialize IH (n)
  28. 0028specialize IH (g)
  29. 0029apply IH
  30. 0030exact havailable
  31. 0031cases hprevious
  32. 0032cases hprevious_witness
  33. 0033have hextend : exists b c. (((exists ff_h_pvs_table_prefix_last. ff_h_pvs_table_prefix_last + S (x) = S ((S (L)) * c)) /\ exists ff_q_pvs_table_prefix_last. b = ff_q_pvs_table_prefix_last * S ((S (L)) * c) + (x))) /\ (forall pfp_i_pvs_table_prefix_preserve pfp_a_pvs_table_prefix_preserve. (exists pfp_gap_pvs_table_prefix_preservebound. pfp_gap_pvs_table_prefix_preservebound + S (pfp_i_pvs_table_prefix_preserve) = (L)) -> (((exists ff_h_pfp_pvs_table_prefix_preserveold. ff_h_pfp_pvs_table_prefix_preserveold + S (pfp_a_pvs_table_prefix_preserve) = S ((S (pfp_i_pvs_table_prefix_preserve)) * x2)) /\ exists ff_q_pfp_pvs_table_prefix_preserveold. x1 = ff_q_pfp_pvs_table_prefix_preserveold * S ((S (pfp_i_pvs_table_prefix_preserve)) * x2) + (pfp_a_pvs_table_prefix_preserve))) -> (((exists ff_h_pfp_pvs_table_prefix_preservenew. ff_h_pfp_pvs_table_prefix_preservenew + S (pfp_a_pvs_table_prefix_preserve) = S ((S (pfp_i_pvs_table_prefix_preserve)) * c)) /\ exists ff_q_pfp_pvs_table_prefix_preservenew. b = ff_q_pfp_pvs_table_prefix_preservenew * S ((S (pfp_i_pvs_table_prefix_preserve)) * c) + (pfp_a_pvs_table_prefix_preserve))))
  34. 0034specialize beta_prefix_extend (L)
  35. 0035specialize beta_prefix_extend (x1)
  36. 0036specialize beta_prefix_extend (x2)
  37. 0037specialize beta_prefix_extend (x)
  38. 0038apply beta_prefix_extend
  39. 0039cases hextend
  40. 0040cases hextend_witness
  41. 0041cases hextend_witness_witness
  42. 0042exists x3
  43. 0043exists x4
  44. 0044specialize perfect_power_root_table_prefix_append (n)
  45. 0045specialize perfect_power_root_table_prefix_append (g)
  46. 0046specialize perfect_power_root_table_prefix_append (x1)
  47. 0047specialize perfect_power_root_table_prefix_append (x2)
  48. 0048specialize perfect_power_root_table_prefix_append (x3)
  49. 0049specialize perfect_power_root_table_prefix_append (x4)
  50. 0050specialize perfect_power_root_table_prefix_append (L)
  51. 0051specialize perfect_power_root_table_prefix_append (x)
  52. 0052apply perfect_power_root_table_prefix_append
  53. 0053exact hprevious_witness_witness
  54. 0054exact hextend_witness_witness_right
  55. 0055exact hextend_witness_witness_left
  56. 0056exact hroot_witness