PA004J · theorem

beta_prefix_replace_exists

Stable checked-use theorem · independently closed

Recode a finite beta prefix while replacing one interior entry.

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. ∀ i. ∀ s. ∀ k. Lt(i,k) → ∃ x. ∃ y. BetaAt(x,y,i,s) ∧ (∀ z. ∀ n. Lt(z,k) → ¬z = i → BetaAt(b,c,z,n) → BetaAt(x,y,z,n))

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 PD0013 BetaAt

5 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

8 occurrences

Exact expanded native-PA statement
forall b c i s k. (exists h. h + S i = k) -> exists z d. ((((exists ff_h_replace_entry. ff_h_replace_entry + S (s) = S ((S (i)) * d)) /\ exists ff_q_replace_entry. z = ff_q_replace_entry * S ((S (i)) * d) + (s))) /\ forall j a. (exists h. h + S j = k) -> ~(j = i) -> (((exists ff_h_replace_old. ff_h_replace_old + S (a) = S ((S (j)) * c)) /\ exists ff_q_replace_old. b = ff_q_replace_old * S ((S (j)) * c) + (a))) -> (((exists ff_h_replace_new. ff_h_replace_new + S (a) = S ((S (j)) * d)) /\ exists ff_q_replace_new. z = ff_q_replace_new * S ((S (j)) * d) + (a))))

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA002X beta_prefix_extend PA0029 beta_at_exists PA002F beta_at_unique

Direct theorem dependents

PA004K beta_prefix_swap_last_from_entries

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

122 script commands · 38 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 (6)
add eq zero rightsucc ne zerofinite lt succ eq or ltbeta prefix extendbeta at existsbeta at unique
01Fix variables and assumptionsL1–4

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro i
  4. L4
    intro s
02Induction on kL5–6

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L5
    induction k
  2. L6
    intro hi
03Separate the logical casesL7–8

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

  1. L7
    exfalso
  2. L8
    cases hi
04Establish hsiL9–17

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

  1. L9
    have hsi : S i = 0
  2. L10
    specialize add_eq_zero_right x
  3. L11
    specialize add_eq_zero_right (S i)
  4. L12
    apply add_eq_zero_right
  5. L13
    exact hi_witness
  6. L14
    specialize succ_ne_zero i
  7. L15
    apply succ_ne_zero
  8. L16
    exact hsi
  9. L17
    intro hi
05Establish hisplitL18–22

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

  1. L18
    have hisplit : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L19
    specialize finite_lt_succ_eq_or_lt k
  3. L20
    specialize finite_lt_succ_eq_or_lt i
  4. L21
    apply finite_lt_succ_eq_or_lt
  5. L22
    exact hi
06Separate the logical casesL23–23

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

  1. L23
    cases hisplit
07Use earlier factsL24–27

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

  1. L24
    specialize beta_prefix_extend k
  2. L25
    specialize beta_prefix_extend b
  3. L26
    specialize beta_prefix_extend c
  4. L27
    specialize beta_prefix_extend s
08Separate the logical casesL28–30

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

  1. L28
    cases beta_prefix_extend
  2. L29
    cases beta_prefix_extend_witness
  3. L30
    cases beta_prefix_extend_witness_witness
09Construct an explicit witnessL31–32

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

  1. L31
    exists x
  2. L32
    exists x1
10Separate the logical casesL33–33

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

  1. L33
    split
11Calculate and transport equalitiesL34–35

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

  1. L34
    rewrite hisplit_left
  2. L35
    rewrite hisplit_left
12Use earlier factsL36–36

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

  1. L36
    exact beta_prefix_extend_witness_witness_left
13Fix variables and assumptionsL37–41

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

  1. L37
    intro j
  2. L38
    intro a
  3. L39
    intro hj
  4. L40
    intro hji
  5. L41
    intro hold
14Establish hjsplitL42–46

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

  1. L42
    have hjsplit : j = k ∨ Lt(j,k)Definitions: Lt(j,k)Original native command in the exact edition
  2. L43
    specialize finite_lt_succ_eq_or_lt k
  3. L44
    specialize finite_lt_succ_eq_or_lt j
  4. L45
    apply finite_lt_succ_eq_or_lt
  5. L46
    exact hj
15Separate the logical casesL47–48

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

  1. L47
    cases hjsplit
  2. L48
    exfalso
16Use earlier factsL49–49

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

  1. L49
    apply hji
17Calculate and transport equalitiesL50–50

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

  1. L50
    trans k
18Use earlier factsL51–51

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

  1. L51
    exact hjsplit_left
19Calculate and transport equalitiesL52–52

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

  1. L52
    symm
20Use earlier factsL53–58

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

  1. L53
    exact hisplit_left
  2. L54
    specialize beta_prefix_extend_witness_witness_right j
  3. L55
    specialize beta_prefix_extend_witness_witness_right a
  4. L56
    apply beta_prefix_extend_witness_witness_right
  5. L57
    exact hjsplit_right
  6. L58
    exact hold
21Establish hreplacedL59–61

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

  1. L59
    have hreplaced : ∃ z. ∃ d. BetaAt(z,d,i,s) ∧ (∀ x. ∀ y. Lt(x,k) → ¬x = i → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))Definitions: BetaAt(z,d,i,s)Lt(x,k)BetaAt(b,c,x,y)BetaAt(z,d,x,y)Original native command in the exact edition
  2. L60
    apply IH
  3. L61
    exact hisplit_right
22Separate the logical casesL62–64

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

  1. L62
    cases hreplaced
  2. L63
    cases hreplaced_witness
  3. L64
    cases hreplaced_witness_witness
23Use earlier factsL65–67

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

  1. L65
    specialize beta_at_exists b
  2. L66
    specialize beta_at_exists c
  3. L67
    specialize beta_at_exists k
24Separate the logical casesL68–68

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

  1. L68
    cases beta_at_exists
25Use earlier factsL69–72

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

  1. L69
    specialize beta_prefix_extend k
  2. L70
    specialize beta_prefix_extend x
  3. L71
    specialize beta_prefix_extend x1
  4. L72
    specialize beta_prefix_extend x2
26Separate the logical casesL73–75

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

  1. L73
    cases beta_prefix_extend
  2. L74
    cases beta_prefix_extend_witness
  3. L75
    cases beta_prefix_extend_witness_witness
27Construct an explicit witnessL76–77

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

  1. L76
    exists x3
  2. L77
    exists x4
28Separate the logical casesL78–78

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

  1. L78
    split
29Use earlier factsL79–83

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

  1. L79
    specialize beta_prefix_extend_witness_witness_right i
  2. L80
    specialize beta_prefix_extend_witness_witness_right s
  3. L81
    apply beta_prefix_extend_witness_witness_right
  4. L82
    exact hisplit_right
  5. L83
    exact hreplaced_witness_witness_left
30Fix variables and assumptionsL84–88

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

  1. L84
    intro j
  2. L85
    intro a
  3. L86
    intro hj
  4. L87
    intro hji
  5. L88
    intro hold
31Establish hjsplitL89–93

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

  1. L89
    have hjsplit : j = k ∨ Lt(j,k)Definitions: Lt(j,k)Original native command in the exact edition
  2. L90
    specialize finite_lt_succ_eq_or_lt k
  3. L91
    specialize finite_lt_succ_eq_or_lt j
  4. L92
    apply finite_lt_succ_eq_or_lt
  5. L93
    exact hj
32Separate the logical casesL94–94

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

  1. L94
    cases hjsplit
33Establish haxL95–104

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

  1. L95
    have hax : a = x2
  2. L96
    specialize beta_at_unique b
  3. L97
    specialize beta_at_unique c
  4. L98
    specialize beta_at_unique k
  5. L99
    specialize beta_at_unique a
  6. L100
    specialize beta_at_unique x2
  7. L101
    apply beta_at_unique
  8. L102
    rewrite hjsplit_left at hold
  9. L103
    rewrite hjsplit_left at hold
  10. L104
    exact hold
34Use earlier factsL105–105

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

  1. L105
    exact beta_at_exists_witness
35Calculate and transport equalitiesL106–109

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

  1. L106
    rewrite hjsplit_left
  2. L107
    rewrite hjsplit_left
  3. L108
    rewrite hax
  4. L109
    rewrite hax
36Use earlier factsL110–110

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

  1. L110
    exact beta_prefix_extend_witness_witness_left
37Establish hmiddleL111–120

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

  1. L111
    have hmiddle : BetaAt(x,x1,j,a)Definitions: BetaAt(x,x1,j,a)Original native command in the exact edition
  2. L112
    specialize hreplaced_witness_witness_right j
  3. L113
    specialize hreplaced_witness_witness_right a
  4. L114
    apply hreplaced_witness_witness_right
  5. L115
    exact hjsplit_right
  6. L116
    exact hji
  7. L117
    exact hold
  8. L118
    specialize beta_prefix_extend_witness_witness_right j
  9. L119
    specialize beta_prefix_extend_witness_witness_right a
  10. L120
    apply beta_prefix_extend_witness_witness_right
38Use earlier factsL121–122

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

  1. L121
    exact hjsplit_right
  2. L122
    exact hmiddle

Library-wide reading audit

Original defined command ledger · 122 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro i
  4. 0004intro s
  5. 0005induction k
  6. 0006intro hi
  7. 0007exfalso
  8. 0008cases hi
  9. 0009have hsi : S i = 0
  10. 0010specialize add_eq_zero_right x
  11. 0011specialize add_eq_zero_right (S i)
  12. 0012apply add_eq_zero_right
  13. 0013exact hi_witness
  14. 0014specialize succ_ne_zero i
  15. 0015apply succ_ne_zero
  16. 0016exact hsi
  17. 0017intro hi
  18. 0018have hisplit : i = k ∨ Lt(i,k)
    Exact native replay linehave hisplit : i = k \/ exists h. h + S i = k
  19. 0019specialize finite_lt_succ_eq_or_lt k
  20. 0020specialize finite_lt_succ_eq_or_lt i
  21. 0021apply finite_lt_succ_eq_or_lt
  22. 0022exact hi
  23. 0023cases hisplit
  24. 0024specialize beta_prefix_extend k
  25. 0025specialize beta_prefix_extend b
  26. 0026specialize beta_prefix_extend c
  27. 0027specialize beta_prefix_extend s
  28. 0028cases beta_prefix_extend
  29. 0029cases beta_prefix_extend_witness
  30. 0030cases beta_prefix_extend_witness_witness
  31. 0031exists x
  32. 0032exists x1
  33. 0033split
  34. 0034rewrite hisplit_left
  35. 0035rewrite hisplit_left
  36. 0036exact beta_prefix_extend_witness_witness_left
  37. 0037intro j
  38. 0038intro a
  39. 0039intro hj
  40. 0040intro hji
  41. 0041intro hold
  42. 0042have hjsplit : j = k ∨ Lt(j,k)
    Exact native replay linehave hjsplit : j = k \/ exists h. h + S j = k
  43. 0043specialize finite_lt_succ_eq_or_lt k
  44. 0044specialize finite_lt_succ_eq_or_lt j
  45. 0045apply finite_lt_succ_eq_or_lt
  46. 0046exact hj
  47. 0047cases hjsplit
  48. 0048exfalso
  49. 0049apply hji
  50. 0050trans k
  51. 0051exact hjsplit_left
  52. 0052symm
  53. 0053exact hisplit_left
  54. 0054specialize beta_prefix_extend_witness_witness_right j
  55. 0055specialize beta_prefix_extend_witness_witness_right a
  56. 0056apply beta_prefix_extend_witness_witness_right
  57. 0057exact hjsplit_right
  58. 0058exact hold
  59. 0059have hreplaced : ∃ z. ∃ d. BetaAt(z,d,i,s) ∧ (∀ x. ∀ y. Lt(x,k) → ¬x = i → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))
    Exact native replay linehave hreplaced : exists z d. (((exists h. h + S s = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + s) /\ forall j a. (exists h. h + S j = k) -> ~(j = i) -> ((exists h. h + S a = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + a))
  60. 0060apply IH
  61. 0061exact hisplit_right
  62. 0062cases hreplaced
  63. 0063cases hreplaced_witness
  64. 0064cases hreplaced_witness_witness
  65. 0065specialize beta_at_exists b
  66. 0066specialize beta_at_exists c
  67. 0067specialize beta_at_exists k
  68. 0068cases beta_at_exists
  69. 0069specialize beta_prefix_extend k
  70. 0070specialize beta_prefix_extend x
  71. 0071specialize beta_prefix_extend x1
  72. 0072specialize beta_prefix_extend x2
  73. 0073cases beta_prefix_extend
  74. 0074cases beta_prefix_extend_witness
  75. 0075cases beta_prefix_extend_witness_witness
  76. 0076exists x3
  77. 0077exists x4
  78. 0078split
  79. 0079specialize beta_prefix_extend_witness_witness_right i
  80. 0080specialize beta_prefix_extend_witness_witness_right s
  81. 0081apply beta_prefix_extend_witness_witness_right
  82. 0082exact hisplit_right
  83. 0083exact hreplaced_witness_witness_left
  84. 0084intro j
  85. 0085intro a
  86. 0086intro hj
  87. 0087intro hji
  88. 0088intro hold
  89. 0089have hjsplit : j = k ∨ Lt(j,k)
    Exact native replay linehave hjsplit : j = k \/ exists h. h + S j = k
  90. 0090specialize finite_lt_succ_eq_or_lt k
  91. 0091specialize finite_lt_succ_eq_or_lt j
  92. 0092apply finite_lt_succ_eq_or_lt
  93. 0093exact hj
  94. 0094cases hjsplit
  95. 0095have hax : a = x2
  96. 0096specialize beta_at_unique b
  97. 0097specialize beta_at_unique c
  98. 0098specialize beta_at_unique k
  99. 0099specialize beta_at_unique a
  100. 0100specialize beta_at_unique x2
  101. 0101apply beta_at_unique
  102. 0102rewrite hjsplit_left at hold
  103. 0103rewrite hjsplit_left at hold
  104. 0104exact hold
  105. 0105exact beta_at_exists_witness
  106. 0106rewrite hjsplit_left
  107. 0107rewrite hjsplit_left
  108. 0108rewrite hax
  109. 0109rewrite hax
  110. 0110exact beta_prefix_extend_witness_witness_left
  111. 0111have hmiddle : BetaAt(x,x1,j,a)
    Exact native replay linehave hmiddle : ((exists h. h + S a = S ((S j) * x1)) /\ exists q. x = q * S ((S j) * x1) + a)
  112. 0112specialize hreplaced_witness_witness_right j
  113. 0113specialize hreplaced_witness_witness_right a
  114. 0114apply hreplaced_witness_witness_right
  115. 0115exact hjsplit_right
  116. 0116exact hji
  117. 0117exact hold
  118. 0118specialize beta_prefix_extend_witness_witness_right j
  119. 0119specialize beta_prefix_extend_witness_witness_right a
  120. 0120apply beta_prefix_extend_witness_witness_right
  121. 0121exact hjsplit_right
  122. 0122exact hmiddle