scaled_inverse_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 a
3. 0003intro n
4. 0004intro u
5. 0005intro v
6. 0006intro hpn
7. 0007intro hp
8. 0008intro hnotqres
9. 0009intro hprefix
10. 0010induction m
11. 0011intro k
12. 0012intro hbalance
13. 0013have hzero_state : exists b c. (((forall espo_position_zero_state_closed espo_source_zero_state_closed espo_mate_zero_state_closed. (exists wpo_gap_zero_state_closed_position_bound. wpo_gap_zero_state_closed_position_bound + S (espo_position_zero_state_closed) = 0) -> (((exists wpo_beta_height_zero_state_closed_source_entry. wpo_beta_height_zero_state_closed_source_entry + S (espo_source_zero_state_closed) = S ((S (espo_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_source_entry. b = wpo_beta_quotient_zero_state_closed_source_entry * S ((S (espo_position_zero_state_closed)) * c) + (espo_source_zero_state_closed))) -> (((exists wpo_beta_height_zero_state_closed_scaled_entry. wpo_beta_height_zero_state_closed_scaled_entry + S (S espo_mate_zero_state_closed) = S ((S (espo_source_zero_state_closed)) * v)) /\ exists wpo_beta_quotient_zero_state_closed_scaled_entry. u = wpo_beta_quotient_zero_state_closed_scaled_entry * S ((S (espo_source_zero_state_closed)) * v) + (S espo_mate_zero_state_closed))) -> exists espo_mate_position_zero_state_closed. ((exists wpo_gap_zero_state_closed_mate_bound. wpo_gap_zero_state_closed_mate_bound + S (espo_mate_position_zero_state_closed) = 0) /\ (((exists wpo_beta_height_zero_state_closed_mate_entry. wpo_beta_height_zero_state_closed_mate_entry + S (espo_mate_zero_state_closed) = S ((S (espo_mate_position_zero_state_closed)) * c)) /\ exists wpo_beta_quotient_zero_state_closed_mate_entry. b = wpo_beta_quotient_zero_state_closed_mate_entry * S ((S (espo_mate_position_zero_state_closed)) * c) + (espo_mate_zero_state_closed))))) /\ (((forall fom_index_zero_state_bounded. (exists fom_gap_zero_state_bounded_index_bound. fom_gap_zero_state_bounded_index_bound + S (fom_index_zero_state_bounded) = 0) -> exists fom_value_zero_state_bounded. ((((exists fom_beta_height_zero_state_bounded_entry. fom_beta_height_zero_state_bounded_entry + S (fom_value_zero_state_bounded) = S ((S (fom_index_zero_state_bounded)) * c)) /\ exists fom_beta_quotient_zero_state_bounded_entry. b = fom_beta_quotient_zero_state_bounded_entry * S ((S (fom_index_zero_state_bounded)) * c) + (fom_value_zero_state_bounded))) /\ (exists fom_gap_zero_state_bounded_value_bound. fom_gap_zero_state_bounded_value_bound + S (fom_value_zero_state_bounded) = n))) /\ (forall wpo_injective_left_zero_state_injective wpo_injective_right_zero_state_injective wpo_injective_value_zero_state_injective. (exists wpo_gap_zero_state_injective_left_bound. wpo_gap_zero_state_injective_left_bound + S (wpo_injective_left_zero_state_injective) = 0) -> (exists wpo_gap_zero_state_injective_right_bound. wpo_gap_zero_state_injective_right_bound + S (wpo_injective_right_zero_state_injective) = 0) -> (((exists wpo_beta_height_zero_state_injective_left_entry. wpo_beta_height_zero_state_injective_left_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_left_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_left_entry. b = wpo_beta_quotient_zero_state_injective_left_entry * S ((S (wpo_injective_left_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> (((exists wpo_beta_height_zero_state_injective_right_entry. wpo_beta_height_zero_state_injective_right_entry + S (wpo_injective_value_zero_state_injective) = S ((S (wpo_injective_right_zero_state_injective)) * c)) /\ exists wpo_beta_quotient_zero_state_injective_right_entry. b = wpo_beta_quotient_zero_state_injective_right_entry * S ((S (wpo_injective_right_zero_state_injective)) * c) + (wpo_injective_value_zero_state_injective))) -> wpo_injective_left_zero_state_injective = wpo_injective_right_zero_state_injective)))))
14. 0014specialize scaled_pair_order_state_zero u
15. 0015specialize scaled_pair_order_state_zero v
16. 0016specialize scaled_pair_order_state_zero n
17. 0017exact scaled_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. 0030exact hzero_state_witness_witness
31. 0031specialize adjacent_scaled_orbit_history_zero u
32. 0032specialize adjacent_scaled_orbit_history_zero v
33. 0033specialize adjacent_scaled_orbit_history_zero x
34. 0034specialize adjacent_scaled_orbit_history_zero x1
35. 0035exact adjacent_scaled_orbit_history_zero
36. 0036intro k
37. 0037intro hbalance
38. 0038have hprevious_normalize : (S m + S m) + (k + k) = (m + m) + (S k + S k)
39. 0039specialize euler_pair_iteration_previous_balance m
40. 0040specialize euler_pair_iteration_previous_balance k
41. 0041exact euler_pair_iteration_previous_balance
42. 0042have hprevious_balance : (m + m) + (S k + S k) = n
43. 0043trans (S m + S m) + (k + k)
44. 0044symm
45. 0045exact hprevious_normalize
46. 0046exact hbalance
47. 0047have hprevious : exists b c. (((((forall espo_position_iteration_state_closed espo_source_iteration_state_closed espo_mate_iteration_state_closed. (exists wpo_gap_iteration_state_closed_position_bound. wpo_gap_iteration_state_closed_position_bound + S (espo_position_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_iteration_state_closed_source_entry. wpo_beta_height_iteration_state_closed_source_entry + S (espo_source_iteration_state_closed) = S ((S (espo_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_source_entry. b = wpo_beta_quotient_iteration_state_closed_source_entry * S ((S (espo_position_iteration_state_closed)) * c) + (espo_source_iteration_state_closed))) -> (((exists wpo_beta_height_iteration_state_closed_scaled_entry. wpo_beta_height_iteration_state_closed_scaled_entry + S (S espo_mate_iteration_state_closed) = S ((S (espo_source_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_iteration_state_closed_scaled_entry. u = wpo_beta_quotient_iteration_state_closed_scaled_entry * S ((S (espo_source_iteration_state_closed)) * v) + (S espo_mate_iteration_state_closed))) -> exists espo_mate_position_iteration_state_closed. ((exists wpo_gap_iteration_state_closed_mate_bound. wpo_gap_iteration_state_closed_mate_bound + S (espo_mate_position_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_iteration_state_closed_mate_entry. wpo_beta_height_iteration_state_closed_mate_entry + S (espo_mate_iteration_state_closed) = S ((S (espo_mate_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_mate_entry. b = wpo_beta_quotient_iteration_state_closed_mate_entry * S ((S (espo_mate_position_iteration_state_closed)) * c) + (espo_mate_iteration_state_closed))))) /\ (((forall fom_index_iteration_state_bounded. (exists fom_gap_iteration_state_bounded_index_bound. fom_gap_iteration_state_bounded_index_bound + S (fom_index_iteration_state_bounded) = m + m) -> exists fom_value_iteration_state_bounded. ((((exists fom_beta_height_iteration_state_bounded_entry. fom_beta_height_iteration_state_bounded_entry + S (fom_value_iteration_state_bounded) = S ((S (fom_index_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_iteration_state_bounded_entry. b = fom_beta_quotient_iteration_state_bounded_entry * S ((S (fom_index_iteration_state_bounded)) * c) + (fom_value_iteration_state_bounded))) /\ (exists fom_gap_iteration_state_bounded_value_bound. fom_gap_iteration_state_bounded_value_bound + S (fom_value_iteration_state_bounded) = n))) /\ (forall wpo_injective_left_iteration_state_injective wpo_injective_right_iteration_state_injective wpo_injective_value_iteration_state_injective. (exists wpo_gap_iteration_state_injective_left_bound. wpo_gap_iteration_state_injective_left_bound + S (wpo_injective_left_iteration_state_injective) = m + m) -> (exists wpo_gap_iteration_state_injective_right_bound. wpo_gap_iteration_state_injective_right_bound + S (wpo_injective_right_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_iteration_state_injective_left_entry. wpo_beta_height_iteration_state_injective_left_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_left_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_left_entry. b = wpo_beta_quotient_iteration_state_injective_left_entry * S ((S (wpo_injective_left_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> (((exists wpo_beta_height_iteration_state_injective_right_entry. wpo_beta_height_iteration_state_injective_right_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_right_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_right_entry. b = wpo_beta_quotient_iteration_state_injective_right_entry * S ((S (wpo_injective_right_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> wpo_injective_left_iteration_state_injective = wpo_injective_right_iteration_state_injective))))) /\ (forall espi_pair_iteration_history. (exists wpo_gap_iteration_history_pair_bound. wpo_gap_iteration_history_pair_bound + S (espi_pair_iteration_history) = m) -> exists espi_left_iteration_history espi_right_iteration_history. (((((exists wpo_beta_height_iteration_history_left_entry. wpo_beta_height_iteration_history_left_entry + S (espi_left_iteration_history) = S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c)) /\ exists wpo_beta_quotient_iteration_history_left_entry. b = wpo_beta_quotient_iteration_history_left_entry * S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c) + (espi_left_iteration_history))) /\ (((((exists wpo_beta_height_iteration_history_right_entry. wpo_beta_height_iteration_history_right_entry + S (espi_right_iteration_history) = S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c)) /\ exists wpo_beta_quotient_iteration_history_right_entry. b = wpo_beta_quotient_iteration_history_right_entry * S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c) + (espi_right_iteration_history))) /\ (((exists wpo_beta_height_iteration_history_scaled_edge. wpo_beta_height_iteration_history_scaled_edge + S (S espi_right_iteration_history) = S ((S (espi_left_iteration_history)) * v)) /\ exists wpo_beta_quotient_iteration_history_scaled_edge. u = wpo_beta_quotient_iteration_history_scaled_edge * S ((S (espi_left_iteration_history)) * v) + (S espi_right_iteration_history))))))))))
48. 0048specialize IH (S k)
49. 0049apply IH
50. 0050exact hprevious_balance
51. 0051cases hprevious
52. 0052cases hprevious_witness
53. 0053cases hprevious_witness_witness
54. 0054have hshort_normalize : S (k + k) + S (m + m) = (S m + S m) + (k + k)
55. 0055specialize euler_pair_iteration_step_short m
56. 0056specialize euler_pair_iteration_step_short k
57. 0057exact euler_pair_iteration_step_short
58. 0058have hshort_eq : S (k + k) + S (m + m) = n
59. 0059trans (S m + S m) + (k + k)
60. 0060exact hshort_normalize
61. 0061exact hbalance
62. 0062have hshort : exists q. q + S (m + m) = n
63. 0063exists S (k + k)
64. 0064exact hshort_eq
65. 0065have hnext : exists z d. (((((forall espo_position_step_result_state_closed espo_source_step_result_state_closed espo_mate_step_result_state_closed. (exists wpo_gap_step_result_state_closed_position_bound. wpo_gap_step_result_state_closed_position_bound + S (espo_position_step_result_state_closed) = S (S (m + m))) -> (((exists wpo_beta_height_step_result_state_closed_source_entry. wpo_beta_height_step_result_state_closed_source_entry + S (espo_source_step_result_state_closed) = S ((S (espo_position_step_result_state_closed)) * d)) /\ exists wpo_beta_quotient_step_result_state_closed_source_entry. z = wpo_beta_quotient_step_result_state_closed_source_entry * S ((S (espo_position_step_result_state_closed)) * d) + (espo_source_step_result_state_closed))) -> (((exists wpo_beta_height_step_result_state_closed_scaled_entry. wpo_beta_height_step_result_state_closed_scaled_entry + S (S espo_mate_step_result_state_closed) = S ((S (espo_source_step_result_state_closed)) * v)) /\ exists wpo_beta_quotient_step_result_state_closed_scaled_entry. u = wpo_beta_quotient_step_result_state_closed_scaled_entry * S ((S (espo_source_step_result_state_closed)) * v) + (S espo_mate_step_result_state_closed))) -> exists espo_mate_position_step_result_state_closed. ((exists wpo_gap_step_result_state_closed_mate_bound. wpo_gap_step_result_state_closed_mate_bound + S (espo_mate_position_step_result_state_closed) = S (S (m + m))) /\ (((exists wpo_beta_height_step_result_state_closed_mate_entry. wpo_beta_height_step_result_state_closed_mate_entry + S (espo_mate_step_result_state_closed) = S ((S (espo_mate_position_step_result_state_closed)) * d)) /\ exists wpo_beta_quotient_step_result_state_closed_mate_entry. z = wpo_beta_quotient_step_result_state_closed_mate_entry * S ((S (espo_mate_position_step_result_state_closed)) * d) + (espo_mate_step_result_state_closed))))) /\ (((forall fom_index_step_result_state_bounded. (exists fom_gap_step_result_state_bounded_index_bound. fom_gap_step_result_state_bounded_index_bound + S (fom_index_step_result_state_bounded) = S (S (m + m))) -> exists fom_value_step_result_state_bounded. ((((exists fom_beta_height_step_result_state_bounded_entry. fom_beta_height_step_result_state_bounded_entry + S (fom_value_step_result_state_bounded) = S ((S (fom_index_step_result_state_bounded)) * d)) /\ exists fom_beta_quotient_step_result_state_bounded_entry. z = fom_beta_quotient_step_result_state_bounded_entry * S ((S (fom_index_step_result_state_bounded)) * d) + (fom_value_step_result_state_bounded))) /\ (exists fom_gap_step_result_state_bounded_value_bound. fom_gap_step_result_state_bounded_value_bound + S (fom_value_step_result_state_bounded) = n))) /\ (forall wpo_injective_left_step_result_state_injective wpo_injective_right_step_result_state_injective wpo_injective_value_step_result_state_injective. (exists wpo_gap_step_result_state_injective_left_bound. wpo_gap_step_result_state_injective_left_bound + S (wpo_injective_left_step_result_state_injective) = S (S (m + m))) -> (exists wpo_gap_step_result_state_injective_right_bound. wpo_gap_step_result_state_injective_right_bound + S (wpo_injective_right_step_result_state_injective) = S (S (m + m))) -> (((exists wpo_beta_height_step_result_state_injective_left_entry. wpo_beta_height_step_result_state_injective_left_entry + S (wpo_injective_value_step_result_state_injective) = S ((S (wpo_injective_left_step_result_state_injective)) * d)) /\ exists wpo_beta_quotient_step_result_state_injective_left_entry. z = wpo_beta_quotient_step_result_state_injective_left_entry * S ((S (wpo_injective_left_step_result_state_injective)) * d) + (wpo_injective_value_step_result_state_injective))) -> (((exists wpo_beta_height_step_result_state_injective_right_entry. wpo_beta_height_step_result_state_injective_right_entry + S (wpo_injective_value_step_result_state_injective) = S ((S (wpo_injective_right_step_result_state_injective)) * d)) /\ exists wpo_beta_quotient_step_result_state_injective_right_entry. z = wpo_beta_quotient_step_result_state_injective_right_entry * S ((S (wpo_injective_right_step_result_state_injective)) * d) + (wpo_injective_value_step_result_state_injective))) -> wpo_injective_left_step_result_state_injective = wpo_injective_right_step_result_state_injective))))) /\ (forall espi_pair_append_new_history. (exists wpo_gap_append_new_history_pair_bound. wpo_gap_append_new_history_pair_bound + S (espi_pair_append_new_history) = S m) -> exists espi_left_append_new_history espi_right_append_new_history. (((((exists wpo_beta_height_append_new_history_left_entry. wpo_beta_height_append_new_history_left_entry + S (espi_left_append_new_history) = S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d)) /\ exists wpo_beta_quotient_append_new_history_left_entry. z = wpo_beta_quotient_append_new_history_left_entry * S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d) + (espi_left_append_new_history))) /\ (((((exists wpo_beta_height_append_new_history_right_entry. wpo_beta_height_append_new_history_right_entry + S (espi_right_append_new_history) = S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d)) /\ exists wpo_beta_quotient_append_new_history_right_entry. z = wpo_beta_quotient_append_new_history_right_entry * S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d) + (espi_right_append_new_history))) /\ (((exists wpo_beta_height_append_new_history_scaled_edge. wpo_beta_height_append_new_history_scaled_edge + S (S espi_right_append_new_history) = S ((S (espi_left_append_new_history)) * v)) /\ exists wpo_beta_quotient_append_new_history_scaled_edge. u = wpo_beta_quotient_append_new_history_scaled_edge * S ((S (espi_left_append_new_history)) * v) + (S espi_right_append_new_history))))))))))
66. 0066specialize scaled_inverse_pair_order_paired_state_step p
67. 0067specialize scaled_inverse_pair_order_paired_state_step a
68. 0068specialize scaled_inverse_pair_order_paired_state_step n
69. 0069specialize scaled_inverse_pair_order_paired_state_step u
70. 0070specialize scaled_inverse_pair_order_paired_state_step v
71. 0071specialize scaled_inverse_pair_order_paired_state_step x
72. 0072specialize scaled_inverse_pair_order_paired_state_step x1
73. 0073specialize scaled_inverse_pair_order_paired_state_step m
74. 0074apply scaled_inverse_pair_order_paired_state_step
75. 0075exact hpn
76. 0076exact hp
77. 0077exact hnotqres
78. 0078exact hprefix
79. 0079exact hshort
80. 0080exact hprevious_witness_witness_left
81. 0081exact hprevious_witness_witness_right
82. 0082cases hnext
83. 0083cases hnext_witness
84. 0084cases hnext_witness_witness
85. 0085have hlength : S (S (m + m)) = S m + S m
86. 0086specialize pair_order_double_succ_length (m + m)
87. 0087specialize pair_order_double_succ_length m
88. 0088apply pair_order_double_succ_length
89. 0089refl
90. 0090have hsuccessor_state : ((forall espo_position_successor_state_closed espo_source_successor_state_closed espo_mate_successor_state_closed. (exists wpo_gap_successor_state_closed_position_bound. wpo_gap_successor_state_closed_position_bound + S (espo_position_successor_state_closed) = S m + S m) -> (((exists wpo_beta_height_successor_state_closed_source_entry. wpo_beta_height_successor_state_closed_source_entry + S (espo_source_successor_state_closed) = S ((S (espo_position_successor_state_closed)) * x3)) /\ exists wpo_beta_quotient_successor_state_closed_source_entry. x2 = wpo_beta_quotient_successor_state_closed_source_entry * S ((S (espo_position_successor_state_closed)) * x3) + (espo_source_successor_state_closed))) -> (((exists wpo_beta_height_successor_state_closed_scaled_entry. wpo_beta_height_successor_state_closed_scaled_entry + S (S espo_mate_successor_state_closed) = S ((S (espo_source_successor_state_closed)) * v)) /\ exists wpo_beta_quotient_successor_state_closed_scaled_entry. u = wpo_beta_quotient_successor_state_closed_scaled_entry * S ((S (espo_source_successor_state_closed)) * v) + (S espo_mate_successor_state_closed))) -> exists espo_mate_position_successor_state_closed. ((exists wpo_gap_successor_state_closed_mate_bound. wpo_gap_successor_state_closed_mate_bound + S (espo_mate_position_successor_state_closed) = S m + S m) /\ (((exists wpo_beta_height_successor_state_closed_mate_entry. wpo_beta_height_successor_state_closed_mate_entry + S (espo_mate_successor_state_closed) = S ((S (espo_mate_position_successor_state_closed)) * x3)) /\ exists wpo_beta_quotient_successor_state_closed_mate_entry. x2 = wpo_beta_quotient_successor_state_closed_mate_entry * S ((S (espo_mate_position_successor_state_closed)) * x3) + (espo_mate_successor_state_closed))))) /\ (((forall fom_index_successor_state_bounded. (exists fom_gap_successor_state_bounded_index_bound. fom_gap_successor_state_bounded_index_bound + S (fom_index_successor_state_bounded) = S m + S m) -> exists fom_value_successor_state_bounded. ((((exists fom_beta_height_successor_state_bounded_entry. fom_beta_height_successor_state_bounded_entry + S (fom_value_successor_state_bounded) = S ((S (fom_index_successor_state_bounded)) * x3)) /\ exists fom_beta_quotient_successor_state_bounded_entry. x2 = fom_beta_quotient_successor_state_bounded_entry * S ((S (fom_index_successor_state_bounded)) * x3) + (fom_value_successor_state_bounded))) /\ (exists fom_gap_successor_state_bounded_value_bound. fom_gap_successor_state_bounded_value_bound + S (fom_value_successor_state_bounded) = n))) /\ (forall wpo_injective_left_successor_state_injective wpo_injective_right_successor_state_injective wpo_injective_value_successor_state_injective. (exists wpo_gap_successor_state_injective_left_bound. wpo_gap_successor_state_injective_left_bound + S (wpo_injective_left_successor_state_injective) = S m + S m) -> (exists wpo_gap_successor_state_injective_right_bound. wpo_gap_successor_state_injective_right_bound + S (wpo_injective_right_successor_state_injective) = S m + S m) -> (((exists wpo_beta_height_successor_state_injective_left_entry. wpo_beta_height_successor_state_injective_left_entry + S (wpo_injective_value_successor_state_injective) = S ((S (wpo_injective_left_successor_state_injective)) * x3)) /\ exists wpo_beta_quotient_successor_state_injective_left_entry. x2 = wpo_beta_quotient_successor_state_injective_left_entry * S ((S (wpo_injective_left_successor_state_injective)) * x3) + (wpo_injective_value_successor_state_injective))) -> (((exists wpo_beta_height_successor_state_injective_right_entry. wpo_beta_height_successor_state_injective_right_entry + S (wpo_injective_value_successor_state_injective) = S ((S (wpo_injective_right_successor_state_injective)) * x3)) /\ exists wpo_beta_quotient_successor_state_injective_right_entry. x2 = wpo_beta_quotient_successor_state_injective_right_entry * S ((S (wpo_injective_right_successor_state_injective)) * x3) + (wpo_injective_value_successor_state_injective))) -> wpo_injective_left_successor_state_injective = wpo_injective_right_successor_state_injective))))
91. 0091rewrite <- hlength
92. 0092rewrite <- hlength
93. 0093rewrite <- hlength
94. 0094rewrite <- hlength
95. 0095rewrite <- hlength
96. 0096exact hnext_witness_witness_left
97. 0097exists x2
98. 0098exists x3
99. 0099split
100. 0100exact hsuccessor_state
101. 0101exact hnext_witness_witness_right