PA004N · theorem

beta_prefix_swap_last_reflect

Stable checked-use theorem · independently closed

Every decoded swapped entry reflects to one of the two moved entries or the original index.

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

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

PD0013 BetaAt

1 occurrences

Exact expanded native-PA statement
forall b c z d n i x y. (((exists ff_h_reflect_new_i. ff_h_reflect_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_reflect_new_i. z = ff_q_reflect_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_reflect_new_n. ff_h_reflect_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_reflect_new_n. z = ff_q_reflect_new_n * S ((S (n)) * d) + (x))) -> (forall k v. (exists h. h + S k = S n) -> ~(k = i) -> ~(k = n) -> (((exists ff_h_reflect_old_k. ff_h_reflect_old_k + S (v) = S ((S (k)) * c)) /\ exists ff_q_reflect_old_k. b = ff_q_reflect_old_k * S ((S (k)) * c) + (v))) -> (((exists ff_h_reflect_new_k. ff_h_reflect_new_k + S (v) = S ((S (k)) * d)) /\ exists ff_q_reflect_new_k. z = ff_q_reflect_new_k * S ((S (k)) * d) + (v)))) -> forall j a. (exists h. h + S j = S n) -> (((exists ff_h_reflect_new_j. ff_h_reflect_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_reflect_new_j. z = ff_q_reflect_new_j * S ((S (j)) * d) + (a))) -> ((j = i /\ a = y) \/ ((j = n /\ a = x) \/ (~(j = i) /\ (~(j = n) /\ (((exists ff_h_reflect_old_j. ff_h_reflect_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_reflect_old_j. b = ff_q_reflect_old_j * S ((S (j)) * c) + (a)))))))

Proof neighborhood

Direct theorem prerequisites

PA004G eq_decidable PA0029 beta_at_exists PA002F beta_at_unique

Direct theorem dependents

PA004O finite_swap_last_injective PA004U finite_swap_last_surjective_back PA0054 beta_reindex_alignment_swap_last

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

77 script commands · 20 reading checkpoints · 2 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)
eq decidablebeta at existsbeta at unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro z
  4. L4
    intro d
  5. L5
    intro n
  6. L6
    intro i
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro hnew_i
  10. L10
    intro hnew_n
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hpreserve
  2. L12
    intro j
  3. L13
    intro a
  4. L14
    intro hj
  5. L15
    intro hnew
03Use earlier factsL16–17

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

  1. L16
    specialize eq_decidable j
  2. L17
    specialize eq_decidable i
04Separate the logical casesL18–20

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

  1. L18
    cases eq_decidable
  2. L19
    left
  3. L20
    split
05Use earlier factsL21–27

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

  1. L21
    exact eq_decidable_left
  2. L22
    specialize beta_at_unique z
  3. L23
    specialize beta_at_unique d
  4. L24
    specialize beta_at_unique i
  5. L25
    specialize beta_at_unique a
  6. L26
    specialize beta_at_unique y
  7. L27
    apply beta_at_unique
06Calculate and transport equalitiesL28–29

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

  1. L28
    rewrite eq_decidable_left at hnew
  2. L29
    rewrite eq_decidable_left at hnew
07Use earlier factsL30–32

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

  1. L30
    exact hnew
  2. L31
    exact hnew_i
  3. L32
    specialize eq_decidable_before2 n
08Separate the logical casesL33–36

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

  1. L33
    cases eq_decidable_before2
  2. L34
    right
  3. L35
    left
  4. L36
    split
09Use earlier factsL37–43

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

  1. L37
    exact eq_decidable_before2_left
  2. L38
    specialize beta_at_unique z
  3. L39
    specialize beta_at_unique d
  4. L40
    specialize beta_at_unique n
  5. L41
    specialize beta_at_unique a
  6. L42
    specialize beta_at_unique x
  7. L43
    apply beta_at_unique
10Calculate and transport equalitiesL44–45

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

  1. L44
    rewrite eq_decidable_before2_left at hnew
  2. L45
    rewrite eq_decidable_before2_left at hnew
11Use earlier factsL46–50

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

  1. L46
    exact hnew
  2. L47
    exact hnew_n
  3. L48
    specialize beta_at_exists b
  4. L49
    specialize beta_at_exists c
  5. L50
    specialize beta_at_exists j
12Separate the logical casesL51–51

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

  1. L51
    cases beta_at_exists
13Establish htransportL52–59

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

  1. L52
    have htransport : BetaAt(z,d,j,x1)Definitions: BetaAt(z,d,j,x1)Original native command in the exact edition
  2. L53
    specialize hpreserve j
  3. L54
    specialize hpreserve x1
  4. L55
    apply hpreserve
  5. L56
    exact hj
  6. L57
    exact eq_decidable_right
  7. L58
    exact eq_decidable_before2_right
  8. L59
    exact beta_at_exists_witness
14Establish havL60–68

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

  1. L60
    have hav : a = x1
  2. L61
    specialize beta_at_unique z
  3. L62
    specialize beta_at_unique d
  4. L63
    specialize beta_at_unique j
  5. L64
    specialize beta_at_unique a
  6. L65
    specialize beta_at_unique x1
  7. L66
    apply beta_at_unique
  8. L67
    exact hnew
  9. L68
    exact htransport
15Separate the logical casesL69–71

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

  1. L69
    right
  2. L70
    right
  3. L71
    split
16Use earlier factsL72–72

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

  1. L72
    exact eq_decidable_right
17Separate the logical casesL73–73

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

  1. L73
    split
18Use earlier factsL74–74

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

  1. L74
    exact eq_decidable_before2_right
19Calculate and transport equalitiesL75–76

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

  1. L75
    rewrite hav
  2. L76
    rewrite hav
20Use earlier factsL77–77

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

  1. L77
    exact beta_at_exists_witness

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro n
  6. 0006intro i
  7. 0007intro x
  8. 0008intro y
  9. 0009intro hnew_i
  10. 0010intro hnew_n
  11. 0011intro hpreserve
  12. 0012intro j
  13. 0013intro a
  14. 0014intro hj
  15. 0015intro hnew
  16. 0016specialize eq_decidable j
  17. 0017specialize eq_decidable i
  18. 0018cases eq_decidable
  19. 0019left
  20. 0020split
  21. 0021exact eq_decidable_left
  22. 0022specialize beta_at_unique z
  23. 0023specialize beta_at_unique d
  24. 0024specialize beta_at_unique i
  25. 0025specialize beta_at_unique a
  26. 0026specialize beta_at_unique y
  27. 0027apply beta_at_unique
  28. 0028rewrite eq_decidable_left at hnew
  29. 0029rewrite eq_decidable_left at hnew
  30. 0030exact hnew
  31. 0031exact hnew_i
  32. 0032specialize eq_decidable_before2 n
  33. 0033cases eq_decidable_before2
  34. 0034right
  35. 0035left
  36. 0036split
  37. 0037exact eq_decidable_before2_left
  38. 0038specialize beta_at_unique z
  39. 0039specialize beta_at_unique d
  40. 0040specialize beta_at_unique n
  41. 0041specialize beta_at_unique a
  42. 0042specialize beta_at_unique x
  43. 0043apply beta_at_unique
  44. 0044rewrite eq_decidable_before2_left at hnew
  45. 0045rewrite eq_decidable_before2_left at hnew
  46. 0046exact hnew
  47. 0047exact hnew_n
  48. 0048specialize beta_at_exists b
  49. 0049specialize beta_at_exists c
  50. 0050specialize beta_at_exists j
  51. 0051cases beta_at_exists
  52. 0052have htransport : BetaAt(z,d,j,x1)
    Exact native replay linehave htransport : ((exists h. h + S x1 = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + x1)
  53. 0053specialize hpreserve j
  54. 0054specialize hpreserve x1
  55. 0055apply hpreserve
  56. 0056exact hj
  57. 0057exact eq_decidable_right
  58. 0058exact eq_decidable_before2_right
  59. 0059exact beta_at_exists_witness
  60. 0060have hav : a = x1
  61. 0061specialize beta_at_unique z
  62. 0062specialize beta_at_unique d
  63. 0063specialize beta_at_unique j
  64. 0064specialize beta_at_unique a
  65. 0065specialize beta_at_unique x1
  66. 0066apply beta_at_unique
  67. 0067exact hnew
  68. 0068exact htransport
  69. 0069right
  70. 0070right
  71. 0071split
  72. 0072exact eq_decidable_right
  73. 0073split
  74. 0074exact eq_decidable_before2_right
  75. 0075rewrite hav
  76. 0076rewrite hav
  77. 0077exact beta_at_exists_witness