PA00AE · theorem

finite_prefix_choose_unused_nonendpoint

Alpha v34 checked-use theorem · independently closed; not Stable

By temporarily appending both endpoints, finite omission constructively selects a missing nonendpoint value.

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. ∀ l. ∀ n. ∀ r. n = S r → Lt(S S l,n) → ∃ x. Lt(x,n) ∧ (¬x = 0 ∧ ¬S x = n ∧ ¬ContainsPrefix(b,c,l,x))

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

PD0002 Lt PD0027 ContainsPrefix

3 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0027 ContainsPrefix

11 occurrences

Exact expanded native-PA statement
forall b c l n r. n = S r -> (exists h. h + S (S (S l)) = n) -> (exists y. ((exists wpo_gap_choose_result_bound. wpo_gap_choose_result_bound + S (y) = n) /\ ((~(y = 0) /\ ~((S y) = n)) /\ (~(exists wpo_index_choose_result_omit_contains. ((exists wpo_gap_choose_result_omit_contains_bound. wpo_gap_choose_result_omit_contains_bound + S (wpo_index_choose_result_omit_contains) = l) /\ (((exists wpo_beta_height_choose_result_omit_contains_entry. wpo_beta_height_choose_result_omit_contains_entry + S (y) = S ((S (wpo_index_choose_result_omit_contains)) * c)) /\ exists wpo_beta_quotient_choose_result_omit_contains_entry. b = wpo_beta_quotient_choose_result_omit_contains_entry * S ((S (wpo_index_choose_result_omit_contains)) * c) + (y)))))))))

Proof neighborhood

Direct theorem prerequisites

PA009K beta_prefix_append_two_exists PA0098 finite_short_prefix_omits PA001A le_refl PA002O le_succ PA003V succ_injective

Direct theorem dependents

PA00AR prime_choose_unused_nonendpoint_orbit

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

86 script commands · 31 reading checkpoints · 7 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 (5)
beta prefix append two existsfinite short prefix omitsle reflle succsucc injective
01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro r
  6. L6
    intro hnr
  7. L7
    intro hshort
02Establish haugmentedL8–14

Establish this local claim before using it. It is not an additional assumption.

  1. L8
    have haugmented : ∃ z. ∃ d. BetaAt(z,d,l,0) ∧ (BetaAt(z,d,S l,r) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y)))Definitions: BetaAt(z,d,l,0)BetaAt(z,d,S l,r)Lt(x,l)BetaAt(b,c,x,y)BetaAt(z,d,x,y)Original native command in the exact edition
  2. L9
    specialize beta_prefix_append_two_exists b
  3. L10
    specialize beta_prefix_append_two_exists c
  4. L11
    specialize beta_prefix_append_two_exists l
  5. L12
    specialize beta_prefix_append_two_exists 0
  6. L13
    specialize beta_prefix_append_two_exists r
  7. L14
    exact beta_prefix_append_two_exists
03Separate the logical casesL15–16

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

  1. L15
    cases haugmented
  2. L16
    cases haugmented_witness
04Establish homittedL17–23

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

  1. L17
    have homitted : ∃ wpo_value_choose_augmented_omit. Lt(wpo_value_choose_augmented_omit,n) ∧ ¬ContainsPrefix(x,x1,S S l,wpo_value_choose_augmented_omit)Definitions: Lt(wpo_value_choose_augmented_omit,n)ContainsPrefix(x,x1,S S l,wpo_value_choose_augmented_omit)Original native command in the exact edition
  2. L18
    specialize finite_short_prefix_omits x
  3. L19
    specialize finite_short_prefix_omits x1
  4. L20
    specialize finite_short_prefix_omits (S (S l))
  5. L21
    specialize finite_short_prefix_omits n
  6. L22
    apply finite_short_prefix_omits
  7. L23
    exact hshort
05Separate the logical casesL24–27

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

  1. L24
    cases homitted
  2. L25
    cases homitted_witness
  3. L26
    cases haugmented_witness_witness
  4. L27
    cases haugmented_witness_witness_right
06Construct an explicit witnessL28–28

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

  1. L28
    exists x2
07Separate the logical casesL29–29

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

  1. L29
    split
08Use earlier factsL30–30

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

  1. L30
    exact homitted_witness_left
09Separate the logical casesL31–32

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

  1. L31
    split
  2. L32
    split
10Fix variables and assumptionsL33–33

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

  1. L33
    intro hxzero
11Use earlier factsL34–34

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

  1. L34
    apply homitted_witness_right
12Construct an explicit witnessL35–35

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

  1. L35
    exists l
13Separate the logical casesL36–36

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

  1. L36
    split
14Use earlier factsL37–41

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

  1. L37
    specialize le_succ (S l)
  2. L38
    specialize le_succ (S l)
  3. L39
    apply le_succ
  4. L40
    specialize le_refl (S l)
  5. L41
    exact le_refl
15Calculate and transport equalitiesL42–43

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L42
    rewrite hxzero
  2. L43
    rewrite hxzero
16Use earlier factsL44–44

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

  1. L44
    exact haugmented_witness_witness_left
17Fix variables and assumptionsL45–45

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

  1. L45
    intro hxlast
18Establish hxrL46–53

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

  1. L46
    have hxr : x2 = r
  2. L47
    specialize succ_injective x2
  3. L48
    specialize succ_injective r
  4. L49
    apply succ_injective
  5. L50
    trans n
  6. L51
    exact hxlast
  7. L52
    exact hnr
  8. L53
    apply homitted_witness_right
19Construct an explicit witnessL54–54

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

  1. L54
    exists (S l)
20Separate the logical casesL55–55

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

  1. L55
    split
21Use earlier factsL56–57

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

  1. L56
    specialize le_refl (S (S l))
  2. L57
    exact le_refl
22Calculate and transport equalitiesL58–59

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L58
    rewrite hxr
  2. L59
    rewrite hxr
23Use earlier factsL60–60

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

  1. L60
    exact haugmented_witness_witness_right_left
24Establish hold_omitL61–62

Establish this local claim before using it. It is not an additional assumption.

  1. L61
    have hold_omit : ¬ContainsPrefix(b,c,l,x2)Definitions: ContainsPrefix(b,c,l,x2)Original native command in the exact edition
  2. L62
    intro hold_contains
25Separate the logical casesL63–64

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

  1. L63
    cases hold_contains
  2. L64
    cases hold_contains_witness
26Establish hliftL65–69

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

  1. L65
    have hlift : Lt(x3,S l)Definitions: Lt(x3,S l)Original native command in the exact edition
  2. L66
    specialize le_succ (S x3)
  3. L67
    specialize le_succ l
  4. L68
    apply le_succ
  5. L69
    exact hold_contains_witness_left
27Establish hlift2L70–74

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

  1. L70
    have hlift2 : Lt(x3,S S l)Definitions: Lt(x3,S S l)Original native command in the exact edition
  2. L71
    specialize le_succ (S x3)
  3. L72
    specialize le_succ (S l)
  4. L73
    apply le_succ
  5. L74
    exact hlift
28Establish hnew_entryL75–81

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

  1. L75
    have hnew_entry : BetaAt(x,x1,x3,x2)Definitions: BetaAt(x,x1,x3,x2)Original native command in the exact edition
  2. L76
    specialize haugmented_witness_witness_right_right x3
  3. L77
    specialize haugmented_witness_witness_right_right x2
  4. L78
    apply haugmented_witness_witness_right_right
  5. L79
    exact hold_contains_witness_left
  6. L80
    exact hold_contains_witness_right
  7. L81
    apply homitted_witness_right
29Construct an explicit witnessL82–82

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

  1. L82
    exists x3
30Separate the logical casesL83–83

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

  1. L83
    split
31Use earlier factsL84–86

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

  1. L84
    exact hlift2
  2. L85
    exact hnew_entry
  3. L86
    exact hold_omit

Library-wide reading audit

Original defined command ledger · 86 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro r
  6. 0006intro hnr
  7. 0007intro hshort
  8. 0008have haugmented : ∃ z. ∃ d. BetaAt(z,d,l,0) ∧ (BetaAt(z,d,S l,r) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y)))
    Exact native replay linehave haugmented : exists z d. (((((exists wpo_beta_height_choose_augmented_trace_first. wpo_beta_height_choose_augmented_trace_first + S (0) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_choose_augmented_trace_first. z = wpo_beta_quotient_choose_augmented_trace_first * S ((S (l)) * d) + (0))) /\ ((((exists wpo_beta_height_choose_augmented_trace_second. wpo_beta_height_choose_augmented_trace_second + S (r) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_choose_augmented_trace_second. z = wpo_beta_quotient_choose_augmented_trace_second * S ((S (S (l))) * d) + (r))) /\ (forall wpo_old_index_choose_augmented_trace wpo_old_value_choose_augmented_trace. (exists wpo_gap_choose_augmented_trace_old_bound. wpo_gap_choose_augmented_trace_old_bound + S (wpo_old_index_choose_augmented_trace) = l) -> (((exists wpo_beta_height_choose_augmented_trace_old_entry. wpo_beta_height_choose_augmented_trace_old_entry + S (wpo_old_value_choose_augmented_trace) = S ((S (wpo_old_index_choose_augmented_trace)) * c)) /\ exists wpo_beta_quotient_choose_augmented_trace_old_entry. b = wpo_beta_quotient_choose_augmented_trace_old_entry * S ((S (wpo_old_index_choose_augmented_trace)) * c) + (wpo_old_value_choose_augmented_trace))) -> (((exists wpo_beta_height_choose_augmented_trace_new_entry. wpo_beta_height_choose_augmented_trace_new_entry + S (wpo_old_value_choose_augmented_trace) = S ((S (wpo_old_index_choose_augmented_trace)) * d)) /\ exists wpo_beta_quotient_choose_augmented_trace_new_entry. z = wpo_beta_quotient_choose_augmented_trace_new_entry * S ((S (wpo_old_index_choose_augmented_trace)) * d) + (wpo_old_value_choose_augmented_trace)))))))
  9. 0009specialize beta_prefix_append_two_exists b
  10. 0010specialize beta_prefix_append_two_exists c
  11. 0011specialize beta_prefix_append_two_exists l
  12. 0012specialize beta_prefix_append_two_exists 0
  13. 0013specialize beta_prefix_append_two_exists r
  14. 0014exact beta_prefix_append_two_exists
  15. 0015cases haugmented
  16. 0016cases haugmented_witness
  17. 0017have homitted : ∃ wpo_value_choose_augmented_omit. Lt(wpo_value_choose_augmented_omit,n) ∧ ¬ContainsPrefix(x,x1,S S l,wpo_value_choose_augmented_omit)
    Exact native replay linehave homitted : exists wpo_value_choose_augmented_omit. ((exists wpo_gap_choose_augmented_omit_value_bound. wpo_gap_choose_augmented_omit_value_bound + S (wpo_value_choose_augmented_omit) = n) /\ (~(exists wpo_index_choose_augmented_omit_omitted_contains. ((exists wpo_gap_choose_augmented_omit_omitted_contains_bound. wpo_gap_choose_augmented_omit_omitted_contains_bound + S (wpo_index_choose_augmented_omit_omitted_contains) = S (S l)) /\ (((exists wpo_beta_height_choose_augmented_omit_omitted_contains_entry. wpo_beta_height_choose_augmented_omit_omitted_contains_entry + S (wpo_value_choose_augmented_omit) = S ((S (wpo_index_choose_augmented_omit_omitted_contains)) * x1)) /\ exists wpo_beta_quotient_choose_augmented_omit_omitted_contains_entry. x = wpo_beta_quotient_choose_augmented_omit_omitted_contains_entry * S ((S (wpo_index_choose_augmented_omit_omitted_contains)) * x1) + (wpo_value_choose_augmented_omit)))))))
  18. 0018specialize finite_short_prefix_omits x
  19. 0019specialize finite_short_prefix_omits x1
  20. 0020specialize finite_short_prefix_omits (S (S l))
  21. 0021specialize finite_short_prefix_omits n
  22. 0022apply finite_short_prefix_omits
  23. 0023exact hshort
  24. 0024cases homitted
  25. 0025cases homitted_witness
  26. 0026cases haugmented_witness_witness
  27. 0027cases haugmented_witness_witness_right
  28. 0028exists x2
  29. 0029split
  30. 0030exact homitted_witness_left
  31. 0031split
  32. 0032split
  33. 0033intro hxzero
  34. 0034apply homitted_witness_right
  35. 0035exists l
  36. 0036split
  37. 0037specialize le_succ (S l)
  38. 0038specialize le_succ (S l)
  39. 0039apply le_succ
  40. 0040specialize le_refl (S l)
  41. 0041exact le_refl
  42. 0042rewrite hxzero
  43. 0043rewrite hxzero
  44. 0044exact haugmented_witness_witness_left
  45. 0045intro hxlast
  46. 0046have hxr : x2 = r
  47. 0047specialize succ_injective x2
  48. 0048specialize succ_injective r
  49. 0049apply succ_injective
  50. 0050trans n
  51. 0051exact hxlast
  52. 0052exact hnr
  53. 0053apply homitted_witness_right
  54. 0054exists (S l)
  55. 0055split
  56. 0056specialize le_refl (S (S l))
  57. 0057exact le_refl
  58. 0058rewrite hxr
  59. 0059rewrite hxr
  60. 0060exact haugmented_witness_witness_right_left
  61. 0061have hold_omit : ¬ContainsPrefix(b,c,l,x2)
    Exact native replay linehave hold_omit : ~(exists wpo_index_choose_old_omit_y_contains. ((exists wpo_gap_choose_old_omit_y_contains_bound. wpo_gap_choose_old_omit_y_contains_bound + S (wpo_index_choose_old_omit_y_contains) = l) /\ (((exists wpo_beta_height_choose_old_omit_y_contains_entry. wpo_beta_height_choose_old_omit_y_contains_entry + S (x2) = S ((S (wpo_index_choose_old_omit_y_contains)) * c)) /\ exists wpo_beta_quotient_choose_old_omit_y_contains_entry. b = wpo_beta_quotient_choose_old_omit_y_contains_entry * S ((S (wpo_index_choose_old_omit_y_contains)) * c) + (x2)))))
  62. 0062intro hold_contains
  63. 0063cases hold_contains
  64. 0064cases hold_contains_witness
  65. 0065have hlift : Lt(x3,S l)
    Exact native replay linehave hlift : exists h. h + S x3 = S l
  66. 0066specialize le_succ (S x3)
  67. 0067specialize le_succ l
  68. 0068apply le_succ
  69. 0069exact hold_contains_witness_left
  70. 0070have hlift2 : Lt(x3,S S l)
    Exact native replay linehave hlift2 : exists h. h + S x3 = S (S l)
  71. 0071specialize le_succ (S x3)
  72. 0072specialize le_succ (S l)
  73. 0073apply le_succ
  74. 0074exact hlift
  75. 0075have hnew_entry : BetaAt(x,x1,x3,x2)
    Exact native replay linehave hnew_entry : ((exists h. h + S x2 = S ((S x3) * x1)) /\ exists q. x = q * S ((S x3) * x1) + x2)
  76. 0076specialize haugmented_witness_witness_right_right x3
  77. 0077specialize haugmented_witness_witness_right_right x2
  78. 0078apply haugmented_witness_witness_right_right
  79. 0079exact hold_contains_witness_left
  80. 0080exact hold_contains_witness_right
  81. 0081apply homitted_witness_right
  82. 0082exists x3
  83. 0083split
  84. 0084exact hlift2
  85. 0085exact hnew_entry
  86. 0086exact hold_omit