PA00AQ

prime_inverse_prefix_nonendpoint_mate

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

The decoded mate of a nonendpoint inverse index is also a nonendpoint.

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 n b c i j. p = S n -> ((~(p = 1) /\ forall wip_prime_left_orbit_prime wip_prime_right_orbit_prime. p = wip_prime_left_orbit_prime * wip_prime_right_orbit_prime -> wip_prime_left_orbit_prime = 1 \/ wip_prime_right_orbit_prime = 1)) -> (forall wip_index_orbit_prefix. (exists wip_gap_orbit_prefix_prefix_bound. wip_gap_orbit_prefix_prefix_bound + S wip_index_orbit_prefix = n) -> exists wip_mate_orbit_prefix. ((((exists wip_beta_height_orbit_prefix_decoded. wip_beta_height_orbit_prefix_decoded + S (wip_mate_orbit_prefix) = S ((S (wip_index_orbit_prefix)) * c)) /\ exists wip_beta_quotient_orbit_prefix_decoded. b = wip_beta_quotient_orbit_prefix_decoded * S ((S (wip_index_orbit_prefix)) * c) + (wip_mate_orbit_prefix))) /\ ((exists wip_gap_orbit_prefix_inverse_index_bound. wip_gap_orbit_prefix_inverse_index_bound + S wip_index_orbit_prefix = n) /\ ((exists wip_gap_orbit_prefix_inverse_mate_bound. wip_gap_orbit_prefix_inverse_mate_bound + S wip_mate_orbit_prefix = n) /\ (exists wip_mod_left_orbit_prefix_inverse_mod wip_mod_right_orbit_prefix_inverse_mod. ((S wip_index_orbit_prefix) * S wip_mate_orbit_prefix) + p * wip_mod_left_orbit_prefix_inverse_mod = 1 + p * wip_mod_right_orbit_prefix_inverse_mod))))) -> (exists wip_gap_orbit_source_bound. wip_gap_orbit_source_bound + S i = n) -> (((exists wip_beta_height_orbit_source_entry. wip_beta_height_orbit_source_entry + S (j) = S ((S (i)) * c)) /\ exists wip_beta_quotient_orbit_source_entry. b = wip_beta_quotient_orbit_source_entry * S ((S (i)) * c) + (j))) -> ((~(i = 0) /\ ~((S i) = n))) -> ((~(j = 0) /\ ~((S j) = n)))

Structural proof guide

Generated structural guide

The decoded mate of a nonendpoint inverse index is also a nonendpoint.

Use the direct prerequisites prime_inverse_prefix_nonendpoint_not_fixed, inverse_prefix_involutive, prime_is_succ_succ, succ_injective, inverse_prefix_zero_fixed, inverse_prefix_last_fixed, beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (15), equality transport (4).

Referenced ingredients

PA00AI prime_inverse_prefix_nonendpoint_not_fixed PA00AN inverse_prefix_involutive PA0061 prime_is_succ_succ PA003V succ_injective PA00AO inverse_prefix_zero_fixed PA00AP inverse_prefix_last_fixed PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA00AI prime_inverse_prefix_nonendpoint_not_fixed PA00AN inverse_prefix_involutive PA0061 prime_is_succ_succ PA003V succ_injective PA00AO inverse_prefix_zero_fixed PA00AP inverse_prefix_last_fixed PA002F beta_at_unique

Direct dependents

PA00AR prime_choose_unused_nonendpoint_orbit

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

128 script commands · 32 reading checkpoints · 15 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 (7)
prime inverse prefix nonendpoint not fixedinverse prefix involutiveprime is succ succsucc injectiveinverse prefix zero fixedinverse prefix last fixedbeta at unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro i
  6. L6
    intro j
  7. L7
    intro hpn
  8. L8
    intro hp
  9. L9
    intro hprefix
  10. L10
    intro hi
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hat
  2. L12
    intro hnonendpoint
03Establish hnonfixedL13–22

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

  1. L13
    have hnonfixed : ~(i = j)
  2. L14
    specialize prime_inverse_prefix_nonendpoint_not_fixed p
  3. L15
    specialize prime_inverse_prefix_nonendpoint_not_fixed n
  4. L16
    specialize prime_inverse_prefix_nonendpoint_not_fixed b
  5. L17
    specialize prime_inverse_prefix_nonendpoint_not_fixed c
  6. L18
    specialize prime_inverse_prefix_nonendpoint_not_fixed i
  7. L19
    specialize prime_inverse_prefix_nonendpoint_not_fixed j
  8. L20
    intro hij
  9. L21
    apply prime_inverse_prefix_nonendpoint_not_fixed
  10. L22
    exact hpn
04Use earlier factsL23–28

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

  1. L23
    exact hp
  2. L24
    exact hprefix
  3. L25
    exact hi
  4. L26
    exact hat
  5. L27
    exact hnonendpoint
  6. L28
    exact hij
05Establish horbitL29–38

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

  1. L29
    have horbit : ((exists wip_gap_orbit_mate_bound. wip_gap_orbit_mate_bound + S j = n) /\ (((exists wip_beta_height_orbit_back_entry. wip_beta_height_orbit_back_entry + S (i) = S ((S (j)) * c)) /\ exists wip_beta_quotient_orbit_back_entry. b = wip_beta_quotient_orbit_back_entry * S ((S (j)) * c) + (i))))
  2. L30
    specialize inverse_prefix_involutive p
  3. L31
    specialize inverse_prefix_involutive n
  4. L32
    specialize inverse_prefix_involutive b
  5. L33
    specialize inverse_prefix_involutive c
  6. L34
    specialize inverse_prefix_involutive i
  7. L35
    specialize inverse_prefix_involutive j
  8. L36
    apply inverse_prefix_involutive
  9. L37
    exact hpn
  10. L38
    exact hprefix
06Use earlier factsL39–40

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

  1. L39
    exact hi
  2. L40
    exact hat
07Separate the logical casesL41–41

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

  1. L41
    cases horbit
08Establish hsucc_shapeL42–43

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

  1. L42
    have hsucc_shape : forall a d. S a = S d -> a = d
  2. L43
    exact succ_injective
09Establish hsucc_mateL44–45

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

  1. L44
    have hsucc_mate : forall a d. S a = S d -> a = d
  2. L45
    exact succ_injective
10Establish hprime_shapeL46–49

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

  1. L46
    have hprime_shape : exists k. p = S (S k)
  2. L47
    specialize prime_is_succ_succ p
  3. L48
    apply prime_is_succ_succ
  4. L49
    exact hp
11Separate the logical casesL50–50

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

  1. L50
    cases hprime_shape
12Establish hnkL51–58

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

  1. L51
    have hnk : n = S x
  2. L52
    specialize hsucc_shape n
  3. L53
    specialize hsucc_shape (S x)
  4. L54
    apply hsucc_shape
  5. L55
    trans p
  6. L56
    symm
  7. L57
    exact hpn
  8. L58
    exact hprime_shape_witness
13Establish hzeroL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply inverse prefix zero fixed.

  1. L59
    have hzero : ((exists wio_beta_height_orbit_zero_fixed. wio_beta_height_orbit_zero_fixed + S (0) = S ((S (0)) * c)) /\ exists wio_beta_quotient_orbit_zero_fixed. b = wio_beta_quotient_orbit_zero_fixed * S ((S (0)) * c) + (0))
  2. L60
    specialize inverse_prefix_zero_fixed p
  3. L61
    specialize inverse_prefix_zero_fixed n
  4. L62
    specialize inverse_prefix_zero_fixed x
  5. L63
    specialize inverse_prefix_zero_fixed b
  6. L64
    specialize inverse_prefix_zero_fixed c
  7. L65
    apply inverse_prefix_zero_fixed
  8. L66
    exact hpn
  9. L67
    exact hnk
  10. L68
    exact hprefix
14Establish hlastL69–78

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply inverse prefix last fixed.

  1. L69
    have hlast : ((exists wip_beta_height_orbit_last_fixed. wip_beta_height_orbit_last_fixed + S (x) = S ((S (x)) * c)) /\ exists wip_beta_quotient_orbit_last_fixed. b = wip_beta_quotient_orbit_last_fixed * S ((S (x)) * c) + (x))
  2. L70
    specialize inverse_prefix_last_fixed p
  3. L71
    specialize inverse_prefix_last_fixed n
  4. L72
    specialize inverse_prefix_last_fixed x
  5. L73
    specialize inverse_prefix_last_fixed b
  6. L74
    specialize inverse_prefix_last_fixed c
  7. L75
    apply inverse_prefix_last_fixed
  8. L76
    exact hpn
  9. L77
    exact hnk
  10. L78
    exact hprefix
15Separate the logical casesL79–79

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

  1. L79
    split
16Fix variables and assumptionsL80–80

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

  1. L80
    intro hjzero
17Establish hback_zero_rawL81–82

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

  1. L81
    have hback_zero_raw : ((exists wip_beta_height_orbit_back_entry. wip_beta_height_orbit_back_entry + S (i) = S ((S (j)) * c)) /\ exists wip_beta_quotient_orbit_back_entry. b = wip_beta_quotient_orbit_back_entry * S ((S (j)) * c) + (i))
  2. L82
    exact horbit_right
18Establish hback_zeroL83–86

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

  1. L83
    have hback_zero : ((exists wio_beta_height_orbit_back_zero. wio_beta_height_orbit_back_zero + S (i) = S ((S (0)) * c)) /\ exists wio_beta_quotient_orbit_back_zero. b = wio_beta_quotient_orbit_back_zero * S ((S (0)) * c) + (i))
  2. L84
    rewrite hjzero at hback_zero_raw
  3. L85
    rewrite hjzero at hback_zero_raw
  4. L86
    exact hback_zero_raw
19Establish hi0L87–96

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

  1. L87
    have hi0 : i = 0
  2. L88
    specialize beta_at_unique b
  3. L89
    specialize beta_at_unique c
  4. L90
    specialize beta_at_unique 0
  5. L91
    specialize beta_at_unique i
  6. L92
    specialize beta_at_unique 0
  7. L93
    apply beta_at_unique
  8. L94
    exact hback_zero
  9. L95
    exact hzero
  10. L96
    apply hnonfixed
20Calculate and transport equalitiesL97–97

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

  1. L97
    trans 0
21Use earlier factsL98–98

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

  1. L98
    exact hi0
22Calculate and transport equalitiesL99–99

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

  1. L99
    symm
23Use earlier factsL100–100

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

  1. L100
    exact hjzero
24Fix variables and assumptionsL101–101

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

  1. L101
    intro hjlast
25Establish hjxL102–108

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

  1. L102
    have hjx : j = x
  2. L103
    specialize hsucc_mate j
  3. L104
    specialize hsucc_mate x
  4. L105
    apply hsucc_mate
  5. L106
    trans n
  6. L107
    exact hjlast
  7. L108
    exact hnk
26Establish hback_last_rawL109–110

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

  1. L109
    have hback_last_raw : ((exists wip_beta_height_orbit_back_entry. wip_beta_height_orbit_back_entry + S (i) = S ((S (j)) * c)) /\ exists wip_beta_quotient_orbit_back_entry. b = wip_beta_quotient_orbit_back_entry * S ((S (j)) * c) + (i))
  2. L110
    exact horbit_right
27Establish hback_lastL111–114

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

  1. L111
    have hback_last : ((exists wip_beta_height_orbit_back_last. wip_beta_height_orbit_back_last + S (i) = S ((S (x)) * c)) /\ exists wip_beta_quotient_orbit_back_last. b = wip_beta_quotient_orbit_back_last * S ((S (x)) * c) + (i))
  2. L112
    rewrite hjx at hback_last_raw
  3. L113
    rewrite hjx at hback_last_raw
  4. L114
    exact hback_last_raw
28Establish hixL115–124

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

  1. L115
    have hix : i = x
  2. L116
    specialize beta_at_unique b
  3. L117
    specialize beta_at_unique c
  4. L118
    specialize beta_at_unique x
  5. L119
    specialize beta_at_unique i
  6. L120
    specialize beta_at_unique x
  7. L121
    apply beta_at_unique
  8. L122
    exact hback_last
  9. L123
    exact hlast
  10. L124
    apply hnonfixed
29Calculate and transport equalitiesL125–125

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

  1. L125
    trans x
30Use earlier factsL126–126

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

  1. L126
    exact hix
31Calculate and transport equalitiesL127–127

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

  1. L127
    symm
32Use earlier factsL128–128

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

  1. L128
    exact hjx

Library-wide reading audit

Original exact command ledger · 128 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro i
  6. 0006intro j
  7. 0007intro hpn
  8. 0008intro hp
  9. 0009intro hprefix
  10. 0010intro hi
  11. 0011intro hat
  12. 0012intro hnonendpoint
  13. 0013have hnonfixed : ~(i = j)
  14. 0014specialize prime_inverse_prefix_nonendpoint_not_fixed p
  15. 0015specialize prime_inverse_prefix_nonendpoint_not_fixed n
  16. 0016specialize prime_inverse_prefix_nonendpoint_not_fixed b
  17. 0017specialize prime_inverse_prefix_nonendpoint_not_fixed c
  18. 0018specialize prime_inverse_prefix_nonendpoint_not_fixed i
  19. 0019specialize prime_inverse_prefix_nonendpoint_not_fixed j
  20. 0020intro hij
  21. 0021apply prime_inverse_prefix_nonendpoint_not_fixed
  22. 0022exact hpn
  23. 0023exact hp
  24. 0024exact hprefix
  25. 0025exact hi
  26. 0026exact hat
  27. 0027exact hnonendpoint
  28. 0028exact hij
  29. 0029have horbit : ((exists wip_gap_orbit_mate_bound. wip_gap_orbit_mate_bound + S j = n) /\ (((exists wip_beta_height_orbit_back_entry. wip_beta_height_orbit_back_entry + S (i) = S ((S (j)) * c)) /\ exists wip_beta_quotient_orbit_back_entry. b = wip_beta_quotient_orbit_back_entry * S ((S (j)) * c) + (i))))
  30. 0030specialize inverse_prefix_involutive p
  31. 0031specialize inverse_prefix_involutive n
  32. 0032specialize inverse_prefix_involutive b
  33. 0033specialize inverse_prefix_involutive c
  34. 0034specialize inverse_prefix_involutive i
  35. 0035specialize inverse_prefix_involutive j
  36. 0036apply inverse_prefix_involutive
  37. 0037exact hpn
  38. 0038exact hprefix
  39. 0039exact hi
  40. 0040exact hat
  41. 0041cases horbit
  42. 0042have hsucc_shape : forall a d. S a = S d -> a = d
  43. 0043exact succ_injective
  44. 0044have hsucc_mate : forall a d. S a = S d -> a = d
  45. 0045exact succ_injective
  46. 0046have hprime_shape : exists k. p = S (S k)
  47. 0047specialize prime_is_succ_succ p
  48. 0048apply prime_is_succ_succ
  49. 0049exact hp
  50. 0050cases hprime_shape
  51. 0051have hnk : n = S x
  52. 0052specialize hsucc_shape n
  53. 0053specialize hsucc_shape (S x)
  54. 0054apply hsucc_shape
  55. 0055trans p
  56. 0056symm
  57. 0057exact hpn
  58. 0058exact hprime_shape_witness
  59. 0059have hzero : ((exists wio_beta_height_orbit_zero_fixed. wio_beta_height_orbit_zero_fixed + S (0) = S ((S (0)) * c)) /\ exists wio_beta_quotient_orbit_zero_fixed. b = wio_beta_quotient_orbit_zero_fixed * S ((S (0)) * c) + (0))
  60. 0060specialize inverse_prefix_zero_fixed p
  61. 0061specialize inverse_prefix_zero_fixed n
  62. 0062specialize inverse_prefix_zero_fixed x
  63. 0063specialize inverse_prefix_zero_fixed b
  64. 0064specialize inverse_prefix_zero_fixed c
  65. 0065apply inverse_prefix_zero_fixed
  66. 0066exact hpn
  67. 0067exact hnk
  68. 0068exact hprefix
  69. 0069have hlast : ((exists wip_beta_height_orbit_last_fixed. wip_beta_height_orbit_last_fixed + S (x) = S ((S (x)) * c)) /\ exists wip_beta_quotient_orbit_last_fixed. b = wip_beta_quotient_orbit_last_fixed * S ((S (x)) * c) + (x))
  70. 0070specialize inverse_prefix_last_fixed p
  71. 0071specialize inverse_prefix_last_fixed n
  72. 0072specialize inverse_prefix_last_fixed x
  73. 0073specialize inverse_prefix_last_fixed b
  74. 0074specialize inverse_prefix_last_fixed c
  75. 0075apply inverse_prefix_last_fixed
  76. 0076exact hpn
  77. 0077exact hnk
  78. 0078exact hprefix
  79. 0079split
  80. 0080intro hjzero
  81. 0081have hback_zero_raw : ((exists wip_beta_height_orbit_back_entry. wip_beta_height_orbit_back_entry + S (i) = S ((S (j)) * c)) /\ exists wip_beta_quotient_orbit_back_entry. b = wip_beta_quotient_orbit_back_entry * S ((S (j)) * c) + (i))
  82. 0082exact horbit_right
  83. 0083have hback_zero : ((exists wio_beta_height_orbit_back_zero. wio_beta_height_orbit_back_zero + S (i) = S ((S (0)) * c)) /\ exists wio_beta_quotient_orbit_back_zero. b = wio_beta_quotient_orbit_back_zero * S ((S (0)) * c) + (i))
  84. 0084rewrite hjzero at hback_zero_raw
  85. 0085rewrite hjzero at hback_zero_raw
  86. 0086exact hback_zero_raw
  87. 0087have hi0 : i = 0
  88. 0088specialize beta_at_unique b
  89. 0089specialize beta_at_unique c
  90. 0090specialize beta_at_unique 0
  91. 0091specialize beta_at_unique i
  92. 0092specialize beta_at_unique 0
  93. 0093apply beta_at_unique
  94. 0094exact hback_zero
  95. 0095exact hzero
  96. 0096apply hnonfixed
  97. 0097trans 0
  98. 0098exact hi0
  99. 0099symm
  100. 0100exact hjzero
  101. 0101intro hjlast
  102. 0102have hjx : j = x
  103. 0103specialize hsucc_mate j
  104. 0104specialize hsucc_mate x
  105. 0105apply hsucc_mate
  106. 0106trans n
  107. 0107exact hjlast
  108. 0108exact hnk
  109. 0109have hback_last_raw : ((exists wip_beta_height_orbit_back_entry. wip_beta_height_orbit_back_entry + S (i) = S ((S (j)) * c)) /\ exists wip_beta_quotient_orbit_back_entry. b = wip_beta_quotient_orbit_back_entry * S ((S (j)) * c) + (i))
  110. 0110exact horbit_right
  111. 0111have hback_last : ((exists wip_beta_height_orbit_back_last. wip_beta_height_orbit_back_last + S (i) = S ((S (x)) * c)) /\ exists wip_beta_quotient_orbit_back_last. b = wip_beta_quotient_orbit_back_last * S ((S (x)) * c) + (i))
  112. 0112rewrite hjx at hback_last_raw
  113. 0113rewrite hjx at hback_last_raw
  114. 0114exact hback_last_raw
  115. 0115have hix : i = x
  116. 0116specialize beta_at_unique b
  117. 0117specialize beta_at_unique c
  118. 0118specialize beta_at_unique x
  119. 0119specialize beta_at_unique i
  120. 0120specialize beta_at_unique x
  121. 0121apply beta_at_unique
  122. 0122exact hback_last
  123. 0123exact hlast
  124. 0124apply hnonfixed
  125. 0125trans x
  126. 0126exact hix
  127. 0127symm
  128. 0128exact hjx