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.

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.

  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