PA004S

finite_surjective_succ_intro

Stable checked-use theorem · independently closed

A surjective prefix plus its new top value is surjective at successor length.

Exact expanded PA statement

forall b c n sn. sn = S n -> (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))) -> (forall fp_value_surj_succ. (exists fp_gap_surj_succ_value. fp_gap_surj_succ_value + S fp_value_surj_succ = sn) -> exists fp_i_surj_succ. ((exists fp_gap_surj_succ_index. fp_gap_surj_succ_index + S fp_i_surj_succ = sn) /\ (((exists ff_h_surj_succ_entry. ff_h_surj_succ_entry + S (fp_value_surj_succ) = S ((S (fp_i_surj_succ)) * c)) /\ exists ff_q_surj_succ_entry. b = ff_q_surj_succ_entry * S ((S (fp_i_surj_succ)) * c) + (fp_value_surj_succ)))))

Structural proof guide

Generated structural guide

A surjective prefix plus its new top value is surjective at successor length.

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

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

Referenced ingredients

PA003D finite_lt_succ_eq_or_lt PA001A le_refl PA002O le_succ

Proof neighborhood

Direct dependencies

PA003D finite_lt_succ_eq_or_lt PA001A le_refl PA002O le_succ

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 hsurj
  7. 0007intro hlast
  8. 0008rewrite hsn
  9. 0009rewrite hsn
  10. 0010intro y
  11. 0011intro hy
  12. 0012have hsplit : y = n \/ exists h. h + S y = n
  13. 0013specialize finite_lt_succ_eq_or_lt n
  14. 0014specialize finite_lt_succ_eq_or_lt y
  15. 0015apply finite_lt_succ_eq_or_lt
  16. 0016exact hy
  17. 0017cases hsplit
  18. 0018exists n
  19. 0019split
  20. 0020specialize le_refl (S n)
  21. 0021exact le_refl
  22. 0022rewrite hsplit_left
  23. 0023rewrite hsplit_left
  24. 0024exact hlast
  25. 0025specialize hsurj y
  26. 0026have hpre : exists i. ((exists h. h + S i = n) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y))
  27. 0027apply hsurj
  28. 0028exact hsplit_right
  29. 0029cases hpre
  30. 0030cases hpre_witness
  31. 0031exists x
  32. 0032split
  33. 0033specialize le_succ (S x)
  34. 0034specialize le_succ n
  35. 0035apply le_succ
  36. 0036exact hpre_witness_left
  37. 0037exact hpre_witness_right