PA004R

finite_last_is_top_from_prefix_surjective

Stable checked-use theorem · independently closed

A bounded injective successor sequence must place the new value last once its prefix is surjective.

Exact expanded PA statement

forall b c n sn. sn = S n -> (forall fp_i_bounded_succ. (exists fp_gap_bounded_succ_index. fp_gap_bounded_succ_index + S fp_i_bounded_succ = sn) -> exists fp_value_bounded_succ. ((((exists ff_h_bounded_succ_entry. ff_h_bounded_succ_entry + S (fp_value_bounded_succ) = S ((S (fp_i_bounded_succ)) * c)) /\ exists ff_q_bounded_succ_entry. b = ff_q_bounded_succ_entry * S ((S (fp_i_bounded_succ)) * c) + (fp_value_bounded_succ))) /\ (exists fp_gap_bounded_succ_value. fp_gap_bounded_succ_value + S fp_value_bounded_succ = sn))) -> (forall fp_i_inj_succ fp_j_inj_succ fp_value_inj_succ. (exists fp_gap_inj_succ_i. fp_gap_inj_succ_i + S fp_i_inj_succ = sn) -> (exists fp_gap_inj_succ_j. fp_gap_inj_succ_j + S fp_j_inj_succ = sn) -> (((exists ff_h_inj_succ_left. ff_h_inj_succ_left + S (fp_value_inj_succ) = S ((S (fp_i_inj_succ)) * c)) /\ exists ff_q_inj_succ_left. b = ff_q_inj_succ_left * S ((S (fp_i_inj_succ)) * c) + (fp_value_inj_succ))) -> (((exists ff_h_inj_succ_right. ff_h_inj_succ_right + S (fp_value_inj_succ) = S ((S (fp_j_inj_succ)) * c)) /\ exists ff_q_inj_succ_right. b = ff_q_inj_succ_right * S ((S (fp_j_inj_succ)) * c) + (fp_value_inj_succ))) -> fp_i_inj_succ = fp_j_inj_succ) -> (forall fp_value_surj_n. (exists fp_gap_surj_n_value. fp_gap_surj_n_value + S fp_value_surj_n = n) -> exists fp_i_surj_n. ((exists fp_gap_surj_n_index. fp_gap_surj_n_index + S fp_i_surj_n = n) /\ (((exists ff_h_surj_n_entry. ff_h_surj_n_entry + S (fp_value_surj_n) = S ((S (fp_i_surj_n)) * c)) /\ exists ff_q_surj_n_entry. b = ff_q_surj_n_entry * S ((S (fp_i_surj_n)) * c) + (fp_value_surj_n))))) -> (((exists ff_h_last_n. ff_h_last_n + S (n) = S ((S (n)) * c)) /\ exists ff_q_last_n. b = ff_q_last_n * S ((S (n)) * c) + (n)))

Structural proof guide

Generated structural guide

A bounded injective successor sequence must place the new value last once its prefix is surjective.

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

The proof proceeds by case analysis (5), intermediate claims (4), equality transport (5).

Referenced ingredients

PA004I finite_bounded_last_succ PA003D finite_lt_succ_eq_or_lt PA001A le_refl PA002O le_succ PA0010 lt_irrefl_expanded

Proof neighborhood

Direct dependencies

PA004I finite_bounded_last_succ PA003D finite_lt_succ_eq_or_lt PA001A le_refl PA002O le_succ PA0010 lt_irrefl_expanded

Direct dependents

PA004T finite_surjective_succ_from_prefix

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 b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro sn
  5. 0005intro hsn
  6. 0006intro hbounded
  7. 0007intro hinj
  8. 0008intro hsurj
  9. 0009rewrite hsn at hinj
  10. 0010rewrite hsn at hinj
  11. 0011have hlast : exists x. (((exists h. h + S x = S ((S n) * c)) /\ exists q. b = q * S ((S n) * c) + x) /\ exists h. h + S x = S n)
  12. 0012specialize finite_bounded_last_succ b
  13. 0013specialize finite_bounded_last_succ c
  14. 0014specialize finite_bounded_last_succ n
  15. 0015specialize finite_bounded_last_succ sn
  16. 0016apply finite_bounded_last_succ
  17. 0017exact hsn
  18. 0018exact hbounded
  19. 0019cases hlast
  20. 0020cases hlast_witness
  21. 0021have hsplit : x = n \/ exists h. h + S x = n
  22. 0022specialize finite_lt_succ_eq_or_lt n
  23. 0023specialize finite_lt_succ_eq_or_lt x
  24. 0024apply finite_lt_succ_eq_or_lt
  25. 0025exact hlast_witness_right
  26. 0026cases hsplit
  27. 0027rewrite hsplit_left at hlast_witness_left
  28. 0028rewrite hsplit_left at hlast_witness_left
  29. 0029exact hlast_witness_left
  30. 0030specialize hsurj x
  31. 0031have hpre : exists i. ((exists h. h + S i = n) /\ ((exists h. h + S x = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + x))
  32. 0032apply hsurj
  33. 0033exact hsplit_right
  34. 0034cases hpre
  35. 0035cases hpre_witness
  36. 0036have hni : n = x1
  37. 0037specialize hinj n
  38. 0038specialize hinj x1
  39. 0039specialize hinj x
  40. 0040apply hinj
  41. 0041specialize le_refl (S n)
  42. 0042exact le_refl
  43. 0043specialize le_succ (S x1)
  44. 0044specialize le_succ n
  45. 0045apply le_succ
  46. 0046exact hpre_witness_left
  47. 0047exact hlast_witness_left
  48. 0048exact hpre_witness_right
  49. 0049exfalso
  50. 0050specialize lt_irrefl_expanded n
  51. 0051apply lt_irrefl_expanded
  52. 0052rewrite hni
  53. 0053exact hpre_witness_left