PA004X · theorem

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.

Statement with defined notation

∀ r. ∀ s. ∀ n. BoundedPrefix(r,s,S n) → InjectivePrefix(r,s,S n) → BetaAt(r,s,n,n) → BoundedPrefix(r,s,n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0013 BetaAt PD0024 BoundedPrefix PD0025 InjectivePrefix

4 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-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)))

Proof neighborhood

Direct theorem prerequisites

PA004P finite_bounded_prefix_without_top PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Direct theorem dependents

PA007X beta_product_permutation_invariant PA00CX beta_sum_permutation_invariant

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ∀ i. Lt(i,n) → ¬BetaAt(r,s,i,n)Definitions: Lt(i,n)BetaAt(r,s,i,n)Original native command in the exact edition
  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
  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
  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 defined 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 : ∀ i. Lt(i,n) → ¬BetaAt(r,s,i,n)
    Exact native replay linehave 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 : Lt(i,S n)
    Exact native replay linehave 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 : Lt(n,S n)
    Exact native replay linehave 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