prime_pair_order_paired_iteration

Proof neighborhood

Direct dependencies

Direct dependents

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 r
6. 0006intro hpn
7. 0007intro hp
8. 0008intro hprefix
9. 0009intro hnr
10. 0010induction m
11. 0011intro k
12. 0012intro hbalance
13. 0013have hzero_state : exists b c. (((forall wpo_position_wpopi_zero_state_closed wpo_source_wpopi_zero_state_closed wpo_mate_wpopi_zero_state_closed. (exists wpo_gap_wpopi_zero_state_closed_position_bound. wpo_gap_wpopi_zero_state_closed_position_bound + S (wpo_position_wpopi_zero_state_closed) = 0) -> (((exists wpo_beta_height_wpopi_zero_state_closed_source_entry. wpo_beta_height_wpopi_zero_state_closed_source_entry + S (wpo_source_wpopi_zero_state_closed) = S ((S (wpo_position_wpopi_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_closed_source_entry. b = wpo_beta_quotient_wpopi_zero_state_closed_source_entry * S ((S (wpo_position_wpopi_zero_state_closed)) * c) + (wpo_source_wpopi_zero_state_closed))) -> (((exists wpo_beta_height_wpopi_zero_state_closed_inverse_entry. wpo_beta_height_wpopi_zero_state_closed_inverse_entry + S (wpo_mate_wpopi_zero_state_closed) = S ((S (wpo_source_wpopi_zero_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_zero_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_zero_state_closed_inverse_entry * S ((S (wpo_source_wpopi_zero_state_closed)) * v) + (wpo_mate_wpopi_zero_state_closed))) -> exists wpo_mate_position_wpopi_zero_state_closed. ((exists wpo_gap_wpopi_zero_state_closed_mate_bound. wpo_gap_wpopi_zero_state_closed_mate_bound + S (wpo_mate_position_wpopi_zero_state_closed) = 0) /\ (((exists wpo_beta_height_wpopi_zero_state_closed_mate_entry. wpo_beta_height_wpopi_zero_state_closed_mate_entry + S (wpo_mate_wpopi_zero_state_closed) = S ((S (wpo_mate_position_wpopi_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_zero_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_zero_state_closed)) * c) + (wpo_mate_wpopi_zero_state_closed))))) /\ ((forall fom_index_wpopi_zero_state_bounded. (exists fom_gap_wpopi_zero_state_bounded_index_bound. fom_gap_wpopi_zero_state_bounded_index_bound + S (fom_index_wpopi_zero_state_bounded) = 0) -> exists fom_value_wpopi_zero_state_bounded. ((((exists fom_beta_height_wpopi_zero_state_bounded_entry. fom_beta_height_wpopi_zero_state_bounded_entry + S (fom_value_wpopi_zero_state_bounded) = S ((S (fom_index_wpopi_zero_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_zero_state_bounded_entry. b = fom_beta_quotient_wpopi_zero_state_bounded_entry * S ((S (fom_index_wpopi_zero_state_bounded)) * c) + (fom_value_wpopi_zero_state_bounded))) /\ (exists fom_gap_wpopi_zero_state_bounded_value_bound. fom_gap_wpopi_zero_state_bounded_value_bound + S (fom_value_wpopi_zero_state_bounded) = n))) /\ ((forall wpo_position_wpopi_zero_state_nonendpoint wpo_value_wpopi_zero_state_nonendpoint. (exists wpo_gap_wpopi_zero_state_nonendpoint_position_bound. wpo_gap_wpopi_zero_state_nonendpoint_position_bound + S (wpo_position_wpopi_zero_state_nonendpoint) = 0) -> (((exists wpo_beta_height_wpopi_zero_state_nonendpoint_entry. wpo_beta_height_wpopi_zero_state_nonendpoint_entry + S (wpo_value_wpopi_zero_state_nonendpoint) = S ((S (wpo_position_wpopi_zero_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_zero_state_nonendpoint_entry * S ((S (wpo_position_wpopi_zero_state_nonendpoint)) * c) + (wpo_value_wpopi_zero_state_nonendpoint))) -> (~(wpo_value_wpopi_zero_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_zero_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_zero_state_injective wpo_injective_right_wpopi_zero_state_injective wpo_injective_value_wpopi_zero_state_injective. (exists wpo_gap_wpopi_zero_state_injective_left_bound. wpo_gap_wpopi_zero_state_injective_left_bound + S (wpo_injective_left_wpopi_zero_state_injective) = 0) -> (exists wpo_gap_wpopi_zero_state_injective_right_bound. wpo_gap_wpopi_zero_state_injective_right_bound + S (wpo_injective_right_wpopi_zero_state_injective) = 0) -> (((exists wpo_beta_height_wpopi_zero_state_injective_left_entry. wpo_beta_height_wpopi_zero_state_injective_left_entry + S (wpo_injective_value_wpopi_zero_state_injective) = S ((S (wpo_injective_left_wpopi_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_injective_left_entry. b = wpo_beta_quotient_wpopi_zero_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_zero_state_injective)) * c) + (wpo_injective_value_wpopi_zero_state_injective))) -> (((exists wpo_beta_height_wpopi_zero_state_injective_right_entry. wpo_beta_height_wpopi_zero_state_injective_right_entry + S (wpo_injective_value_wpopi_zero_state_injective) = S ((S (wpo_injective_right_wpopi_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_zero_state_injective_right_entry. b = wpo_beta_quotient_wpopi_zero_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_zero_state_injective)) * c) + (wpo_injective_value_wpopi_zero_state_injective))) -> wpo_injective_left_wpopi_zero_state_injective = wpo_injective_right_wpopi_zero_state_injective)))))
14. 0014specialize pair_order_state_zero u
15. 0015specialize pair_order_state_zero v
16. 0016specialize pair_order_state_zero n
17. 0017exact pair_order_state_zero
18. 0018cases hzero_state
19. 0019cases hzero_state_witness
20. 0020have hzero : 0 + 0 = 0
21. 0021simp
22. 0022exists x
23. 0023exists x1
24. 0024split
25. 0025rewrite hzero
26. 0026rewrite hzero
27. 0027rewrite hzero
28. 0028rewrite hzero
29. 0029rewrite hzero
30. 0030rewrite hzero
31. 0031exact hzero_state_witness_witness
32. 0032specialize paired_inverse_witness_zero u
33. 0033specialize paired_inverse_witness_zero v
34. 0034specialize paired_inverse_witness_zero x
35. 0035specialize paired_inverse_witness_zero x1
36. 0036exact paired_inverse_witness_zero
37. 0037intro k
38. 0038intro hbalance
39. 0039have hprevious_normalize : (k + k) + S (S (S m + S m)) = (S k + S k) + S (S (m + m))
40. 0040specialize pair_order_iteration_previous_balance m
41. 0041specialize pair_order_iteration_previous_balance k
42. 0042exact pair_order_iteration_previous_balance
43. 0043have hprevious_balance : (S k + S k) + S (S (m + m)) = n
44. 0044trans (k + k) + S (S (S m + S m))
45. 0045symm
46. 0046exact hprevious_normalize
47. 0047exact hbalance
48. 0048have hprevious : exists b c. ((((forall wpo_position_wpopi_iteration_state_closed wpo_source_wpopi_iteration_state_closed wpo_mate_wpopi_iteration_state_closed. (exists wpo_gap_wpopi_iteration_state_closed_position_bound. wpo_gap_wpopi_iteration_state_closed_position_bound + S (wpo_position_wpopi_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_source_entry. wpo_beta_height_wpopi_iteration_state_closed_source_entry + S (wpo_source_wpopi_iteration_state_closed) = S ((S (wpo_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_source_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_source_entry * S ((S (wpo_position_wpopi_iteration_state_closed)) * c) + (wpo_source_wpopi_iteration_state_closed))) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_inverse_entry. wpo_beta_height_wpopi_iteration_state_closed_inverse_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_source_wpopi_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry * S ((S (wpo_source_wpopi_iteration_state_closed)) * v) + (wpo_mate_wpopi_iteration_state_closed))) -> exists wpo_mate_position_wpopi_iteration_state_closed. ((exists wpo_gap_wpopi_iteration_state_closed_mate_bound. wpo_gap_wpopi_iteration_state_closed_mate_bound + S (wpo_mate_position_wpopi_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_wpopi_iteration_state_closed_mate_entry. wpo_beta_height_wpopi_iteration_state_closed_mate_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c) + (wpo_mate_wpopi_iteration_state_closed))))) /\ ((forall fom_index_wpopi_iteration_state_bounded. (exists fom_gap_wpopi_iteration_state_bounded_index_bound. fom_gap_wpopi_iteration_state_bounded_index_bound + S (fom_index_wpopi_iteration_state_bounded) = m + m) -> exists fom_value_wpopi_iteration_state_bounded. ((((exists fom_beta_height_wpopi_iteration_state_bounded_entry. fom_beta_height_wpopi_iteration_state_bounded_entry + S (fom_value_wpopi_iteration_state_bounded) = S ((S (fom_index_wpopi_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_iteration_state_bounded_entry. b = fom_beta_quotient_wpopi_iteration_state_bounded_entry * S ((S (fom_index_wpopi_iteration_state_bounded)) * c) + (fom_value_wpopi_iteration_state_bounded))) /\ (exists fom_gap_wpopi_iteration_state_bounded_value_bound. fom_gap_wpopi_iteration_state_bounded_value_bound + S (fom_value_wpopi_iteration_state_bounded) = n))) /\ ((forall wpo_position_wpopi_iteration_state_nonendpoint wpo_value_wpopi_iteration_state_nonendpoint. (exists wpo_gap_wpopi_iteration_state_nonendpoint_position_bound. wpo_gap_wpopi_iteration_state_nonendpoint_position_bound + S (wpo_position_wpopi_iteration_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_nonendpoint_entry. wpo_beta_height_wpopi_iteration_state_nonendpoint_entry + S (wpo_value_wpopi_iteration_state_nonendpoint) = S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry * S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c) + (wpo_value_wpopi_iteration_state_nonendpoint))) -> (~(wpo_value_wpopi_iteration_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_iteration_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_iteration_state_injective wpo_injective_right_wpopi_iteration_state_injective wpo_injective_value_wpopi_iteration_state_injective. (exists wpo_gap_wpopi_iteration_state_injective_left_bound. wpo_gap_wpopi_iteration_state_injective_left_bound + S (wpo_injective_left_wpopi_iteration_state_injective) = m + m) -> (exists wpo_gap_wpopi_iteration_state_injective_right_bound. wpo_gap_wpopi_iteration_state_injective_right_bound + S (wpo_injective_right_wpopi_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_left_entry. wpo_beta_height_wpopi_iteration_state_injective_left_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_left_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_right_entry. wpo_beta_height_wpopi_iteration_state_injective_right_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_right_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> wpo_injective_left_wpopi_iteration_state_injective = wpo_injective_right_wpopi_iteration_state_injective))))) /\ (forall wpop_pair_wpopi_iteration_history. (exists wpo_gap_wpopi_iteration_history_pair_bound. wpo_gap_wpopi_iteration_history_pair_bound + S (wpop_pair_wpopi_iteration_history) = m) -> exists wpop_left_wpopi_iteration_history wpop_right_wpopi_iteration_history. ((((exists wpo_beta_height_wpopi_iteration_history_left_entry. wpo_beta_height_wpopi_iteration_history_left_entry + S (wpop_left_wpopi_iteration_history) = S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_left_entry. b = wpo_beta_quotient_wpopi_iteration_history_left_entry * S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c) + (wpop_left_wpopi_iteration_history))) /\ ((((exists wpo_beta_height_wpopi_iteration_history_right_entry. wpo_beta_height_wpopi_iteration_history_right_entry + S (wpop_right_wpopi_iteration_history) = S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_right_entry. b = wpo_beta_quotient_wpopi_iteration_history_right_entry * S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c) + (wpop_right_wpopi_iteration_history))) /\ (((exists wpo_beta_height_wpopi_iteration_history_inverse_entry. wpo_beta_height_wpopi_iteration_history_inverse_entry + S (wpop_right_wpopi_iteration_history) = S ((S (wpop_left_wpopi_iteration_history)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_history_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_history_inverse_entry * S ((S (wpop_left_wpopi_iteration_history)) * v) + (wpop_right_wpopi_iteration_history)))))))
49. 0049specialize IH (S k)
50. 0050apply IH
51. 0051exact hprevious_balance
52. 0052cases hprevious
53. 0053cases hprevious_witness
54. 0054cases hprevious_witness_witness
55. 0055have hroom_normalize : (k + k) + S (S (S m + S m)) = S (k + k) + S (S (S (m + m)))
56. 0056specialize pair_order_iteration_step_room m
57. 0057specialize pair_order_iteration_step_room k
58. 0058exact pair_order_iteration_step_room
59. 0059have hroom_eq : S (k + k) + S (S (S (m + m))) = n
60. 0060trans (k + k) + S (S (S m + S m))
61. 0061symm
62. 0062exact hroom_normalize
63. 0063exact hbalance
64. 0064have hroom : exists h. h + S (S (S (m + m))) = n
65. 0065exists S (k + k)
66. 0066exact hroom_eq
67. 0067have hnext : exists z d. ((((forall wpo_position_wpopi_next_state_closed wpo_source_wpopi_next_state_closed wpo_mate_wpopi_next_state_closed. (exists wpo_gap_wpopi_next_state_closed_position_bound. wpo_gap_wpopi_next_state_closed_position_bound + S (wpo_position_wpopi_next_state_closed) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_closed_source_entry. wpo_beta_height_wpopi_next_state_closed_source_entry + S (wpo_source_wpopi_next_state_closed) = S ((S (wpo_position_wpopi_next_state_closed)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_source_entry. z = wpo_beta_quotient_wpopi_next_state_closed_source_entry * S ((S (wpo_position_wpopi_next_state_closed)) * d) + (wpo_source_wpopi_next_state_closed))) -> (((exists wpo_beta_height_wpopi_next_state_closed_inverse_entry. wpo_beta_height_wpopi_next_state_closed_inverse_entry + S (wpo_mate_wpopi_next_state_closed) = S ((S (wpo_source_wpopi_next_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_next_state_closed_inverse_entry * S ((S (wpo_source_wpopi_next_state_closed)) * v) + (wpo_mate_wpopi_next_state_closed))) -> exists wpo_mate_position_wpopi_next_state_closed. ((exists wpo_gap_wpopi_next_state_closed_mate_bound. wpo_gap_wpopi_next_state_closed_mate_bound + S (wpo_mate_position_wpopi_next_state_closed) = S (S (m + m))) /\ (((exists wpo_beta_height_wpopi_next_state_closed_mate_entry. wpo_beta_height_wpopi_next_state_closed_mate_entry + S (wpo_mate_wpopi_next_state_closed) = S ((S (wpo_mate_position_wpopi_next_state_closed)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_mate_entry. z = wpo_beta_quotient_wpopi_next_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_next_state_closed)) * d) + (wpo_mate_wpopi_next_state_closed))))) /\ ((forall fom_index_wpopi_next_state_bounded. (exists fom_gap_wpopi_next_state_bounded_index_bound. fom_gap_wpopi_next_state_bounded_index_bound + S (fom_index_wpopi_next_state_bounded) = S (S (m + m))) -> exists fom_value_wpopi_next_state_bounded. ((((exists fom_beta_height_wpopi_next_state_bounded_entry. fom_beta_height_wpopi_next_state_bounded_entry + S (fom_value_wpopi_next_state_bounded) = S ((S (fom_index_wpopi_next_state_bounded)) * d)) /\ exists fom_beta_quotient_wpopi_next_state_bounded_entry. z = fom_beta_quotient_wpopi_next_state_bounded_entry * S ((S (fom_index_wpopi_next_state_bounded)) * d) + (fom_value_wpopi_next_state_bounded))) /\ (exists fom_gap_wpopi_next_state_bounded_value_bound. fom_gap_wpopi_next_state_bounded_value_bound + S (fom_value_wpopi_next_state_bounded) = n))) /\ ((forall wpo_position_wpopi_next_state_nonendpoint wpo_value_wpopi_next_state_nonendpoint. (exists wpo_gap_wpopi_next_state_nonendpoint_position_bound. wpo_gap_wpopi_next_state_nonendpoint_position_bound + S (wpo_position_wpopi_next_state_nonendpoint) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_nonendpoint_entry. wpo_beta_height_wpopi_next_state_nonendpoint_entry + S (wpo_value_wpopi_next_state_nonendpoint) = S ((S (wpo_position_wpopi_next_state_nonendpoint)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_nonendpoint_entry. z = wpo_beta_quotient_wpopi_next_state_nonendpoint_entry * S ((S (wpo_position_wpopi_next_state_nonendpoint)) * d) + (wpo_value_wpopi_next_state_nonendpoint))) -> (~(wpo_value_wpopi_next_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_next_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_next_state_injective wpo_injective_right_wpopi_next_state_injective wpo_injective_value_wpopi_next_state_injective. (exists wpo_gap_wpopi_next_state_injective_left_bound. wpo_gap_wpopi_next_state_injective_left_bound + S (wpo_injective_left_wpopi_next_state_injective) = S (S (m + m))) -> (exists wpo_gap_wpopi_next_state_injective_right_bound. wpo_gap_wpopi_next_state_injective_right_bound + S (wpo_injective_right_wpopi_next_state_injective) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_injective_left_entry. wpo_beta_height_wpopi_next_state_injective_left_entry + S (wpo_injective_value_wpopi_next_state_injective) = S ((S (wpo_injective_left_wpopi_next_state_injective)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_injective_left_entry. z = wpo_beta_quotient_wpopi_next_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_next_state_injective)) * d) + (wpo_injective_value_wpopi_next_state_injective))) -> (((exists wpo_beta_height_wpopi_next_state_injective_right_entry. wpo_beta_height_wpopi_next_state_injective_right_entry + S (wpo_injective_value_wpopi_next_state_injective) = S ((S (wpo_injective_right_wpopi_next_state_injective)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_injective_right_entry. z = wpo_beta_quotient_wpopi_next_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_next_state_injective)) * d) + (wpo_injective_value_wpopi_next_state_injective))) -> wpo_injective_left_wpopi_next_state_injective = wpo_injective_right_wpopi_next_state_injective))))) /\ (forall wpop_pair_wpop_new_pairs. (exists wpo_gap_wpop_new_pairs_pair_bound. wpo_gap_wpop_new_pairs_pair_bound + S (wpop_pair_wpop_new_pairs) = S m) -> exists wpop_left_wpop_new_pairs wpop_right_wpop_new_pairs. ((((exists wpo_beta_height_wpop_new_pairs_left_entry. wpo_beta_height_wpop_new_pairs_left_entry + S (wpop_left_wpop_new_pairs) = S ((S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs)) * d)) /\ exists wpo_beta_quotient_wpop_new_pairs_left_entry. z = wpo_beta_quotient_wpop_new_pairs_left_entry * S ((S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs)) * d) + (wpop_left_wpop_new_pairs))) /\ ((((exists wpo_beta_height_wpop_new_pairs_right_entry. wpo_beta_height_wpop_new_pairs_right_entry + S (wpop_right_wpop_new_pairs) = S ((S (S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs))) * d)) /\ exists wpo_beta_quotient_wpop_new_pairs_right_entry. z = wpo_beta_quotient_wpop_new_pairs_right_entry * S ((S (S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs))) * d) + (wpop_right_wpop_new_pairs))) /\ (((exists wpo_beta_height_wpop_new_pairs_inverse_entry. wpo_beta_height_wpop_new_pairs_inverse_entry + S (wpop_right_wpop_new_pairs) = S ((S (wpop_left_wpop_new_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_new_pairs_inverse_entry. u = wpo_beta_quotient_wpop_new_pairs_inverse_entry * S ((S (wpop_left_wpop_new_pairs)) * v) + (wpop_right_wpop_new_pairs)))))))
68. 0068specialize prime_pair_order_paired_state_step p
69. 0069specialize prime_pair_order_paired_state_step n
70. 0070specialize prime_pair_order_paired_state_step u
71. 0071specialize prime_pair_order_paired_state_step v
72. 0072specialize prime_pair_order_paired_state_step x
73. 0073specialize prime_pair_order_paired_state_step x1
74. 0074specialize prime_pair_order_paired_state_step m
75. 0075specialize prime_pair_order_paired_state_step r
76. 0076apply prime_pair_order_paired_state_step
77. 0077exact hpn
78. 0078exact hp
79. 0079exact hprefix
80. 0080exact hnr
81. 0081exact hroom
82. 0082exact hprevious_witness_witness_left
83. 0083exact hprevious_witness_witness_right
84. 0084cases hnext
85. 0085cases hnext_witness
86. 0086cases hnext_witness_witness
87. 0087have hlength : S (S (m + m)) = S m + S m
88. 0088specialize pair_order_double_succ_length (m + m)
89. 0089specialize pair_order_double_succ_length m
90. 0090apply pair_order_double_succ_length
91. 0091refl
92. 0092have hsuccessor_state : ((forall wpo_position_wpopi_successor_state_closed wpo_source_wpopi_successor_state_closed wpo_mate_wpopi_successor_state_closed. (exists wpo_gap_wpopi_successor_state_closed_position_bound. wpo_gap_wpopi_successor_state_closed_position_bound + S (wpo_position_wpopi_successor_state_closed) = S m + S m) -> (((exists wpo_beta_height_wpopi_successor_state_closed_source_entry. wpo_beta_height_wpopi_successor_state_closed_source_entry + S (wpo_source_wpopi_successor_state_closed) = S ((S (wpo_position_wpopi_successor_state_closed)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_closed_source_entry. x2 = wpo_beta_quotient_wpopi_successor_state_closed_source_entry * S ((S (wpo_position_wpopi_successor_state_closed)) * x3) + (wpo_source_wpopi_successor_state_closed))) -> (((exists wpo_beta_height_wpopi_successor_state_closed_inverse_entry. wpo_beta_height_wpopi_successor_state_closed_inverse_entry + S (wpo_mate_wpopi_successor_state_closed) = S ((S (wpo_source_wpopi_successor_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_successor_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_successor_state_closed_inverse_entry * S ((S (wpo_source_wpopi_successor_state_closed)) * v) + (wpo_mate_wpopi_successor_state_closed))) -> exists wpo_mate_position_wpopi_successor_state_closed. ((exists wpo_gap_wpopi_successor_state_closed_mate_bound. wpo_gap_wpopi_successor_state_closed_mate_bound + S (wpo_mate_position_wpopi_successor_state_closed) = S m + S m) /\ (((exists wpo_beta_height_wpopi_successor_state_closed_mate_entry. wpo_beta_height_wpopi_successor_state_closed_mate_entry + S (wpo_mate_wpopi_successor_state_closed) = S ((S (wpo_mate_position_wpopi_successor_state_closed)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_closed_mate_entry. x2 = wpo_beta_quotient_wpopi_successor_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_successor_state_closed)) * x3) + (wpo_mate_wpopi_successor_state_closed))))) /\ ((forall fom_index_wpopi_successor_state_bounded. (exists fom_gap_wpopi_successor_state_bounded_index_bound. fom_gap_wpopi_successor_state_bounded_index_bound + S (fom_index_wpopi_successor_state_bounded) = S m + S m) -> exists fom_value_wpopi_successor_state_bounded. ((((exists fom_beta_height_wpopi_successor_state_bounded_entry. fom_beta_height_wpopi_successor_state_bounded_entry + S (fom_value_wpopi_successor_state_bounded) = S ((S (fom_index_wpopi_successor_state_bounded)) * x3)) /\ exists fom_beta_quotient_wpopi_successor_state_bounded_entry. x2 = fom_beta_quotient_wpopi_successor_state_bounded_entry * S ((S (fom_index_wpopi_successor_state_bounded)) * x3) + (fom_value_wpopi_successor_state_bounded))) /\ (exists fom_gap_wpopi_successor_state_bounded_value_bound. fom_gap_wpopi_successor_state_bounded_value_bound + S (fom_value_wpopi_successor_state_bounded) = n))) /\ ((forall wpo_position_wpopi_successor_state_nonendpoint wpo_value_wpopi_successor_state_nonendpoint. (exists wpo_gap_wpopi_successor_state_nonendpoint_position_bound. wpo_gap_wpopi_successor_state_nonendpoint_position_bound + S (wpo_position_wpopi_successor_state_nonendpoint) = S m + S m) -> (((exists wpo_beta_height_wpopi_successor_state_nonendpoint_entry. wpo_beta_height_wpopi_successor_state_nonendpoint_entry + S (wpo_value_wpopi_successor_state_nonendpoint) = S ((S (wpo_position_wpopi_successor_state_nonendpoint)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_nonendpoint_entry. x2 = wpo_beta_quotient_wpopi_successor_state_nonendpoint_entry * S ((S (wpo_position_wpopi_successor_state_nonendpoint)) * x3) + (wpo_value_wpopi_successor_state_nonendpoint))) -> (~(wpo_value_wpopi_successor_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_successor_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_successor_state_injective wpo_injective_right_wpopi_successor_state_injective wpo_injective_value_wpopi_successor_state_injective. (exists wpo_gap_wpopi_successor_state_injective_left_bound. wpo_gap_wpopi_successor_state_injective_left_bound + S (wpo_injective_left_wpopi_successor_state_injective) = S m + S m) -> (exists wpo_gap_wpopi_successor_state_injective_right_bound. wpo_gap_wpopi_successor_state_injective_right_bound + S (wpo_injective_right_wpopi_successor_state_injective) = S m + S m) -> (((exists wpo_beta_height_wpopi_successor_state_injective_left_entry. wpo_beta_height_wpopi_successor_state_injective_left_entry + S (wpo_injective_value_wpopi_successor_state_injective) = S ((S (wpo_injective_left_wpopi_successor_state_injective)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_injective_left_entry. x2 = wpo_beta_quotient_wpopi_successor_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_successor_state_injective)) * x3) + (wpo_injective_value_wpopi_successor_state_injective))) -> (((exists wpo_beta_height_wpopi_successor_state_injective_right_entry. wpo_beta_height_wpopi_successor_state_injective_right_entry + S (wpo_injective_value_wpopi_successor_state_injective) = S ((S (wpo_injective_right_wpopi_successor_state_injective)) * x3)) /\ exists wpo_beta_quotient_wpopi_successor_state_injective_right_entry. x2 = wpo_beta_quotient_wpopi_successor_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_successor_state_injective)) * x3) + (wpo_injective_value_wpopi_successor_state_injective))) -> wpo_injective_left_wpopi_successor_state_injective = wpo_injective_right_wpopi_successor_state_injective))))
93. 0093rewrite <- hlength
94. 0094rewrite <- hlength
95. 0095rewrite <- hlength
96. 0096rewrite <- hlength
97. 0097rewrite <- hlength
98. 0098rewrite <- hlength
99. 0099exact hnext_witness_witness_left
100. 0100exists x2
101. 0101exists x3
102. 0102split
103. 0103exact hsuccessor_state
104. 0104exact hnext_witness_witness_right