PA008B · theorem

prime_mul_index_map_exists_up_to

Alpha v34 checked-use theorem · independently closed; not Stable

Canonical nonzero products modulo a prime form a beta-coded index map.

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

∀ l. ∀ n. ∀ p. ∀ a. Le(l,n) → p = S n → Prime(p) → ¬Dvd(p,a) → ∃ x. ∃ y. ∀ z. Lt(z,l) → ∃ m. Lt(m,n) ∧ (BetaAt(x,y,z,m) ∧ ModEq(p,a · S z,S m))

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

PD0001 Le PD0002 Lt PD0003 Dvd PD0004 Prime PD0008 ModEq PD0013 BetaAt

7 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0003 Dvd PD0007 DivRem PD0008 ModEq PD0013 BetaAt

18 occurrences

Exact expanded native-PA statement
forall l n p a. (exists frm_weak_gap_index_map_length. frm_weak_gap_index_map_length + l = n) -> p = S n -> ((~(p = 1) /\ forall frm_prime_left_index_map_prime frm_prime_right_index_map_prime. p = frm_prime_left_index_map_prime * frm_prime_right_index_map_prime -> frm_prime_left_index_map_prime = 1 \/ frm_prime_right_index_map_prime = 1)) -> (~(exists frm_factor_index_map_multiplier. a = p * frm_factor_index_map_multiplier)) -> exists r s. (forall frm_index_result. (exists frm_gap_result_index_bound. frm_gap_result_index_bound + S frm_index_result = l) -> (exists frm_residue_result_result. (exists frm_gap_result_result_residue_bound. frm_gap_result_result_residue_bound + S frm_residue_result_result = n) /\ ((((exists ff_h_frm_result_result_decoded. ff_h_frm_result_result_decoded + S (frm_residue_result_result) = S ((S (frm_index_result)) * s)) /\ exists ff_q_frm_result_result_decoded. r = ff_q_frm_result_result_decoded * S ((S (frm_index_result)) * s) + (frm_residue_result_result))) /\ (exists frm_mod_left_result_result_congruence frm_mod_right_result_result_congruence. a * S frm_index_result + p * frm_mod_left_result_result_congruence = S frm_residue_result_result + p * frm_mod_right_result_result_congruence))))

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA000X lt_to_le PA002K succ_le_succ PA0031 prime_nonzero PA001D division_remainder_exists PA0038 euclid_prime_dvd_product PA0039 divisor_le_nonzero PA003A lt_not_le PA001V nonzero_is_succ PA000V le_of_succ_le_succ PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA003D finite_lt_succ_eq_or_lt PA002X beta_prefix_extend

Direct theorem dependents

PA008I prime_mul_residue_reindex_exists

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

168 script commands · 52 reading checkpoints · 18 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 (15)
add eq zero rightsucc ne zerolt to lesucc le succprime nonzerodivision remainder existseuclid prime dvd productdivisor le nonzerolt not lenonzero is succle of succ le succmul commremainder decomposition to mod eqfinite lt succ eq or ltbeta prefix extend
01Induction on lL1–8

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L1
    induction l
  2. L2
    intro n
  3. L3
    intro p
  4. L4
    intro a
  5. L5
    intro hln
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hnotdiv
02Construct an explicit witnessL9–10

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

  1. L9
    exists 0
  2. L10
    exists 0
03Fix variables and assumptionsL11–12

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

  1. L11
    intro i
  2. L12
    intro hi
04Separate the logical casesL13–14

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

  1. L13
    exfalso
  2. L14
    cases hi
05Establish hsiL15–24

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

  1. L15
    have hsi : S i = 0
  2. L16
    specialize add_eq_zero_right x
  3. L17
    specialize add_eq_zero_right (S i)
  4. L18
    apply add_eq_zero_right
  5. L19
    exact hi_witness
  6. L20
    specialize succ_ne_zero i
  7. L21
    apply succ_ne_zero
  8. L22
    exact hsi
  9. L23
    intro n
  10. L24
    intro p
06Fix variables and assumptionsL25–29

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

  1. L25
    intro a
  2. L26
    intro hln
  3. L27
    intro hpn
  4. L28
    intro hp
  5. L29
    intro hnotdiv
07Establish hln_prevL30–34

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

  1. L30
    have hln_prev : Le(l,n)Definitions: Le(l,n)Original native command in the exact edition
  2. L31
    specialize lt_to_le l
  3. L32
    specialize lt_to_le n
  4. L33
    apply lt_to_le
  5. L34
    exact hln
08Establish hprevL35–43

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

  1. L35
    have hprev : ∃ r. ∃ s. ∀ x. Lt(x,l) → ∃ y. Lt(y,n) ∧ (BetaAt(r,s,x,y) ∧ ModEq(p,a · S x,S y))Definitions: Lt(x,l)Lt(y,n)BetaAt(r,s,x,y)ModEq(p,a · S x,S y)Original native command in the exact edition
  2. L36
    specialize IH n
  3. L37
    specialize IH p
  4. L38
    specialize IH a
  5. L39
    apply IH
  6. L40
    exact hln_prev
  7. L41
    exact hpn
  8. L42
    exact hp
  9. L43
    exact hnotdiv
09Separate the logical casesL44–45

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

  1. L44
    cases hprev
  2. L45
    cases hprev_witness
10Establish hslpL46–51

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

  1. L46
  2. L47
    rewrite hpn
  3. L48
    specialize succ_le_succ (S l)
  4. L49
    specialize succ_le_succ n
  5. L50
    apply succ_le_succ
  6. L51
    exact hln
11Establish hp0L52–57

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

  1. L52
    have hp0 : ~(p = 0)
  2. L53
    intro hpzero
  3. L54
    specialize prime_nonzero p
  4. L55
    apply prime_nonzero
  5. L56
    exact hp
  6. L57
    exact hpzero
12Establish hdivL58–62

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

  1. L58
    have hdiv : ∃ q. ∃ rem. DivRem(a · S l,p,q,rem)Definitions: DivRem(a · S l,p,q,rem)Original native command in the exact edition
  2. L59
    specialize division_remainder_exists p
  3. L60
    specialize division_remainder_exists (a * S l)
  4. L61
    apply division_remainder_exists
  5. L62
    exact hp0
13Separate the logical casesL63–65

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

  1. L63
    cases hdiv
  2. L64
    cases hdiv_witness
  3. L65
    cases hdiv_witness_witness
14Establish hrem0L66–67

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

  1. L66
    have hrem0 : ~(x3 = 0)
  2. L67
    intro hremzero
15Establish hmultipleL68–68

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

  1. L68
    have hmultiple : Dvd(p,a · S l)Definitions: Dvd(p,a · S l)Original native command in the exact edition
16Construct an explicit witnessL69–69

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

  1. L69
    exists x2
17Calculate and transport equalitiesL70–70

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

  1. L70
    trans p * x2 + x3
18Use earlier factsL71–71

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

  1. L71
    exact hdiv_witness_witness_left
19Calculate and transport equalitiesL72–72

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

  1. L72
    rewrite hremzero
20Use earlier factsL73–73

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

  1. L73
    apply PA3
21Establish hfactorL74–80

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclid prime dvd product.

  1. L74
    have hfactor : Dvd(p,a) ∨ Dvd(p,S l)Definitions: Dvd(p,a)Dvd(p,S l)Original native command in the exact edition
  2. L75
    specialize euclid_prime_dvd_product p
  3. L76
    specialize euclid_prime_dvd_product a
  4. L77
    specialize euclid_prime_dvd_product (S l)
  5. L78
    apply euclid_prime_dvd_product
  6. L79
    exact hp
  7. L80
    exact hmultiple
22Separate the logical casesL81–81

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

  1. L81
    cases hfactor
23Use earlier factsL82–83

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

  1. L82
    apply hnotdiv
  2. L83
    exact hfactor_left
24Establish hsl0L84–86

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

  1. L84
    have hsl0 : ~(S l = 0)
  2. L85
    specialize succ_ne_zero l
  3. L86
    exact succ_ne_zero
25Establish hpleL87–96

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

  1. L87
  2. L88
    specialize divisor_le_nonzero p
  3. L89
    specialize divisor_le_nonzero (S l)
  4. L90
    apply divisor_le_nonzero
  5. L91
    exact hsl0
  6. L92
    exact hfactor_right
  7. L93
    specialize lt_not_le (S l)
  8. L94
    specialize lt_not_le p
  9. L95
    apply lt_not_le
  10. L96
    exact hslp
26Use earlier factsL97–97

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

  1. L97
    exact hple
27Establish hrem_succL98–101

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

  1. L98
    have hrem_succ : exists j. x3 = S j
  2. L99
    specialize nonzero_is_succ x3
  3. L100
    apply nonzero_is_succ
  4. L101
    exact hrem0
28Separate the logical casesL102–102

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

  1. L102
    cases hrem_succ
29Establish hjnL103–109

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

  1. L103
  2. L104
    specialize le_of_succ_le_succ (S x4)
  3. L105
    specialize le_of_succ_le_succ n
  4. L106
    apply le_of_succ_le_succ
  5. L107
    rewrite <- hrem_succ_witness
  6. L108
    rewrite <- hpn
  7. L109
    exact hdiv_witness_witness_right
30Establish hdecompL110–115

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

  1. L110
    have hdecomp : a * S l = x2 * p + x3
  2. L111
    trans p * x2 + x3
  3. L112
    exact hdiv_witness_witness_left
  4. L113
    congr
  5. L114
    apply mul_comm
  6. L115
    refl
31Establish hmodremL116–122

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L116
    have hmodrem : ModEq(p,a · S l,x3)Definitions: ModEq(p,a · S l,x3)Original native command in the exact edition
  2. L117
    specialize remainder_decomposition_to_mod_eq p
  3. L118
    specialize remainder_decomposition_to_mod_eq (a * S l)
  4. L119
    specialize remainder_decomposition_to_mod_eq x2
  5. L120
    specialize remainder_decomposition_to_mod_eq x3
  6. L121
    apply remainder_decomposition_to_mod_eq
  7. L122
    exact hdecomp
32Establish hmodL123–129

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

  1. L123
    have hmod : ModEq(p,a · S l,S x4)Definitions: ModEq(p,a · S l,S x4)Original native command in the exact edition
  2. L124
    rewrite <- hrem_succ_witness
  3. L125
    exact hmodrem
  4. L126
    specialize beta_prefix_extend l
  5. L127
    specialize beta_prefix_extend x
  6. L128
    specialize beta_prefix_extend x1
  7. L129
    specialize beta_prefix_extend x4
33Separate the logical casesL130–132

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

  1. L130
    cases beta_prefix_extend
  2. L131
    cases beta_prefix_extend_witness
  3. L132
    cases beta_prefix_extend_witness_witness
34Construct an explicit witnessL133–134

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

  1. L133
    exists x5
  2. L134
    exists x6
35Fix variables and assumptionsL135–136

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

  1. L135
    intro i
  2. L136
    intro hi
36Establish hsplitL137–141

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

  1. L137
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L138
    specialize finite_lt_succ_eq_or_lt l
  3. L139
    specialize finite_lt_succ_eq_or_lt i
  4. L140
    apply finite_lt_succ_eq_or_lt
  5. L141
    exact hi
37Separate the logical casesL142–142

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

  1. L142
    cases hsplit
38Construct an explicit witnessL143–143

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

  1. L143
    exists x4
39Separate the logical casesL144–144

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

  1. L144
    split
40Use earlier factsL145–145

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

  1. L145
    exact hjn
41Separate the logical casesL146–146

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

  1. L146
    split
42Calculate and transport equalitiesL147–148

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

  1. L147
    rewrite hsplit_left
  2. L148
    rewrite hsplit_left
43Use earlier factsL149–149

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

  1. L149
    exact beta_prefix_extend_witness_witness_left
44Calculate and transport equalitiesL150–150

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

  1. L150
    rewrite hsplit_left
45Use earlier factsL151–151

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

  1. L151
    exact hmod
46Establish holdL152–155

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

  1. L152
    have hold : ∃ y. Lt(y,n) ∧ (BetaAt(x,x1,i,y) ∧ ModEq(p,a · S i,S y))Definitions: Lt(y,n)BetaAt(x,x1,i,y)ModEq(p,a · S i,S y)Original native command in the exact edition
  2. L153
    specialize hprev_witness_witness i
  3. L154
    apply hprev_witness_witness
  4. L155
    exact hsplit_right
47Separate the logical casesL156–158

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

  1. L156
    cases hold
  2. L157
    cases hold_witness
  3. L158
    cases hold_witness_right
48Construct an explicit witnessL159–159

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

  1. L159
    exists x7
49Separate the logical casesL160–160

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

  1. L160
    split
50Use earlier factsL161–161

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

  1. L161
    exact hold_witness_left
51Separate the logical casesL162–162

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

  1. L162
    split
52Use earlier factsL163–168

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

  1. L163
    specialize beta_prefix_extend_witness_witness_right i
  2. L164
    specialize beta_prefix_extend_witness_witness_right x7
  3. L165
    apply beta_prefix_extend_witness_witness_right
  4. L166
    exact hsplit_right
  5. L167
    exact hold_witness_right_left
  6. L168
    exact hold_witness_right_right

Library-wide reading audit

Original defined command ledger · 168 lines
  1. 0001induction l
  2. 0002intro n
  3. 0003intro p
  4. 0004intro a
  5. 0005intro hln
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hnotdiv
  9. 0009exists 0
  10. 0010exists 0
  11. 0011intro i
  12. 0012intro hi
  13. 0013exfalso
  14. 0014cases hi
  15. 0015have hsi : S i = 0
  16. 0016specialize add_eq_zero_right x
  17. 0017specialize add_eq_zero_right (S i)
  18. 0018apply add_eq_zero_right
  19. 0019exact hi_witness
  20. 0020specialize succ_ne_zero i
  21. 0021apply succ_ne_zero
  22. 0022exact hsi
  23. 0023intro n
  24. 0024intro p
  25. 0025intro a
  26. 0026intro hln
  27. 0027intro hpn
  28. 0028intro hp
  29. 0029intro hnotdiv
  30. 0030have hln_prev : Le(l,n)
    Exact native replay linehave hln_prev : exists h. h + l = n
  31. 0031specialize lt_to_le l
  32. 0032specialize lt_to_le n
  33. 0033apply lt_to_le
  34. 0034exact hln
  35. 0035have hprev : ∃ r. ∃ s. ∀ x. Lt(x,l) → ∃ y. Lt(y,n) ∧ (BetaAt(r,s,x,y) ∧ ModEq(p,a · S x,S y))
    Exact native replay linehave hprev : exists r s. (forall frm_index_previous. (exists frm_gap_previous_index_bound. frm_gap_previous_index_bound + S frm_index_previous = l) -> (exists frm_residue_previous_result. (exists frm_gap_previous_result_residue_bound. frm_gap_previous_result_residue_bound + S frm_residue_previous_result = n) /\ ((((exists ff_h_frm_previous_result_decoded. ff_h_frm_previous_result_decoded + S (frm_residue_previous_result) = S ((S (frm_index_previous)) * s)) /\ exists ff_q_frm_previous_result_decoded. r = ff_q_frm_previous_result_decoded * S ((S (frm_index_previous)) * s) + (frm_residue_previous_result))) /\ (exists frm_mod_left_previous_result_congruence frm_mod_right_previous_result_congruence. a * S frm_index_previous + p * frm_mod_left_previous_result_congruence = S frm_residue_previous_result + p * frm_mod_right_previous_result_congruence))))
  36. 0036specialize IH n
  37. 0037specialize IH p
  38. 0038specialize IH a
  39. 0039apply IH
  40. 0040exact hln_prev
  41. 0041exact hpn
  42. 0042exact hp
  43. 0043exact hnotdiv
  44. 0044cases hprev
  45. 0045cases hprev_witness
  46. 0046have hslp : Lt(S l,p)
    Exact native replay linehave hslp : exists h. h + S (S l) = p
  47. 0047rewrite hpn
  48. 0048specialize succ_le_succ (S l)
  49. 0049specialize succ_le_succ n
  50. 0050apply succ_le_succ
  51. 0051exact hln
  52. 0052have hp0 : ~(p = 0)
  53. 0053intro hpzero
  54. 0054specialize prime_nonzero p
  55. 0055apply prime_nonzero
  56. 0056exact hp
  57. 0057exact hpzero
  58. 0058have hdiv : ∃ q. ∃ rem. DivRem(a · S l,p,q,rem)
    Exact native replay linehave hdiv : exists q rem. a * S l = p * q + rem /\ exists h. h + S rem = p
  59. 0059specialize division_remainder_exists p
  60. 0060specialize division_remainder_exists (a * S l)
  61. 0061apply division_remainder_exists
  62. 0062exact hp0
  63. 0063cases hdiv
  64. 0064cases hdiv_witness
  65. 0065cases hdiv_witness_witness
  66. 0066have hrem0 : ~(x3 = 0)
  67. 0067intro hremzero
  68. 0068have hmultiple : Dvd(p,a · S l)
    Exact native replay linehave hmultiple : exists k. a * S l = p * k
  69. 0069exists x2
  70. 0070trans p * x2 + x3
  71. 0071exact hdiv_witness_witness_left
  72. 0072rewrite hremzero
  73. 0073apply PA3
  74. 0074have hfactor : Dvd(p,a) ∨ Dvd(p,S l)
    Exact native replay linehave hfactor : (exists u. a = p * u) \/ exists v. S l = p * v
  75. 0075specialize euclid_prime_dvd_product p
  76. 0076specialize euclid_prime_dvd_product a
  77. 0077specialize euclid_prime_dvd_product (S l)
  78. 0078apply euclid_prime_dvd_product
  79. 0079exact hp
  80. 0080exact hmultiple
  81. 0081cases hfactor
  82. 0082apply hnotdiv
  83. 0083exact hfactor_left
  84. 0084have hsl0 : ~(S l = 0)
  85. 0085specialize succ_ne_zero l
  86. 0086exact succ_ne_zero
  87. 0087have hple : Le(p,S l)
    Exact native replay linehave hple : exists k. k + p = S l
  88. 0088specialize divisor_le_nonzero p
  89. 0089specialize divisor_le_nonzero (S l)
  90. 0090apply divisor_le_nonzero
  91. 0091exact hsl0
  92. 0092exact hfactor_right
  93. 0093specialize lt_not_le (S l)
  94. 0094specialize lt_not_le p
  95. 0095apply lt_not_le
  96. 0096exact hslp
  97. 0097exact hple
  98. 0098have hrem_succ : exists j. x3 = S j
  99. 0099specialize nonzero_is_succ x3
  100. 0100apply nonzero_is_succ
  101. 0101exact hrem0
  102. 0102cases hrem_succ
  103. 0103have hjn : Lt(x4,n)
    Exact native replay linehave hjn : exists h. h + S x4 = n
  104. 0104specialize le_of_succ_le_succ (S x4)
  105. 0105specialize le_of_succ_le_succ n
  106. 0106apply le_of_succ_le_succ
  107. 0107rewrite <- hrem_succ_witness
  108. 0108rewrite <- hpn
  109. 0109exact hdiv_witness_witness_right
  110. 0110have hdecomp : a * S l = x2 * p + x3
  111. 0111trans p * x2 + x3
  112. 0112exact hdiv_witness_witness_left
  113. 0113congr
  114. 0114apply mul_comm
  115. 0115refl
  116. 0116have hmodrem : ModEq(p,a · S l,x3)
    Exact native replay linehave hmodrem : exists u v. a * S l + p * u = x3 + p * v
  117. 0117specialize remainder_decomposition_to_mod_eq p
  118. 0118specialize remainder_decomposition_to_mod_eq (a * S l)
  119. 0119specialize remainder_decomposition_to_mod_eq x2
  120. 0120specialize remainder_decomposition_to_mod_eq x3
  121. 0121apply remainder_decomposition_to_mod_eq
  122. 0122exact hdecomp
  123. 0123have hmod : ModEq(p,a · S l,S x4)
    Exact native replay linehave hmod : exists u v. a * S l + p * u = S x4 + p * v
  124. 0124rewrite <- hrem_succ_witness
  125. 0125exact hmodrem
  126. 0126specialize beta_prefix_extend l
  127. 0127specialize beta_prefix_extend x
  128. 0128specialize beta_prefix_extend x1
  129. 0129specialize beta_prefix_extend x4
  130. 0130cases beta_prefix_extend
  131. 0131cases beta_prefix_extend_witness
  132. 0132cases beta_prefix_extend_witness_witness
  133. 0133exists x5
  134. 0134exists x6
  135. 0135intro i
  136. 0136intro hi
  137. 0137have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists h. h + S i = l
  138. 0138specialize finite_lt_succ_eq_or_lt l
  139. 0139specialize finite_lt_succ_eq_or_lt i
  140. 0140apply finite_lt_succ_eq_or_lt
  141. 0141exact hi
  142. 0142cases hsplit
  143. 0143exists x4
  144. 0144split
  145. 0145exact hjn
  146. 0146split
  147. 0147rewrite hsplit_left
  148. 0148rewrite hsplit_left
  149. 0149exact beta_prefix_extend_witness_witness_left
  150. 0150rewrite hsplit_left
  151. 0151exact hmod
  152. 0152have hold : ∃ y. Lt(y,n) ∧ (BetaAt(x,x1,i,y) ∧ ModEq(p,a · S i,S y))
    Exact native replay linehave hold : (exists frm_residue_previous_at_i. (exists frm_gap_previous_at_i_residue_bound. frm_gap_previous_at_i_residue_bound + S frm_residue_previous_at_i = n) /\ ((((exists ff_h_frm_previous_at_i_decoded. ff_h_frm_previous_at_i_decoded + S (frm_residue_previous_at_i) = S ((S (i)) * x1)) /\ exists ff_q_frm_previous_at_i_decoded. x = ff_q_frm_previous_at_i_decoded * S ((S (i)) * x1) + (frm_residue_previous_at_i))) /\ (exists frm_mod_left_previous_at_i_congruence frm_mod_right_previous_at_i_congruence. a * S i + p * frm_mod_left_previous_at_i_congruence = S frm_residue_previous_at_i + p * frm_mod_right_previous_at_i_congruence)))
  153. 0153specialize hprev_witness_witness i
  154. 0154apply hprev_witness_witness
  155. 0155exact hsplit_right
  156. 0156cases hold
  157. 0157cases hold_witness
  158. 0158cases hold_witness_right
  159. 0159exists x7
  160. 0160split
  161. 0161exact hold_witness_left
  162. 0162split
  163. 0163specialize beta_prefix_extend_witness_witness_right i
  164. 0164specialize beta_prefix_extend_witness_witness_right x7
  165. 0165apply beta_prefix_extend_witness_witness_right
  166. 0166exact hsplit_right
  167. 0167exact hold_witness_right_left
  168. 0168exact hold_witness_right_right