PA009X

scaled_pair_order_successor_lift_adjacent_targets

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

A successor-lifted terminal scaled-orbit history has adjacent products congruent to a.

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 p a n u v b c f g h. n = h + h -> (forall esip_index_enr_prefix. (exists esip_gap_enr_prefix_prefix_bound. esip_gap_enr_prefix_prefix_bound + S (esip_index_enr_prefix) = n) -> exists esip_mate_enr_prefix. ((((exists ff_h_esip_enr_prefix_entry. ff_h_esip_enr_prefix_entry + S (esip_mate_enr_prefix) = S ((S (esip_index_enr_prefix)) * v)) /\ exists ff_q_esip_enr_prefix_entry. u = ff_q_esip_enr_prefix_entry * S ((S (esip_index_enr_prefix)) * v) + (esip_mate_enr_prefix))) /\ ((exists esip_gap_enr_prefix_relation_index_bound. esip_gap_enr_prefix_relation_index_bound + S (esip_index_enr_prefix) = n) /\ ((((~((S esip_index_enr_prefix) = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_left_bound. esip_gap_enr_prefix_relation_scaled_left_bound + S (S esip_index_enr_prefix) = p))) /\ (((~(esip_mate_enr_prefix = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_right_bound. esip_gap_enr_prefix_relation_scaled_right_bound + S (esip_mate_enr_prefix) = p))) /\ (exists esi_mod_left_enr_prefix_relation_scaled_mod esi_mod_right_enr_prefix_relation_scaled_mod. ((S esip_index_enr_prefix) * esip_mate_enr_prefix) + p * esi_mod_left_enr_prefix_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_relation_scaled_mod))))))) -> (forall fom_index_enr_raw_bounded. (exists fom_gap_enr_raw_bounded_index_bound. fom_gap_enr_raw_bounded_index_bound + S (fom_index_enr_raw_bounded) = h + h) -> exists fom_value_enr_raw_bounded. ((((exists fom_beta_height_enr_raw_bounded_entry. fom_beta_height_enr_raw_bounded_entry + S (fom_value_enr_raw_bounded) = S ((S (fom_index_enr_raw_bounded)) * c)) /\ exists fom_beta_quotient_enr_raw_bounded_entry. b = fom_beta_quotient_enr_raw_bounded_entry * S ((S (fom_index_enr_raw_bounded)) * c) + (fom_value_enr_raw_bounded))) /\ (exists fom_gap_enr_raw_bounded_value_bound. fom_gap_enr_raw_bounded_value_bound + S (fom_value_enr_raw_bounded) = n))) -> (forall espi_pair_enr_history. (exists wpo_gap_enr_history_pair_bound. wpo_gap_enr_history_pair_bound + S (espi_pair_enr_history) = h) -> exists espi_left_enr_history espi_right_enr_history. (((((exists wpo_beta_height_enr_history_left_entry. wpo_beta_height_enr_history_left_entry + S (espi_left_enr_history) = S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c)) /\ exists wpo_beta_quotient_enr_history_left_entry. b = wpo_beta_quotient_enr_history_left_entry * S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c) + (espi_left_enr_history))) /\ (((((exists wpo_beta_height_enr_history_right_entry. wpo_beta_height_enr_history_right_entry + S (espi_right_enr_history) = S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c)) /\ exists wpo_beta_quotient_enr_history_right_entry. b = wpo_beta_quotient_enr_history_right_entry * S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c) + (espi_right_enr_history))) /\ (((exists wpo_beta_height_enr_history_scaled_edge. wpo_beta_height_enr_history_scaled_edge + S (S espi_right_enr_history) = S ((S (espi_left_enr_history)) * v)) /\ exists wpo_beta_quotient_enr_history_scaled_edge. u = wpo_beta_quotient_enr_history_scaled_edge * S ((S (espi_left_enr_history)) * v) + (S espi_right_enr_history)))))))) -> (forall wsl_index_enr_lift_n wsl_value_enr_lift_n. (exists wpo_gap_enr_lift_n_bound. wpo_gap_enr_lift_n_bound + S (wsl_index_enr_lift_n) = n) -> (((exists wpo_beta_height_enr_lift_n_source. wpo_beta_height_enr_lift_n_source + S (wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * c)) /\ exists wpo_beta_quotient_enr_lift_n_source. b = wpo_beta_quotient_enr_lift_n_source * S ((S (wsl_index_enr_lift_n)) * c) + (wsl_value_enr_lift_n))) -> (((exists wpo_beta_height_enr_lift_n_target. wpo_beta_height_enr_lift_n_target + S (S wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * g)) /\ exists wpo_beta_quotient_enr_lift_n_target. f = wpo_beta_quotient_enr_lift_n_target * S ((S (wsl_index_enr_lift_n)) * g) + (S wsl_value_enr_lift_n)))) -> (forall wpp_pair_enr_target_pairs wpp_left_enr_target_pairs wpp_right_enr_target_pairs. (exists wpp_gap_enr_target_pairs_pair_bound. wpp_gap_enr_target_pairs_pair_bound + S (wpp_pair_enr_target_pairs) = h) -> (((exists wpp_beta_height_enr_target_pairs_left_entry. wpp_beta_height_enr_target_pairs_left_entry + S (wpp_left_enr_target_pairs) = S ((S ((wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g)) /\ exists wpp_beta_quotient_enr_target_pairs_left_entry. f = wpp_beta_quotient_enr_target_pairs_left_entry * S ((S ((wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g) + (wpp_left_enr_target_pairs))) -> (((exists wpp_beta_height_enr_target_pairs_right_entry. wpp_beta_height_enr_target_pairs_right_entry + S (wpp_right_enr_target_pairs) = S ((S (S (wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g)) /\ exists wpp_beta_quotient_enr_target_pairs_right_entry. f = wpp_beta_quotient_enr_target_pairs_right_entry * S ((S (S (wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g) + (wpp_right_enr_target_pairs))) -> (exists wpp_mod_left_enr_target_pairs_pair_mod wpp_mod_right_enr_target_pairs_pair_mod. (wpp_left_enr_target_pairs * wpp_right_enr_target_pairs) + p * wpp_mod_left_enr_target_pairs_pair_mod = (a) + p * wpp_mod_right_enr_target_pairs_pair_mod))

Structural proof guide

Generated structural guide

A successor-lifted terminal scaled-orbit history has adjacent products congruent to a.

Use the direct prerequisites pair_index_left_below_double, pair_index_right_below_double, beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (11), intermediate claims (14), equality transport (6).

Referenced ingredients

PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA002F beta_at_unique

Direct dependents

PA00BK scaled_pair_order_terminal_power_mod_predecessor

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

115 script commands · 22 reading checkpoints · 14 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.

Named ingredients (3)
pair index left below doublepair index right below doublebeta at unique

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro n
  4. L4
    intro u
  5. L5
    intro v
  6. L6
    intro b
  7. L7
    intro c
  8. L8
    intro f
  9. L9
    intro g
  10. L10
    intro h
02Fix variables and assumptionsL11–20

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

  1. L11
    intro heven
  2. L12
    intro hprefix
  3. L13
    intro hbounded
  4. L14
    intro hhistory
  5. L15
    intro hlift
  6. L16
    intro t
  7. L17
    intro left
  8. L18
    intro right
  9. L19
    intro ht
  10. L20
    intro hleft
03Fix variables and assumptionsL21–21

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

  1. L21
    intro hright
04Establish horbitL22–25

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

  1. L22
    have horbit : exists i j. (((exists ff_h_enr_history_left. ff_h_enr_history_left + S (i) = S ((S (t + t)) * c)) /\ exists ff_q_enr_history_left. b = ff_q_enr_history_left * S ((S (t + t)) * c) + (i))) /\ ((((exists ff_h_enr_history_right. ff_h_enr_history_right + S (j) = S ((S (S (t + t))) * c)) /\ exists ff_q_enr_history_right. b = ff_q_enr_history_right * S ((S (S (t + t))) * c) + (j))) /\ (((exists ff_h_enr_history_scaled. ff_h_enr_history_scaled + S (S j) = S ((S (i)) * v)) /\ exists ff_q_enr_history_scaled. u = ff_q_enr_history_scaled * S ((S (i)) * v) + (S j))))
  2. L23
    specialize hhistory t
  3. L24
    apply hhistory
  4. L25
    exact ht
05Separate the logical casesL26–29

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

  1. L26
    cases horbit
  2. L27
    cases horbit_witness
  3. L28
    cases horbit_witness_witness
  4. L29
    cases horbit_witness_witness_right
06Establish heven_rawL30–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair index left below double.

  1. L30
    have heven_raw : exists wpo_gap_enr_even_bound_raw. wpo_gap_enr_even_bound_raw + S (t + t) = h + h
  2. L31
    specialize pair_index_left_below_double t
  3. L32
    specialize pair_index_left_below_double h
  4. L33
    apply pair_index_left_below_double
  5. L34
    exact ht
07Establish hodd_rawL35–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair index right below double.

  1. L35
    have hodd_raw : exists wpo_gap_enr_odd_bound_raw. wpo_gap_enr_odd_bound_raw + S (S (t + t)) = h + h
  2. L36
    specialize pair_index_right_below_double t
  3. L37
    specialize pair_index_right_below_double h
  4. L38
    apply pair_index_right_below_double
  5. L39
    exact ht
08Establish heven_nL40–42

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

  1. L40
    have heven_n : exists wpo_gap_enr_even_bound_n. wpo_gap_enr_even_bound_n + S (t + t) = n
  2. L41
    rewrite heven
  3. L42
    exact heven_raw
09Establish hodd_nL43–45

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

  1. L43
    have hodd_n : exists wpo_gap_enr_odd_bound_n. wpo_gap_enr_odd_bound_n + S (S (t + t)) = n
  2. L44
    rewrite heven
  3. L45
    exact hodd_raw
10Establish hlift_leftL46–51

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

  1. L46
    have hlift_left : ((exists ff_h_enr_lifted_left. ff_h_enr_lifted_left + S (S x) = S ((S (t + t)) * g)) /\ exists ff_q_enr_lifted_left. f = ff_q_enr_lifted_left * S ((S (t + t)) * g) + (S x))
  2. L47
    specialize hlift (t + t)
  3. L48
    specialize hlift x
  4. L49
    apply hlift
  5. L50
    exact heven_n
  6. L51
    exact horbit_witness_witness_left
11Establish hlift_rightL52–57

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

  1. L52
    have hlift_right : ((exists ff_h_enr_lifted_right. ff_h_enr_lifted_right + S (S x1) = S ((S (S (t + t))) * g)) /\ exists ff_q_enr_lifted_right. f = ff_q_enr_lifted_right * S ((S (S (t + t))) * g) + (S x1))
  2. L53
    specialize hlift (S (t + t))
  3. L54
    specialize hlift x1
  4. L55
    apply hlift
  5. L56
    exact hodd_n
  6. L57
    exact horbit_witness_witness_right_left
12Establish hleft_eqL58–66

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

  1. L58
    have hleft_eq : left = S x
  2. L59
    specialize beta_at_unique f
  3. L60
    specialize beta_at_unique g
  4. L61
    specialize beta_at_unique (t + t)
  5. L62
    specialize beta_at_unique left
  6. L63
    specialize beta_at_unique (S x)
  7. L64
    apply beta_at_unique
  8. L65
    exact hleft
  9. L66
    exact hlift_left
13Establish hright_eqL67–75

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

  1. L67
    have hright_eq : right = S x1
  2. L68
    specialize beta_at_unique f
  3. L69
    specialize beta_at_unique g
  4. L70
    specialize beta_at_unique (S (t + t))
  5. L71
    specialize beta_at_unique right
  6. L72
    specialize beta_at_unique (S x1)
  7. L73
    apply beta_at_unique
  8. L74
    exact hright
  9. L75
    exact hlift_right
14Establish hbounded_evenL76–79

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

  1. L76
    have hbounded_even : exists w. (((exists ff_h_enr_bounded_even_entry. ff_h_enr_bounded_even_entry + S (w) = S ((S (t + t)) * c)) /\ exists ff_q_enr_bounded_even_entry. b = ff_q_enr_bounded_even_entry * S ((S (t + t)) * c) + (w))) /\ (exists wpo_gap_enr_bounded_even_value. wpo_gap_enr_bounded_even_value + S (w) = n)
  2. L77
    specialize hbounded (t + t)
  3. L78
    apply hbounded
  4. L79
    exact heven_raw
15Separate the logical casesL80–81

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

  1. L80
    cases hbounded_even
  2. L81
    cases hbounded_even_witness
16Establish hsource_eqL82–90

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

  1. L82
    have hsource_eq : x = x2
  2. L83
    specialize beta_at_unique b
  3. L84
    specialize beta_at_unique c
  4. L85
    specialize beta_at_unique (t + t)
  5. L86
    specialize beta_at_unique x
  6. L87
    specialize beta_at_unique x2
  7. L88
    apply beta_at_unique
  8. L89
    exact horbit_witness_witness_left
  9. L90
    exact hbounded_even_witness_left
17Establish hsource_boundL91–93

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

  1. L91
    have hsource_bound : exists gap. gap + S x = n
  2. L92
    rewrite hsource_eq
  3. L93
    exact hbounded_even_witness_right
18Establish hprefix_dataL94–97

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

  1. L94
    have hprefix_data : ∃ y. BetaAt(u,v,x,y) ∧ ScaledInverseIndex(p,a,n,x,y)Definitions: BetaAtScaledInverseIndex
  2. L95
    specialize hprefix x
  3. L96
    apply hprefix
  4. L97
    exact hsource_bound
19Separate the logical casesL98–102

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

  1. L98
    cases hprefix_data
  2. L99
    cases hprefix_data_witness
  3. L100
    cases hprefix_data_witness_right
  4. L101
    cases hprefix_data_witness_right_right
  5. L102
    cases hprefix_data_witness_right_right_right
20Establish hmate_eqL103–112

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

  1. L103
    have hmate_eq : x3 = S x1
  2. L104
    specialize beta_at_unique u
  3. L105
    specialize beta_at_unique v
  4. L106
    specialize beta_at_unique x
  5. L107
    specialize beta_at_unique x3
  6. L108
    specialize beta_at_unique (S x1)
  7. L109
    apply beta_at_unique
  8. L110
    exact hprefix_data_witness_left
  9. L111
    exact horbit_witness_witness_right_right
  10. L112
    rewrite hleft_eq
21Calculate and transport equalitiesL113–114

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

  1. L113
    rewrite hright_eq
  2. L114
    rewrite <- hmate_eq
22Use earlier factsL115–115

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

  1. L115
    exact hprefix_data_witness_right_right_right_right

Library-wide reading audit

Original exact command ledger · 115 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro b
  7. 0007intro c
  8. 0008intro f
  9. 0009intro g
  10. 0010intro h
  11. 0011intro heven
  12. 0012intro hprefix
  13. 0013intro hbounded
  14. 0014intro hhistory
  15. 0015intro hlift
  16. 0016intro t
  17. 0017intro left
  18. 0018intro right
  19. 0019intro ht
  20. 0020intro hleft
  21. 0021intro hright
  22. 0022have horbit : exists i j. (((exists ff_h_enr_history_left. ff_h_enr_history_left + S (i) = S ((S (t + t)) * c)) /\ exists ff_q_enr_history_left. b = ff_q_enr_history_left * S ((S (t + t)) * c) + (i))) /\ ((((exists ff_h_enr_history_right. ff_h_enr_history_right + S (j) = S ((S (S (t + t))) * c)) /\ exists ff_q_enr_history_right. b = ff_q_enr_history_right * S ((S (S (t + t))) * c) + (j))) /\ (((exists ff_h_enr_history_scaled. ff_h_enr_history_scaled + S (S j) = S ((S (i)) * v)) /\ exists ff_q_enr_history_scaled. u = ff_q_enr_history_scaled * S ((S (i)) * v) + (S j))))
  23. 0023specialize hhistory t
  24. 0024apply hhistory
  25. 0025exact ht
  26. 0026cases horbit
  27. 0027cases horbit_witness
  28. 0028cases horbit_witness_witness
  29. 0029cases horbit_witness_witness_right
  30. 0030have heven_raw : exists wpo_gap_enr_even_bound_raw. wpo_gap_enr_even_bound_raw + S (t + t) = h + h
  31. 0031specialize pair_index_left_below_double t
  32. 0032specialize pair_index_left_below_double h
  33. 0033apply pair_index_left_below_double
  34. 0034exact ht
  35. 0035have hodd_raw : exists wpo_gap_enr_odd_bound_raw. wpo_gap_enr_odd_bound_raw + S (S (t + t)) = h + h
  36. 0036specialize pair_index_right_below_double t
  37. 0037specialize pair_index_right_below_double h
  38. 0038apply pair_index_right_below_double
  39. 0039exact ht
  40. 0040have heven_n : exists wpo_gap_enr_even_bound_n. wpo_gap_enr_even_bound_n + S (t + t) = n
  41. 0041rewrite heven
  42. 0042exact heven_raw
  43. 0043have hodd_n : exists wpo_gap_enr_odd_bound_n. wpo_gap_enr_odd_bound_n + S (S (t + t)) = n
  44. 0044rewrite heven
  45. 0045exact hodd_raw
  46. 0046have hlift_left : ((exists ff_h_enr_lifted_left. ff_h_enr_lifted_left + S (S x) = S ((S (t + t)) * g)) /\ exists ff_q_enr_lifted_left. f = ff_q_enr_lifted_left * S ((S (t + t)) * g) + (S x))
  47. 0047specialize hlift (t + t)
  48. 0048specialize hlift x
  49. 0049apply hlift
  50. 0050exact heven_n
  51. 0051exact horbit_witness_witness_left
  52. 0052have hlift_right : ((exists ff_h_enr_lifted_right. ff_h_enr_lifted_right + S (S x1) = S ((S (S (t + t))) * g)) /\ exists ff_q_enr_lifted_right. f = ff_q_enr_lifted_right * S ((S (S (t + t))) * g) + (S x1))
  53. 0053specialize hlift (S (t + t))
  54. 0054specialize hlift x1
  55. 0055apply hlift
  56. 0056exact hodd_n
  57. 0057exact horbit_witness_witness_right_left
  58. 0058have hleft_eq : left = S x
  59. 0059specialize beta_at_unique f
  60. 0060specialize beta_at_unique g
  61. 0061specialize beta_at_unique (t + t)
  62. 0062specialize beta_at_unique left
  63. 0063specialize beta_at_unique (S x)
  64. 0064apply beta_at_unique
  65. 0065exact hleft
  66. 0066exact hlift_left
  67. 0067have hright_eq : right = S x1
  68. 0068specialize beta_at_unique f
  69. 0069specialize beta_at_unique g
  70. 0070specialize beta_at_unique (S (t + t))
  71. 0071specialize beta_at_unique right
  72. 0072specialize beta_at_unique (S x1)
  73. 0073apply beta_at_unique
  74. 0074exact hright
  75. 0075exact hlift_right
  76. 0076have hbounded_even : exists w. (((exists ff_h_enr_bounded_even_entry. ff_h_enr_bounded_even_entry + S (w) = S ((S (t + t)) * c)) /\ exists ff_q_enr_bounded_even_entry. b = ff_q_enr_bounded_even_entry * S ((S (t + t)) * c) + (w))) /\ (exists wpo_gap_enr_bounded_even_value. wpo_gap_enr_bounded_even_value + S (w) = n)
  77. 0077specialize hbounded (t + t)
  78. 0078apply hbounded
  79. 0079exact heven_raw
  80. 0080cases hbounded_even
  81. 0081cases hbounded_even_witness
  82. 0082have hsource_eq : x = x2
  83. 0083specialize beta_at_unique b
  84. 0084specialize beta_at_unique c
  85. 0085specialize beta_at_unique (t + t)
  86. 0086specialize beta_at_unique x
  87. 0087specialize beta_at_unique x2
  88. 0088apply beta_at_unique
  89. 0089exact horbit_witness_witness_left
  90. 0090exact hbounded_even_witness_left
  91. 0091have hsource_bound : exists gap. gap + S x = n
  92. 0092rewrite hsource_eq
  93. 0093exact hbounded_even_witness_right
  94. 0094have hprefix_data : exists y. (((exists ff_h_enr_prefix_at_x_entry. ff_h_enr_prefix_at_x_entry + S (y) = S ((S (x)) * v)) /\ exists ff_q_enr_prefix_at_x_entry. u = ff_q_enr_prefix_at_x_entry * S ((S (x)) * v) + (y))) /\ ((exists esip_gap_enr_prefix_at_x_relation_index_bound. esip_gap_enr_prefix_at_x_relation_index_bound + S (x) = n) /\ ((((~((S x) = 0) /\ (exists esip_gap_enr_prefix_at_x_relation_scaled_left_bound. esip_gap_enr_prefix_at_x_relation_scaled_left_bound + S (S x) = p))) /\ (((~(y = 0) /\ (exists esip_gap_enr_prefix_at_x_relation_scaled_right_bound. esip_gap_enr_prefix_at_x_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_enr_prefix_at_x_relation_scaled_mod esi_mod_right_enr_prefix_at_x_relation_scaled_mod. ((S x) * y) + p * esi_mod_left_enr_prefix_at_x_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_at_x_relation_scaled_mod)))))
  95. 0095specialize hprefix x
  96. 0096apply hprefix
  97. 0097exact hsource_bound
  98. 0098cases hprefix_data
  99. 0099cases hprefix_data_witness
  100. 0100cases hprefix_data_witness_right
  101. 0101cases hprefix_data_witness_right_right
  102. 0102cases hprefix_data_witness_right_right_right
  103. 0103have hmate_eq : x3 = S x1
  104. 0104specialize beta_at_unique u
  105. 0105specialize beta_at_unique v
  106. 0106specialize beta_at_unique x
  107. 0107specialize beta_at_unique x3
  108. 0108specialize beta_at_unique (S x1)
  109. 0109apply beta_at_unique
  110. 0110exact hprefix_data_witness_left
  111. 0111exact horbit_witness_witness_right_right
  112. 0112rewrite hleft_eq
  113. 0113rewrite hright_eq
  114. 0114rewrite <- hmate_eq
  115. 0115exact hprefix_data_witness_right_right_right_right