PA004K · theorem

beta_prefix_swap_last_from_entries

Stable checked-use theorem · independently closed

Swap a chosen interior beta entry with the last entry, given both decoded values.

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

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

8 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

12 occurrences

Exact expanded native-PA statement
forall b c n i x y. (exists h. h + S i = n) -> (((exists ff_h_swap_old_i. ff_h_swap_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_swap_old_i. b = ff_q_swap_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_swap_old_n. ff_h_swap_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_swap_old_n. b = ff_q_swap_old_n * S ((S (n)) * c) + (y))) -> exists z d. ((((exists ff_h_swap_new_i. ff_h_swap_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_swap_new_i. z = ff_q_swap_new_i * S ((S (i)) * d) + (y))) /\ ((((exists ff_h_swap_new_n. ff_h_swap_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_swap_new_n. z = ff_q_swap_new_n * S ((S (n)) * d) + (x))) /\ forall j a. (exists h. h + S j = S n) -> ~(j = i) -> ~(j = n) -> (((exists ff_h_swap_old_j. ff_h_swap_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_swap_old_j. b = ff_q_swap_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_swap_new_j. ff_h_swap_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_swap_new_j. z = ff_q_swap_new_j * S ((S (j)) * d) + (a)))))

Proof neighborhood

Direct theorem prerequisites

PA004J beta_prefix_replace_exists PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Direct theorem dependents

PA004W finite_bounded_injective_surjective PA007X beta_product_permutation_invariant PA00CX beta_sum_permutation_invariant

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

87 script commands · 18 reading checkpoints · 8 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 (4)
beta prefix replace existsle succle refllt irrefl expanded
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 i
  5. L5
    intro x
  6. L6
    intro y
  7. L7
    intro hi
  8. L8
    intro hxi
  9. L9
    intro hyn
02Establish hisnL10–14

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

  1. L10
  2. L11
    specialize le_succ (S i)
  3. L12
    specialize le_succ n
  4. L13
    apply le_succ
  5. L14
    exact hi
03Establish hnsnL15–17

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

  1. L15
  2. L16
    specialize le_refl (S n)
  3. L17
    exact le_refl
04Establish hinL18–23

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

  1. L18
    have hin : ~(i = n)
  2. L19
    intro hin_eq
  3. L20
    specialize lt_irrefl_expanded n
  4. L21
    apply lt_irrefl_expanded
  5. L22
    rewrite hin_eq at hi
  6. L23
    exact hi
05Establish hniL24–28

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

  1. L24
    have hni : ~(n = i)
  2. L25
    intro hni_eq
  3. L26
    apply hin
  4. L27
    symm
  5. L28
    exact hni_eq
06Establish hfirstL29–36

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

  1. L29
    have hfirst : ∃ z. ∃ d. BetaAt(z,d,i,y) ∧ (∀ x. ∀ m. Lt(x,S n) → ¬x = i → BetaAt(b,c,x,m) → BetaAt(z,d,x,m))Definitions: BetaAt(z,d,i,y)Lt(x,S n)BetaAt(b,c,x,m)BetaAt(z,d,x,m)Original native command in the exact edition
  2. L30
    specialize beta_prefix_replace_exists b
  3. L31
    specialize beta_prefix_replace_exists c
  4. L32
    specialize beta_prefix_replace_exists i
  5. L33
    specialize beta_prefix_replace_exists y
  6. L34
    specialize beta_prefix_replace_exists (S n)
  7. L35
    apply beta_prefix_replace_exists
  8. L36
    exact hisn
07Separate the logical casesL37–39

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

  1. L37
    cases hfirst
  2. L38
    cases hfirst_witness
  3. L39
    cases hfirst_witness_witness
08Establish hfirst_nL40–46

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

  1. L40
    have hfirst_n : BetaAt(x1,x2,n,y)Definitions: BetaAt(x1,x2,n,y)Original native command in the exact edition
  2. L41
    specialize hfirst_witness_witness_right n
  3. L42
    specialize hfirst_witness_witness_right y
  4. L43
    apply hfirst_witness_witness_right
  5. L44
    exact hnsn
  6. L45
    exact hni
  7. L46
    exact hyn
09Establish hsecondL47–54

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

  1. L47
    have hsecond : ∃ z. ∃ d. BetaAt(z,d,n,x) ∧ (∀ y. ∀ m. Lt(y,S n) → ¬y = n → BetaAt(x1,x2,y,m) → BetaAt(z,d,y,m))Definitions: BetaAt(z,d,n,x)Lt(y,S n)BetaAt(x1,x2,y,m)BetaAt(z,d,y,m)Original native command in the exact edition
  2. L48
    specialize beta_prefix_replace_exists x1
  3. L49
    specialize beta_prefix_replace_exists x2
  4. L50
    specialize beta_prefix_replace_exists n
  5. L51
    specialize beta_prefix_replace_exists x
  6. L52
    specialize beta_prefix_replace_exists (S n)
  7. L53
    apply beta_prefix_replace_exists
  8. L54
    exact hnsn
10Separate the logical casesL55–57

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

  1. L55
    cases hsecond
  2. L56
    cases hsecond_witness
  3. L57
    cases hsecond_witness_witness
11Construct an explicit witnessL58–59

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

  1. L58
    exists x3
  2. L59
    exists x4
12Separate the logical casesL60–60

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

  1. L60
    split
13Use earlier factsL61–66

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

  1. L61
    specialize hsecond_witness_witness_right i
  2. L62
    specialize hsecond_witness_witness_right y
  3. L63
    apply hsecond_witness_witness_right
  4. L64
    exact hisn
  5. L65
    exact hin
  6. L66
    exact hfirst_witness_witness_left
14Separate the logical casesL67–67

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

  1. L67
    split
15Use earlier factsL68–68

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

  1. L68
    exact hsecond_witness_witness_left
16Fix variables and assumptionsL69–74

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

  1. L69
    intro j
  2. L70
    intro a
  3. L71
    intro hj
  4. L72
    intro hji
  5. L73
    intro hjn
  6. L74
    intro hold
17Establish hmiddleL75–84

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

  1. L75
    have hmiddle : BetaAt(x1,x2,j,a)Definitions: BetaAt(x1,x2,j,a)Original native command in the exact edition
  2. L76
    specialize hfirst_witness_witness_right j
  3. L77
    specialize hfirst_witness_witness_right a
  4. L78
    apply hfirst_witness_witness_right
  5. L79
    exact hj
  6. L80
    exact hji
  7. L81
    exact hold
  8. L82
    specialize hsecond_witness_witness_right j
  9. L83
    specialize hsecond_witness_witness_right a
  10. L84
    apply hsecond_witness_witness_right
18Use earlier factsL85–87

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

  1. L85
    exact hj
  2. L86
    exact hjn
  3. L87
    exact hmiddle

Library-wide reading audit

Original defined command ledger · 87 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro i
  5. 0005intro x
  6. 0006intro y
  7. 0007intro hi
  8. 0008intro hxi
  9. 0009intro hyn
  10. 0010have hisn : Lt(i,S n)
    Exact native replay linehave hisn : exists h. h + S i = S n
  11. 0011specialize le_succ (S i)
  12. 0012specialize le_succ n
  13. 0013apply le_succ
  14. 0014exact hi
  15. 0015have hnsn : Lt(n,S n)
    Exact native replay linehave hnsn : exists h. h + S n = S n
  16. 0016specialize le_refl (S n)
  17. 0017exact le_refl
  18. 0018have hin : ~(i = n)
  19. 0019intro hin_eq
  20. 0020specialize lt_irrefl_expanded n
  21. 0021apply lt_irrefl_expanded
  22. 0022rewrite hin_eq at hi
  23. 0023exact hi
  24. 0024have hni : ~(n = i)
  25. 0025intro hni_eq
  26. 0026apply hin
  27. 0027symm
  28. 0028exact hni_eq
  29. 0029have hfirst : ∃ z. ∃ d. BetaAt(z,d,i,y) ∧ (∀ x. ∀ m. Lt(x,S n) → ¬x = i → BetaAt(b,c,x,m) → BetaAt(z,d,x,m))
    Exact native replay linehave hfirst : exists z d. (((exists h. h + S y = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + y) /\ forall j a. (exists h. h + S j = S n) -> ~(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))
  30. 0030specialize beta_prefix_replace_exists b
  31. 0031specialize beta_prefix_replace_exists c
  32. 0032specialize beta_prefix_replace_exists i
  33. 0033specialize beta_prefix_replace_exists y
  34. 0034specialize beta_prefix_replace_exists (S n)
  35. 0035apply beta_prefix_replace_exists
  36. 0036exact hisn
  37. 0037cases hfirst
  38. 0038cases hfirst_witness
  39. 0039cases hfirst_witness_witness
  40. 0040have hfirst_n : BetaAt(x1,x2,n,y)
    Exact native replay linehave hfirst_n : ((exists h. h + S y = S ((S n) * x2)) /\ exists q. x1 = q * S ((S n) * x2) + y)
  41. 0041specialize hfirst_witness_witness_right n
  42. 0042specialize hfirst_witness_witness_right y
  43. 0043apply hfirst_witness_witness_right
  44. 0044exact hnsn
  45. 0045exact hni
  46. 0046exact hyn
  47. 0047have hsecond : ∃ z. ∃ d. BetaAt(z,d,n,x) ∧ (∀ y. ∀ m. Lt(y,S n) → ¬y = n → BetaAt(x1,x2,y,m) → BetaAt(z,d,y,m))
    Exact native replay linehave hsecond : exists z d. (((exists h. h + S x = S ((S n) * d)) /\ exists q. z = q * S ((S n) * d) + x) /\ forall j a. (exists h. h + S j = S n) -> ~(j = n) -> ((exists h. h + S a = S ((S j) * x2)) /\ exists q. x1 = q * S ((S j) * x2) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + a))
  48. 0048specialize beta_prefix_replace_exists x1
  49. 0049specialize beta_prefix_replace_exists x2
  50. 0050specialize beta_prefix_replace_exists n
  51. 0051specialize beta_prefix_replace_exists x
  52. 0052specialize beta_prefix_replace_exists (S n)
  53. 0053apply beta_prefix_replace_exists
  54. 0054exact hnsn
  55. 0055cases hsecond
  56. 0056cases hsecond_witness
  57. 0057cases hsecond_witness_witness
  58. 0058exists x3
  59. 0059exists x4
  60. 0060split
  61. 0061specialize hsecond_witness_witness_right i
  62. 0062specialize hsecond_witness_witness_right y
  63. 0063apply hsecond_witness_witness_right
  64. 0064exact hisn
  65. 0065exact hin
  66. 0066exact hfirst_witness_witness_left
  67. 0067split
  68. 0068exact hsecond_witness_witness_left
  69. 0069intro j
  70. 0070intro a
  71. 0071intro hj
  72. 0072intro hji
  73. 0073intro hjn
  74. 0074intro hold
  75. 0075have hmiddle : BetaAt(x1,x2,j,a)
    Exact native replay linehave hmiddle : ((exists h. h + S a = S ((S j) * x2)) /\ exists q. x1 = q * S ((S j) * x2) + a)
  76. 0076specialize hfirst_witness_witness_right j
  77. 0077specialize hfirst_witness_witness_right a
  78. 0078apply hfirst_witness_witness_right
  79. 0079exact hj
  80. 0080exact hji
  81. 0081exact hold
  82. 0082specialize hsecond_witness_witness_right j
  83. 0083specialize hsecond_witness_witness_right a
  84. 0084apply hsecond_witness_witness_right
  85. 0085exact hj
  86. 0086exact hjn
  87. 0087exact hmiddle