PA004T

finite_surjective_succ_from_prefix

Stable checked-use theorem · independently closed

The available successor branch extends prefix surjectivity to the full prefix.

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))))) -> (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

The available successor branch extends prefix surjectivity to the full prefix.

Use the direct prerequisites finite_last_is_top_from_prefix_surjective, finite_surjective_succ_intro as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro

Proof neighborhood

Direct dependencies

PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro

Direct dependents

PA004V finite_no_top_successor_gate PA004W finite_bounded_injective_surjective

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. 0009have hlast : ((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))
  10. 0010specialize finite_last_is_top_from_prefix_surjective b
  11. 0011specialize finite_last_is_top_from_prefix_surjective c
  12. 0012specialize finite_last_is_top_from_prefix_surjective n
  13. 0013specialize finite_last_is_top_from_prefix_surjective sn
  14. 0014apply finite_last_is_top_from_prefix_surjective
  15. 0015exact hsn
  16. 0016exact hbounded
  17. 0017exact hinj
  18. 0018exact hsurj
  19. 0019specialize finite_surjective_succ_intro b
  20. 0020specialize finite_surjective_succ_intro c
  21. 0021specialize finite_surjective_succ_intro n
  22. 0022specialize finite_surjective_succ_intro sn
  23. 0023apply finite_surjective_succ_intro
  24. 0024exact hsn
  25. 0025exact hsurj
  26. 0026exact hlast