prime_wilson_terminal_product_package_exists

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 m
7. 0007intro hpn
8. 0008intro hp
9. 0009intro hinverse
10. 0010intro hnr
11. 0011intro hterminal
12. 0012have hpair_state : exists b c. ((((forall wpo_position_wtp_cap_state_closed wpo_source_wtp_cap_state_closed wpo_mate_wtp_cap_state_closed. (exists wpo_gap_wtp_cap_state_closed_position_bound. wpo_gap_wtp_cap_state_closed_position_bound + S (wpo_position_wtp_cap_state_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_closed_source_entry. wpo_beta_height_wtp_cap_state_closed_source_entry + S (wpo_source_wtp_cap_state_closed) = S ((S (wpo_position_wtp_cap_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_source_entry. b = wpo_beta_quotient_wtp_cap_state_closed_source_entry * S ((S (wpo_position_wtp_cap_state_closed)) * c) + (wpo_source_wtp_cap_state_closed))) -> (((exists wpo_beta_height_wtp_cap_state_closed_inverse_entry. wpo_beta_height_wtp_cap_state_closed_inverse_entry + S (wpo_mate_wtp_cap_state_closed) = S ((S (wpo_source_wtp_cap_state_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_state_closed_inverse_entry * S ((S (wpo_source_wtp_cap_state_closed)) * v) + (wpo_mate_wtp_cap_state_closed))) -> exists wpo_mate_position_wtp_cap_state_closed. ((exists wpo_gap_wtp_cap_state_closed_mate_bound. wpo_gap_wtp_cap_state_closed_mate_bound + S (wpo_mate_position_wtp_cap_state_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_state_closed_mate_entry. wpo_beta_height_wtp_cap_state_closed_mate_entry + S (wpo_mate_wtp_cap_state_closed) = S ((S (wpo_mate_position_wtp_cap_state_closed)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_closed_mate_entry. b = wpo_beta_quotient_wtp_cap_state_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_state_closed)) * c) + (wpo_mate_wtp_cap_state_closed))))) /\ ((forall fom_index_wtp_cap_state_bounded. (exists fom_gap_wtp_cap_state_bounded_index_bound. fom_gap_wtp_cap_state_bounded_index_bound + S (fom_index_wtp_cap_state_bounded) = m + m) -> exists fom_value_wtp_cap_state_bounded. ((((exists fom_beta_height_wtp_cap_state_bounded_entry. fom_beta_height_wtp_cap_state_bounded_entry + S (fom_value_wtp_cap_state_bounded) = S ((S (fom_index_wtp_cap_state_bounded)) * c)) /\ exists fom_beta_quotient_wtp_cap_state_bounded_entry. b = fom_beta_quotient_wtp_cap_state_bounded_entry * S ((S (fom_index_wtp_cap_state_bounded)) * c) + (fom_value_wtp_cap_state_bounded))) /\ (exists fom_gap_wtp_cap_state_bounded_value_bound. fom_gap_wtp_cap_state_bounded_value_bound + S (fom_value_wtp_cap_state_bounded) = n))) /\ ((forall wpo_position_wtp_cap_state_nonendpoint wpo_value_wtp_cap_state_nonendpoint. (exists wpo_gap_wtp_cap_state_nonendpoint_position_bound. wpo_gap_wtp_cap_state_nonendpoint_position_bound + S (wpo_position_wtp_cap_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_nonendpoint_entry. wpo_beta_height_wtp_cap_state_nonendpoint_entry + S (wpo_value_wtp_cap_state_nonendpoint) = S ((S (wpo_position_wtp_cap_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_nonendpoint_entry. b = wpo_beta_quotient_wtp_cap_state_nonendpoint_entry * S ((S (wpo_position_wtp_cap_state_nonendpoint)) * c) + (wpo_value_wtp_cap_state_nonendpoint))) -> (~(wpo_value_wtp_cap_state_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_cap_state_injective wpo_injective_right_wtp_cap_state_injective wpo_injective_value_wtp_cap_state_injective. (exists wpo_gap_wtp_cap_state_injective_left_bound. wpo_gap_wtp_cap_state_injective_left_bound + S (wpo_injective_left_wtp_cap_state_injective) = m + m) -> (exists wpo_gap_wtp_cap_state_injective_right_bound. wpo_gap_wtp_cap_state_injective_right_bound + S (wpo_injective_right_wtp_cap_state_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_injective_left_entry. wpo_beta_height_wtp_cap_state_injective_left_entry + S (wpo_injective_value_wtp_cap_state_injective) = S ((S (wpo_injective_left_wtp_cap_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_injective_left_entry. b = wpo_beta_quotient_wtp_cap_state_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_state_injective)) * c) + (wpo_injective_value_wtp_cap_state_injective))) -> (((exists wpo_beta_height_wtp_cap_state_injective_right_entry. wpo_beta_height_wtp_cap_state_injective_right_entry + S (wpo_injective_value_wtp_cap_state_injective) = S ((S (wpo_injective_right_wtp_cap_state_injective)) * c)) /\ exists wpo_beta_quotient_wtp_cap_state_injective_right_entry. b = wpo_beta_quotient_wtp_cap_state_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_state_injective)) * c) + (wpo_injective_value_wtp_cap_state_injective))) -> wpo_injective_left_wtp_cap_state_injective = wpo_injective_right_wtp_cap_state_injective))))) /\ (forall wpop_pair_wtp_cap_history. (exists wpo_gap_wtp_cap_history_pair_bound. wpo_gap_wtp_cap_history_pair_bound + S (wpop_pair_wtp_cap_history) = m) -> exists wpop_left_wtp_cap_history wpop_right_wtp_cap_history. ((((exists wpo_beta_height_wtp_cap_history_left_entry. wpo_beta_height_wtp_cap_history_left_entry + S (wpop_left_wtp_cap_history) = S ((S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history)) * c)) /\ exists wpo_beta_quotient_wtp_cap_history_left_entry. b = wpo_beta_quotient_wtp_cap_history_left_entry * S ((S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history)) * c) + (wpop_left_wtp_cap_history))) /\ ((((exists wpo_beta_height_wtp_cap_history_right_entry. wpo_beta_height_wtp_cap_history_right_entry + S (wpop_right_wtp_cap_history) = S ((S (S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history))) * c)) /\ exists wpo_beta_quotient_wtp_cap_history_right_entry. b = wpo_beta_quotient_wtp_cap_history_right_entry * S ((S (S (wpop_pair_wtp_cap_history + wpop_pair_wtp_cap_history))) * c) + (wpop_right_wtp_cap_history))) /\ (((exists wpo_beta_height_wtp_cap_history_inverse_entry. wpo_beta_height_wtp_cap_history_inverse_entry + S (wpop_right_wtp_cap_history) = S ((S (wpop_left_wtp_cap_history)) * v)) /\ exists wpo_beta_quotient_wtp_cap_history_inverse_entry. u = wpo_beta_quotient_wtp_cap_history_inverse_entry * S ((S (wpop_left_wtp_cap_history)) * v) + (wpop_right_wtp_cap_history)))))))
13. 0013specialize prime_pair_order_paired_terminal_state_exists p
14. 0014specialize prime_pair_order_paired_terminal_state_exists n
15. 0015specialize prime_pair_order_paired_terminal_state_exists u
16. 0016specialize prime_pair_order_paired_terminal_state_exists v
17. 0017specialize prime_pair_order_paired_terminal_state_exists r
18. 0018specialize prime_pair_order_paired_terminal_state_exists m
19. 0019apply prime_pair_order_paired_terminal_state_exists
20. 0020exact hpn
21. 0021exact hp
22. 0022exact hinverse
23. 0023exact hnr
24. 0024exact hterminal
25. 0025cases hpair_state
26. 0026cases hpair_state_witness
27. 0027cases hpair_state_witness_witness
28. 0028have hstate : ((forall wpo_position_wtp_cap_state_x_closed wpo_source_wtp_cap_state_x_closed wpo_mate_wtp_cap_state_x_closed. (exists wpo_gap_wtp_cap_state_x_closed_position_bound. wpo_gap_wtp_cap_state_x_closed_position_bound + S (wpo_position_wtp_cap_state_x_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_closed_source_entry. wpo_beta_height_wtp_cap_state_x_closed_source_entry + S (wpo_source_wtp_cap_state_x_closed) = S ((S (wpo_position_wtp_cap_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_source_entry. x = wpo_beta_quotient_wtp_cap_state_x_closed_source_entry * S ((S (wpo_position_wtp_cap_state_x_closed)) * x1) + (wpo_source_wtp_cap_state_x_closed))) -> (((exists wpo_beta_height_wtp_cap_state_x_closed_inverse_entry. wpo_beta_height_wtp_cap_state_x_closed_inverse_entry + S (wpo_mate_wtp_cap_state_x_closed) = S ((S (wpo_source_wtp_cap_state_x_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_state_x_closed_inverse_entry * S ((S (wpo_source_wtp_cap_state_x_closed)) * v) + (wpo_mate_wtp_cap_state_x_closed))) -> exists wpo_mate_position_wtp_cap_state_x_closed. ((exists wpo_gap_wtp_cap_state_x_closed_mate_bound. wpo_gap_wtp_cap_state_x_closed_mate_bound + S (wpo_mate_position_wtp_cap_state_x_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_state_x_closed_mate_entry. wpo_beta_height_wtp_cap_state_x_closed_mate_entry + S (wpo_mate_wtp_cap_state_x_closed) = S ((S (wpo_mate_position_wtp_cap_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_mate_entry. x = wpo_beta_quotient_wtp_cap_state_x_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_state_x_closed)) * x1) + (wpo_mate_wtp_cap_state_x_closed))))) /\ ((forall fom_index_wtp_cap_state_x_bounded. (exists fom_gap_wtp_cap_state_x_bounded_index_bound. fom_gap_wtp_cap_state_x_bounded_index_bound + S (fom_index_wtp_cap_state_x_bounded) = m + m) -> exists fom_value_wtp_cap_state_x_bounded. ((((exists fom_beta_height_wtp_cap_state_x_bounded_entry. fom_beta_height_wtp_cap_state_x_bounded_entry + S (fom_value_wtp_cap_state_x_bounded) = S ((S (fom_index_wtp_cap_state_x_bounded)) * x1)) /\ exists fom_beta_quotient_wtp_cap_state_x_bounded_entry. x = fom_beta_quotient_wtp_cap_state_x_bounded_entry * S ((S (fom_index_wtp_cap_state_x_bounded)) * x1) + (fom_value_wtp_cap_state_x_bounded))) /\ (exists fom_gap_wtp_cap_state_x_bounded_value_bound. fom_gap_wtp_cap_state_x_bounded_value_bound + S (fom_value_wtp_cap_state_x_bounded) = n))) /\ ((forall wpo_position_wtp_cap_state_x_nonendpoint wpo_value_wtp_cap_state_x_nonendpoint. (exists wpo_gap_wtp_cap_state_x_nonendpoint_position_bound. wpo_gap_wtp_cap_state_x_nonendpoint_position_bound + S (wpo_position_wtp_cap_state_x_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_nonendpoint_entry. wpo_beta_height_wtp_cap_state_x_nonendpoint_entry + S (wpo_value_wtp_cap_state_x_nonendpoint) = S ((S (wpo_position_wtp_cap_state_x_nonendpoint)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_nonendpoint_entry. x = wpo_beta_quotient_wtp_cap_state_x_nonendpoint_entry * S ((S (wpo_position_wtp_cap_state_x_nonendpoint)) * x1) + (wpo_value_wtp_cap_state_x_nonendpoint))) -> (~(wpo_value_wtp_cap_state_x_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_state_x_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_cap_state_x_injective wpo_injective_right_wtp_cap_state_x_injective wpo_injective_value_wtp_cap_state_x_injective. (exists wpo_gap_wtp_cap_state_x_injective_left_bound. wpo_gap_wtp_cap_state_x_injective_left_bound + S (wpo_injective_left_wtp_cap_state_x_injective) = m + m) -> (exists wpo_gap_wtp_cap_state_x_injective_right_bound. wpo_gap_wtp_cap_state_x_injective_right_bound + S (wpo_injective_right_wtp_cap_state_x_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_injective_left_entry. wpo_beta_height_wtp_cap_state_x_injective_left_entry + S (wpo_injective_value_wtp_cap_state_x_injective) = S ((S (wpo_injective_left_wtp_cap_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_injective_left_entry. x = wpo_beta_quotient_wtp_cap_state_x_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_state_x_injective))) -> (((exists wpo_beta_height_wtp_cap_state_x_injective_right_entry. wpo_beta_height_wtp_cap_state_x_injective_right_entry + S (wpo_injective_value_wtp_cap_state_x_injective) = S ((S (wpo_injective_right_wtp_cap_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_injective_right_entry. x = wpo_beta_quotient_wtp_cap_state_x_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_state_x_injective))) -> wpo_injective_left_wtp_cap_state_x_injective = wpo_injective_right_wtp_cap_state_x_injective))))
29. 0029exact hpair_state_witness_witness_left
30. 0030have hhistory : forall wpop_pair_wtp_cap_history_x. (exists wpo_gap_wtp_cap_history_x_pair_bound. wpo_gap_wtp_cap_history_x_pair_bound + S (wpop_pair_wtp_cap_history_x) = m) -> exists wpop_left_wtp_cap_history_x wpop_right_wtp_cap_history_x. ((((exists wpo_beta_height_wtp_cap_history_x_left_entry. wpo_beta_height_wtp_cap_history_x_left_entry + S (wpop_left_wtp_cap_history_x) = S ((S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_history_x_left_entry. x = wpo_beta_quotient_wtp_cap_history_x_left_entry * S ((S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x)) * x1) + (wpop_left_wtp_cap_history_x))) /\ ((((exists wpo_beta_height_wtp_cap_history_x_right_entry. wpo_beta_height_wtp_cap_history_x_right_entry + S (wpop_right_wtp_cap_history_x) = S ((S (S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x))) * x1)) /\ exists wpo_beta_quotient_wtp_cap_history_x_right_entry. x = wpo_beta_quotient_wtp_cap_history_x_right_entry * S ((S (S (wpop_pair_wtp_cap_history_x + wpop_pair_wtp_cap_history_x))) * x1) + (wpop_right_wtp_cap_history_x))) /\ (((exists wpo_beta_height_wtp_cap_history_x_inverse_entry. wpo_beta_height_wtp_cap_history_x_inverse_entry + S (wpop_right_wtp_cap_history_x) = S ((S (wpop_left_wtp_cap_history_x)) * v)) /\ exists wpo_beta_quotient_wtp_cap_history_x_inverse_entry. u = wpo_beta_quotient_wtp_cap_history_x_inverse_entry * S ((S (wpop_left_wtp_cap_history_x)) * v) + (wpop_right_wtp_cap_history_x)))))
31. 0031exact hpair_state_witness_witness_right
32. 0032have hstate_parts : ((forall wpo_position_wtp_cap_state_x_closed wpo_source_wtp_cap_state_x_closed wpo_mate_wtp_cap_state_x_closed. (exists wpo_gap_wtp_cap_state_x_closed_position_bound. wpo_gap_wtp_cap_state_x_closed_position_bound + S (wpo_position_wtp_cap_state_x_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_closed_source_entry. wpo_beta_height_wtp_cap_state_x_closed_source_entry + S (wpo_source_wtp_cap_state_x_closed) = S ((S (wpo_position_wtp_cap_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_source_entry. x = wpo_beta_quotient_wtp_cap_state_x_closed_source_entry * S ((S (wpo_position_wtp_cap_state_x_closed)) * x1) + (wpo_source_wtp_cap_state_x_closed))) -> (((exists wpo_beta_height_wtp_cap_state_x_closed_inverse_entry. wpo_beta_height_wtp_cap_state_x_closed_inverse_entry + S (wpo_mate_wtp_cap_state_x_closed) = S ((S (wpo_source_wtp_cap_state_x_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_state_x_closed_inverse_entry * S ((S (wpo_source_wtp_cap_state_x_closed)) * v) + (wpo_mate_wtp_cap_state_x_closed))) -> exists wpo_mate_position_wtp_cap_state_x_closed. ((exists wpo_gap_wtp_cap_state_x_closed_mate_bound. wpo_gap_wtp_cap_state_x_closed_mate_bound + S (wpo_mate_position_wtp_cap_state_x_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_state_x_closed_mate_entry. wpo_beta_height_wtp_cap_state_x_closed_mate_entry + S (wpo_mate_wtp_cap_state_x_closed) = S ((S (wpo_mate_position_wtp_cap_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_closed_mate_entry. x = wpo_beta_quotient_wtp_cap_state_x_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_state_x_closed)) * x1) + (wpo_mate_wtp_cap_state_x_closed))))) /\ ((forall fom_index_wtp_cap_state_x_bounded. (exists fom_gap_wtp_cap_state_x_bounded_index_bound. fom_gap_wtp_cap_state_x_bounded_index_bound + S (fom_index_wtp_cap_state_x_bounded) = m + m) -> exists fom_value_wtp_cap_state_x_bounded. ((((exists fom_beta_height_wtp_cap_state_x_bounded_entry. fom_beta_height_wtp_cap_state_x_bounded_entry + S (fom_value_wtp_cap_state_x_bounded) = S ((S (fom_index_wtp_cap_state_x_bounded)) * x1)) /\ exists fom_beta_quotient_wtp_cap_state_x_bounded_entry. x = fom_beta_quotient_wtp_cap_state_x_bounded_entry * S ((S (fom_index_wtp_cap_state_x_bounded)) * x1) + (fom_value_wtp_cap_state_x_bounded))) /\ (exists fom_gap_wtp_cap_state_x_bounded_value_bound. fom_gap_wtp_cap_state_x_bounded_value_bound + S (fom_value_wtp_cap_state_x_bounded) = n))) /\ ((forall wpo_position_wtp_cap_state_x_nonendpoint wpo_value_wtp_cap_state_x_nonendpoint. (exists wpo_gap_wtp_cap_state_x_nonendpoint_position_bound. wpo_gap_wtp_cap_state_x_nonendpoint_position_bound + S (wpo_position_wtp_cap_state_x_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_nonendpoint_entry. wpo_beta_height_wtp_cap_state_x_nonendpoint_entry + S (wpo_value_wtp_cap_state_x_nonendpoint) = S ((S (wpo_position_wtp_cap_state_x_nonendpoint)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_nonendpoint_entry. x = wpo_beta_quotient_wtp_cap_state_x_nonendpoint_entry * S ((S (wpo_position_wtp_cap_state_x_nonendpoint)) * x1) + (wpo_value_wtp_cap_state_x_nonendpoint))) -> (~(wpo_value_wtp_cap_state_x_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_state_x_nonendpoint) = n))) /\ (forall wpo_injective_left_wtp_cap_state_x_injective wpo_injective_right_wtp_cap_state_x_injective wpo_injective_value_wtp_cap_state_x_injective. (exists wpo_gap_wtp_cap_state_x_injective_left_bound. wpo_gap_wtp_cap_state_x_injective_left_bound + S (wpo_injective_left_wtp_cap_state_x_injective) = m + m) -> (exists wpo_gap_wtp_cap_state_x_injective_right_bound. wpo_gap_wtp_cap_state_x_injective_right_bound + S (wpo_injective_right_wtp_cap_state_x_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_state_x_injective_left_entry. wpo_beta_height_wtp_cap_state_x_injective_left_entry + S (wpo_injective_value_wtp_cap_state_x_injective) = S ((S (wpo_injective_left_wtp_cap_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_injective_left_entry. x = wpo_beta_quotient_wtp_cap_state_x_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_state_x_injective))) -> (((exists wpo_beta_height_wtp_cap_state_x_injective_right_entry. wpo_beta_height_wtp_cap_state_x_injective_right_entry + S (wpo_injective_value_wtp_cap_state_x_injective) = S ((S (wpo_injective_right_wtp_cap_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_state_x_injective_right_entry. x = wpo_beta_quotient_wtp_cap_state_x_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_state_x_injective))) -> wpo_injective_left_wtp_cap_state_x_injective = wpo_injective_right_wtp_cap_state_x_injective))))
33. 0033exact hstate
34. 0034cases hstate_parts
35. 0035cases hstate_parts_right
36. 0036cases hstate_parts_right_right
37. 0037have hexact_state : ((forall wpo_position_wtp_cap_exact_state_x_closed wpo_source_wtp_cap_exact_state_x_closed wpo_mate_wtp_cap_exact_state_x_closed. (exists wpo_gap_wtp_cap_exact_state_x_closed_position_bound. wpo_gap_wtp_cap_exact_state_x_closed_position_bound + S (wpo_position_wtp_cap_exact_state_x_closed) = m + m) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_closed_source_entry. wpo_beta_height_wtp_cap_exact_state_x_closed_source_entry + S (wpo_source_wtp_cap_exact_state_x_closed) = S ((S (wpo_position_wtp_cap_exact_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_closed_source_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_closed_source_entry * S ((S (wpo_position_wtp_cap_exact_state_x_closed)) * x1) + (wpo_source_wtp_cap_exact_state_x_closed))) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_closed_inverse_entry. wpo_beta_height_wtp_cap_exact_state_x_closed_inverse_entry + S (wpo_mate_wtp_cap_exact_state_x_closed) = S ((S (wpo_source_wtp_cap_exact_state_x_closed)) * v)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_closed_inverse_entry. u = wpo_beta_quotient_wtp_cap_exact_state_x_closed_inverse_entry * S ((S (wpo_source_wtp_cap_exact_state_x_closed)) * v) + (wpo_mate_wtp_cap_exact_state_x_closed))) -> exists wpo_mate_position_wtp_cap_exact_state_x_closed. ((exists wpo_gap_wtp_cap_exact_state_x_closed_mate_bound. wpo_gap_wtp_cap_exact_state_x_closed_mate_bound + S (wpo_mate_position_wtp_cap_exact_state_x_closed) = m + m) /\ (((exists wpo_beta_height_wtp_cap_exact_state_x_closed_mate_entry. wpo_beta_height_wtp_cap_exact_state_x_closed_mate_entry + S (wpo_mate_wtp_cap_exact_state_x_closed) = S ((S (wpo_mate_position_wtp_cap_exact_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_closed_mate_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_closed_mate_entry * S ((S (wpo_mate_position_wtp_cap_exact_state_x_closed)) * x1) + (wpo_mate_wtp_cap_exact_state_x_closed))))) /\ ((forall fom_index_wtp_cap_exact_state_x_bounded. (exists fom_gap_wtp_cap_exact_state_x_bounded_index_bound. fom_gap_wtp_cap_exact_state_x_bounded_index_bound + S (fom_index_wtp_cap_exact_state_x_bounded) = m + m) -> exists fom_value_wtp_cap_exact_state_x_bounded. ((((exists fom_beta_height_wtp_cap_exact_state_x_bounded_entry. fom_beta_height_wtp_cap_exact_state_x_bounded_entry + S (fom_value_wtp_cap_exact_state_x_bounded) = S ((S (fom_index_wtp_cap_exact_state_x_bounded)) * x1)) /\ exists fom_beta_quotient_wtp_cap_exact_state_x_bounded_entry. x = fom_beta_quotient_wtp_cap_exact_state_x_bounded_entry * S ((S (fom_index_wtp_cap_exact_state_x_bounded)) * x1) + (fom_value_wtp_cap_exact_state_x_bounded))) /\ (exists fom_gap_wtp_cap_exact_state_x_bounded_value_bound. fom_gap_wtp_cap_exact_state_x_bounded_value_bound + S (fom_value_wtp_cap_exact_state_x_bounded) = S (S (m + m))))) /\ ((forall wpo_position_wtp_cap_exact_state_x_nonendpoint wpo_value_wtp_cap_exact_state_x_nonendpoint. (exists wpo_gap_wtp_cap_exact_state_x_nonendpoint_position_bound. wpo_gap_wtp_cap_exact_state_x_nonendpoint_position_bound + S (wpo_position_wtp_cap_exact_state_x_nonendpoint) = m + m) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_nonendpoint_entry. wpo_beta_height_wtp_cap_exact_state_x_nonendpoint_entry + S (wpo_value_wtp_cap_exact_state_x_nonendpoint) = S ((S (wpo_position_wtp_cap_exact_state_x_nonendpoint)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_nonendpoint_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_nonendpoint_entry * S ((S (wpo_position_wtp_cap_exact_state_x_nonendpoint)) * x1) + (wpo_value_wtp_cap_exact_state_x_nonendpoint))) -> (~(wpo_value_wtp_cap_exact_state_x_nonendpoint = 0) /\ ~((S wpo_value_wtp_cap_exact_state_x_nonendpoint) = S (S (m + m))))) /\ (forall wpo_injective_left_wtp_cap_exact_state_x_injective wpo_injective_right_wtp_cap_exact_state_x_injective wpo_injective_value_wtp_cap_exact_state_x_injective. (exists wpo_gap_wtp_cap_exact_state_x_injective_left_bound. wpo_gap_wtp_cap_exact_state_x_injective_left_bound + S (wpo_injective_left_wtp_cap_exact_state_x_injective) = m + m) -> (exists wpo_gap_wtp_cap_exact_state_x_injective_right_bound. wpo_gap_wtp_cap_exact_state_x_injective_right_bound + S (wpo_injective_right_wtp_cap_exact_state_x_injective) = m + m) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_injective_left_entry. wpo_beta_height_wtp_cap_exact_state_x_injective_left_entry + S (wpo_injective_value_wtp_cap_exact_state_x_injective) = S ((S (wpo_injective_left_wtp_cap_exact_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_injective_left_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_injective_left_entry * S ((S (wpo_injective_left_wtp_cap_exact_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_exact_state_x_injective))) -> (((exists wpo_beta_height_wtp_cap_exact_state_x_injective_right_entry. wpo_beta_height_wtp_cap_exact_state_x_injective_right_entry + S (wpo_injective_value_wtp_cap_exact_state_x_injective) = S ((S (wpo_injective_right_wtp_cap_exact_state_x_injective)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_exact_state_x_injective_right_entry. x = wpo_beta_quotient_wtp_cap_exact_state_x_injective_right_entry * S ((S (wpo_injective_right_wtp_cap_exact_state_x_injective)) * x1) + (wpo_injective_value_wtp_cap_exact_state_x_injective))) -> wpo_injective_left_wtp_cap_exact_state_x_injective = wpo_injective_right_wtp_cap_exact_state_x_injective))))
38. 0038rewrite <- hterminal
39. 0039rewrite <- hterminal
40. 0040exact hstate
41. 0041have hcoverage : forall s. (exists wpo_gap_wtp_cap_coverage_value_bound. wpo_gap_wtp_cap_coverage_value_bound + S (s) = S (S (m + m))) -> (~(s = 0) /\ ~((S s) = S (S (m + m)))) -> exists q. ((exists wpo_gap_wtp_cap_coverage_index_bound. wpo_gap_wtp_cap_coverage_index_bound + S (q) = m + m) /\ (((exists wpo_beta_height_wtp_cap_coverage_entry_x. wpo_beta_height_wtp_cap_coverage_entry_x + S (s) = S ((S (q)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_coverage_entry_x. x = wpo_beta_quotient_wtp_cap_coverage_entry_x * S ((S (q)) * x1) + (s))))
42. 0042specialize pair_order_state_terminal_coverage u
43. 0043specialize pair_order_state_terminal_coverage v
44. 0044specialize pair_order_state_terminal_coverage x
45. 0045specialize pair_order_state_terminal_coverage x1
46. 0046specialize pair_order_state_terminal_coverage (m + m)
47. 0047apply pair_order_state_terminal_coverage
48. 0048exact hexact_state
49. 0049have hrange : forall gmp_index_wtp_cap_range. (exists gsp_lt_gap_wtp_cap_range_index_bound. gsp_lt_gap_wtp_cap_range_index_bound + S gmp_index_wtp_cap_range = m + m) -> exists gmp_magnitude_wtp_cap_range. ((((exists ff_h_gmp_wtp_cap_range_decoded. ff_h_gmp_wtp_cap_range_decoded + S (gmp_magnitude_wtp_cap_range) = S ((S (gmp_index_wtp_cap_range)) * x1)) /\ exists ff_q_gmp_wtp_cap_range_decoded. x = ff_q_gmp_wtp_cap_range_decoded * S ((S (gmp_index_wtp_cap_range)) * x1) + (gmp_magnitude_wtp_cap_range))) /\ ((exists gsp_lt_gap_wtp_cap_range_positive. gsp_lt_gap_wtp_cap_range_positive + S 0 = gmp_magnitude_wtp_cap_range) /\ (exists gsp_le_gap_wtp_cap_range_bounded. gsp_le_gap_wtp_cap_range_bounded + gmp_magnitude_wtp_cap_range = m + m)))
50. 0050specialize pair_order_terminal_state_magnitude_range u
51. 0051specialize pair_order_terminal_state_magnitude_range v
52. 0052specialize pair_order_terminal_state_magnitude_range x
53. 0053specialize pair_order_terminal_state_magnitude_range x1
54. 0054specialize pair_order_terminal_state_magnitude_range (m + m)
55. 0055specialize pair_order_terminal_state_magnitude_range n
56. 0056apply pair_order_terminal_state_magnitude_range
57. 0057exact hterminal
58. 0058exact hstate
59. 0059have hfactor_product : exists f g Q. ((forall wsl_index_wtp_cap_lift_x wsl_value_wtp_cap_lift_x. (exists wpo_gap_wtp_cap_lift_x_bound. wpo_gap_wtp_cap_lift_x_bound + S (wsl_index_wtp_cap_lift_x) = m + m) -> (((exists wpo_beta_height_wtp_cap_lift_x_source. wpo_beta_height_wtp_cap_lift_x_source + S (wsl_value_wtp_cap_lift_x) = S ((S (wsl_index_wtp_cap_lift_x)) * x1)) /\ exists wpo_beta_quotient_wtp_cap_lift_x_source. x = wpo_beta_quotient_wtp_cap_lift_x_source * S ((S (wsl_index_wtp_cap_lift_x)) * x1) + (wsl_value_wtp_cap_lift_x))) -> (((exists wpo_beta_height_wtp_cap_lift_x_target. wpo_beta_height_wtp_cap_lift_x_target + S (S wsl_value_wtp_cap_lift_x) = S ((S (wsl_index_wtp_cap_lift_x)) * g)) /\ exists wpo_beta_quotient_wtp_cap_lift_x_target. f = wpo_beta_quotient_wtp_cap_lift_x_target * S ((S (wsl_index_wtp_cap_lift_x)) * g) + (S wsl_value_wtp_cap_lift_x)))) /\ (((forall wpp_pair_wtp_cap_adjacent wpp_left_wtp_cap_adjacent wpp_right_wtp_cap_adjacent. (exists wpp_gap_wtp_cap_adjacent_pair_bound. wpp_gap_wtp_cap_adjacent_pair_bound + S (wpp_pair_wtp_cap_adjacent) = m) -> (((exists wpp_beta_height_wtp_cap_adjacent_left_entry. wpp_beta_height_wtp_cap_adjacent_left_entry + S (wpp_left_wtp_cap_adjacent) = S ((S ((wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g)) /\ exists wpp_beta_quotient_wtp_cap_adjacent_left_entry. f = wpp_beta_quotient_wtp_cap_adjacent_left_entry * S ((S ((wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g) + (wpp_left_wtp_cap_adjacent))) -> (((exists wpp_beta_height_wtp_cap_adjacent_right_entry. wpp_beta_height_wtp_cap_adjacent_right_entry + S (wpp_right_wtp_cap_adjacent) = S ((S (S (wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g)) /\ exists wpp_beta_quotient_wtp_cap_adjacent_right_entry. f = wpp_beta_quotient_wtp_cap_adjacent_right_entry * S ((S (S (wpp_pair_wtp_cap_adjacent + wpp_pair_wtp_cap_adjacent))) * g) + (wpp_right_wtp_cap_adjacent))) -> (exists wpp_mod_left_wtp_cap_adjacent_pair_mod wpp_mod_right_wtp_cap_adjacent_pair_mod. (wpp_left_wtp_cap_adjacent * wpp_right_wtp_cap_adjacent) + p * wpp_mod_left_wtp_cap_adjacent_pair_mod = (1) + p * wpp_mod_right_wtp_cap_adjacent_pair_mod)) /\ (((exists ff_u_wtp_cap_lifted_product ff_v_wtp_cap_lifted_product. ((((exists ff_h_wtp_cap_lifted_product_start. ff_h_wtp_cap_lifted_product_start + S (1) = S ((S (0)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_start. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_start * S ((S (0)) * ff_v_wtp_cap_lifted_product) + (1))) /\ ((((exists ff_h_wtp_cap_lifted_product_terminal. ff_h_wtp_cap_lifted_product_terminal + S (Q) = S ((S (m + m)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_terminal. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_terminal * S ((S (m + m)) * ff_v_wtp_cap_lifted_product) + (Q))) /\ forall ff_i_wtp_cap_lifted_product. (exists ff_lt_wtp_cap_lifted_product_bound. ff_lt_wtp_cap_lifted_product_bound + S ff_i_wtp_cap_lifted_product = m + m) -> exists ff_p_wtp_cap_lifted_product ff_r_wtp_cap_lifted_product ff_s_wtp_cap_lifted_product. ((((exists ff_h_wtp_cap_lifted_product_factor. ff_h_wtp_cap_lifted_product_factor + S (ff_p_wtp_cap_lifted_product) = S ((S (ff_i_wtp_cap_lifted_product)) * g)) /\ exists ff_q_wtp_cap_lifted_product_factor. f = ff_q_wtp_cap_lifted_product_factor * S ((S (ff_i_wtp_cap_lifted_product)) * g) + (ff_p_wtp_cap_lifted_product))) /\ ((((exists ff_h_wtp_cap_lifted_product_partial. ff_h_wtp_cap_lifted_product_partial + S (ff_r_wtp_cap_lifted_product) = S ((S (ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_partial. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_partial * S ((S (ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product) + (ff_r_wtp_cap_lifted_product))) /\ ((((exists ff_h_wtp_cap_lifted_product_successor. ff_h_wtp_cap_lifted_product_successor + S (ff_s_wtp_cap_lifted_product) = S ((S (S ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product)) /\ exists ff_q_wtp_cap_lifted_product_successor. ff_u_wtp_cap_lifted_product = ff_q_wtp_cap_lifted_product_successor * S ((S (S ff_i_wtp_cap_lifted_product)) * ff_v_wtp_cap_lifted_product) + (ff_s_wtp_cap_lifted_product))) /\ ff_s_wtp_cap_lifted_product = ff_r_wtp_cap_lifted_product * ff_p_wtp_cap_lifted_product)))))) /\ (exists wpp_mod_left_wtp_cap_mod_one wpp_mod_right_wtp_cap_mod_one. (Q) + p * wpp_mod_left_wtp_cap_mod_one = (1) + p * wpp_mod_right_wtp_cap_mod_one))))))
60. 0060specialize paired_pair_order_product_one_exists p
61. 0061specialize paired_pair_order_product_one_exists n
62. 0062specialize paired_pair_order_product_one_exists u
63. 0063specialize paired_pair_order_product_one_exists v
64. 0064specialize paired_pair_order_product_one_exists x
65. 0065specialize paired_pair_order_product_one_exists x1
66. 0066specialize paired_pair_order_product_one_exists m
67. 0067apply paired_pair_order_product_one_exists
68. 0068exact hinverse
69. 0069exact hstate_parts_right_left
70. 0070exact hhistory
71. 0071cases hfactor_product
72. 0072cases hfactor_product_witness
73. 0073cases hfactor_product_witness_witness
74. 0074cases hfactor_product_witness_witness_witness
75. 0075cases hfactor_product_witness_witness_witness_right
76. 0076cases hfactor_product_witness_witness_witness_right_right
77. 0077have hcanonical_range_exists : exists z d. (forall wtp_range_index_wtp_cap_range_two. (exists wtp_range_gap_wtp_cap_range_two. wtp_range_gap_wtp_cap_range_two + S wtp_range_index_wtp_cap_range_two = m + m) -> (((exists ff_h_wtp_cap_range_two_decoded. ff_h_wtp_cap_range_two_decoded + S (2 + wtp_range_index_wtp_cap_range_two) = S ((S (wtp_range_index_wtp_cap_range_two)) * d)) /\ exists ff_q_wtp_cap_range_two_decoded. z = ff_q_wtp_cap_range_two_decoded * S ((S (wtp_range_index_wtp_cap_range_two)) * d) + (2 + wtp_range_index_wtp_cap_range_two))))
78. 0078specialize beta_range_exists 2
79. 0079specialize beta_range_exists (m + m)
80. 0080exact beta_range_exists
81. 0081cases hcanonical_range_exists
82. 0082cases hcanonical_range_exists_witness
83. 0083have hcanonical_product_exists : exists P. (exists ff_u_wtp_cap_canonical_product_x5_x6 ff_v_wtp_cap_canonical_product_x5_x6. ((((exists ff_h_wtp_cap_canonical_product_x5_x6_start. ff_h_wtp_cap_canonical_product_x5_x6_start + S (1) = S ((S (0)) * ff_v_wtp_cap_canonical_product_x5_x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_start. ff_u_wtp_cap_canonical_product_x5_x6 = ff_q_wtp_cap_canonical_product_x5_x6_start * S ((S (0)) * ff_v_wtp_cap_canonical_product_x5_x6) + (1))) /\ ((((exists ff_h_wtp_cap_canonical_product_x5_x6_terminal. ff_h_wtp_cap_canonical_product_x5_x6_terminal + S (P) = S ((S (m + m)) * ff_v_wtp_cap_canonical_product_x5_x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_terminal. ff_u_wtp_cap_canonical_product_x5_x6 = ff_q_wtp_cap_canonical_product_x5_x6_terminal * S ((S (m + m)) * ff_v_wtp_cap_canonical_product_x5_x6) + (P))) /\ forall ff_i_wtp_cap_canonical_product_x5_x6. (exists ff_lt_wtp_cap_canonical_product_x5_x6_bound. ff_lt_wtp_cap_canonical_product_x5_x6_bound + S ff_i_wtp_cap_canonical_product_x5_x6 = m + m) -> exists ff_p_wtp_cap_canonical_product_x5_x6 ff_r_wtp_cap_canonical_product_x5_x6 ff_s_wtp_cap_canonical_product_x5_x6. ((((exists ff_h_wtp_cap_canonical_product_x5_x6_factor. ff_h_wtp_cap_canonical_product_x5_x6_factor + S (ff_p_wtp_cap_canonical_product_x5_x6) = S ((S (ff_i_wtp_cap_canonical_product_x5_x6)) * x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_factor. x5 = ff_q_wtp_cap_canonical_product_x5_x6_factor * S ((S (ff_i_wtp_cap_canonical_product_x5_x6)) * x6) + (ff_p_wtp_cap_canonical_product_x5_x6))) /\ ((((exists ff_h_wtp_cap_canonical_product_x5_x6_partial. ff_h_wtp_cap_canonical_product_x5_x6_partial + S (ff_r_wtp_cap_canonical_product_x5_x6) = S ((S (ff_i_wtp_cap_canonical_product_x5_x6)) * ff_v_wtp_cap_canonical_product_x5_x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_partial. ff_u_wtp_cap_canonical_product_x5_x6 = ff_q_wtp_cap_canonical_product_x5_x6_partial * S ((S (ff_i_wtp_cap_canonical_product_x5_x6)) * ff_v_wtp_cap_canonical_product_x5_x6) + (ff_r_wtp_cap_canonical_product_x5_x6))) /\ ((((exists ff_h_wtp_cap_canonical_product_x5_x6_successor. ff_h_wtp_cap_canonical_product_x5_x6_successor + S (ff_s_wtp_cap_canonical_product_x5_x6) = S ((S (S ff_i_wtp_cap_canonical_product_x5_x6)) * ff_v_wtp_cap_canonical_product_x5_x6)) /\ exists ff_q_wtp_cap_canonical_product_x5_x6_successor. ff_u_wtp_cap_canonical_product_x5_x6 = ff_q_wtp_cap_canonical_product_x5_x6_successor * S ((S (S ff_i_wtp_cap_canonical_product_x5_x6)) * ff_v_wtp_cap_canonical_product_x5_x6) + (ff_s_wtp_cap_canonical_product_x5_x6))) /\ ff_s_wtp_cap_canonical_product_x5_x6 = ff_r_wtp_cap_canonical_product_x5_x6 * ff_p_wtp_cap_canonical_product_x5_x6))))))
84. 0084specialize beta_product_exists x5
85. 0085specialize beta_product_exists x6
86. 0086specialize beta_product_exists (m + m)
87. 0087exact beta_product_exists
88. 0088cases hcanonical_product_exists
89. 0089have hrecode_exists : exists rb rc. forall gmp_index_wtp_cap_recode gmp_predecessor_wtp_cap_recode. (exists gsp_lt_gap_wtp_cap_recode_index_bound. gsp_lt_gap_wtp_cap_recode_index_bound + S gmp_index_wtp_cap_recode = m + m) -> (((exists gsp_beta_height_gmp_wtp_cap_recode_source. gsp_beta_height_gmp_wtp_cap_recode_source + S (S gmp_predecessor_wtp_cap_recode) = S ((S (gmp_index_wtp_cap_recode)) * x1)) /\ exists gsp_beta_quotient_gmp_wtp_cap_recode_source. x = gsp_beta_quotient_gmp_wtp_cap_recode_source * S ((S (gmp_index_wtp_cap_recode)) * x1) + (S gmp_predecessor_wtp_cap_recode))) -> (((exists ff_h_gmp_wtp_cap_recode_target. ff_h_gmp_wtp_cap_recode_target + S (gmp_predecessor_wtp_cap_recode) = S ((S (gmp_index_wtp_cap_recode)) * rc)) /\ exists ff_q_gmp_wtp_cap_recode_target. rb = ff_q_gmp_wtp_cap_recode_target * S ((S (gmp_index_wtp_cap_recode)) * rc) + (gmp_predecessor_wtp_cap_recode)))
90. 0090specialize beta_magnitude_predecessor_recode_exists x
91. 0091specialize beta_magnitude_predecessor_recode_exists x1
92. 0092specialize beta_magnitude_predecessor_recode_exists (m + m)
93. 0093specialize beta_magnitude_predecessor_recode_exists (m + m)
94. 0094apply beta_magnitude_predecessor_recode_exists
95. 0095exact hrange
96. 0096cases hrecode_exists
97. 0097cases hrecode_exists_witness
98. 0098have hequal : x7 = x4
99. 0099specialize pair_order_terminal_successor_product_eq_range_two x
100. 0100specialize pair_order_terminal_successor_product_eq_range_two x1
101. 0101specialize pair_order_terminal_successor_product_eq_range_two x8
102. 0102specialize pair_order_terminal_successor_product_eq_range_two x9
103. 0103specialize pair_order_terminal_successor_product_eq_range_two x5
104. 0104specialize pair_order_terminal_successor_product_eq_range_two x6
105. 0105specialize pair_order_terminal_successor_product_eq_range_two x2
106. 0106specialize pair_order_terminal_successor_product_eq_range_two x3
107. 0107specialize pair_order_terminal_successor_product_eq_range_two (m + m)
108. 0108specialize pair_order_terminal_successor_product_eq_range_two x7
109. 0109specialize pair_order_terminal_successor_product_eq_range_two x4
110. 0110apply pair_order_terminal_successor_product_eq_range_two
111. 0111exact hrange
112. 0112exact hstate_parts_right_right_right
113. 0113exact hrecode_exists_witness_witness
114. 0114exact hfactor_product_witness_witness_witness_left
115. 0115exact hcanonical_range_exists_witness_witness
116. 0116exact hcanonical_product_exists_witness
117. 0117exact hfactor_product_witness_witness_witness_right_right_left
118. 0118exists x
119. 0119exists x1
120. 0120exists x2
121. 0121exists x3
122. 0122exists x4
123. 0123exists x5
124. 0124exists x6
125. 0125exists x7
126. 0126split
127. 0127exact hstate
128. 0128split
129. 0129exact hhistory
130. 0130split
131. 0131exact hcoverage
132. 0132split
133. 0133exact hfactor_product_witness_witness_witness_left
134. 0134split
135. 0135exact hfactor_product_witness_witness_witness_right_left
136. 0136split
137. 0137exact hfactor_product_witness_witness_witness_right_right_left
138. 0138split
139. 0139exact hfactor_product_witness_witness_witness_right_right_right
140. 0140split
141. 0141exact hcanonical_range_exists_witness_witness
142. 0142split
143. 0143exact hcanonical_product_exists_witness
144. 0144exact hequal