PA004O · theorem

finite_swap_last_injective

Stable checked-use theorem · independently closed

A swap-last recoding preserves injectivity 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) → InjectivePrefix(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)) → InjectivePrefix(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 PD0025 InjectivePrefix

10 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

26 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_inj_old fp_j_swap_inj_old fp_value_swap_inj_old. (exists fp_gap_swap_inj_old_i. fp_gap_swap_inj_old_i + S fp_i_swap_inj_old = sn) -> (exists fp_gap_swap_inj_old_j. fp_gap_swap_inj_old_j + S fp_j_swap_inj_old = sn) -> (((exists ff_h_swap_inj_old_left. ff_h_swap_inj_old_left + S (fp_value_swap_inj_old) = S ((S (fp_i_swap_inj_old)) * c)) /\ exists ff_q_swap_inj_old_left. b = ff_q_swap_inj_old_left * S ((S (fp_i_swap_inj_old)) * c) + (fp_value_swap_inj_old))) -> (((exists ff_h_swap_inj_old_right. ff_h_swap_inj_old_right + S (fp_value_swap_inj_old) = S ((S (fp_j_swap_inj_old)) * c)) /\ exists ff_q_swap_inj_old_right. b = ff_q_swap_inj_old_right * S ((S (fp_j_swap_inj_old)) * c) + (fp_value_swap_inj_old))) -> fp_i_swap_inj_old = fp_j_swap_inj_old) -> (((exists ff_h_swap_inj_old_i. ff_h_swap_inj_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_swap_inj_old_i. b = ff_q_swap_inj_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_swap_inj_old_n. ff_h_swap_inj_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_swap_inj_old_n. b = ff_q_swap_inj_old_n * S ((S (n)) * c) + (y))) -> (((exists ff_h_swap_inj_new_i. ff_h_swap_inj_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_swap_inj_new_i. z = ff_q_swap_inj_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_swap_inj_new_n. ff_h_swap_inj_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_swap_inj_new_n. z = ff_q_swap_inj_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_inj_old_j. ff_h_swap_inj_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_swap_inj_old_j. b = ff_q_swap_inj_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_swap_inj_new_j. ff_h_swap_inj_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_swap_inj_new_j. z = ff_q_swap_inj_new_j * S ((S (j)) * d) + (a)))) -> (forall fp_i_swap_inj_new fp_j_swap_inj_new fp_value_swap_inj_new. (exists fp_gap_swap_inj_new_i. fp_gap_swap_inj_new_i + S fp_i_swap_inj_new = sn) -> (exists fp_gap_swap_inj_new_j. fp_gap_swap_inj_new_j + S fp_j_swap_inj_new = sn) -> (((exists ff_h_swap_inj_new_left. ff_h_swap_inj_new_left + S (fp_value_swap_inj_new) = S ((S (fp_i_swap_inj_new)) * d)) /\ exists ff_q_swap_inj_new_left. z = ff_q_swap_inj_new_left * S ((S (fp_i_swap_inj_new)) * d) + (fp_value_swap_inj_new))) -> (((exists ff_h_swap_inj_new_right. ff_h_swap_inj_new_right + S (fp_value_swap_inj_new) = S ((S (fp_j_swap_inj_new)) * d)) /\ exists ff_q_swap_inj_new_right. z = ff_q_swap_inj_new_right * S ((S (fp_j_swap_inj_new)) * d) + (fp_value_swap_inj_new))) -> fp_i_swap_inj_new = fp_j_swap_inj_new)

Proof neighborhood

Direct theorem prerequisites

PA004N beta_prefix_swap_last_reflect 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

220 script commands · 70 reading checkpoints · 16 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)
beta prefix swap last reflectle 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 hinjective
  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 hinjective
  2. L19
    rewrite hsn at hinjective
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 hreflect_jL28–29

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

  1. L28
    have hreflect_j : ∀ 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)))Definitions: BetaAt(z,d,i,y)BetaAt(z,d,n,x)Lt(m,S n)BetaAt(b,c,m,k)BetaAt(z,d,m,k)Original native command in the exact edition
  2. L29
    exact beta_prefix_swap_last_reflect
07Establish hreflect_kL30–39

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

  1. L30
    have hreflect_k : ∀ 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)))Definitions: BetaAt(z,d,i,y)BetaAt(z,d,n,x)Lt(m,S n)BetaAt(b,c,m,k)BetaAt(z,d,m,k)Original native command in the exact edition
  2. L31
    exact beta_prefix_swap_last_reflect
  3. L32
    rewrite hsn
  4. L33
    rewrite hsn
  5. L34
    intro j
  6. L35
    intro k
  7. L36
    intro a
  8. L37
    intro hj
  9. L38
    intro hk
  10. L39
    intro hnew_j
08Fix variables and assumptionsL40–40

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

  1. L40
    intro hnew_k
09Use earlier factsL41–48

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

  1. L41
    specialize hreflect_j b
  2. L42
    specialize hreflect_j c
  3. L43
    specialize hreflect_j z
  4. L44
    specialize hreflect_j d
  5. L45
    specialize hreflect_j n
  6. L46
    specialize hreflect_j i
  7. L47
    specialize hreflect_j x
  8. L48
    specialize hreflect_j y
10Establish hreflect_entries_jL49–55

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

  1. L49
    have hreflect_entries_j : ∀ j. ∀ a. Lt(j,S n) → BetaAt(z,d,j,a) → j = i ∧ a = y ∨ (j = n ∧ a = x ∨ ¬j = i ∧ (¬j = n ∧ BetaAt(b,c,j,a)))Definitions: Lt(j,S n)BetaAt(z,d,j,a)BetaAt(b,c,j,a)Original native command in the exact edition
  2. L50
    apply hreflect_j
  3. L51
    exact hnew_i
  4. L52
    exact hnew_n
  5. L53
    exact hpreserve
  6. L54
    specialize hreflect_entries_j j
  7. L55
    specialize hreflect_entries_j a
11Establish hclass_jL56–65

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

  1. L56
    have hclass_j : j = i ∧ a = y ∨ (j = n ∧ a = x ∨ ¬j = i ∧ (¬j = n ∧ BetaAt(b,c,j,a)))Definitions: BetaAt(b,c,j,a)Original native command in the exact edition
  2. L57
    apply hreflect_entries_j
  3. L58
    exact hj
  4. L59
    exact hnew_j
  5. L60
    specialize hreflect_k b
  6. L61
    specialize hreflect_k c
  7. L62
    specialize hreflect_k z
  8. L63
    specialize hreflect_k d
  9. L64
    specialize hreflect_k n
  10. L65
    specialize hreflect_k i
12Use earlier factsL66–67

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

  1. L66
    specialize hreflect_k x
  2. L67
    specialize hreflect_k y
13Establish hreflect_entries_kL68–74

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

  1. L68
    have hreflect_entries_k : ∀ j. ∀ a. Lt(j,S n) → BetaAt(z,d,j,a) → j = i ∧ a = y ∨ (j = n ∧ a = x ∨ ¬j = i ∧ (¬j = n ∧ BetaAt(b,c,j,a)))Definitions: Lt(j,S n)BetaAt(z,d,j,a)BetaAt(b,c,j,a)Original native command in the exact edition
  2. L69
    apply hreflect_k
  3. L70
    exact hnew_i
  4. L71
    exact hnew_n
  5. L72
    exact hpreserve
  6. L73
    specialize hreflect_entries_k k
  7. L74
    specialize hreflect_entries_k a
14Establish hclass_kL75–78

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

  1. L75
    have hclass_k : k = i ∧ a = y ∨ (k = n ∧ a = x ∨ ¬k = i ∧ (¬k = n ∧ BetaAt(b,c,k,a)))Definitions: BetaAt(b,c,k,a)Original native command in the exact edition
  2. L76
    apply hreflect_entries_k
  3. L77
    exact hk
  4. L78
    exact hnew_k
15Separate the logical casesL79–82

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

  1. L79
    cases hclass_j
  2. L80
    cases hclass_j_left
  3. L81
    cases hclass_k
  4. L82
    cases hclass_k_left
16Calculate and transport equalitiesL83–83

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

  1. L83
    trans i
17Use earlier factsL84–84

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

  1. L84
    exact hclass_j_left_left
18Calculate and transport equalitiesL85–85

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

  1. L85
    symm
19Use earlier factsL86–86

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

  1. L86
    exact hclass_k_left_left
20Separate the logical casesL87–88

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

  1. L87
    cases hclass_k_right
  2. L88
    cases hclass_k_right_left
21Establish hxyL89–93

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

  1. L89
    have hxy : x = y
  2. L90
    trans a
  3. L91
    symm
  4. L92
    exact hclass_k_right_left_right
  5. L93
    exact hclass_j_left_right
22Establish hinL94–103

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

  1. L94
    have hin : i = n
  2. L95
    specialize hinjective i
  3. L96
    specialize hinjective n
  4. L97
    specialize hinjective x
  5. L98
    apply hinjective
  6. L99
    exact hisn
  7. L100
    exact hnsn
  8. L101
    exact hold_i
  9. L102
    rewrite hxy
  10. L103
    rewrite hxy
23Use earlier factsL104–104

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

  1. L104
    exact hold_n
24Calculate and transport equalitiesL105–105

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

  1. L105
    trans i
25Use earlier factsL106–106

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

  1. L106
    exact hclass_j_left_left
26Calculate and transport equalitiesL107–107

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

  1. L107
    trans n
27Use earlier factsL108–108

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

  1. L108
    exact hin
28Calculate and transport equalitiesL109–109

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

  1. L109
    symm
29Use earlier factsL110–110

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

  1. L110
    exact hclass_k_right_left_left
30Separate the logical casesL111–112

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

  1. L111
    cases hclass_k_right_right
  2. L112
    cases hclass_k_right_right_right
31Establish hnkL113–122

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

  1. L113
    have hnk : n = k
  2. L114
    specialize hinjective n
  3. L115
    specialize hinjective k
  4. L116
    specialize hinjective y
  5. L117
    apply hinjective
  6. L118
    exact hnsn
  7. L119
    exact hk
  8. L120
    exact hold_n
  9. L121
    rewrite <- hclass_j_left_right
  10. L122
    rewrite <- hclass_j_left_right
32Use earlier factsL123–123

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

  1. L123
    exact hclass_k_right_right_right_right
33Separate the logical casesL124–124

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

  1. L124
    exfalso
34Use earlier factsL125–125

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

  1. L125
    apply hclass_k_right_right_right_left
35Calculate and transport equalitiesL126–126

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

  1. L126
    symm
36Use earlier factsL127–127

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

  1. L127
    exact hnk
37Separate the logical casesL128–131

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

  1. L128
    cases hclass_j_right
  2. L129
    cases hclass_j_right_left
  3. L130
    cases hclass_k
  4. L131
    cases hclass_k_left
38Establish hxy2L132–136

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

  1. L132
    have hxy2 : x = y
  2. L133
    trans a
  3. L134
    symm
  4. L135
    exact hclass_j_right_left_right
  5. L136
    exact hclass_k_left_right
39Establish hin2L137–146

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

  1. L137
    have hin2 : n = i
  2. L138
    specialize hinjective n
  3. L139
    specialize hinjective i
  4. L140
    specialize hinjective y
  5. L141
    apply hinjective
  6. L142
    exact hnsn
  7. L143
    exact hisn
  8. L144
    exact hold_n
  9. L145
    rewrite <- hxy2
  10. L146
    rewrite <- hxy2
40Use earlier factsL147–147

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

  1. L147
    exact hold_i
41Calculate and transport equalitiesL148–148

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

  1. L148
    trans n
42Use earlier factsL149–149

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

  1. L149
    exact hclass_j_right_left_left
43Calculate and transport equalitiesL150–150

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

  1. L150
    trans i
44Use earlier factsL151–151

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

  1. L151
    exact hin2
45Calculate and transport equalitiesL152–152

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

  1. L152
    symm
46Use earlier factsL153–153

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

  1. L153
    exact hclass_k_left_left
47Separate the logical casesL154–155

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

  1. L154
    cases hclass_k_right
  2. L155
    cases hclass_k_right_left
48Calculate and transport equalitiesL156–156

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

  1. L156
    trans n
49Use earlier factsL157–157

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

  1. L157
    exact hclass_j_right_left_left
50Calculate and transport equalitiesL158–158

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

  1. L158
    symm
51Use earlier factsL159–159

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

  1. L159
    exact hclass_k_right_left_left
52Separate the logical casesL160–161

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

  1. L160
    cases hclass_k_right_right
  2. L161
    cases hclass_k_right_right_right
53Establish hikL162–171

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

  1. L162
    have hik : i = k
  2. L163
    specialize hinjective i
  3. L164
    specialize hinjective k
  4. L165
    specialize hinjective x
  5. L166
    apply hinjective
  6. L167
    exact hisn
  7. L168
    exact hk
  8. L169
    exact hold_i
  9. L170
    rewrite <- hclass_j_right_left_right
  10. L171
    rewrite <- hclass_j_right_left_right
54Use earlier factsL172–172

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

  1. L172
    exact hclass_k_right_right_right_right
55Separate the logical casesL173–173

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

  1. L173
    exfalso
56Use earlier factsL174–174

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

  1. L174
    apply hclass_k_right_right_left
57Calculate and transport equalitiesL175–175

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

  1. L175
    symm
58Use earlier factsL176–176

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

  1. L176
    exact hik
59Separate the logical casesL177–180

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

  1. L177
    cases hclass_j_right_right
  2. L178
    cases hclass_j_right_right_right
  3. L179
    cases hclass_k
  4. L180
    cases hclass_k_left
60Establish hjnL181–190

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

  1. L181
    have hjn : j = n
  2. L182
    specialize hinjective j
  3. L183
    specialize hinjective n
  4. L184
    specialize hinjective y
  5. L185
    apply hinjective
  6. L186
    exact hj
  7. L187
    exact hnsn
  8. L188
    rewrite <- hclass_k_left_right
  9. L189
    rewrite <- hclass_k_left_right
  10. L190
    exact hclass_j_right_right_right_right
61Use earlier factsL191–191

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

  1. L191
    exact hold_n
62Separate the logical casesL192–192

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

  1. L192
    exfalso
63Use earlier factsL193–194

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

  1. L193
    apply hclass_j_right_right_right_left
  2. L194
    exact hjn
64Separate the logical casesL195–196

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

  1. L195
    cases hclass_k_right
  2. L196
    cases hclass_k_right_left
65Establish hjiL197–206

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

  1. L197
    have hji : j = i
  2. L198
    specialize hinjective j
  3. L199
    specialize hinjective i
  4. L200
    specialize hinjective x
  5. L201
    apply hinjective
  6. L202
    exact hj
  7. L203
    exact hisn
  8. L204
    rewrite <- hclass_k_right_left_right
  9. L205
    rewrite <- hclass_k_right_left_right
  10. L206
    exact hclass_j_right_right_right_right
66Use earlier factsL207–207

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

  1. L207
    exact hold_i
67Separate the logical casesL208–208

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

  1. L208
    exfalso
68Use earlier factsL209–210

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

  1. L209
    apply hclass_j_right_right_left
  2. L210
    exact hji
69Separate the logical casesL211–212

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

  1. L211
    cases hclass_k_right_right
  2. L212
    cases hclass_k_right_right_right
70Use earlier factsL213–220

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

  1. L213
    specialize hinjective j
  2. L214
    specialize hinjective k
  3. L215
    specialize hinjective a
  4. L216
    apply hinjective
  5. L217
    exact hj
  6. L218
    exact hk
  7. L219
    exact hclass_j_right_right_right_right
  8. L220
    exact hclass_k_right_right_right_right

Library-wide reading audit

Original defined command ledger · 220 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 hinjective
  13. 0013intro hold_i
  14. 0014intro hold_n
  15. 0015intro hnew_i
  16. 0016intro hnew_n
  17. 0017intro hpreserve
  18. 0018rewrite hsn at hinjective
  19. 0019rewrite hsn at hinjective
  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 hreflect_j : ∀ 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)))
    Exact native replay linehave hreflect_j : 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)))))))
  29. 0029exact beta_prefix_swap_last_reflect
  30. 0030have hreflect_k : ∀ 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)))
    Exact native replay linehave hreflect_k : 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)))))))
  31. 0031exact beta_prefix_swap_last_reflect
  32. 0032rewrite hsn
  33. 0033rewrite hsn
  34. 0034intro j
  35. 0035intro k
  36. 0036intro a
  37. 0037intro hj
  38. 0038intro hk
  39. 0039intro hnew_j
  40. 0040intro hnew_k
  41. 0041specialize hreflect_j b
  42. 0042specialize hreflect_j c
  43. 0043specialize hreflect_j z
  44. 0044specialize hreflect_j d
  45. 0045specialize hreflect_j n
  46. 0046specialize hreflect_j i
  47. 0047specialize hreflect_j x
  48. 0048specialize hreflect_j y
  49. 0049have hreflect_entries_j : ∀ j. ∀ a. Lt(j,S n) → BetaAt(z,d,j,a) → j = i ∧ a = y ∨ (j = n ∧ a = x ∨ ¬j = i ∧ (¬j = n ∧ BetaAt(b,c,j,a)))
    Exact native replay linehave hreflect_entries_j : 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)))))))
  50. 0050apply hreflect_j
  51. 0051exact hnew_i
  52. 0052exact hnew_n
  53. 0053exact hpreserve
  54. 0054specialize hreflect_entries_j j
  55. 0055specialize hreflect_entries_j a
  56. 0056have hclass_j : j = i ∧ a = y ∨ (j = n ∧ a = x ∨ ¬j = i ∧ (¬j = n ∧ BetaAt(b,c,j,a)))
    Exact native replay linehave hclass_j : ((j = i /\ a = y) \/ ((j = n /\ a = x) \/ (~(j = i) /\ (~(j = n) /\ ((exists h. h + S a = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + a)))))
  57. 0057apply hreflect_entries_j
  58. 0058exact hj
  59. 0059exact hnew_j
  60. 0060specialize hreflect_k b
  61. 0061specialize hreflect_k c
  62. 0062specialize hreflect_k z
  63. 0063specialize hreflect_k d
  64. 0064specialize hreflect_k n
  65. 0065specialize hreflect_k i
  66. 0066specialize hreflect_k x
  67. 0067specialize hreflect_k y
  68. 0068have hreflect_entries_k : ∀ j. ∀ a. Lt(j,S n) → BetaAt(z,d,j,a) → j = i ∧ a = y ∨ (j = n ∧ a = x ∨ ¬j = i ∧ (¬j = n ∧ BetaAt(b,c,j,a)))
    Exact native replay linehave hreflect_entries_k : 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)))))))
  69. 0069apply hreflect_k
  70. 0070exact hnew_i
  71. 0071exact hnew_n
  72. 0072exact hpreserve
  73. 0073specialize hreflect_entries_k k
  74. 0074specialize hreflect_entries_k a
  75. 0075have hclass_k : k = i ∧ a = y ∨ (k = n ∧ a = x ∨ ¬k = i ∧ (¬k = n ∧ BetaAt(b,c,k,a)))
    Exact native replay linehave hclass_k : ((k = i /\ a = y) \/ ((k = n /\ a = x) \/ (~(k = i) /\ (~(k = n) /\ ((exists h. h + S a = S ((S k) * c)) /\ exists q. b = q * S ((S k) * c) + a)))))
  76. 0076apply hreflect_entries_k
  77. 0077exact hk
  78. 0078exact hnew_k
  79. 0079cases hclass_j
  80. 0080cases hclass_j_left
  81. 0081cases hclass_k
  82. 0082cases hclass_k_left
  83. 0083trans i
  84. 0084exact hclass_j_left_left
  85. 0085symm
  86. 0086exact hclass_k_left_left
  87. 0087cases hclass_k_right
  88. 0088cases hclass_k_right_left
  89. 0089have hxy : x = y
  90. 0090trans a
  91. 0091symm
  92. 0092exact hclass_k_right_left_right
  93. 0093exact hclass_j_left_right
  94. 0094have hin : i = n
  95. 0095specialize hinjective i
  96. 0096specialize hinjective n
  97. 0097specialize hinjective x
  98. 0098apply hinjective
  99. 0099exact hisn
  100. 0100exact hnsn
  101. 0101exact hold_i
  102. 0102rewrite hxy
  103. 0103rewrite hxy
  104. 0104exact hold_n
  105. 0105trans i
  106. 0106exact hclass_j_left_left
  107. 0107trans n
  108. 0108exact hin
  109. 0109symm
  110. 0110exact hclass_k_right_left_left
  111. 0111cases hclass_k_right_right
  112. 0112cases hclass_k_right_right_right
  113. 0113have hnk : n = k
  114. 0114specialize hinjective n
  115. 0115specialize hinjective k
  116. 0116specialize hinjective y
  117. 0117apply hinjective
  118. 0118exact hnsn
  119. 0119exact hk
  120. 0120exact hold_n
  121. 0121rewrite <- hclass_j_left_right
  122. 0122rewrite <- hclass_j_left_right
  123. 0123exact hclass_k_right_right_right_right
  124. 0124exfalso
  125. 0125apply hclass_k_right_right_right_left
  126. 0126symm
  127. 0127exact hnk
  128. 0128cases hclass_j_right
  129. 0129cases hclass_j_right_left
  130. 0130cases hclass_k
  131. 0131cases hclass_k_left
  132. 0132have hxy2 : x = y
  133. 0133trans a
  134. 0134symm
  135. 0135exact hclass_j_right_left_right
  136. 0136exact hclass_k_left_right
  137. 0137have hin2 : n = i
  138. 0138specialize hinjective n
  139. 0139specialize hinjective i
  140. 0140specialize hinjective y
  141. 0141apply hinjective
  142. 0142exact hnsn
  143. 0143exact hisn
  144. 0144exact hold_n
  145. 0145rewrite <- hxy2
  146. 0146rewrite <- hxy2
  147. 0147exact hold_i
  148. 0148trans n
  149. 0149exact hclass_j_right_left_left
  150. 0150trans i
  151. 0151exact hin2
  152. 0152symm
  153. 0153exact hclass_k_left_left
  154. 0154cases hclass_k_right
  155. 0155cases hclass_k_right_left
  156. 0156trans n
  157. 0157exact hclass_j_right_left_left
  158. 0158symm
  159. 0159exact hclass_k_right_left_left
  160. 0160cases hclass_k_right_right
  161. 0161cases hclass_k_right_right_right
  162. 0162have hik : i = k
  163. 0163specialize hinjective i
  164. 0164specialize hinjective k
  165. 0165specialize hinjective x
  166. 0166apply hinjective
  167. 0167exact hisn
  168. 0168exact hk
  169. 0169exact hold_i
  170. 0170rewrite <- hclass_j_right_left_right
  171. 0171rewrite <- hclass_j_right_left_right
  172. 0172exact hclass_k_right_right_right_right
  173. 0173exfalso
  174. 0174apply hclass_k_right_right_left
  175. 0175symm
  176. 0176exact hik
  177. 0177cases hclass_j_right_right
  178. 0178cases hclass_j_right_right_right
  179. 0179cases hclass_k
  180. 0180cases hclass_k_left
  181. 0181have hjn : j = n
  182. 0182specialize hinjective j
  183. 0183specialize hinjective n
  184. 0184specialize hinjective y
  185. 0185apply hinjective
  186. 0186exact hj
  187. 0187exact hnsn
  188. 0188rewrite <- hclass_k_left_right
  189. 0189rewrite <- hclass_k_left_right
  190. 0190exact hclass_j_right_right_right_right
  191. 0191exact hold_n
  192. 0192exfalso
  193. 0193apply hclass_j_right_right_right_left
  194. 0194exact hjn
  195. 0195cases hclass_k_right
  196. 0196cases hclass_k_right_left
  197. 0197have hji : j = i
  198. 0198specialize hinjective j
  199. 0199specialize hinjective i
  200. 0200specialize hinjective x
  201. 0201apply hinjective
  202. 0202exact hj
  203. 0203exact hisn
  204. 0204rewrite <- hclass_k_right_left_right
  205. 0205rewrite <- hclass_k_right_left_right
  206. 0206exact hclass_j_right_right_right_right
  207. 0207exact hold_i
  208. 0208exfalso
  209. 0209apply hclass_j_right_right_left
  210. 0210exact hji
  211. 0211cases hclass_k_right_right
  212. 0212cases hclass_k_right_right_right
  213. 0213specialize hinjective j
  214. 0214specialize hinjective k
  215. 0215specialize hinjective a
  216. 0216apply hinjective
  217. 0217exact hj
  218. 0218exact hk
  219. 0219exact hclass_j_right_right_right_right
  220. 0220exact hclass_k_right_right_right_right