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.
Exact expanded 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)))))))Structural proof guide
Generated structural guide
Every decoded swapped entry reflects to one of the two moved entries or the original index.
Use the direct prerequisites eq_decidable, beta_at_exists, beta_at_unique as previously established PA formulas.
The proof proceeds by case analysis (3), intermediate claims (2), equality transport (6).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
Read the argument
Proof checkpoints
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.
Named ingredients (3)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–15
03Use earlier factsL16–17
04Separate the logical casesL18–20
05Use earlier factsL21–27
06Calculate and transport equalitiesL28–29
07Use earlier factsL30–32
08Separate the logical casesL33–36
09Use earlier factsL37–43
10Calculate and transport equalitiesL44–45
11Use earlier factsL46–50
12Separate the logical casesL51–51
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- 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.
14Establish havL60–68
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
15Separate the logical casesL69–71
16Use earlier factsL72–72
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L72
exact eq_decidable_right
17Separate the logical casesL73–73
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L73
split
18Use earlier factsL74–74
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L74
exact eq_decidable_before2_right
19Calculate and transport equalitiesL75–76
20Use earlier factsL77–77
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L77
exact beta_at_exists_witness
Original exact command ledger · 77 lines
- 0001
intro b - 0002
intro c - 0003
intro z - 0004
intro d - 0005
intro n - 0006
intro i - 0007
intro x - 0008
intro y - 0009
intro hnew_i - 0010
intro hnew_n - 0011
intro hpreserve - 0012
intro j - 0013
intro a - 0014
intro hj - 0015
intro hnew - 0016
specialize eq_decidable j - 0017
specialize eq_decidable i - 0018
cases eq_decidable - 0019
left - 0020
split - 0021
exact eq_decidable_left - 0022
specialize beta_at_unique z - 0023
specialize beta_at_unique d - 0024
specialize beta_at_unique i - 0025
specialize beta_at_unique a - 0026
specialize beta_at_unique y - 0027
apply beta_at_unique - 0028
rewrite eq_decidable_left at hnew - 0029
rewrite eq_decidable_left at hnew - 0030
exact hnew - 0031
exact hnew_i - 0032
specialize eq_decidable_before2 n - 0033
cases eq_decidable_before2 - 0034
right - 0035
left - 0036
split - 0037
exact eq_decidable_before2_left - 0038
specialize beta_at_unique z - 0039
specialize beta_at_unique d - 0040
specialize beta_at_unique n - 0041
specialize beta_at_unique a - 0042
specialize beta_at_unique x - 0043
apply beta_at_unique - 0044
rewrite eq_decidable_before2_left at hnew - 0045
rewrite eq_decidable_before2_left at hnew - 0046
exact hnew - 0047
exact hnew_n - 0048
specialize beta_at_exists b - 0049
specialize beta_at_exists c - 0050
specialize beta_at_exists j - 0051
cases beta_at_exists - 0052
have htransport : ((exists h. h + S x1 = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + x1) - 0053
specialize hpreserve j - 0054
specialize hpreserve x1 - 0055
apply hpreserve - 0056
exact hj - 0057
exact eq_decidable_right - 0058
exact eq_decidable_before2_right - 0059
exact beta_at_exists_witness - 0060
have hav : a = x1 - 0061
specialize beta_at_unique z - 0062
specialize beta_at_unique d - 0063
specialize beta_at_unique j - 0064
specialize beta_at_unique a - 0065
specialize beta_at_unique x1 - 0066
apply beta_at_unique - 0067
exact hnew - 0068
exact htransport - 0069
right - 0070
right - 0071
split - 0072
exact eq_decidable_right - 0073
split - 0074
exact eq_decidable_before2_right - 0075
rewrite hav - 0076
rewrite hav - 0077
exact beta_at_exists_witness