PA00AR

prime_choose_unused_nonendpoint_orbit

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

Choose an omitted nonendpoint index and extract its distinct, nonendpoint inverse mate together with both decoded directions.

Exact expanded PA statement

forall p n u v b c l r. p = S n -> ((~(p = 1) /\ forall wip_prime_left_choose_orbit_prime wip_prime_right_choose_orbit_prime. p = wip_prime_left_choose_orbit_prime * wip_prime_right_choose_orbit_prime -> wip_prime_left_choose_orbit_prime = 1 \/ wip_prime_right_choose_orbit_prime = 1)) -> (forall wip_index_choose_orbit_full_prefix. (exists wip_gap_choose_orbit_full_prefix_prefix_bound. wip_gap_choose_orbit_full_prefix_prefix_bound + S wip_index_choose_orbit_full_prefix = n) -> exists wip_mate_choose_orbit_full_prefix. ((((exists wip_beta_height_choose_orbit_full_prefix_decoded. wip_beta_height_choose_orbit_full_prefix_decoded + S (wip_mate_choose_orbit_full_prefix) = S ((S (wip_index_choose_orbit_full_prefix)) * v)) /\ exists wip_beta_quotient_choose_orbit_full_prefix_decoded. u = wip_beta_quotient_choose_orbit_full_prefix_decoded * S ((S (wip_index_choose_orbit_full_prefix)) * v) + (wip_mate_choose_orbit_full_prefix))) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_index_bound. wip_gap_choose_orbit_full_prefix_inverse_index_bound + S wip_index_choose_orbit_full_prefix = n) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_mate_bound. wip_gap_choose_orbit_full_prefix_inverse_mate_bound + S wip_mate_choose_orbit_full_prefix = n) /\ (exists wip_mod_left_choose_orbit_full_prefix_inverse_mod wip_mod_right_choose_orbit_full_prefix_inverse_mod. ((S wip_index_choose_orbit_full_prefix) * S wip_mate_choose_orbit_full_prefix) + p * wip_mod_left_choose_orbit_full_prefix_inverse_mod = 1 + p * wip_mod_right_choose_orbit_full_prefix_inverse_mod))))) -> n = S r -> (exists h. h + S (S (S l)) = n) -> (exists i j. ((exists wpo_gap_choose_orbit_source_bound. wpo_gap_choose_orbit_source_bound + S (i) = n) /\ ((~(i = 0) /\ ~((S i) = n)) /\ ((~(exists wpo_index_choose_orbit_source_omit_contains. ((exists wpo_gap_choose_orbit_source_omit_contains_bound. wpo_gap_choose_orbit_source_omit_contains_bound + S (wpo_index_choose_orbit_source_omit_contains) = l) /\ (((exists wpo_beta_height_choose_orbit_source_omit_contains_entry. wpo_beta_height_choose_orbit_source_omit_contains_entry + S (i) = S ((S (wpo_index_choose_orbit_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_choose_orbit_source_omit_contains_entry. b = wpo_beta_quotient_choose_orbit_source_omit_contains_entry * S ((S (wpo_index_choose_orbit_source_omit_contains)) * c) + (i)))))) /\ ((((exists wpo_beta_height_choose_orbit_forward. wpo_beta_height_choose_orbit_forward + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_choose_orbit_forward. u = wpo_beta_quotient_choose_orbit_forward * S ((S (i)) * v) + (j))) /\ ((exists wpo_gap_choose_orbit_mate_bound. wpo_gap_choose_orbit_mate_bound + S (j) = n) /\ ((~(j = 0) /\ ~((S j) = n)) /\ (~(i = j) /\ (((exists wpo_beta_height_choose_orbit_back. wpo_beta_height_choose_orbit_back + S (i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_choose_orbit_back. u = wpo_beta_quotient_choose_orbit_back * S ((S (j)) * v) + (i)))))))))))

Structural proof guide

Generated structural guide

Choose an omitted nonendpoint index and extract its distinct, nonendpoint inverse mate together with both decoded directions.

Use the direct prerequisites finite_prefix_choose_unused_nonendpoint, prime_inverse_prefix_nonendpoint_mate, prime_inverse_prefix_nonendpoint_not_fixed, inverse_prefix_involutive as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (8).

Referenced ingredients

PA00AE finite_prefix_choose_unused_nonendpoint PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AI prime_inverse_prefix_nonendpoint_not_fixed PA00AN inverse_prefix_involutive

Proof neighborhood

Direct dependencies

PA00AE finite_prefix_choose_unused_nonendpoint PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AI prime_inverse_prefix_nonendpoint_not_fixed PA00AN inverse_prefix_involutive

Direct dependents

PA00AV prime_pair_order_choose_append

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 u
  4. 0004intro v
  5. 0005intro b
  6. 0006intro c
  7. 0007intro l
  8. 0008intro r
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hprefix
  12. 0012intro hnr
  13. 0013intro hshort
  14. 0014have hchoose : exists y. ((exists wpo_gap_choose_result_bound. wpo_gap_choose_result_bound + S (y) = n) /\ ((~(y = 0) /\ ~((S y) = n)) /\ (~(exists wpo_index_choose_result_omit_contains. ((exists wpo_gap_choose_result_omit_contains_bound. wpo_gap_choose_result_omit_contains_bound + S (wpo_index_choose_result_omit_contains) = l) /\ (((exists wpo_beta_height_choose_result_omit_contains_entry. wpo_beta_height_choose_result_omit_contains_entry + S (y) = S ((S (wpo_index_choose_result_omit_contains)) * c)) /\ exists wpo_beta_quotient_choose_result_omit_contains_entry. b = wpo_beta_quotient_choose_result_omit_contains_entry * S ((S (wpo_index_choose_result_omit_contains)) * c) + (y))))))))
  15. 0015specialize finite_prefix_choose_unused_nonendpoint b
  16. 0016specialize finite_prefix_choose_unused_nonendpoint c
  17. 0017specialize finite_prefix_choose_unused_nonendpoint l
  18. 0018specialize finite_prefix_choose_unused_nonendpoint n
  19. 0019specialize finite_prefix_choose_unused_nonendpoint r
  20. 0020apply finite_prefix_choose_unused_nonendpoint
  21. 0021exact hnr
  22. 0022exact hshort
  23. 0023cases hchoose
  24. 0024cases hchoose_witness
  25. 0025cases hchoose_witness_right
  26. 0026have hmate_prefix : forall wip_index_choose_orbit_full_prefix. (exists wip_gap_choose_orbit_full_prefix_prefix_bound. wip_gap_choose_orbit_full_prefix_prefix_bound + S wip_index_choose_orbit_full_prefix = n) -> exists wip_mate_choose_orbit_full_prefix. ((((exists wip_beta_height_choose_orbit_full_prefix_decoded. wip_beta_height_choose_orbit_full_prefix_decoded + S (wip_mate_choose_orbit_full_prefix) = S ((S (wip_index_choose_orbit_full_prefix)) * v)) /\ exists wip_beta_quotient_choose_orbit_full_prefix_decoded. u = wip_beta_quotient_choose_orbit_full_prefix_decoded * S ((S (wip_index_choose_orbit_full_prefix)) * v) + (wip_mate_choose_orbit_full_prefix))) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_index_bound. wip_gap_choose_orbit_full_prefix_inverse_index_bound + S wip_index_choose_orbit_full_prefix = n) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_mate_bound. wip_gap_choose_orbit_full_prefix_inverse_mate_bound + S wip_mate_choose_orbit_full_prefix = n) /\ (exists wip_mod_left_choose_orbit_full_prefix_inverse_mod wip_mod_right_choose_orbit_full_prefix_inverse_mod. ((S wip_index_choose_orbit_full_prefix) * S wip_mate_choose_orbit_full_prefix) + p * wip_mod_left_choose_orbit_full_prefix_inverse_mod = 1 + p * wip_mod_right_choose_orbit_full_prefix_inverse_mod))))
  27. 0027exact hprefix
  28. 0028have hnonfixed_prefix : forall wip_index_choose_orbit_full_prefix. (exists wip_gap_choose_orbit_full_prefix_prefix_bound. wip_gap_choose_orbit_full_prefix_prefix_bound + S wip_index_choose_orbit_full_prefix = n) -> exists wip_mate_choose_orbit_full_prefix. ((((exists wip_beta_height_choose_orbit_full_prefix_decoded. wip_beta_height_choose_orbit_full_prefix_decoded + S (wip_mate_choose_orbit_full_prefix) = S ((S (wip_index_choose_orbit_full_prefix)) * v)) /\ exists wip_beta_quotient_choose_orbit_full_prefix_decoded. u = wip_beta_quotient_choose_orbit_full_prefix_decoded * S ((S (wip_index_choose_orbit_full_prefix)) * v) + (wip_mate_choose_orbit_full_prefix))) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_index_bound. wip_gap_choose_orbit_full_prefix_inverse_index_bound + S wip_index_choose_orbit_full_prefix = n) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_mate_bound. wip_gap_choose_orbit_full_prefix_inverse_mate_bound + S wip_mate_choose_orbit_full_prefix = n) /\ (exists wip_mod_left_choose_orbit_full_prefix_inverse_mod wip_mod_right_choose_orbit_full_prefix_inverse_mod. ((S wip_index_choose_orbit_full_prefix) * S wip_mate_choose_orbit_full_prefix) + p * wip_mod_left_choose_orbit_full_prefix_inverse_mod = 1 + p * wip_mod_right_choose_orbit_full_prefix_inverse_mod))))
  29. 0029exact hprefix
  30. 0030have hback_prefix : forall wip_index_choose_orbit_full_prefix. (exists wip_gap_choose_orbit_full_prefix_prefix_bound. wip_gap_choose_orbit_full_prefix_prefix_bound + S wip_index_choose_orbit_full_prefix = n) -> exists wip_mate_choose_orbit_full_prefix. ((((exists wip_beta_height_choose_orbit_full_prefix_decoded. wip_beta_height_choose_orbit_full_prefix_decoded + S (wip_mate_choose_orbit_full_prefix) = S ((S (wip_index_choose_orbit_full_prefix)) * v)) /\ exists wip_beta_quotient_choose_orbit_full_prefix_decoded. u = wip_beta_quotient_choose_orbit_full_prefix_decoded * S ((S (wip_index_choose_orbit_full_prefix)) * v) + (wip_mate_choose_orbit_full_prefix))) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_index_bound. wip_gap_choose_orbit_full_prefix_inverse_index_bound + S wip_index_choose_orbit_full_prefix = n) /\ ((exists wip_gap_choose_orbit_full_prefix_inverse_mate_bound. wip_gap_choose_orbit_full_prefix_inverse_mate_bound + S wip_mate_choose_orbit_full_prefix = n) /\ (exists wip_mod_left_choose_orbit_full_prefix_inverse_mod wip_mod_right_choose_orbit_full_prefix_inverse_mod. ((S wip_index_choose_orbit_full_prefix) * S wip_mate_choose_orbit_full_prefix) + p * wip_mod_left_choose_orbit_full_prefix_inverse_mod = 1 + p * wip_mod_right_choose_orbit_full_prefix_inverse_mod))))
  31. 0031exact hprefix
  32. 0032have hstored : exists j. ((((exists wpo_beta_height_choose_orbit_stored_x_entry. wpo_beta_height_choose_orbit_stored_x_entry + S (j) = S ((S (x)) * v)) /\ exists wpo_beta_quotient_choose_orbit_stored_x_entry. u = wpo_beta_quotient_choose_orbit_stored_x_entry * S ((S (x)) * v) + (j))) /\ ((exists wip_gap_choose_orbit_stored_x_inverse_index_bound. wip_gap_choose_orbit_stored_x_inverse_index_bound + S x = n) /\ ((exists wip_gap_choose_orbit_stored_x_inverse_mate_bound. wip_gap_choose_orbit_stored_x_inverse_mate_bound + S j = n) /\ (exists wip_mod_left_choose_orbit_stored_x_inverse_mod wip_mod_right_choose_orbit_stored_x_inverse_mod. ((S x) * S j) + p * wip_mod_left_choose_orbit_stored_x_inverse_mod = 1 + p * wip_mod_right_choose_orbit_stored_x_inverse_mod))))
  33. 0033specialize hprefix x
  34. 0034apply hprefix
  35. 0035exact hchoose_witness_left
  36. 0036cases hstored
  37. 0037cases hstored_witness
  38. 0038have hmate_nonendpoint : (~(x1 = 0) /\ ~((S x1) = n))
  39. 0039specialize prime_inverse_prefix_nonendpoint_mate p
  40. 0040specialize prime_inverse_prefix_nonendpoint_mate n
  41. 0041specialize prime_inverse_prefix_nonendpoint_mate u
  42. 0042specialize prime_inverse_prefix_nonendpoint_mate v
  43. 0043specialize prime_inverse_prefix_nonendpoint_mate x
  44. 0044specialize prime_inverse_prefix_nonendpoint_mate x1
  45. 0045apply prime_inverse_prefix_nonendpoint_mate
  46. 0046exact hpn
  47. 0047exact hp
  48. 0048exact hmate_prefix
  49. 0049exact hchoose_witness_left
  50. 0050exact hstored_witness_left
  51. 0051exact hchoose_witness_right_left
  52. 0052have hnonfixed : ~(x = x1)
  53. 0053intro hxx1
  54. 0054specialize prime_inverse_prefix_nonendpoint_not_fixed p
  55. 0055specialize prime_inverse_prefix_nonendpoint_not_fixed n
  56. 0056specialize prime_inverse_prefix_nonendpoint_not_fixed u
  57. 0057specialize prime_inverse_prefix_nonendpoint_not_fixed v
  58. 0058specialize prime_inverse_prefix_nonendpoint_not_fixed x
  59. 0059specialize prime_inverse_prefix_nonendpoint_not_fixed x1
  60. 0060apply prime_inverse_prefix_nonendpoint_not_fixed
  61. 0061exact hpn
  62. 0062exact hp
  63. 0063exact hnonfixed_prefix
  64. 0064exact hchoose_witness_left
  65. 0065exact hstored_witness_left
  66. 0066exact hchoose_witness_right_left
  67. 0067exact hxx1
  68. 0068have hback : ((exists wpo_gap_choose_orbit_back_x_bound. wpo_gap_choose_orbit_back_x_bound + S (x1) = n) /\ (((exists wpo_beta_height_choose_orbit_back_x_entry. wpo_beta_height_choose_orbit_back_x_entry + S (x) = S ((S (x1)) * v)) /\ exists wpo_beta_quotient_choose_orbit_back_x_entry. u = wpo_beta_quotient_choose_orbit_back_x_entry * S ((S (x1)) * v) + (x))))
  69. 0069specialize inverse_prefix_involutive p
  70. 0070specialize inverse_prefix_involutive n
  71. 0071specialize inverse_prefix_involutive u
  72. 0072specialize inverse_prefix_involutive v
  73. 0073specialize inverse_prefix_involutive x
  74. 0074specialize inverse_prefix_involutive x1
  75. 0075apply inverse_prefix_involutive
  76. 0076exact hpn
  77. 0077exact hback_prefix
  78. 0078exact hchoose_witness_left
  79. 0079exact hstored_witness_left
  80. 0080cases hback
  81. 0081exists x
  82. 0082exists x1
  83. 0083split
  84. 0084exact hchoose_witness_left
  85. 0085split
  86. 0086exact hchoose_witness_right_left
  87. 0087split
  88. 0088exact hchoose_witness_right_right
  89. 0089split
  90. 0090exact hstored_witness_left
  91. 0091split
  92. 0092exact hback_left
  93. 0093split
  94. 0094exact hmate_nonendpoint
  95. 0095split
  96. 0096exact hnonfixed
  97. 0097exact hback_right