PA004M · theorem

finite_swap_last_bounded

Stable checked-use theorem · independently closed

A swap-last recoding preserves boundedness of the full successor prefix.

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. ∀ sn. ∀ i. ∀ x. ∀ y. sn = S n → Lt(i,n) → BoundedPrefix(b,c,sn) → BetaAt(b,c,i,x) → BetaAt(b,c,n,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)) → BoundedPrefix(z,d,sn)

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 PD0024 BoundedPrefix

10 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0024 BoundedPrefix

14 occurrences

Exact expanded native-PA statement
forall b c z d n sn i x y. sn = S n -> (exists h. h + S i = n) -> (forall fp_i_swap_bound_old. (exists fp_gap_swap_bound_old_index. fp_gap_swap_bound_old_index + S fp_i_swap_bound_old = sn) -> exists fp_value_swap_bound_old. ((((exists ff_h_swap_bound_old_entry. ff_h_swap_bound_old_entry + S (fp_value_swap_bound_old) = S ((S (fp_i_swap_bound_old)) * c)) /\ exists ff_q_swap_bound_old_entry. b = ff_q_swap_bound_old_entry * S ((S (fp_i_swap_bound_old)) * c) + (fp_value_swap_bound_old))) /\ (exists fp_gap_swap_bound_old_value. fp_gap_swap_bound_old_value + S fp_value_swap_bound_old = sn))) -> (((exists ff_h_swap_bound_old_i. ff_h_swap_bound_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_swap_bound_old_i. b = ff_q_swap_bound_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_swap_bound_old_n. ff_h_swap_bound_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_swap_bound_old_n. b = ff_q_swap_bound_old_n * S ((S (n)) * c) + (y))) -> (((exists ff_h_swap_bound_new_i. ff_h_swap_bound_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_swap_bound_new_i. z = ff_q_swap_bound_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_swap_bound_new_n. ff_h_swap_bound_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_swap_bound_new_n. z = ff_q_swap_bound_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_bound_old_j. ff_h_swap_bound_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_swap_bound_old_j. b = ff_q_swap_bound_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_swap_bound_new_j. ff_h_swap_bound_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_swap_bound_new_j. z = ff_q_swap_bound_new_j * S ((S (j)) * d) + (a)))) -> (forall fp_i_swap_bound_new. (exists fp_gap_swap_bound_new_index. fp_gap_swap_bound_new_index + S fp_i_swap_bound_new = sn) -> exists fp_value_swap_bound_new. ((((exists ff_h_swap_bound_new_entry. ff_h_swap_bound_new_entry + S (fp_value_swap_bound_new) = S ((S (fp_i_swap_bound_new)) * d)) /\ exists ff_q_swap_bound_new_entry. z = ff_q_swap_bound_new_entry * S ((S (fp_i_swap_bound_new)) * d) + (fp_value_swap_bound_new))) /\ (exists fp_gap_swap_bound_new_value. fp_gap_swap_bound_new_value + S fp_value_swap_bound_new = sn)))

Proof neighborhood

Direct theorem prerequisites

PA004L finite_bounded_entry_lt PA004G eq_decidable PA002O le_succ PA001A le_refl

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

93 script commands · 26 reading checkpoints · 9 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)
finite bounded entry lteq decidablele succle refl
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 sn
  7. L7
    intro i
  8. L8
    intro x
  9. L9
    intro y
  10. L10
    intro hsn
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hi
  2. L12
    intro hbounded
  3. L13
    intro hold_i
  4. L14
    intro hold_n
  5. L15
    intro hnew_i
  6. L16
    intro hnew_n
  7. L17
    intro hpreserve
03Calculate and transport equalitiesL18–19

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

  1. L18
    rewrite hsn at hbounded
  2. L19
    rewrite hsn at hbounded
04Establish hisnL20–24

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

  1. L20
  2. L21
    specialize le_succ (S i)
  3. L22
    specialize le_succ n
  4. L23
    apply le_succ
  5. L24
    exact hi
05Establish hnsnL25–27

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

  1. L25
  2. L26
    specialize le_refl (S n)
  3. L27
    exact le_refl
06Establish hentry_bound_iL28–29

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

  1. L28
    have hentry_bound_i : ∀ b. ∀ c. ∀ l. ∀ i. ∀ x. BoundedPrefix(b,c,l) → Lt(i,l) → BetaAt(b,c,i,x) → Lt(x,l)Definitions: BoundedPrefix(b,c,l)Lt(i,l)BetaAt(b,c,i,x)Lt(x,l)Original native command in the exact edition
  2. L29
    exact finite_bounded_entry_lt
07Establish hentry_bound_nL30–31

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

  1. L30
    have hentry_bound_n : ∀ b. ∀ c. ∀ l. ∀ i. ∀ x. BoundedPrefix(b,c,l) → Lt(i,l) → BetaAt(b,c,i,x) → Lt(x,l)Definitions: BoundedPrefix(b,c,l)Lt(i,l)BetaAt(b,c,i,x)Lt(x,l)Original native command in the exact edition
  2. L31
    exact finite_bounded_entry_lt
08Establish hxbL32–41

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

  1. L32
  2. L33
    specialize hentry_bound_i b
  3. L34
    specialize hentry_bound_i c
  4. L35
    specialize hentry_bound_i (S n)
  5. L36
    specialize hentry_bound_i i
  6. L37
    specialize hentry_bound_i x
  7. L38
    apply hentry_bound_i
  8. L39
    exact hbounded
  9. L40
    exact hisn
  10. L41
    exact hold_i
09Establish hybL42–51

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

  1. L42
  2. L43
    specialize hentry_bound_n b
  3. L44
    specialize hentry_bound_n c
  4. L45
    specialize hentry_bound_n (S n)
  5. L46
    specialize hentry_bound_n n
  6. L47
    specialize hentry_bound_n y
  7. L48
    apply hentry_bound_n
  8. L49
    exact hbounded
  9. L50
    exact hnsn
  10. L51
    exact hold_n
10Establish heq_iL52–53

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

  1. L52
    have heq_i : forall u v. u = v \/ ~(u = v)
  2. L53
    exact eq_decidable
11Establish heq_nL54–61

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

  1. L54
    have heq_n : forall u v. u = v \/ ~(u = v)
  2. L55
    exact eq_decidable
  3. L56
    rewrite hsn
  4. L57
    rewrite hsn
  5. L58
    intro j
  6. L59
    intro hj
  7. L60
    specialize heq_i j
  8. L61
    specialize heq_i i
12Separate the logical casesL62–62

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

  1. L62
    cases heq_i
13Construct an explicit witnessL63–63

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

  1. L63
    exists y
14Separate the logical casesL64–64

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

  1. L64
    split
15Calculate and transport equalitiesL65–66

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

  1. L65
    rewrite heq_i_left
  2. L66
    rewrite heq_i_left
16Use earlier factsL67–70

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

  1. L67
    exact hnew_i
  2. L68
    exact hyb
  3. L69
    specialize heq_n j
  4. L70
    specialize heq_n n
17Separate the logical casesL71–71

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

  1. L71
    cases heq_n
18Construct an explicit witnessL72–72

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

  1. L72
    exists x
19Separate the logical casesL73–73

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

  1. L73
    split
20Calculate and transport equalitiesL74–75

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

  1. L74
    rewrite heq_n_left
  2. L75
    rewrite heq_n_left
21Use earlier factsL76–78

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

  1. L76
    exact hnew_n
  2. L77
    exact hxb
  3. L78
    specialize hbounded j
22Establish holdL79–81

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

  1. L79
    have hold : ∃ a. BetaAt(b,c,j,a) ∧ Lt(a,S n)Definitions: BetaAt(b,c,j,a)Lt(a,S n)Original native command in the exact edition
  2. L80
    apply hbounded
  3. L81
    exact hj
23Separate the logical casesL82–83

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

  1. L82
    cases hold
  2. L83
    cases hold_witness
24Construct an explicit witnessL84–84

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

  1. L84
    exists x1
25Separate the logical casesL85–85

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

  1. L85
    split
26Use earlier factsL86–93

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

  1. L86
    specialize hpreserve j
  2. L87
    specialize hpreserve x1
  3. L88
    apply hpreserve
  4. L89
    exact hj
  5. L90
    exact heq_i_right
  6. L91
    exact heq_n_right
  7. L92
    exact hold_witness_left
  8. L93
    exact hold_witness_right

Library-wide reading audit

Original defined command ledger · 93 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro n
  6. 0006intro sn
  7. 0007intro i
  8. 0008intro x
  9. 0009intro y
  10. 0010intro hsn
  11. 0011intro hi
  12. 0012intro hbounded
  13. 0013intro hold_i
  14. 0014intro hold_n
  15. 0015intro hnew_i
  16. 0016intro hnew_n
  17. 0017intro hpreserve
  18. 0018rewrite hsn at hbounded
  19. 0019rewrite hsn at hbounded
  20. 0020have hisn : Lt(i,S n)
    Exact native replay linehave hisn : exists h. h + S i = S n
  21. 0021specialize le_succ (S i)
  22. 0022specialize le_succ n
  23. 0023apply le_succ
  24. 0024exact hi
  25. 0025have hnsn : Lt(n,S n)
    Exact native replay linehave hnsn : exists h. h + S n = S n
  26. 0026specialize le_refl (S n)
  27. 0027exact le_refl
  28. 0028have hentry_bound_i : ∀ b. ∀ c. ∀ l. ∀ i. ∀ x. BoundedPrefix(b,c,l) → Lt(i,l) → BetaAt(b,c,i,x) → Lt(x,l)
    Exact native replay linehave hentry_bound_i : forall b c l i x. (forall fp_i_entry_bound. (exists fp_gap_entry_bound_index. fp_gap_entry_bound_index + S fp_i_entry_bound = l) -> exists fp_value_entry_bound. ((((exists ff_h_entry_bound_entry. ff_h_entry_bound_entry + S (fp_value_entry_bound) = S ((S (fp_i_entry_bound)) * c)) /\ exists ff_q_entry_bound_entry. b = ff_q_entry_bound_entry * S ((S (fp_i_entry_bound)) * c) + (fp_value_entry_bound))) /\ (exists fp_gap_entry_bound_value. fp_gap_entry_bound_value + S fp_value_entry_bound = l))) -> (exists h. h + S i = l) -> (((exists ff_h_entry_bound_at. ff_h_entry_bound_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_entry_bound_at. b = ff_q_entry_bound_at * S ((S (i)) * c) + (x))) -> exists h. h + S x = l
  29. 0029exact finite_bounded_entry_lt
  30. 0030have hentry_bound_n : ∀ b. ∀ c. ∀ l. ∀ i. ∀ x. BoundedPrefix(b,c,l) → Lt(i,l) → BetaAt(b,c,i,x) → Lt(x,l)
    Exact native replay linehave hentry_bound_n : forall b c l i x. (forall fp_i_entry_bound. (exists fp_gap_entry_bound_index. fp_gap_entry_bound_index + S fp_i_entry_bound = l) -> exists fp_value_entry_bound. ((((exists ff_h_entry_bound_entry. ff_h_entry_bound_entry + S (fp_value_entry_bound) = S ((S (fp_i_entry_bound)) * c)) /\ exists ff_q_entry_bound_entry. b = ff_q_entry_bound_entry * S ((S (fp_i_entry_bound)) * c) + (fp_value_entry_bound))) /\ (exists fp_gap_entry_bound_value. fp_gap_entry_bound_value + S fp_value_entry_bound = l))) -> (exists h. h + S i = l) -> (((exists ff_h_entry_bound_at. ff_h_entry_bound_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_entry_bound_at. b = ff_q_entry_bound_at * S ((S (i)) * c) + (x))) -> exists h. h + S x = l
  31. 0031exact finite_bounded_entry_lt
  32. 0032have hxb : Lt(x,S n)
    Exact native replay linehave hxb : exists h. h + S x = S n
  33. 0033specialize hentry_bound_i b
  34. 0034specialize hentry_bound_i c
  35. 0035specialize hentry_bound_i (S n)
  36. 0036specialize hentry_bound_i i
  37. 0037specialize hentry_bound_i x
  38. 0038apply hentry_bound_i
  39. 0039exact hbounded
  40. 0040exact hisn
  41. 0041exact hold_i
  42. 0042have hyb : Lt(y,S n)
    Exact native replay linehave hyb : exists h. h + S y = S n
  43. 0043specialize hentry_bound_n b
  44. 0044specialize hentry_bound_n c
  45. 0045specialize hentry_bound_n (S n)
  46. 0046specialize hentry_bound_n n
  47. 0047specialize hentry_bound_n y
  48. 0048apply hentry_bound_n
  49. 0049exact hbounded
  50. 0050exact hnsn
  51. 0051exact hold_n
  52. 0052have heq_i : forall u v. u = v \/ ~(u = v)
  53. 0053exact eq_decidable
  54. 0054have heq_n : forall u v. u = v \/ ~(u = v)
  55. 0055exact eq_decidable
  56. 0056rewrite hsn
  57. 0057rewrite hsn
  58. 0058intro j
  59. 0059intro hj
  60. 0060specialize heq_i j
  61. 0061specialize heq_i i
  62. 0062cases heq_i
  63. 0063exists y
  64. 0064split
  65. 0065rewrite heq_i_left
  66. 0066rewrite heq_i_left
  67. 0067exact hnew_i
  68. 0068exact hyb
  69. 0069specialize heq_n j
  70. 0070specialize heq_n n
  71. 0071cases heq_n
  72. 0072exists x
  73. 0073split
  74. 0074rewrite heq_n_left
  75. 0075rewrite heq_n_left
  76. 0076exact hnew_n
  77. 0077exact hxb
  78. 0078specialize hbounded j
  79. 0079have hold : ∃ a. BetaAt(b,c,j,a) ∧ Lt(a,S n)
    Exact native replay linehave hold : exists a. (((exists h. h + S a = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + a) /\ exists h. h + S a = S n)
  80. 0080apply hbounded
  81. 0081exact hj
  82. 0082cases hold
  83. 0083cases hold_witness
  84. 0084exists x1
  85. 0085split
  86. 0086specialize hpreserve j
  87. 0087specialize hpreserve x1
  88. 0088apply hpreserve
  89. 0089exact hj
  90. 0090exact heq_i_right
  91. 0091exact heq_n_right
  92. 0092exact hold_witness_left
  93. 0093exact hold_witness_right