PA00AQ

prime_inverse_prefix_nonendpoint_mate

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

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

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-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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