PA004V · theorem

finite_no_top_successor_gate

Stable checked-use theorem · independently closed

The no-top branch of the constructive successor induction is complete.

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) → ¬ContainsPrefix(b,c,n,n) → (BoundedPrefix(b,c,n) → InjectivePrefix(b,c,n) → 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 PD0027 ContainsPrefix

7 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0024 BoundedPrefix PD0025 InjectivePrefix PD0026 SurjectivePrefix

5 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) -> ~(exists fp_i_contains_top. ((exists fp_gap_contains_top_index. fp_gap_contains_top_index + S fp_i_contains_top = n) /\ (((exists ff_h_contains_top_entry. ff_h_contains_top_entry + S (n) = S ((S (fp_i_contains_top)) * c)) /\ exists ff_q_contains_top_entry. b = ff_q_contains_top_entry * S ((S (fp_i_contains_top)) * c) + (n))))) -> ((forall fp_i_bounded_prefix. (exists fp_gap_bounded_prefix_index. fp_gap_bounded_prefix_index + S fp_i_bounded_prefix = n) -> exists fp_value_bounded_prefix. ((((exists ff_h_bounded_prefix_entry. ff_h_bounded_prefix_entry + S (fp_value_bounded_prefix) = S ((S (fp_i_bounded_prefix)) * c)) /\ exists ff_q_bounded_prefix_entry. b = ff_q_bounded_prefix_entry * S ((S (fp_i_bounded_prefix)) * c) + (fp_value_bounded_prefix))) /\ (exists fp_gap_bounded_prefix_value. fp_gap_bounded_prefix_value + S fp_value_bounded_prefix = n))) -> (forall fp_i_inj_prefix fp_j_inj_prefix fp_value_inj_prefix. (exists fp_gap_inj_prefix_i. fp_gap_inj_prefix_i + S fp_i_inj_prefix = n) -> (exists fp_gap_inj_prefix_j. fp_gap_inj_prefix_j + S fp_j_inj_prefix = n) -> (((exists ff_h_inj_prefix_left. ff_h_inj_prefix_left + S (fp_value_inj_prefix) = S ((S (fp_i_inj_prefix)) * c)) /\ exists ff_q_inj_prefix_left. b = ff_q_inj_prefix_left * S ((S (fp_i_inj_prefix)) * c) + (fp_value_inj_prefix))) -> (((exists ff_h_inj_prefix_right. ff_h_inj_prefix_right + S (fp_value_inj_prefix) = S ((S (fp_j_inj_prefix)) * c)) /\ exists ff_q_inj_prefix_right. b = ff_q_inj_prefix_right * S ((S (fp_j_inj_prefix)) * c) + (fp_value_inj_prefix))) -> fp_i_inj_prefix = fp_j_inj_prefix) -> (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

PA004P finite_bounded_prefix_without_top PA004Q finite_injective_prefix_succ PA004T finite_surjective_succ_from_prefix

Direct theorem dependents

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

48 script commands · 9 reading checkpoints · 4 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 (3)
finite bounded prefix without topfinite injective prefix succfinite surjective succ from prefix
01Fix variables and assumptionsL1–9

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 hmissing
  9. L9
    intro hinduction
02Establish hnotopL10–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hmissing.

  1. L10
    have hnotop : ∀ i. Lt(i,n) → ¬BetaAt(b,c,i,n)Definitions: Lt(i,n)BetaAt(b,c,i,n)Original native command in the exact edition
  2. L11
    intro i
  3. L12
    intro hi
  4. L13
    intro hentry
  5. L14
    apply hmissing
03Construct an explicit witnessL15–15

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists i
04Separate the logical casesL16–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    split
05Use earlier factsL17–18

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

  1. L17
    exact hi
  2. L18
    exact hentry
06Establish hprefix_boundedL19–27

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

  1. L19
    have hprefix_bounded : BoundedPrefix(b,c,n)Definitions: BoundedPrefix(b,c,n)Original native command in the exact edition
  2. L20
    specialize finite_bounded_prefix_without_top b
  3. L21
    specialize finite_bounded_prefix_without_top c
  4. L22
    specialize finite_bounded_prefix_without_top n
  5. L23
    specialize finite_bounded_prefix_without_top sn
  6. L24
    apply finite_bounded_prefix_without_top
  7. L25
    exact hsn
  8. L26
    exact hbounded
  9. L27
    exact hnotop
07Establish hprefix_injectiveL28–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite injective prefix succ.

  1. L28
    have hprefix_injective : InjectivePrefix(b,c,n)Definitions: InjectivePrefix(b,c,n)Original native command in the exact edition
  2. L29
    specialize finite_injective_prefix_succ b
  3. L30
    specialize finite_injective_prefix_succ c
  4. L31
    specialize finite_injective_prefix_succ n
  5. L32
    specialize finite_injective_prefix_succ sn
  6. L33
    apply finite_injective_prefix_succ
  7. L34
    exact hsn
  8. L35
    exact hinj
08Establish hprefix_surjectiveL36–45

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hinduction.

  1. L36
    have hprefix_surjective : SurjectivePrefix(b,c,n)Definitions: SurjectivePrefix(b,c,n)Original native command in the exact edition
  2. L37
    apply hinduction
  3. L38
    exact hprefix_bounded
  4. L39
    exact hprefix_injective
  5. L40
    specialize finite_surjective_succ_from_prefix b
  6. L41
    specialize finite_surjective_succ_from_prefix c
  7. L42
    specialize finite_surjective_succ_from_prefix n
  8. L43
    specialize finite_surjective_succ_from_prefix sn
  9. L44
    apply finite_surjective_succ_from_prefix
  10. L45
    exact hsn
09Use earlier factsL46–48

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

  1. L46
    exact hbounded
  2. L47
    exact hinj
  3. L48
    exact hprefix_surjective

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro sn
  5. 0005intro hsn
  6. 0006intro hbounded
  7. 0007intro hinj
  8. 0008intro hmissing
  9. 0009intro hinduction
  10. 0010have hnotop : ∀ i. Lt(i,n) → ¬BetaAt(b,c,i,n)
    Exact native replay linehave hnotop : forall i. (exists h. h + S i = n) -> ~((exists h. h + S n = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + n)
  11. 0011intro i
  12. 0012intro hi
  13. 0013intro hentry
  14. 0014apply hmissing
  15. 0015exists i
  16. 0016split
  17. 0017exact hi
  18. 0018exact hentry
  19. 0019have hprefix_bounded : BoundedPrefix(b,c,n)
    Exact native replay linehave hprefix_bounded : forall fp_i_bounded_prefix. (exists fp_gap_bounded_prefix_index. fp_gap_bounded_prefix_index + S fp_i_bounded_prefix = n) -> exists fp_value_bounded_prefix. ((((exists ff_h_bounded_prefix_entry. ff_h_bounded_prefix_entry + S (fp_value_bounded_prefix) = S ((S (fp_i_bounded_prefix)) * c)) /\ exists ff_q_bounded_prefix_entry. b = ff_q_bounded_prefix_entry * S ((S (fp_i_bounded_prefix)) * c) + (fp_value_bounded_prefix))) /\ (exists fp_gap_bounded_prefix_value. fp_gap_bounded_prefix_value + S fp_value_bounded_prefix = n))
  20. 0020specialize finite_bounded_prefix_without_top b
  21. 0021specialize finite_bounded_prefix_without_top c
  22. 0022specialize finite_bounded_prefix_without_top n
  23. 0023specialize finite_bounded_prefix_without_top sn
  24. 0024apply finite_bounded_prefix_without_top
  25. 0025exact hsn
  26. 0026exact hbounded
  27. 0027exact hnotop
  28. 0028have hprefix_injective : InjectivePrefix(b,c,n)
    Exact native replay linehave hprefix_injective : forall fp_i_inj_prefix fp_j_inj_prefix fp_value_inj_prefix. (exists fp_gap_inj_prefix_i. fp_gap_inj_prefix_i + S fp_i_inj_prefix = n) -> (exists fp_gap_inj_prefix_j. fp_gap_inj_prefix_j + S fp_j_inj_prefix = n) -> (((exists ff_h_inj_prefix_left. ff_h_inj_prefix_left + S (fp_value_inj_prefix) = S ((S (fp_i_inj_prefix)) * c)) /\ exists ff_q_inj_prefix_left. b = ff_q_inj_prefix_left * S ((S (fp_i_inj_prefix)) * c) + (fp_value_inj_prefix))) -> (((exists ff_h_inj_prefix_right. ff_h_inj_prefix_right + S (fp_value_inj_prefix) = S ((S (fp_j_inj_prefix)) * c)) /\ exists ff_q_inj_prefix_right. b = ff_q_inj_prefix_right * S ((S (fp_j_inj_prefix)) * c) + (fp_value_inj_prefix))) -> fp_i_inj_prefix = fp_j_inj_prefix
  29. 0029specialize finite_injective_prefix_succ b
  30. 0030specialize finite_injective_prefix_succ c
  31. 0031specialize finite_injective_prefix_succ n
  32. 0032specialize finite_injective_prefix_succ sn
  33. 0033apply finite_injective_prefix_succ
  34. 0034exact hsn
  35. 0035exact hinj
  36. 0036have hprefix_surjective : SurjectivePrefix(b,c,n)
    Exact native replay linehave hprefix_surjective : 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))))
  37. 0037apply hinduction
  38. 0038exact hprefix_bounded
  39. 0039exact hprefix_injective
  40. 0040specialize finite_surjective_succ_from_prefix b
  41. 0041specialize finite_surjective_succ_from_prefix c
  42. 0042specialize finite_surjective_succ_from_prefix n
  43. 0043specialize finite_surjective_succ_from_prefix sn
  44. 0044apply finite_surjective_succ_from_prefix
  45. 0045exact hsn
  46. 0046exact hbounded
  47. 0047exact hinj
  48. 0048exact hprefix_surjective