PA00AR

prime_choose_unused_nonendpoint_orbit

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

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

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

Read the argument

Proof checkpoints

97 script commands · 31 reading checkpoints · 8 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 (4)
finite prefix choose unused nonendpointprime inverse prefix nonendpoint mateprime inverse prefix nonendpoint not fixedinverse prefix involutive

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 n
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro l
  8. L8
    intro r
  9. L9
    intro hpn
  10. L10
    intro hp
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hprefix
  2. L12
    intro hnr
  3. L13
    intro hshort
03Establish hchooseL14–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite prefix choose unused nonendpoint.

  1. L14
    have hchoose : ∃ y. Lt(y,n) ∧ (¬y = 0 ∧ ¬S y = n ∧ ¬ContainsPrefix(b,c,l,y))Definitions: LtContainsPrefix
  2. L15
    specialize finite_prefix_choose_unused_nonendpoint b
  3. L16
    specialize finite_prefix_choose_unused_nonendpoint c
  4. L17
    specialize finite_prefix_choose_unused_nonendpoint l
  5. L18
    specialize finite_prefix_choose_unused_nonendpoint n
  6. L19
    specialize finite_prefix_choose_unused_nonendpoint r
  7. L20
    apply finite_prefix_choose_unused_nonendpoint
  8. L21
    exact hnr
  9. L22
    exact hshort
04Separate the logical casesL23–25

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

  1. L23
    cases hchoose
  2. L24
    cases hchoose_witness
  3. L25
    cases hchoose_witness_right
05Establish hmate_prefixL26–27

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

  1. L26
    have hmate_prefix : InversePrefix(p,n,u,v,n)Definitions: InversePrefix
  2. L27
    exact hprefix
06Establish hnonfixed_prefixL28–29

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

  1. L28
    have hnonfixed_prefix : InversePrefix(p,n,u,v,n)Definitions: InversePrefix
  2. L29
    exact hprefix
07Establish hback_prefixL30–31

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

  1. L30
    have hback_prefix : InversePrefix(p,n,u,v,n)Definitions: InversePrefix
  2. L31
    exact hprefix
08Establish hstoredL32–35

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

  1. L32
    have hstored : ∃ j. BetaAt(u,v,x,j) ∧ InverseIndex(p,n,x,j)Definitions: BetaAtInverseIndex
  2. L33
    specialize hprefix x
  3. L34
    apply hprefix
  4. L35
    exact hchoose_witness_left
09Separate the logical casesL36–37

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

  1. L36
    cases hstored
  2. L37
    cases hstored_witness
10Establish hmate_nonendpointL38–47

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

  1. L38
    have hmate_nonendpoint : (~(x1 = 0) /\ ~((S x1) = n))
  2. L39
    specialize prime_inverse_prefix_nonendpoint_mate p
  3. L40
    specialize prime_inverse_prefix_nonendpoint_mate n
  4. L41
    specialize prime_inverse_prefix_nonendpoint_mate u
  5. L42
    specialize prime_inverse_prefix_nonendpoint_mate v
  6. L43
    specialize prime_inverse_prefix_nonendpoint_mate x
  7. L44
    specialize prime_inverse_prefix_nonendpoint_mate x1
  8. L45
    apply prime_inverse_prefix_nonendpoint_mate
  9. L46
    exact hpn
  10. L47
    exact hp
11Use earlier factsL48–51

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

  1. L48
    exact hmate_prefix
  2. L49
    exact hchoose_witness_left
  3. L50
    exact hstored_witness_left
  4. L51
    exact hchoose_witness_right_left
12Establish hnonfixedL52–61

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. L52
    have hnonfixed : ~(x = x1)
  2. L53
    intro hxx1
  3. L54
    specialize prime_inverse_prefix_nonendpoint_not_fixed p
  4. L55
    specialize prime_inverse_prefix_nonendpoint_not_fixed n
  5. L56
    specialize prime_inverse_prefix_nonendpoint_not_fixed u
  6. L57
    specialize prime_inverse_prefix_nonendpoint_not_fixed v
  7. L58
    specialize prime_inverse_prefix_nonendpoint_not_fixed x
  8. L59
    specialize prime_inverse_prefix_nonendpoint_not_fixed x1
  9. L60
    apply prime_inverse_prefix_nonendpoint_not_fixed
  10. L61
    exact hpn
13Use earlier factsL62–67

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

  1. L62
    exact hp
  2. L63
    exact hnonfixed_prefix
  3. L64
    exact hchoose_witness_left
  4. L65
    exact hstored_witness_left
  5. L66
    exact hchoose_witness_right_left
  6. L67
    exact hxx1
14Establish hbackL68–77

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

  1. L68
    have 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))))
  2. L69
    specialize inverse_prefix_involutive p
  3. L70
    specialize inverse_prefix_involutive n
  4. L71
    specialize inverse_prefix_involutive u
  5. L72
    specialize inverse_prefix_involutive v
  6. L73
    specialize inverse_prefix_involutive x
  7. L74
    specialize inverse_prefix_involutive x1
  8. L75
    apply inverse_prefix_involutive
  9. L76
    exact hpn
  10. L77
    exact hback_prefix
15Use earlier factsL78–79

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

  1. L78
    exact hchoose_witness_left
  2. L79
    exact hstored_witness_left
16Separate the logical casesL80–80

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

  1. L80
    cases hback
17Construct an explicit witnessL81–82

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

  1. L81
    exists x
  2. L82
    exists x1
18Separate the logical casesL83–83

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

  1. L83
    split
19Use earlier factsL84–84

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

  1. L84
    exact hchoose_witness_left
20Separate the logical casesL85–85

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

  1. L85
    split
21Use earlier factsL86–86

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

  1. L86
    exact hchoose_witness_right_left
22Separate the logical casesL87–87

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

  1. L87
    split
23Use earlier factsL88–88

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

  1. L88
    exact hchoose_witness_right_right
24Separate the logical casesL89–89

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

  1. L89
    split
25Use earlier factsL90–90

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

  1. L90
    exact hstored_witness_left
26Separate the logical casesL91–91

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

  1. L91
    split
27Use earlier factsL92–92

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

  1. L92
    exact hback_left
28Separate the logical casesL93–93

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

  1. L93
    split
29Use earlier factsL94–94

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

  1. L94
    exact hmate_nonendpoint
30Separate the logical casesL95–95

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

  1. L95
    split
31Use earlier factsL96–97

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

  1. L96
    exact hnonfixed
  2. L97
    exact hback_right

Library-wide reading audit

Original exact command ledger · 97 lines
  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