PA004T · theorem

finite_surjective_succ_from_prefix

Stable checked-use theorem · independently closed

The available successor branch extends prefix surjectivity to the full 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

∀ b. ∀ c. ∀ n. ∀ sn. sn = S n → BoundedPrefix(b,c,sn) → InjectivePrefix(b,c,sn) → SurjectivePrefix(b,c,n) → SurjectivePrefix(b,c,sn)

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

PD0024 BoundedPrefix PD0025 InjectivePrefix PD0026 SurjectivePrefix

4 occurrences

In local proof propositions

PD0013 BetaAt

1 occurrences

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

Proof neighborhood

Direct theorem prerequisites

PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro

Direct theorem dependents

PA004V finite_no_top_successor_gate PA004W finite_bounded_injective_surjective

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

26 script commands · 3 reading checkpoints · 1 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 (2)
finite last is top from prefix surjectivefinite surjective succ intro
01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro n
  4. L4
    intro sn
  5. L5
    intro hsn
  6. L6
    intro hbounded
  7. L7
    intro hinj
  8. L8
    intro hsurj
02Establish hlastL9–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite last is top from prefix surjective.

  1. L9
    have hlast : BetaAt(b,c,n,n)Definitions: BetaAt(b,c,n,n)Original native command in the exact edition
  2. L10
    specialize finite_last_is_top_from_prefix_surjective b
  3. L11
    specialize finite_last_is_top_from_prefix_surjective c
  4. L12
    specialize finite_last_is_top_from_prefix_surjective n
  5. L13
    specialize finite_last_is_top_from_prefix_surjective sn
  6. L14
    apply finite_last_is_top_from_prefix_surjective
  7. L15
    exact hsn
  8. L16
    exact hbounded
  9. L17
    exact hinj
  10. L18
    exact hsurj
03Use earlier factsL19–26

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L19
    specialize finite_surjective_succ_intro b
  2. L20
    specialize finite_surjective_succ_intro c
  3. L21
    specialize finite_surjective_succ_intro n
  4. L22
    specialize finite_surjective_succ_intro sn
  5. L23
    apply finite_surjective_succ_intro
  6. L24
    exact hsn
  7. L25
    exact hsurj
  8. L26
    exact hlast

Library-wide reading audit

Original defined command ledger · 26 lines
  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 : BetaAt(b,c,n,n)
    Exact native replay linehave 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