prime_terminal_range_two_product_mod_one_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 m
4. 0004intro hpn
5. 0005intro hp
6. 0006intro hterminal
7. 0007have hinverse : exists u v. (forall wip_index_wer_terminal_inverse. (exists wip_gap_wer_terminal_inverse_prefix_bound. wip_gap_wer_terminal_inverse_prefix_bound + S wip_index_wer_terminal_inverse = n) -> exists wip_mate_wer_terminal_inverse. ((((exists wip_beta_height_wer_terminal_inverse_decoded. wip_beta_height_wer_terminal_inverse_decoded + S (wip_mate_wer_terminal_inverse) = S ((S (wip_index_wer_terminal_inverse)) * v)) /\ exists wip_beta_quotient_wer_terminal_inverse_decoded. u = wip_beta_quotient_wer_terminal_inverse_decoded * S ((S (wip_index_wer_terminal_inverse)) * v) + (wip_mate_wer_terminal_inverse))) /\ ((exists wip_gap_wer_terminal_inverse_inverse_index_bound. wip_gap_wer_terminal_inverse_inverse_index_bound + S wip_index_wer_terminal_inverse = n) /\ ((exists wip_gap_wer_terminal_inverse_inverse_mate_bound. wip_gap_wer_terminal_inverse_inverse_mate_bound + S wip_mate_wer_terminal_inverse = n) /\ (exists wip_mod_left_wer_terminal_inverse_inverse_mod wip_mod_right_wer_terminal_inverse_inverse_mod. ((S wip_index_wer_terminal_inverse) * S wip_mate_wer_terminal_inverse) + p * wip_mod_left_wer_terminal_inverse_inverse_mod = 1 + p * wip_mod_right_wer_terminal_inverse_inverse_mod)))))
8. 0008specialize prime_inverse_prefix_exists p
9. 0009specialize prime_inverse_prefix_exists n
10. 0010apply prime_inverse_prefix_exists
11. 0011exact hpn
12. 0012exact hp
13. 0013cases hinverse
14. 0014cases hinverse_witness
15. 0015have hpackage : exists b c f g Q z d P. ((((forall wpo_position_wer_terminal_state_x_closed wpo_source_wer_terminal_state_x_closed wpo_mate_wer_terminal_state_x_closed. (exists wpo_gap_wer_terminal_state_x_closed_position_bound. wpo_gap_wer_terminal_state_x_closed_position_bound + S (wpo_position_wer_terminal_state_x_closed) = m + m) -> (((exists wpo_beta_height_wer_terminal_state_x_closed_source_entry. wpo_beta_height_wer_terminal_state_x_closed_source_entry + S (wpo_source_wer_terminal_state_x_closed) = S ((S (wpo_position_wer_terminal_state_x_closed)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_closed_source_entry. b = wpo_beta_quotient_wer_terminal_state_x_closed_source_entry * S ((S (wpo_position_wer_terminal_state_x_closed)) * c) + (wpo_source_wer_terminal_state_x_closed))) -> (((exists wpo_beta_height_wer_terminal_state_x_closed_inverse_entry. wpo_beta_height_wer_terminal_state_x_closed_inverse_entry + S (wpo_mate_wer_terminal_state_x_closed) = S ((S (wpo_source_wer_terminal_state_x_closed)) * x1)) /\ exists wpo_beta_quotient_wer_terminal_state_x_closed_inverse_entry. x = wpo_beta_quotient_wer_terminal_state_x_closed_inverse_entry * S ((S (wpo_source_wer_terminal_state_x_closed)) * x1) + (wpo_mate_wer_terminal_state_x_closed))) -> exists wpo_mate_position_wer_terminal_state_x_closed. ((exists wpo_gap_wer_terminal_state_x_closed_mate_bound. wpo_gap_wer_terminal_state_x_closed_mate_bound + S (wpo_mate_position_wer_terminal_state_x_closed) = m + m) /\ (((exists wpo_beta_height_wer_terminal_state_x_closed_mate_entry. wpo_beta_height_wer_terminal_state_x_closed_mate_entry + S (wpo_mate_wer_terminal_state_x_closed) = S ((S (wpo_mate_position_wer_terminal_state_x_closed)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_closed_mate_entry. b = wpo_beta_quotient_wer_terminal_state_x_closed_mate_entry * S ((S (wpo_mate_position_wer_terminal_state_x_closed)) * c) + (wpo_mate_wer_terminal_state_x_closed))))) /\ ((forall fom_index_wer_terminal_state_x_bounded. (exists fom_gap_wer_terminal_state_x_bounded_index_bound. fom_gap_wer_terminal_state_x_bounded_index_bound + S (fom_index_wer_terminal_state_x_bounded) = m + m) -> exists fom_value_wer_terminal_state_x_bounded. ((((exists fom_beta_height_wer_terminal_state_x_bounded_entry. fom_beta_height_wer_terminal_state_x_bounded_entry + S (fom_value_wer_terminal_state_x_bounded) = S ((S (fom_index_wer_terminal_state_x_bounded)) * c)) /\ exists fom_beta_quotient_wer_terminal_state_x_bounded_entry. b = fom_beta_quotient_wer_terminal_state_x_bounded_entry * S ((S (fom_index_wer_terminal_state_x_bounded)) * c) + (fom_value_wer_terminal_state_x_bounded))) /\ (exists fom_gap_wer_terminal_state_x_bounded_value_bound. fom_gap_wer_terminal_state_x_bounded_value_bound + S (fom_value_wer_terminal_state_x_bounded) = n))) /\ ((forall wpo_position_wer_terminal_state_x_nonendpoint wpo_value_wer_terminal_state_x_nonendpoint. (exists wpo_gap_wer_terminal_state_x_nonendpoint_position_bound. wpo_gap_wer_terminal_state_x_nonendpoint_position_bound + S (wpo_position_wer_terminal_state_x_nonendpoint) = m + m) -> (((exists wpo_beta_height_wer_terminal_state_x_nonendpoint_entry. wpo_beta_height_wer_terminal_state_x_nonendpoint_entry + S (wpo_value_wer_terminal_state_x_nonendpoint) = S ((S (wpo_position_wer_terminal_state_x_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_nonendpoint_entry. b = wpo_beta_quotient_wer_terminal_state_x_nonendpoint_entry * S ((S (wpo_position_wer_terminal_state_x_nonendpoint)) * c) + (wpo_value_wer_terminal_state_x_nonendpoint))) -> (~(wpo_value_wer_terminal_state_x_nonendpoint = 0) /\ ~((S wpo_value_wer_terminal_state_x_nonendpoint) = n))) /\ (forall wpo_injective_left_wer_terminal_state_x_injective wpo_injective_right_wer_terminal_state_x_injective wpo_injective_value_wer_terminal_state_x_injective. (exists wpo_gap_wer_terminal_state_x_injective_left_bound. wpo_gap_wer_terminal_state_x_injective_left_bound + S (wpo_injective_left_wer_terminal_state_x_injective) = m + m) -> (exists wpo_gap_wer_terminal_state_x_injective_right_bound. wpo_gap_wer_terminal_state_x_injective_right_bound + S (wpo_injective_right_wer_terminal_state_x_injective) = m + m) -> (((exists wpo_beta_height_wer_terminal_state_x_injective_left_entry. wpo_beta_height_wer_terminal_state_x_injective_left_entry + S (wpo_injective_value_wer_terminal_state_x_injective) = S ((S (wpo_injective_left_wer_terminal_state_x_injective)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_injective_left_entry. b = wpo_beta_quotient_wer_terminal_state_x_injective_left_entry * S ((S (wpo_injective_left_wer_terminal_state_x_injective)) * c) + (wpo_injective_value_wer_terminal_state_x_injective))) -> (((exists wpo_beta_height_wer_terminal_state_x_injective_right_entry. wpo_beta_height_wer_terminal_state_x_injective_right_entry + S (wpo_injective_value_wer_terminal_state_x_injective) = S ((S (wpo_injective_right_wer_terminal_state_x_injective)) * c)) /\ exists wpo_beta_quotient_wer_terminal_state_x_injective_right_entry. b = wpo_beta_quotient_wer_terminal_state_x_injective_right_entry * S ((S (wpo_injective_right_wer_terminal_state_x_injective)) * c) + (wpo_injective_value_wer_terminal_state_x_injective))) -> wpo_injective_left_wer_terminal_state_x_injective = wpo_injective_right_wer_terminal_state_x_injective))))) /\ (((forall wpop_pair_wer_terminal_history_x. (exists wpo_gap_wer_terminal_history_x_pair_bound. wpo_gap_wer_terminal_history_x_pair_bound + S (wpop_pair_wer_terminal_history_x) = m) -> exists wpop_left_wer_terminal_history_x wpop_right_wer_terminal_history_x. ((((exists wpo_beta_height_wer_terminal_history_x_left_entry. wpo_beta_height_wer_terminal_history_x_left_entry + S (wpop_left_wer_terminal_history_x) = S ((S (wpop_pair_wer_terminal_history_x + wpop_pair_wer_terminal_history_x)) * c)) /\ exists wpo_beta_quotient_wer_terminal_history_x_left_entry. b = wpo_beta_quotient_wer_terminal_history_x_left_entry * S ((S (wpop_pair_wer_terminal_history_x + wpop_pair_wer_terminal_history_x)) * c) + (wpop_left_wer_terminal_history_x))) /\ ((((exists wpo_beta_height_wer_terminal_history_x_right_entry. wpo_beta_height_wer_terminal_history_x_right_entry + S (wpop_right_wer_terminal_history_x) = S ((S (S (wpop_pair_wer_terminal_history_x + wpop_pair_wer_terminal_history_x))) * c)) /\ exists wpo_beta_quotient_wer_terminal_history_x_right_entry. b = wpo_beta_quotient_wer_terminal_history_x_right_entry * S ((S (S (wpop_pair_wer_terminal_history_x + wpop_pair_wer_terminal_history_x))) * c) + (wpop_right_wer_terminal_history_x))) /\ (((exists wpo_beta_height_wer_terminal_history_x_inverse_entry. wpo_beta_height_wer_terminal_history_x_inverse_entry + S (wpop_right_wer_terminal_history_x) = S ((S (wpop_left_wer_terminal_history_x)) * x1)) /\ exists wpo_beta_quotient_wer_terminal_history_x_inverse_entry. x = wpo_beta_quotient_wer_terminal_history_x_inverse_entry * S ((S (wpop_left_wer_terminal_history_x)) * x1) + (wpop_right_wer_terminal_history_x)))))) /\ (((forall s. (exists wpo_gap_wer_terminal_coverage_value_bound. wpo_gap_wer_terminal_coverage_value_bound + S (s) = S (S (m + m))) -> (~(s = 0) /\ ~((S s) = S (S (m + m)))) -> exists q. ((exists wpo_gap_wer_terminal_coverage_index_bound. wpo_gap_wer_terminal_coverage_index_bound + S (q) = m + m) /\ (((exists wpo_beta_height_wer_terminal_coverage_entry. wpo_beta_height_wer_terminal_coverage_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wer_terminal_coverage_entry. b = wpo_beta_quotient_wer_terminal_coverage_entry * S ((S (q)) * c) + (s))))) /\ (((forall wsl_index_wer_terminal_lift wsl_value_wer_terminal_lift. (exists wpo_gap_wer_terminal_lift_bound. wpo_gap_wer_terminal_lift_bound + S (wsl_index_wer_terminal_lift) = m + m) -> (((exists wpo_beta_height_wer_terminal_lift_source. wpo_beta_height_wer_terminal_lift_source + S (wsl_value_wer_terminal_lift) = S ((S (wsl_index_wer_terminal_lift)) * c)) /\ exists wpo_beta_quotient_wer_terminal_lift_source. b = wpo_beta_quotient_wer_terminal_lift_source * S ((S (wsl_index_wer_terminal_lift)) * c) + (wsl_value_wer_terminal_lift))) -> (((exists wpo_beta_height_wer_terminal_lift_target. wpo_beta_height_wer_terminal_lift_target + S (S wsl_value_wer_terminal_lift) = S ((S (wsl_index_wer_terminal_lift)) * g)) /\ exists wpo_beta_quotient_wer_terminal_lift_target. f = wpo_beta_quotient_wer_terminal_lift_target * S ((S (wsl_index_wer_terminal_lift)) * g) + (S wsl_value_wer_terminal_lift)))) /\ (((forall wpp_pair_wer_terminal_adjacent wpp_left_wer_terminal_adjacent wpp_right_wer_terminal_adjacent. (exists wpp_gap_wer_terminal_adjacent_pair_bound. wpp_gap_wer_terminal_adjacent_pair_bound + S (wpp_pair_wer_terminal_adjacent) = m) -> (((exists wpp_beta_height_wer_terminal_adjacent_left_entry. wpp_beta_height_wer_terminal_adjacent_left_entry + S (wpp_left_wer_terminal_adjacent) = S ((S ((wpp_pair_wer_terminal_adjacent + wpp_pair_wer_terminal_adjacent))) * g)) /\ exists wpp_beta_quotient_wer_terminal_adjacent_left_entry. f = wpp_beta_quotient_wer_terminal_adjacent_left_entry * S ((S ((wpp_pair_wer_terminal_adjacent + wpp_pair_wer_terminal_adjacent))) * g) + (wpp_left_wer_terminal_adjacent))) -> (((exists wpp_beta_height_wer_terminal_adjacent_right_entry. wpp_beta_height_wer_terminal_adjacent_right_entry + S (wpp_right_wer_terminal_adjacent) = S ((S (S (wpp_pair_wer_terminal_adjacent + wpp_pair_wer_terminal_adjacent))) * g)) /\ exists wpp_beta_quotient_wer_terminal_adjacent_right_entry. f = wpp_beta_quotient_wer_terminal_adjacent_right_entry * S ((S (S (wpp_pair_wer_terminal_adjacent + wpp_pair_wer_terminal_adjacent))) * g) + (wpp_right_wer_terminal_adjacent))) -> (exists wpp_mod_left_wer_terminal_adjacent_pair_mod wpp_mod_right_wer_terminal_adjacent_pair_mod. (wpp_left_wer_terminal_adjacent * wpp_right_wer_terminal_adjacent) + p * wpp_mod_left_wer_terminal_adjacent_pair_mod = (1) + p * wpp_mod_right_wer_terminal_adjacent_pair_mod)) /\ (((exists ff_u_wer_terminal_lifted_product ff_v_wer_terminal_lifted_product. ((((exists ff_h_wer_terminal_lifted_product_start. ff_h_wer_terminal_lifted_product_start + S (1) = S ((S (0)) * ff_v_wer_terminal_lifted_product)) /\ exists ff_q_wer_terminal_lifted_product_start. ff_u_wer_terminal_lifted_product = ff_q_wer_terminal_lifted_product_start * S ((S (0)) * ff_v_wer_terminal_lifted_product) + (1))) /\ ((((exists ff_h_wer_terminal_lifted_product_terminal. ff_h_wer_terminal_lifted_product_terminal + S (Q) = S ((S (m + m)) * ff_v_wer_terminal_lifted_product)) /\ exists ff_q_wer_terminal_lifted_product_terminal. ff_u_wer_terminal_lifted_product = ff_q_wer_terminal_lifted_product_terminal * S ((S (m + m)) * ff_v_wer_terminal_lifted_product) + (Q))) /\ forall ff_i_wer_terminal_lifted_product. (exists ff_lt_wer_terminal_lifted_product_bound. ff_lt_wer_terminal_lifted_product_bound + S ff_i_wer_terminal_lifted_product = m + m) -> exists ff_p_wer_terminal_lifted_product ff_r_wer_terminal_lifted_product ff_s_wer_terminal_lifted_product. ((((exists ff_h_wer_terminal_lifted_product_factor. ff_h_wer_terminal_lifted_product_factor + S (ff_p_wer_terminal_lifted_product) = S ((S (ff_i_wer_terminal_lifted_product)) * g)) /\ exists ff_q_wer_terminal_lifted_product_factor. f = ff_q_wer_terminal_lifted_product_factor * S ((S (ff_i_wer_terminal_lifted_product)) * g) + (ff_p_wer_terminal_lifted_product))) /\ ((((exists ff_h_wer_terminal_lifted_product_partial. ff_h_wer_terminal_lifted_product_partial + S (ff_r_wer_terminal_lifted_product) = S ((S (ff_i_wer_terminal_lifted_product)) * ff_v_wer_terminal_lifted_product)) /\ exists ff_q_wer_terminal_lifted_product_partial. ff_u_wer_terminal_lifted_product = ff_q_wer_terminal_lifted_product_partial * S ((S (ff_i_wer_terminal_lifted_product)) * ff_v_wer_terminal_lifted_product) + (ff_r_wer_terminal_lifted_product))) /\ ((((exists ff_h_wer_terminal_lifted_product_successor. ff_h_wer_terminal_lifted_product_successor + S (ff_s_wer_terminal_lifted_product) = S ((S (S ff_i_wer_terminal_lifted_product)) * ff_v_wer_terminal_lifted_product)) /\ exists ff_q_wer_terminal_lifted_product_successor. ff_u_wer_terminal_lifted_product = ff_q_wer_terminal_lifted_product_successor * S ((S (S ff_i_wer_terminal_lifted_product)) * ff_v_wer_terminal_lifted_product) + (ff_s_wer_terminal_lifted_product))) /\ ff_s_wer_terminal_lifted_product = ff_r_wer_terminal_lifted_product * ff_p_wer_terminal_lifted_product)))))) /\ (((exists wpp_mod_left_wer_terminal_mod_one wpp_mod_right_wer_terminal_mod_one. (Q) + p * wpp_mod_left_wer_terminal_mod_one = (1) + p * wpp_mod_right_wer_terminal_mod_one) /\ (((forall wtp_range_index_wer_terminal_range. (exists wtp_range_gap_wer_terminal_range. wtp_range_gap_wer_terminal_range + S wtp_range_index_wer_terminal_range = m + m) -> (((exists ff_h_wer_terminal_range_decoded. ff_h_wer_terminal_range_decoded + S (2 + wtp_range_index_wer_terminal_range) = S ((S (wtp_range_index_wer_terminal_range)) * d)) /\ exists ff_q_wer_terminal_range_decoded. z = ff_q_wer_terminal_range_decoded * S ((S (wtp_range_index_wer_terminal_range)) * d) + (2 + wtp_range_index_wer_terminal_range)))) /\ (((exists ff_u_wer_terminal_canonical_product ff_v_wer_terminal_canonical_product. ((((exists ff_h_wer_terminal_canonical_product_start. ff_h_wer_terminal_canonical_product_start + S (1) = S ((S (0)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_start. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_start * S ((S (0)) * ff_v_wer_terminal_canonical_product) + (1))) /\ ((((exists ff_h_wer_terminal_canonical_product_terminal. ff_h_wer_terminal_canonical_product_terminal + S (P) = S ((S (m + m)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_terminal. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_terminal * S ((S (m + m)) * ff_v_wer_terminal_canonical_product) + (P))) /\ forall ff_i_wer_terminal_canonical_product. (exists ff_lt_wer_terminal_canonical_product_bound. ff_lt_wer_terminal_canonical_product_bound + S ff_i_wer_terminal_canonical_product = m + m) -> exists ff_p_wer_terminal_canonical_product ff_r_wer_terminal_canonical_product ff_s_wer_terminal_canonical_product. ((((exists ff_h_wer_terminal_canonical_product_factor. ff_h_wer_terminal_canonical_product_factor + S (ff_p_wer_terminal_canonical_product) = S ((S (ff_i_wer_terminal_canonical_product)) * d)) /\ exists ff_q_wer_terminal_canonical_product_factor. z = ff_q_wer_terminal_canonical_product_factor * S ((S (ff_i_wer_terminal_canonical_product)) * d) + (ff_p_wer_terminal_canonical_product))) /\ ((((exists ff_h_wer_terminal_canonical_product_partial. ff_h_wer_terminal_canonical_product_partial + S (ff_r_wer_terminal_canonical_product) = S ((S (ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_partial. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_partial * S ((S (ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product) + (ff_r_wer_terminal_canonical_product))) /\ ((((exists ff_h_wer_terminal_canonical_product_successor. ff_h_wer_terminal_canonical_product_successor + S (ff_s_wer_terminal_canonical_product) = S ((S (S ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product)) /\ exists ff_q_wer_terminal_canonical_product_successor. ff_u_wer_terminal_canonical_product = ff_q_wer_terminal_canonical_product_successor * S ((S (S ff_i_wer_terminal_canonical_product)) * ff_v_wer_terminal_canonical_product) + (ff_s_wer_terminal_canonical_product))) /\ ff_s_wer_terminal_canonical_product = ff_r_wer_terminal_canonical_product * ff_p_wer_terminal_canonical_product)))))) /\ (P = Q))))))))))))))))))
16. 0016specialize prime_wilson_terminal_product_package_exists p
17. 0017specialize prime_wilson_terminal_product_package_exists n
18. 0018specialize prime_wilson_terminal_product_package_exists x
19. 0019specialize prime_wilson_terminal_product_package_exists x1
20. 0020specialize prime_wilson_terminal_product_package_exists (S (m + m))
21. 0021specialize prime_wilson_terminal_product_package_exists m
22. 0022apply prime_wilson_terminal_product_package_exists
23. 0023exact hpn
24. 0024exact hp
25. 0025exact hinverse_witness_witness
26. 0026exact hterminal
27. 0027exact hterminal
28. 0028cases hpackage
29. 0029cases hpackage_witness
30. 0030cases hpackage_witness_witness
31. 0031cases hpackage_witness_witness_witness
32. 0032cases hpackage_witness_witness_witness_witness
33. 0033cases hpackage_witness_witness_witness_witness_witness
34. 0034cases hpackage_witness_witness_witness_witness_witness_witness
35. 0035cases hpackage_witness_witness_witness_witness_witness_witness_witness
36. 0036have hparts : ((((forall wpo_position_wer_witness_state_closed wpo_source_wer_witness_state_closed wpo_mate_wer_witness_state_closed. (exists wpo_gap_wer_witness_state_closed_position_bound. wpo_gap_wer_witness_state_closed_position_bound + S (wpo_position_wer_witness_state_closed) = m + m) -> (((exists wpo_beta_height_wer_witness_state_closed_source_entry. wpo_beta_height_wer_witness_state_closed_source_entry + S (wpo_source_wer_witness_state_closed) = S ((S (wpo_position_wer_witness_state_closed)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_closed_source_entry. x2 = wpo_beta_quotient_wer_witness_state_closed_source_entry * S ((S (wpo_position_wer_witness_state_closed)) * x3) + (wpo_source_wer_witness_state_closed))) -> (((exists wpo_beta_height_wer_witness_state_closed_inverse_entry. wpo_beta_height_wer_witness_state_closed_inverse_entry + S (wpo_mate_wer_witness_state_closed) = S ((S (wpo_source_wer_witness_state_closed)) * x1)) /\ exists wpo_beta_quotient_wer_witness_state_closed_inverse_entry. x = wpo_beta_quotient_wer_witness_state_closed_inverse_entry * S ((S (wpo_source_wer_witness_state_closed)) * x1) + (wpo_mate_wer_witness_state_closed))) -> exists wpo_mate_position_wer_witness_state_closed. ((exists wpo_gap_wer_witness_state_closed_mate_bound. wpo_gap_wer_witness_state_closed_mate_bound + S (wpo_mate_position_wer_witness_state_closed) = m + m) /\ (((exists wpo_beta_height_wer_witness_state_closed_mate_entry. wpo_beta_height_wer_witness_state_closed_mate_entry + S (wpo_mate_wer_witness_state_closed) = S ((S (wpo_mate_position_wer_witness_state_closed)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_closed_mate_entry. x2 = wpo_beta_quotient_wer_witness_state_closed_mate_entry * S ((S (wpo_mate_position_wer_witness_state_closed)) * x3) + (wpo_mate_wer_witness_state_closed))))) /\ ((forall fom_index_wer_witness_state_bounded. (exists fom_gap_wer_witness_state_bounded_index_bound. fom_gap_wer_witness_state_bounded_index_bound + S (fom_index_wer_witness_state_bounded) = m + m) -> exists fom_value_wer_witness_state_bounded. ((((exists fom_beta_height_wer_witness_state_bounded_entry. fom_beta_height_wer_witness_state_bounded_entry + S (fom_value_wer_witness_state_bounded) = S ((S (fom_index_wer_witness_state_bounded)) * x3)) /\ exists fom_beta_quotient_wer_witness_state_bounded_entry. x2 = fom_beta_quotient_wer_witness_state_bounded_entry * S ((S (fom_index_wer_witness_state_bounded)) * x3) + (fom_value_wer_witness_state_bounded))) /\ (exists fom_gap_wer_witness_state_bounded_value_bound. fom_gap_wer_witness_state_bounded_value_bound + S (fom_value_wer_witness_state_bounded) = n))) /\ ((forall wpo_position_wer_witness_state_nonendpoint wpo_value_wer_witness_state_nonendpoint. (exists wpo_gap_wer_witness_state_nonendpoint_position_bound. wpo_gap_wer_witness_state_nonendpoint_position_bound + S (wpo_position_wer_witness_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wer_witness_state_nonendpoint_entry. wpo_beta_height_wer_witness_state_nonendpoint_entry + S (wpo_value_wer_witness_state_nonendpoint) = S ((S (wpo_position_wer_witness_state_nonendpoint)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_nonendpoint_entry. x2 = wpo_beta_quotient_wer_witness_state_nonendpoint_entry * S ((S (wpo_position_wer_witness_state_nonendpoint)) * x3) + (wpo_value_wer_witness_state_nonendpoint))) -> (~(wpo_value_wer_witness_state_nonendpoint = 0) /\ ~((S wpo_value_wer_witness_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wer_witness_state_injective wpo_injective_right_wer_witness_state_injective wpo_injective_value_wer_witness_state_injective. (exists wpo_gap_wer_witness_state_injective_left_bound. wpo_gap_wer_witness_state_injective_left_bound + S (wpo_injective_left_wer_witness_state_injective) = m + m) -> (exists wpo_gap_wer_witness_state_injective_right_bound. wpo_gap_wer_witness_state_injective_right_bound + S (wpo_injective_right_wer_witness_state_injective) = m + m) -> (((exists wpo_beta_height_wer_witness_state_injective_left_entry. wpo_beta_height_wer_witness_state_injective_left_entry + S (wpo_injective_value_wer_witness_state_injective) = S ((S (wpo_injective_left_wer_witness_state_injective)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_injective_left_entry. x2 = wpo_beta_quotient_wer_witness_state_injective_left_entry * S ((S (wpo_injective_left_wer_witness_state_injective)) * x3) + (wpo_injective_value_wer_witness_state_injective))) -> (((exists wpo_beta_height_wer_witness_state_injective_right_entry. wpo_beta_height_wer_witness_state_injective_right_entry + S (wpo_injective_value_wer_witness_state_injective) = S ((S (wpo_injective_right_wer_witness_state_injective)) * x3)) /\ exists wpo_beta_quotient_wer_witness_state_injective_right_entry. x2 = wpo_beta_quotient_wer_witness_state_injective_right_entry * S ((S (wpo_injective_right_wer_witness_state_injective)) * x3) + (wpo_injective_value_wer_witness_state_injective))) -> wpo_injective_left_wer_witness_state_injective = wpo_injective_right_wer_witness_state_injective))))) /\ (((forall wpop_pair_wer_witness_history. (exists wpo_gap_wer_witness_history_pair_bound. wpo_gap_wer_witness_history_pair_bound + S (wpop_pair_wer_witness_history) = m) -> exists wpop_left_wer_witness_history wpop_right_wer_witness_history. ((((exists wpo_beta_height_wer_witness_history_left_entry. wpo_beta_height_wer_witness_history_left_entry + S (wpop_left_wer_witness_history) = S ((S (wpop_pair_wer_witness_history + wpop_pair_wer_witness_history)) * x3)) /\ exists wpo_beta_quotient_wer_witness_history_left_entry. x2 = wpo_beta_quotient_wer_witness_history_left_entry * S ((S (wpop_pair_wer_witness_history + wpop_pair_wer_witness_history)) * x3) + (wpop_left_wer_witness_history))) /\ ((((exists wpo_beta_height_wer_witness_history_right_entry. wpo_beta_height_wer_witness_history_right_entry + S (wpop_right_wer_witness_history) = S ((S (S (wpop_pair_wer_witness_history + wpop_pair_wer_witness_history))) * x3)) /\ exists wpo_beta_quotient_wer_witness_history_right_entry. x2 = wpo_beta_quotient_wer_witness_history_right_entry * S ((S (S (wpop_pair_wer_witness_history + wpop_pair_wer_witness_history))) * x3) + (wpop_right_wer_witness_history))) /\ (((exists wpo_beta_height_wer_witness_history_inverse_entry. wpo_beta_height_wer_witness_history_inverse_entry + S (wpop_right_wer_witness_history) = S ((S (wpop_left_wer_witness_history)) * x1)) /\ exists wpo_beta_quotient_wer_witness_history_inverse_entry. x = wpo_beta_quotient_wer_witness_history_inverse_entry * S ((S (wpop_left_wer_witness_history)) * x1) + (wpop_right_wer_witness_history)))))) /\ (((forall s. (exists wpo_gap_wer_terminal_coverage_value_bound. wpo_gap_wer_terminal_coverage_value_bound + S (s) = S (S (m + m))) -> (~(s = 0) /\ ~((S s) = S (S (m + m)))) -> exists q. ((exists wpo_gap_wer_terminal_coverage_index_bound. wpo_gap_wer_terminal_coverage_index_bound + S (q) = m + m) /\ (((exists wpo_beta_height_wer_witness_coverage_entry. wpo_beta_height_wer_witness_coverage_entry + S (s) = S ((S (q)) * x3)) /\ exists wpo_beta_quotient_wer_witness_coverage_entry. x2 = wpo_beta_quotient_wer_witness_coverage_entry * S ((S (q)) * x3) + (s))))) /\ (((forall wsl_index_wer_witness_lift wsl_value_wer_witness_lift. (exists wpo_gap_wer_witness_lift_bound. wpo_gap_wer_witness_lift_bound + S (wsl_index_wer_witness_lift) = m + m) -> (((exists wpo_beta_height_wer_witness_lift_source. wpo_beta_height_wer_witness_lift_source + S (wsl_value_wer_witness_lift) = S ((S (wsl_index_wer_witness_lift)) * x3)) /\ exists wpo_beta_quotient_wer_witness_lift_source. x2 = wpo_beta_quotient_wer_witness_lift_source * S ((S (wsl_index_wer_witness_lift)) * x3) + (wsl_value_wer_witness_lift))) -> (((exists wpo_beta_height_wer_witness_lift_target. wpo_beta_height_wer_witness_lift_target + S (S wsl_value_wer_witness_lift) = S ((S (wsl_index_wer_witness_lift)) * x5)) /\ exists wpo_beta_quotient_wer_witness_lift_target. x4 = wpo_beta_quotient_wer_witness_lift_target * S ((S (wsl_index_wer_witness_lift)) * x5) + (S wsl_value_wer_witness_lift)))) /\ (((forall wpp_pair_wer_witness_adjacent wpp_left_wer_witness_adjacent wpp_right_wer_witness_adjacent. (exists wpp_gap_wer_witness_adjacent_pair_bound. wpp_gap_wer_witness_adjacent_pair_bound + S (wpp_pair_wer_witness_adjacent) = m) -> (((exists wpp_beta_height_wer_witness_adjacent_left_entry. wpp_beta_height_wer_witness_adjacent_left_entry + S (wpp_left_wer_witness_adjacent) = S ((S ((wpp_pair_wer_witness_adjacent + wpp_pair_wer_witness_adjacent))) * x5)) /\ exists wpp_beta_quotient_wer_witness_adjacent_left_entry. x4 = wpp_beta_quotient_wer_witness_adjacent_left_entry * S ((S ((wpp_pair_wer_witness_adjacent + wpp_pair_wer_witness_adjacent))) * x5) + (wpp_left_wer_witness_adjacent))) -> (((exists wpp_beta_height_wer_witness_adjacent_right_entry. wpp_beta_height_wer_witness_adjacent_right_entry + S (wpp_right_wer_witness_adjacent) = S ((S (S (wpp_pair_wer_witness_adjacent + wpp_pair_wer_witness_adjacent))) * x5)) /\ exists wpp_beta_quotient_wer_witness_adjacent_right_entry. x4 = wpp_beta_quotient_wer_witness_adjacent_right_entry * S ((S (S (wpp_pair_wer_witness_adjacent + wpp_pair_wer_witness_adjacent))) * x5) + (wpp_right_wer_witness_adjacent))) -> (exists wpp_mod_left_wer_witness_adjacent_pair_mod wpp_mod_right_wer_witness_adjacent_pair_mod. (wpp_left_wer_witness_adjacent * wpp_right_wer_witness_adjacent) + p * wpp_mod_left_wer_witness_adjacent_pair_mod = (1) + p * wpp_mod_right_wer_witness_adjacent_pair_mod)) /\ (((exists ff_u_wer_witness_lifted_product ff_v_wer_witness_lifted_product. ((((exists ff_h_wer_witness_lifted_product_start. ff_h_wer_witness_lifted_product_start + S (1) = S ((S (0)) * ff_v_wer_witness_lifted_product)) /\ exists ff_q_wer_witness_lifted_product_start. ff_u_wer_witness_lifted_product = ff_q_wer_witness_lifted_product_start * S ((S (0)) * ff_v_wer_witness_lifted_product) + (1))) /\ ((((exists ff_h_wer_witness_lifted_product_terminal. ff_h_wer_witness_lifted_product_terminal + S (x6) = S ((S (m + m)) * ff_v_wer_witness_lifted_product)) /\ exists ff_q_wer_witness_lifted_product_terminal. ff_u_wer_witness_lifted_product = ff_q_wer_witness_lifted_product_terminal * S ((S (m + m)) * ff_v_wer_witness_lifted_product) + (x6))) /\ forall ff_i_wer_witness_lifted_product. (exists ff_lt_wer_witness_lifted_product_bound. ff_lt_wer_witness_lifted_product_bound + S ff_i_wer_witness_lifted_product = m + m) -> exists ff_p_wer_witness_lifted_product ff_r_wer_witness_lifted_product ff_s_wer_witness_lifted_product. ((((exists ff_h_wer_witness_lifted_product_factor. ff_h_wer_witness_lifted_product_factor + S (ff_p_wer_witness_lifted_product) = S ((S (ff_i_wer_witness_lifted_product)) * x5)) /\ exists ff_q_wer_witness_lifted_product_factor. x4 = ff_q_wer_witness_lifted_product_factor * S ((S (ff_i_wer_witness_lifted_product)) * x5) + (ff_p_wer_witness_lifted_product))) /\ ((((exists ff_h_wer_witness_lifted_product_partial. ff_h_wer_witness_lifted_product_partial + S (ff_r_wer_witness_lifted_product) = S ((S (ff_i_wer_witness_lifted_product)) * ff_v_wer_witness_lifted_product)) /\ exists ff_q_wer_witness_lifted_product_partial. ff_u_wer_witness_lifted_product = ff_q_wer_witness_lifted_product_partial * S ((S (ff_i_wer_witness_lifted_product)) * ff_v_wer_witness_lifted_product) + (ff_r_wer_witness_lifted_product))) /\ ((((exists ff_h_wer_witness_lifted_product_successor. ff_h_wer_witness_lifted_product_successor + S (ff_s_wer_witness_lifted_product) = S ((S (S ff_i_wer_witness_lifted_product)) * ff_v_wer_witness_lifted_product)) /\ exists ff_q_wer_witness_lifted_product_successor. ff_u_wer_witness_lifted_product = ff_q_wer_witness_lifted_product_successor * S ((S (S ff_i_wer_witness_lifted_product)) * ff_v_wer_witness_lifted_product) + (ff_s_wer_witness_lifted_product))) /\ ff_s_wer_witness_lifted_product = ff_r_wer_witness_lifted_product * ff_p_wer_witness_lifted_product)))))) /\ (((exists wpp_mod_left_wer_witness_mod_one wpp_mod_right_wer_witness_mod_one. (x6) + p * wpp_mod_left_wer_witness_mod_one = (1) + p * wpp_mod_right_wer_witness_mod_one) /\ (((forall wtp_range_index_wer_witness_range. (exists wtp_range_gap_wer_witness_range. wtp_range_gap_wer_witness_range + S wtp_range_index_wer_witness_range = m + m) -> (((exists ff_h_wer_witness_range_decoded. ff_h_wer_witness_range_decoded + S (2 + wtp_range_index_wer_witness_range) = S ((S (wtp_range_index_wer_witness_range)) * x8)) /\ exists ff_q_wer_witness_range_decoded. x7 = ff_q_wer_witness_range_decoded * S ((S (wtp_range_index_wer_witness_range)) * x8) + (2 + wtp_range_index_wer_witness_range)))) /\ (((exists ff_u_wer_witness_product ff_v_wer_witness_product. ((((exists ff_h_wer_witness_product_start. ff_h_wer_witness_product_start + S (1) = S ((S (0)) * ff_v_wer_witness_product)) /\ exists ff_q_wer_witness_product_start. ff_u_wer_witness_product = ff_q_wer_witness_product_start * S ((S (0)) * ff_v_wer_witness_product) + (1))) /\ ((((exists ff_h_wer_witness_product_terminal. ff_h_wer_witness_product_terminal + S (x9) = S ((S (m + m)) * ff_v_wer_witness_product)) /\ exists ff_q_wer_witness_product_terminal. ff_u_wer_witness_product = ff_q_wer_witness_product_terminal * S ((S (m + m)) * ff_v_wer_witness_product) + (x9))) /\ forall ff_i_wer_witness_product. (exists ff_lt_wer_witness_product_bound. ff_lt_wer_witness_product_bound + S ff_i_wer_witness_product = m + m) -> exists ff_p_wer_witness_product ff_r_wer_witness_product ff_s_wer_witness_product. ((((exists ff_h_wer_witness_product_factor. ff_h_wer_witness_product_factor + S (ff_p_wer_witness_product) = S ((S (ff_i_wer_witness_product)) * x8)) /\ exists ff_q_wer_witness_product_factor. x7 = ff_q_wer_witness_product_factor * S ((S (ff_i_wer_witness_product)) * x8) + (ff_p_wer_witness_product))) /\ ((((exists ff_h_wer_witness_product_partial. ff_h_wer_witness_product_partial + S (ff_r_wer_witness_product) = S ((S (ff_i_wer_witness_product)) * ff_v_wer_witness_product)) /\ exists ff_q_wer_witness_product_partial. ff_u_wer_witness_product = ff_q_wer_witness_product_partial * S ((S (ff_i_wer_witness_product)) * ff_v_wer_witness_product) + (ff_r_wer_witness_product))) /\ ((((exists ff_h_wer_witness_product_successor. ff_h_wer_witness_product_successor + S (ff_s_wer_witness_product) = S ((S (S ff_i_wer_witness_product)) * ff_v_wer_witness_product)) /\ exists ff_q_wer_witness_product_successor. ff_u_wer_witness_product = ff_q_wer_witness_product_successor * S ((S (S ff_i_wer_witness_product)) * ff_v_wer_witness_product) + (ff_s_wer_witness_product))) /\ ff_s_wer_witness_product = ff_r_wer_witness_product * ff_p_wer_witness_product)))))) /\ (x9 = x6))))))))))))))))))
37. 0037exact hpackage_witness_witness_witness_witness_witness_witness_witness_witness
38. 0038cases hparts
39. 0039cases hparts_right
40. 0040cases hparts_right_right
41. 0041cases hparts_right_right_right
42. 0042cases hparts_right_right_right_right
43. 0043cases hparts_right_right_right_right_right
44. 0044cases hparts_right_right_right_right_right_right
45. 0045cases hparts_right_right_right_right_right_right_right
46. 0046cases hparts_right_right_right_right_right_right_right_right
47. 0047have hmod_product : exists wpp_mod_left_wer_witness_mod_product wpp_mod_right_wer_witness_mod_product. (x9) + p * wpp_mod_left_wer_witness_mod_product = (1) + p * wpp_mod_right_wer_witness_mod_product
48. 0048rewrite hparts_right_right_right_right_right_right_right_right_right
49. 0049exact hparts_right_right_right_right_right_right_left
50. 0050exists x7
51. 0051exists x8
52. 0052exists x9
53. 0053split
54. 0054exact hparts_right_right_right_right_right_right_right_left
55. 0055split
56. 0056exact hparts_right_right_right_right_right_right_right_right_left
57. 0057exact hmod_product