PA004X

finite_fixed_last_prefix_bounded

Stable checked-use theorem · independently closed

A bounded injective successor reindexing fixed at its last position is bounded on the old prefix.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall r s n. (forall fp_i_fixed_last_bounded_succ. (exists fp_gap_fixed_last_bounded_succ_index. fp_gap_fixed_last_bounded_succ_index + S fp_i_fixed_last_bounded_succ = S n) -> exists fp_value_fixed_last_bounded_succ. ((((exists ff_h_fixed_last_bounded_succ_entry. ff_h_fixed_last_bounded_succ_entry + S (fp_value_fixed_last_bounded_succ) = S ((S (fp_i_fixed_last_bounded_succ)) * s)) /\ exists ff_q_fixed_last_bounded_succ_entry. r = ff_q_fixed_last_bounded_succ_entry * S ((S (fp_i_fixed_last_bounded_succ)) * s) + (fp_value_fixed_last_bounded_succ))) /\ (exists fp_gap_fixed_last_bounded_succ_value. fp_gap_fixed_last_bounded_succ_value + S fp_value_fixed_last_bounded_succ = S n))) -> (forall fp_i_fixed_last_injective_succ fp_j_fixed_last_injective_succ fp_value_fixed_last_injective_succ. (exists fp_gap_fixed_last_injective_succ_i. fp_gap_fixed_last_injective_succ_i + S fp_i_fixed_last_injective_succ = S n) -> (exists fp_gap_fixed_last_injective_succ_j. fp_gap_fixed_last_injective_succ_j + S fp_j_fixed_last_injective_succ = S n) -> (((exists ff_h_fixed_last_injective_succ_left. ff_h_fixed_last_injective_succ_left + S (fp_value_fixed_last_injective_succ) = S ((S (fp_i_fixed_last_injective_succ)) * s)) /\ exists ff_q_fixed_last_injective_succ_left. r = ff_q_fixed_last_injective_succ_left * S ((S (fp_i_fixed_last_injective_succ)) * s) + (fp_value_fixed_last_injective_succ))) -> (((exists ff_h_fixed_last_injective_succ_right. ff_h_fixed_last_injective_succ_right + S (fp_value_fixed_last_injective_succ) = S ((S (fp_j_fixed_last_injective_succ)) * s)) /\ exists ff_q_fixed_last_injective_succ_right. r = ff_q_fixed_last_injective_succ_right * S ((S (fp_j_fixed_last_injective_succ)) * s) + (fp_value_fixed_last_injective_succ))) -> fp_i_fixed_last_injective_succ = fp_j_fixed_last_injective_succ) -> (((exists ff_h_fixed_last_entry. ff_h_fixed_last_entry + S (n) = S ((S (n)) * s)) /\ exists ff_q_fixed_last_entry. r = ff_q_fixed_last_entry * S ((S (n)) * s) + (n))) -> (forall fp_i_fixed_last_bounded_prefix. (exists fp_gap_fixed_last_bounded_prefix_index. fp_gap_fixed_last_bounded_prefix_index + S fp_i_fixed_last_bounded_prefix = n) -> exists fp_value_fixed_last_bounded_prefix. ((((exists ff_h_fixed_last_bounded_prefix_entry. ff_h_fixed_last_bounded_prefix_entry + S (fp_value_fixed_last_bounded_prefix) = S ((S (fp_i_fixed_last_bounded_prefix)) * s)) /\ exists ff_q_fixed_last_bounded_prefix_entry. r = ff_q_fixed_last_bounded_prefix_entry * S ((S (fp_i_fixed_last_bounded_prefix)) * s) + (fp_value_fixed_last_bounded_prefix))) /\ (exists fp_gap_fixed_last_bounded_prefix_value. fp_gap_fixed_last_bounded_prefix_value + S fp_value_fixed_last_bounded_prefix = n)))

Structural proof guide

Generated structural guide

A bounded injective successor reindexing fixed at its last position is bounded on the old prefix.

Use the direct prerequisites finite_bounded_prefix_without_top, le_succ, le_refl, lt_irrefl_expanded as previously established PA formulas.

The proof proceeds by intermediate claims (4), equality transport (1).

Referenced ingredients

PA004P finite_bounded_prefix_without_top PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Proof neighborhood

Direct dependencies

PA004P finite_bounded_prefix_without_top PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Direct dependents

PA007X beta_product_permutation_invariant PA00CX beta_sum_permutation_invariant

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

39 script commands · 10 reading checkpoints · 4 local claims

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

Named ingredients (4)
finite bounded prefix without tople succle refllt irrefl expanded
01Fix variables and assumptionsL1–6

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro n
  4. L4
    intro hbounded
  5. L5
    intro hinjective
  6. L6
    intro hlast
02Establish hnotopL7–10

Establish this local claim before using it. It is not an additional assumption.

  1. L7
    have hnotop : forall i. (exists h. h + S i = n) -> ~((exists h. h + S n = S ((S i) * s)) /\ exists q. r = q * S ((S i) * s) + n)
  2. L8
    intro i
  3. L9
    intro hi
  4. L10
    intro htop
03Establish hisnL11–15

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

  1. L11
    have hisn : exists h. h + S i = S n
  2. L12
    specialize le_succ (S i)
  3. L13
    specialize le_succ n
  4. L14
    apply le_succ
  5. L15
    exact hi
04Establish hnsnL16–18

Establish this local claim before using it. It is not an additional assumption.

  1. L16
    have hnsn : exists h. h + S n = S n
  2. L17
    specialize le_refl (S n)
  3. L18
    exact le_refl
05Establish hinL19–28

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

  1. L19
    have hin : i = n
  2. L20
    specialize hinjective i
  3. L21
    specialize hinjective n
  4. L22
    specialize hinjective n
  5. L23
    apply hinjective
  6. L24
    exact hisn
  7. L25
    exact hnsn
  8. L26
    exact htop
  9. L27
    exact hlast
  10. L28
    specialize lt_irrefl_expanded n
06Use earlier factsL29–29

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

  1. L29
    apply lt_irrefl_expanded
07Calculate and transport equalitiesL30–30

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

  1. L30
    rewrite hin at hi
08Use earlier factsL31–36

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

  1. L31
    exact hi
  2. L32
    specialize finite_bounded_prefix_without_top r
  3. L33
    specialize finite_bounded_prefix_without_top s
  4. L34
    specialize finite_bounded_prefix_without_top n
  5. L35
    specialize finite_bounded_prefix_without_top (S n)
  6. L36
    apply finite_bounded_prefix_without_top
09Calculate and transport equalitiesL37–37

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

  1. L37
    refl
10Use earlier factsL38–39

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

  1. L38
    exact hbounded
  2. L39
    exact hnotop

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro n
  4. 0004intro hbounded
  5. 0005intro hinjective
  6. 0006intro hlast
  7. 0007have hnotop : forall i. (exists h. h + S i = n) -> ~((exists h. h + S n = S ((S i) * s)) /\ exists q. r = q * S ((S i) * s) + n)
  8. 0008intro i
  9. 0009intro hi
  10. 0010intro htop
  11. 0011have hisn : exists h. h + S i = S n
  12. 0012specialize le_succ (S i)
  13. 0013specialize le_succ n
  14. 0014apply le_succ
  15. 0015exact hi
  16. 0016have hnsn : exists h. h + S n = S n
  17. 0017specialize le_refl (S n)
  18. 0018exact le_refl
  19. 0019have hin : i = n
  20. 0020specialize hinjective i
  21. 0021specialize hinjective n
  22. 0022specialize hinjective n
  23. 0023apply hinjective
  24. 0024exact hisn
  25. 0025exact hnsn
  26. 0026exact htop
  27. 0027exact hlast
  28. 0028specialize lt_irrefl_expanded n
  29. 0029apply lt_irrefl_expanded
  30. 0030rewrite hin at hi
  31. 0031exact hi
  32. 0032specialize finite_bounded_prefix_without_top r
  33. 0033specialize finite_bounded_prefix_without_top s
  34. 0034specialize finite_bounded_prefix_without_top n
  35. 0035specialize finite_bounded_prefix_without_top (S n)
  36. 0036apply finite_bounded_prefix_without_top
  37. 0037refl
  38. 0038exact hbounded
  39. 0039exact hnotop