PA009T

scaled_inverse_pair_order_paired_state_step

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

Append one fixed-point-free scaled orbit and preserve iterable state plus history.

Exact expanded PA statement

forall p a n u v b c m. p = S n -> ((~(p = 1) /\ forall esi_prime_left_iteration_prime esi_prime_right_iteration_prime. p = esi_prime_left_iteration_prime * esi_prime_right_iteration_prime -> esi_prime_left_iteration_prime = 1 \/ esi_prime_right_iteration_prime = 1)) -> ~(exists qr_x_iteration_nonresidue. exists qr_u_iteration_nonresidue qr_v_iteration_nonresidue. qr_x_iteration_nonresidue * qr_x_iteration_nonresidue + p * qr_u_iteration_nonresidue = a + p * qr_v_iteration_nonresidue) -> (forall esip_index_iteration_prefix. (exists esip_gap_iteration_prefix_prefix_bound. esip_gap_iteration_prefix_prefix_bound + S (esip_index_iteration_prefix) = n) -> exists esip_mate_iteration_prefix. ((((exists ff_h_esip_iteration_prefix_entry. ff_h_esip_iteration_prefix_entry + S (esip_mate_iteration_prefix) = S ((S (esip_index_iteration_prefix)) * v)) /\ exists ff_q_esip_iteration_prefix_entry. u = ff_q_esip_iteration_prefix_entry * S ((S (esip_index_iteration_prefix)) * v) + (esip_mate_iteration_prefix))) /\ ((exists esip_gap_iteration_prefix_relation_index_bound. esip_gap_iteration_prefix_relation_index_bound + S (esip_index_iteration_prefix) = n) /\ ((((~((S esip_index_iteration_prefix) = 0) /\ (exists esip_gap_iteration_prefix_relation_scaled_left_bound. esip_gap_iteration_prefix_relation_scaled_left_bound + S (S esip_index_iteration_prefix) = p))) /\ (((~(esip_mate_iteration_prefix = 0) /\ (exists esip_gap_iteration_prefix_relation_scaled_right_bound. esip_gap_iteration_prefix_relation_scaled_right_bound + S (esip_mate_iteration_prefix) = p))) /\ (exists esi_mod_left_iteration_prefix_relation_scaled_mod esi_mod_right_iteration_prefix_relation_scaled_mod. ((S esip_index_iteration_prefix) * esip_mate_iteration_prefix) + p * esi_mod_left_iteration_prefix_relation_scaled_mod = (a) + p * esi_mod_right_iteration_prefix_relation_scaled_mod))))))) -> (exists wpo_gap_iteration_short. wpo_gap_iteration_short + S (m + m) = n) -> (((forall espo_position_step_old_state_closed espo_source_step_old_state_closed espo_mate_step_old_state_closed. (exists wpo_gap_step_old_state_closed_position_bound. wpo_gap_step_old_state_closed_position_bound + S (espo_position_step_old_state_closed) = m + m) -> (((exists wpo_beta_height_step_old_state_closed_source_entry. wpo_beta_height_step_old_state_closed_source_entry + S (espo_source_step_old_state_closed) = S ((S (espo_position_step_old_state_closed)) * c)) /\ exists wpo_beta_quotient_step_old_state_closed_source_entry. b = wpo_beta_quotient_step_old_state_closed_source_entry * S ((S (espo_position_step_old_state_closed)) * c) + (espo_source_step_old_state_closed))) -> (((exists wpo_beta_height_step_old_state_closed_scaled_entry. wpo_beta_height_step_old_state_closed_scaled_entry + S (S espo_mate_step_old_state_closed) = S ((S (espo_source_step_old_state_closed)) * v)) /\ exists wpo_beta_quotient_step_old_state_closed_scaled_entry. u = wpo_beta_quotient_step_old_state_closed_scaled_entry * S ((S (espo_source_step_old_state_closed)) * v) + (S espo_mate_step_old_state_closed))) -> exists espo_mate_position_step_old_state_closed. ((exists wpo_gap_step_old_state_closed_mate_bound. wpo_gap_step_old_state_closed_mate_bound + S (espo_mate_position_step_old_state_closed) = m + m) /\ (((exists wpo_beta_height_step_old_state_closed_mate_entry. wpo_beta_height_step_old_state_closed_mate_entry + S (espo_mate_step_old_state_closed) = S ((S (espo_mate_position_step_old_state_closed)) * c)) /\ exists wpo_beta_quotient_step_old_state_closed_mate_entry. b = wpo_beta_quotient_step_old_state_closed_mate_entry * S ((S (espo_mate_position_step_old_state_closed)) * c) + (espo_mate_step_old_state_closed))))) /\ (((forall fom_index_step_old_state_bounded. (exists fom_gap_step_old_state_bounded_index_bound. fom_gap_step_old_state_bounded_index_bound + S (fom_index_step_old_state_bounded) = m + m) -> exists fom_value_step_old_state_bounded. ((((exists fom_beta_height_step_old_state_bounded_entry. fom_beta_height_step_old_state_bounded_entry + S (fom_value_step_old_state_bounded) = S ((S (fom_index_step_old_state_bounded)) * c)) /\ exists fom_beta_quotient_step_old_state_bounded_entry. b = fom_beta_quotient_step_old_state_bounded_entry * S ((S (fom_index_step_old_state_bounded)) * c) + (fom_value_step_old_state_bounded))) /\ (exists fom_gap_step_old_state_bounded_value_bound. fom_gap_step_old_state_bounded_value_bound + S (fom_value_step_old_state_bounded) = n))) /\ (forall wpo_injective_left_step_old_state_injective wpo_injective_right_step_old_state_injective wpo_injective_value_step_old_state_injective. (exists wpo_gap_step_old_state_injective_left_bound. wpo_gap_step_old_state_injective_left_bound + S (wpo_injective_left_step_old_state_injective) = m + m) -> (exists wpo_gap_step_old_state_injective_right_bound. wpo_gap_step_old_state_injective_right_bound + S (wpo_injective_right_step_old_state_injective) = m + m) -> (((exists wpo_beta_height_step_old_state_injective_left_entry. wpo_beta_height_step_old_state_injective_left_entry + S (wpo_injective_value_step_old_state_injective) = S ((S (wpo_injective_left_step_old_state_injective)) * c)) /\ exists wpo_beta_quotient_step_old_state_injective_left_entry. b = wpo_beta_quotient_step_old_state_injective_left_entry * S ((S (wpo_injective_left_step_old_state_injective)) * c) + (wpo_injective_value_step_old_state_injective))) -> (((exists wpo_beta_height_step_old_state_injective_right_entry. wpo_beta_height_step_old_state_injective_right_entry + S (wpo_injective_value_step_old_state_injective) = S ((S (wpo_injective_right_step_old_state_injective)) * c)) /\ exists wpo_beta_quotient_step_old_state_injective_right_entry. b = wpo_beta_quotient_step_old_state_injective_right_entry * S ((S (wpo_injective_right_step_old_state_injective)) * c) + (wpo_injective_value_step_old_state_injective))) -> wpo_injective_left_step_old_state_injective = wpo_injective_right_step_old_state_injective))))) -> (forall espi_pair_step_old_history. (exists wpo_gap_step_old_history_pair_bound. wpo_gap_step_old_history_pair_bound + S (espi_pair_step_old_history) = m) -> exists espi_left_step_old_history espi_right_step_old_history. (((((exists wpo_beta_height_step_old_history_left_entry. wpo_beta_height_step_old_history_left_entry + S (espi_left_step_old_history) = S ((S (espi_pair_step_old_history + espi_pair_step_old_history)) * c)) /\ exists wpo_beta_quotient_step_old_history_left_entry. b = wpo_beta_quotient_step_old_history_left_entry * S ((S (espi_pair_step_old_history + espi_pair_step_old_history)) * c) + (espi_left_step_old_history))) /\ (((((exists wpo_beta_height_step_old_history_right_entry. wpo_beta_height_step_old_history_right_entry + S (espi_right_step_old_history) = S ((S (S (espi_pair_step_old_history + espi_pair_step_old_history))) * c)) /\ exists wpo_beta_quotient_step_old_history_right_entry. b = wpo_beta_quotient_step_old_history_right_entry * S ((S (S (espi_pair_step_old_history + espi_pair_step_old_history))) * c) + (espi_right_step_old_history))) /\ (((exists wpo_beta_height_step_old_history_scaled_edge. wpo_beta_height_step_old_history_scaled_edge + S (S espi_right_step_old_history) = S ((S (espi_left_step_old_history)) * v)) /\ exists wpo_beta_quotient_step_old_history_scaled_edge. u = wpo_beta_quotient_step_old_history_scaled_edge * S ((S (espi_left_step_old_history)) * v) + (S espi_right_step_old_history)))))))) -> (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)))))))))))

Structural proof guide

Generated structural guide

Append one fixed-point-free scaled orbit and preserve iterable state plus history.

Use the direct prerequisites scaled_inverse_pair_order_choose_append, beta_prefix_append_two_bounded_into, adjacent_scaled_orbit_history_append as previously established PA formulas.

The proof proceeds by case analysis (15), intermediate claims (5).

Referenced ingredients

PA009O scaled_inverse_pair_order_choose_append PA009P beta_prefix_append_two_bounded_into PA009S adjacent_scaled_orbit_history_append

Proof neighborhood

Direct dependencies

PA009O scaled_inverse_pair_order_choose_append PA009P beta_prefix_append_two_bounded_into PA009S adjacent_scaled_orbit_history_append

Direct dependents

PA009V scaled_inverse_pair_order_paired_iteration

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 b
  7. 0007intro c
  8. 0008intro m
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hnotqres
  12. 0012intro hprefix
  13. 0013intro hshort
  14. 0014intro hstate
  15. 0015intro hhistory
  16. 0016cases hstate
  17. 0017cases hstate_right
  18. 0018have hraw : exists z d i j. (((((((exists wpo_beta_height_step_payload_trace_first. wpo_beta_height_step_payload_trace_first + S (i) = S ((S (m + m)) * d)) /\ exists wpo_beta_quotient_step_payload_trace_first. z = wpo_beta_quotient_step_payload_trace_first * S ((S (m + m)) * d) + (i))) /\ ((((exists wpo_beta_height_step_payload_trace_second. wpo_beta_height_step_payload_trace_second + S (j) = S ((S (S (m + m))) * d)) /\ exists wpo_beta_quotient_step_payload_trace_second. z = wpo_beta_quotient_step_payload_trace_second * S ((S (S (m + m))) * d) + (j))) /\ (forall wpo_old_index_step_payload_trace wpo_old_value_step_payload_trace. (exists wpo_gap_step_payload_trace_old_bound. wpo_gap_step_payload_trace_old_bound + S (wpo_old_index_step_payload_trace) = m + m) -> (((exists wpo_beta_height_step_payload_trace_old_entry. wpo_beta_height_step_payload_trace_old_entry + S (wpo_old_value_step_payload_trace) = S ((S (wpo_old_index_step_payload_trace)) * c)) /\ exists wpo_beta_quotient_step_payload_trace_old_entry. b = wpo_beta_quotient_step_payload_trace_old_entry * S ((S (wpo_old_index_step_payload_trace)) * c) + (wpo_old_value_step_payload_trace))) -> (((exists wpo_beta_height_step_payload_trace_new_entry. wpo_beta_height_step_payload_trace_new_entry + S (wpo_old_value_step_payload_trace) = S ((S (wpo_old_index_step_payload_trace)) * d)) /\ exists wpo_beta_quotient_step_payload_trace_new_entry. z = wpo_beta_quotient_step_payload_trace_new_entry * S ((S (wpo_old_index_step_payload_trace)) * d) + (wpo_old_value_step_payload_trace))))))) /\ (((exists wpo_gap_step_payload_source_bound. wpo_gap_step_payload_source_bound + S (i) = n) /\ (((exists wpo_gap_step_payload_mate_bound. wpo_gap_step_payload_mate_bound + S (j) = n) /\ (((~(exists wpo_index_step_payload_source_omit_contains. ((exists wpo_gap_step_payload_source_omit_contains_bound. wpo_gap_step_payload_source_omit_contains_bound + S (wpo_index_step_payload_source_omit_contains) = m + m) /\ (((exists wpo_beta_height_step_payload_source_omit_contains_entry. wpo_beta_height_step_payload_source_omit_contains_entry + S (i) = S ((S (wpo_index_step_payload_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_payload_source_omit_contains_entry. b = wpo_beta_quotient_step_payload_source_omit_contains_entry * S ((S (wpo_index_step_payload_source_omit_contains)) * c) + (i)))))) /\ (((~(exists wpo_index_step_payload_mate_omit_contains. ((exists wpo_gap_step_payload_mate_omit_contains_bound. wpo_gap_step_payload_mate_omit_contains_bound + S (wpo_index_step_payload_mate_omit_contains) = m + m) /\ (((exists wpo_beta_height_step_payload_mate_omit_contains_entry. wpo_beta_height_step_payload_mate_omit_contains_entry + S (j) = S ((S (wpo_index_step_payload_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_payload_mate_omit_contains_entry. b = wpo_beta_quotient_step_payload_mate_omit_contains_entry * S ((S (wpo_index_step_payload_mate_omit_contains)) * c) + (j)))))) /\ (((~(i = j)) /\ (((((exists wpo_beta_height_step_payload_forward. wpo_beta_height_step_payload_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_step_payload_forward. u = wpo_beta_quotient_step_payload_forward * S ((S (i)) * v) + (S j))) /\ (((((exists wpo_beta_height_step_payload_back. wpo_beta_height_step_payload_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_step_payload_back. u = wpo_beta_quotient_step_payload_back * S ((S (j)) * v) + (S i))) /\ (((forall espo_position_step_payload_closed_after espo_source_step_payload_closed_after espo_mate_step_payload_closed_after. (exists wpo_gap_step_payload_closed_after_position_bound. wpo_gap_step_payload_closed_after_position_bound + S (espo_position_step_payload_closed_after) = S (S (m + m))) -> (((exists wpo_beta_height_step_payload_closed_after_source_entry. wpo_beta_height_step_payload_closed_after_source_entry + S (espo_source_step_payload_closed_after) = S ((S (espo_position_step_payload_closed_after)) * d)) /\ exists wpo_beta_quotient_step_payload_closed_after_source_entry. z = wpo_beta_quotient_step_payload_closed_after_source_entry * S ((S (espo_position_step_payload_closed_after)) * d) + (espo_source_step_payload_closed_after))) -> (((exists wpo_beta_height_step_payload_closed_after_scaled_entry. wpo_beta_height_step_payload_closed_after_scaled_entry + S (S espo_mate_step_payload_closed_after) = S ((S (espo_source_step_payload_closed_after)) * v)) /\ exists wpo_beta_quotient_step_payload_closed_after_scaled_entry. u = wpo_beta_quotient_step_payload_closed_after_scaled_entry * S ((S (espo_source_step_payload_closed_after)) * v) + (S espo_mate_step_payload_closed_after))) -> exists espo_mate_position_step_payload_closed_after. ((exists wpo_gap_step_payload_closed_after_mate_bound. wpo_gap_step_payload_closed_after_mate_bound + S (espo_mate_position_step_payload_closed_after) = S (S (m + m))) /\ (((exists wpo_beta_height_step_payload_closed_after_mate_entry. wpo_beta_height_step_payload_closed_after_mate_entry + S (espo_mate_step_payload_closed_after) = S ((S (espo_mate_position_step_payload_closed_after)) * d)) /\ exists wpo_beta_quotient_step_payload_closed_after_mate_entry. z = wpo_beta_quotient_step_payload_closed_after_mate_entry * S ((S (espo_mate_position_step_payload_closed_after)) * d) + (espo_mate_step_payload_closed_after))))) /\ (forall wpo_injective_left_step_payload_injective_after wpo_injective_right_step_payload_injective_after wpo_injective_value_step_payload_injective_after. (exists wpo_gap_step_payload_injective_after_left_bound. wpo_gap_step_payload_injective_after_left_bound + S (wpo_injective_left_step_payload_injective_after) = S (S (m + m))) -> (exists wpo_gap_step_payload_injective_after_right_bound. wpo_gap_step_payload_injective_after_right_bound + S (wpo_injective_right_step_payload_injective_after) = S (S (m + m))) -> (((exists wpo_beta_height_step_payload_injective_after_left_entry. wpo_beta_height_step_payload_injective_after_left_entry + S (wpo_injective_value_step_payload_injective_after) = S ((S (wpo_injective_left_step_payload_injective_after)) * d)) /\ exists wpo_beta_quotient_step_payload_injective_after_left_entry. z = wpo_beta_quotient_step_payload_injective_after_left_entry * S ((S (wpo_injective_left_step_payload_injective_after)) * d) + (wpo_injective_value_step_payload_injective_after))) -> (((exists wpo_beta_height_step_payload_injective_after_right_entry. wpo_beta_height_step_payload_injective_after_right_entry + S (wpo_injective_value_step_payload_injective_after) = S ((S (wpo_injective_right_step_payload_injective_after)) * d)) /\ exists wpo_beta_quotient_step_payload_injective_after_right_entry. z = wpo_beta_quotient_step_payload_injective_after_right_entry * S ((S (wpo_injective_right_step_payload_injective_after)) * d) + (wpo_injective_value_step_payload_injective_after))) -> wpo_injective_left_step_payload_injective_after = wpo_injective_right_step_payload_injective_after)))))))))))))))))))
  19. 0019specialize scaled_inverse_pair_order_choose_append p
  20. 0020specialize scaled_inverse_pair_order_choose_append a
  21. 0021specialize scaled_inverse_pair_order_choose_append n
  22. 0022specialize scaled_inverse_pair_order_choose_append u
  23. 0023specialize scaled_inverse_pair_order_choose_append v
  24. 0024specialize scaled_inverse_pair_order_choose_append b
  25. 0025specialize scaled_inverse_pair_order_choose_append c
  26. 0026specialize scaled_inverse_pair_order_choose_append (m + m)
  27. 0027apply scaled_inverse_pair_order_choose_append
  28. 0028exact hpn
  29. 0029exact hp
  30. 0030exact hnotqres
  31. 0031exact hprefix
  32. 0032exact hshort
  33. 0033exact hstate_left
  34. 0034exact hstate_right_right
  35. 0035cases hraw
  36. 0036cases hraw_witness
  37. 0037cases hraw_witness_witness
  38. 0038cases hraw_witness_witness_witness
  39. 0039have hparts : ((((((exists wpo_beta_height_step_payload_x_trace_first. wpo_beta_height_step_payload_x_trace_first + S (x2) = S ((S (m + m)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_trace_first. x = wpo_beta_quotient_step_payload_x_trace_first * S ((S (m + m)) * x1) + (x2))) /\ ((((exists wpo_beta_height_step_payload_x_trace_second. wpo_beta_height_step_payload_x_trace_second + S (x3) = S ((S (S (m + m))) * x1)) /\ exists wpo_beta_quotient_step_payload_x_trace_second. x = wpo_beta_quotient_step_payload_x_trace_second * S ((S (S (m + m))) * x1) + (x3))) /\ (forall wpo_old_index_step_payload_x_trace wpo_old_value_step_payload_x_trace. (exists wpo_gap_step_payload_x_trace_old_bound. wpo_gap_step_payload_x_trace_old_bound + S (wpo_old_index_step_payload_x_trace) = m + m) -> (((exists wpo_beta_height_step_payload_x_trace_old_entry. wpo_beta_height_step_payload_x_trace_old_entry + S (wpo_old_value_step_payload_x_trace) = S ((S (wpo_old_index_step_payload_x_trace)) * c)) /\ exists wpo_beta_quotient_step_payload_x_trace_old_entry. b = wpo_beta_quotient_step_payload_x_trace_old_entry * S ((S (wpo_old_index_step_payload_x_trace)) * c) + (wpo_old_value_step_payload_x_trace))) -> (((exists wpo_beta_height_step_payload_x_trace_new_entry. wpo_beta_height_step_payload_x_trace_new_entry + S (wpo_old_value_step_payload_x_trace) = S ((S (wpo_old_index_step_payload_x_trace)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_trace_new_entry. x = wpo_beta_quotient_step_payload_x_trace_new_entry * S ((S (wpo_old_index_step_payload_x_trace)) * x1) + (wpo_old_value_step_payload_x_trace))))))) /\ (((exists wpo_gap_step_payload_x_source_bound. wpo_gap_step_payload_x_source_bound + S (x2) = n) /\ (((exists wpo_gap_step_payload_x_mate_bound. wpo_gap_step_payload_x_mate_bound + S (x3) = n) /\ (((~(exists wpo_index_step_payload_x_source_omit_contains. ((exists wpo_gap_step_payload_x_source_omit_contains_bound. wpo_gap_step_payload_x_source_omit_contains_bound + S (wpo_index_step_payload_x_source_omit_contains) = m + m) /\ (((exists wpo_beta_height_step_payload_x_source_omit_contains_entry. wpo_beta_height_step_payload_x_source_omit_contains_entry + S (x2) = S ((S (wpo_index_step_payload_x_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_payload_x_source_omit_contains_entry. b = wpo_beta_quotient_step_payload_x_source_omit_contains_entry * S ((S (wpo_index_step_payload_x_source_omit_contains)) * c) + (x2)))))) /\ (((~(exists wpo_index_step_payload_x_mate_omit_contains. ((exists wpo_gap_step_payload_x_mate_omit_contains_bound. wpo_gap_step_payload_x_mate_omit_contains_bound + S (wpo_index_step_payload_x_mate_omit_contains) = m + m) /\ (((exists wpo_beta_height_step_payload_x_mate_omit_contains_entry. wpo_beta_height_step_payload_x_mate_omit_contains_entry + S (x3) = S ((S (wpo_index_step_payload_x_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_payload_x_mate_omit_contains_entry. b = wpo_beta_quotient_step_payload_x_mate_omit_contains_entry * S ((S (wpo_index_step_payload_x_mate_omit_contains)) * c) + (x3)))))) /\ (((~(x2 = x3)) /\ (((((exists wpo_beta_height_step_payload_x_forward. wpo_beta_height_step_payload_x_forward + S (S x3) = S ((S (x2)) * v)) /\ exists wpo_beta_quotient_step_payload_x_forward. u = wpo_beta_quotient_step_payload_x_forward * S ((S (x2)) * v) + (S x3))) /\ (((((exists wpo_beta_height_step_payload_x_back. wpo_beta_height_step_payload_x_back + S (S x2) = S ((S (x3)) * v)) /\ exists wpo_beta_quotient_step_payload_x_back. u = wpo_beta_quotient_step_payload_x_back * S ((S (x3)) * v) + (S x2))) /\ (((forall espo_position_step_payload_x_closed_after espo_source_step_payload_x_closed_after espo_mate_step_payload_x_closed_after. (exists wpo_gap_step_payload_x_closed_after_position_bound. wpo_gap_step_payload_x_closed_after_position_bound + S (espo_position_step_payload_x_closed_after) = S (S (m + m))) -> (((exists wpo_beta_height_step_payload_x_closed_after_source_entry. wpo_beta_height_step_payload_x_closed_after_source_entry + S (espo_source_step_payload_x_closed_after) = S ((S (espo_position_step_payload_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_closed_after_source_entry. x = wpo_beta_quotient_step_payload_x_closed_after_source_entry * S ((S (espo_position_step_payload_x_closed_after)) * x1) + (espo_source_step_payload_x_closed_after))) -> (((exists wpo_beta_height_step_payload_x_closed_after_scaled_entry. wpo_beta_height_step_payload_x_closed_after_scaled_entry + S (S espo_mate_step_payload_x_closed_after) = S ((S (espo_source_step_payload_x_closed_after)) * v)) /\ exists wpo_beta_quotient_step_payload_x_closed_after_scaled_entry. u = wpo_beta_quotient_step_payload_x_closed_after_scaled_entry * S ((S (espo_source_step_payload_x_closed_after)) * v) + (S espo_mate_step_payload_x_closed_after))) -> exists espo_mate_position_step_payload_x_closed_after. ((exists wpo_gap_step_payload_x_closed_after_mate_bound. wpo_gap_step_payload_x_closed_after_mate_bound + S (espo_mate_position_step_payload_x_closed_after) = S (S (m + m))) /\ (((exists wpo_beta_height_step_payload_x_closed_after_mate_entry. wpo_beta_height_step_payload_x_closed_after_mate_entry + S (espo_mate_step_payload_x_closed_after) = S ((S (espo_mate_position_step_payload_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_closed_after_mate_entry. x = wpo_beta_quotient_step_payload_x_closed_after_mate_entry * S ((S (espo_mate_position_step_payload_x_closed_after)) * x1) + (espo_mate_step_payload_x_closed_after))))) /\ (forall wpo_injective_left_step_payload_x_injective_after wpo_injective_right_step_payload_x_injective_after wpo_injective_value_step_payload_x_injective_after. (exists wpo_gap_step_payload_x_injective_after_left_bound. wpo_gap_step_payload_x_injective_after_left_bound + S (wpo_injective_left_step_payload_x_injective_after) = S (S (m + m))) -> (exists wpo_gap_step_payload_x_injective_after_right_bound. wpo_gap_step_payload_x_injective_after_right_bound + S (wpo_injective_right_step_payload_x_injective_after) = S (S (m + m))) -> (((exists wpo_beta_height_step_payload_x_injective_after_left_entry. wpo_beta_height_step_payload_x_injective_after_left_entry + S (wpo_injective_value_step_payload_x_injective_after) = S ((S (wpo_injective_left_step_payload_x_injective_after)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_injective_after_left_entry. x = wpo_beta_quotient_step_payload_x_injective_after_left_entry * S ((S (wpo_injective_left_step_payload_x_injective_after)) * x1) + (wpo_injective_value_step_payload_x_injective_after))) -> (((exists wpo_beta_height_step_payload_x_injective_after_right_entry. wpo_beta_height_step_payload_x_injective_after_right_entry + S (wpo_injective_value_step_payload_x_injective_after) = S ((S (wpo_injective_right_step_payload_x_injective_after)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_injective_after_right_entry. x = wpo_beta_quotient_step_payload_x_injective_after_right_entry * S ((S (wpo_injective_right_step_payload_x_injective_after)) * x1) + (wpo_injective_value_step_payload_x_injective_after))) -> wpo_injective_left_step_payload_x_injective_after = wpo_injective_right_step_payload_x_injective_after))))))))))))))))))
  40. 0040exact hraw_witness_witness_witness_witness
  41. 0041cases hparts
  42. 0042cases hparts_right
  43. 0043cases hparts_right_right
  44. 0044cases hparts_right_right_right
  45. 0045cases hparts_right_right_right_right
  46. 0046cases hparts_right_right_right_right_right
  47. 0047cases hparts_right_right_right_right_right_right
  48. 0048cases hparts_right_right_right_right_right_right_right
  49. 0049cases hparts_right_right_right_right_right_right_right_right
  50. 0050have hbounded_after : forall fom_index_bounded_after_x. (exists fom_gap_bounded_after_x_index_bound. fom_gap_bounded_after_x_index_bound + S (fom_index_bounded_after_x) = S (S (m + m))) -> exists fom_value_bounded_after_x. ((((exists fom_beta_height_bounded_after_x_entry. fom_beta_height_bounded_after_x_entry + S (fom_value_bounded_after_x) = S ((S (fom_index_bounded_after_x)) * x1)) /\ exists fom_beta_quotient_bounded_after_x_entry. x = fom_beta_quotient_bounded_after_x_entry * S ((S (fom_index_bounded_after_x)) * x1) + (fom_value_bounded_after_x))) /\ (exists fom_gap_bounded_after_x_value_bound. fom_gap_bounded_after_x_value_bound + S (fom_value_bounded_after_x) = n))
  51. 0051specialize beta_prefix_append_two_bounded_into b
  52. 0052specialize beta_prefix_append_two_bounded_into c
  53. 0053specialize beta_prefix_append_two_bounded_into x
  54. 0054specialize beta_prefix_append_two_bounded_into x1
  55. 0055specialize beta_prefix_append_two_bounded_into (m + m)
  56. 0056specialize beta_prefix_append_two_bounded_into n
  57. 0057specialize beta_prefix_append_two_bounded_into x2
  58. 0058specialize beta_prefix_append_two_bounded_into x3
  59. 0059apply beta_prefix_append_two_bounded_into
  60. 0060exact hparts_left
  61. 0061exact hstate_right_left
  62. 0062exact hparts_right_left
  63. 0063exact hparts_right_right_left
  64. 0064have hhistory_after : forall espi_pair_history_after_x. (exists wpo_gap_history_after_x_pair_bound. wpo_gap_history_after_x_pair_bound + S (espi_pair_history_after_x) = S m) -> exists espi_left_history_after_x espi_right_history_after_x. (((((exists wpo_beta_height_history_after_x_left_entry. wpo_beta_height_history_after_x_left_entry + S (espi_left_history_after_x) = S ((S (espi_pair_history_after_x + espi_pair_history_after_x)) * x1)) /\ exists wpo_beta_quotient_history_after_x_left_entry. x = wpo_beta_quotient_history_after_x_left_entry * S ((S (espi_pair_history_after_x + espi_pair_history_after_x)) * x1) + (espi_left_history_after_x))) /\ (((((exists wpo_beta_height_history_after_x_right_entry. wpo_beta_height_history_after_x_right_entry + S (espi_right_history_after_x) = S ((S (S (espi_pair_history_after_x + espi_pair_history_after_x))) * x1)) /\ exists wpo_beta_quotient_history_after_x_right_entry. x = wpo_beta_quotient_history_after_x_right_entry * S ((S (S (espi_pair_history_after_x + espi_pair_history_after_x))) * x1) + (espi_right_history_after_x))) /\ (((exists wpo_beta_height_history_after_x_scaled_edge. wpo_beta_height_history_after_x_scaled_edge + S (S espi_right_history_after_x) = S ((S (espi_left_history_after_x)) * v)) /\ exists wpo_beta_quotient_history_after_x_scaled_edge. u = wpo_beta_quotient_history_after_x_scaled_edge * S ((S (espi_left_history_after_x)) * v) + (S espi_right_history_after_x)))))))
  65. 0065specialize adjacent_scaled_orbit_history_append u
  66. 0066specialize adjacent_scaled_orbit_history_append v
  67. 0067specialize adjacent_scaled_orbit_history_append b
  68. 0068specialize adjacent_scaled_orbit_history_append c
  69. 0069specialize adjacent_scaled_orbit_history_append x
  70. 0070specialize adjacent_scaled_orbit_history_append x1
  71. 0071specialize adjacent_scaled_orbit_history_append m
  72. 0072specialize adjacent_scaled_orbit_history_append x2
  73. 0073specialize adjacent_scaled_orbit_history_append x3
  74. 0074apply adjacent_scaled_orbit_history_append
  75. 0075exact hhistory
  76. 0076exact hparts_left
  77. 0077exact hparts_right_right_right_right_right_right_left
  78. 0078have hstate_after : ((forall espo_position_state_after_x_closed espo_source_state_after_x_closed espo_mate_state_after_x_closed. (exists wpo_gap_state_after_x_closed_position_bound. wpo_gap_state_after_x_closed_position_bound + S (espo_position_state_after_x_closed) = S (S (m + m))) -> (((exists wpo_beta_height_state_after_x_closed_source_entry. wpo_beta_height_state_after_x_closed_source_entry + S (espo_source_state_after_x_closed) = S ((S (espo_position_state_after_x_closed)) * x1)) /\ exists wpo_beta_quotient_state_after_x_closed_source_entry. x = wpo_beta_quotient_state_after_x_closed_source_entry * S ((S (espo_position_state_after_x_closed)) * x1) + (espo_source_state_after_x_closed))) -> (((exists wpo_beta_height_state_after_x_closed_scaled_entry. wpo_beta_height_state_after_x_closed_scaled_entry + S (S espo_mate_state_after_x_closed) = S ((S (espo_source_state_after_x_closed)) * v)) /\ exists wpo_beta_quotient_state_after_x_closed_scaled_entry. u = wpo_beta_quotient_state_after_x_closed_scaled_entry * S ((S (espo_source_state_after_x_closed)) * v) + (S espo_mate_state_after_x_closed))) -> exists espo_mate_position_state_after_x_closed. ((exists wpo_gap_state_after_x_closed_mate_bound. wpo_gap_state_after_x_closed_mate_bound + S (espo_mate_position_state_after_x_closed) = S (S (m + m))) /\ (((exists wpo_beta_height_state_after_x_closed_mate_entry. wpo_beta_height_state_after_x_closed_mate_entry + S (espo_mate_state_after_x_closed) = S ((S (espo_mate_position_state_after_x_closed)) * x1)) /\ exists wpo_beta_quotient_state_after_x_closed_mate_entry. x = wpo_beta_quotient_state_after_x_closed_mate_entry * S ((S (espo_mate_position_state_after_x_closed)) * x1) + (espo_mate_state_after_x_closed))))) /\ (((forall fom_index_state_after_x_bounded. (exists fom_gap_state_after_x_bounded_index_bound. fom_gap_state_after_x_bounded_index_bound + S (fom_index_state_after_x_bounded) = S (S (m + m))) -> exists fom_value_state_after_x_bounded. ((((exists fom_beta_height_state_after_x_bounded_entry. fom_beta_height_state_after_x_bounded_entry + S (fom_value_state_after_x_bounded) = S ((S (fom_index_state_after_x_bounded)) * x1)) /\ exists fom_beta_quotient_state_after_x_bounded_entry. x = fom_beta_quotient_state_after_x_bounded_entry * S ((S (fom_index_state_after_x_bounded)) * x1) + (fom_value_state_after_x_bounded))) /\ (exists fom_gap_state_after_x_bounded_value_bound. fom_gap_state_after_x_bounded_value_bound + S (fom_value_state_after_x_bounded) = n))) /\ (forall wpo_injective_left_state_after_x_injective wpo_injective_right_state_after_x_injective wpo_injective_value_state_after_x_injective. (exists wpo_gap_state_after_x_injective_left_bound. wpo_gap_state_after_x_injective_left_bound + S (wpo_injective_left_state_after_x_injective) = S (S (m + m))) -> (exists wpo_gap_state_after_x_injective_right_bound. wpo_gap_state_after_x_injective_right_bound + S (wpo_injective_right_state_after_x_injective) = S (S (m + m))) -> (((exists wpo_beta_height_state_after_x_injective_left_entry. wpo_beta_height_state_after_x_injective_left_entry + S (wpo_injective_value_state_after_x_injective) = S ((S (wpo_injective_left_state_after_x_injective)) * x1)) /\ exists wpo_beta_quotient_state_after_x_injective_left_entry. x = wpo_beta_quotient_state_after_x_injective_left_entry * S ((S (wpo_injective_left_state_after_x_injective)) * x1) + (wpo_injective_value_state_after_x_injective))) -> (((exists wpo_beta_height_state_after_x_injective_right_entry. wpo_beta_height_state_after_x_injective_right_entry + S (wpo_injective_value_state_after_x_injective) = S ((S (wpo_injective_right_state_after_x_injective)) * x1)) /\ exists wpo_beta_quotient_state_after_x_injective_right_entry. x = wpo_beta_quotient_state_after_x_injective_right_entry * S ((S (wpo_injective_right_state_after_x_injective)) * x1) + (wpo_injective_value_state_after_x_injective))) -> wpo_injective_left_state_after_x_injective = wpo_injective_right_state_after_x_injective))))
  79. 0079split
  80. 0080exact hparts_right_right_right_right_right_right_right_right_left
  81. 0081split
  82. 0082exact hbounded_after
  83. 0083exact hparts_right_right_right_right_right_right_right_right_right
  84. 0084exists x
  85. 0085exists x1
  86. 0086split
  87. 0087exact hstate_after
  88. 0088exact hhistory_after