PA00B0

prime_pair_order_paired_state_step

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

Preserve the bounded PairOrder state and every adjacent inverse-pair witness through one append.

Exact expanded PA statement

forall p n u v b c m r. p = S n -> ((~(p = 1) /\ forall wip_prime_left_wpopi_prime wip_prime_right_wpopi_prime. p = wip_prime_left_wpopi_prime * wip_prime_right_wpopi_prime -> wip_prime_left_wpopi_prime = 1 \/ wip_prime_right_wpopi_prime = 1)) -> (forall wip_index_wpopi_inverse. (exists wip_gap_wpopi_inverse_prefix_bound. wip_gap_wpopi_inverse_prefix_bound + S wip_index_wpopi_inverse = n) -> exists wip_mate_wpopi_inverse. ((((exists wip_beta_height_wpopi_inverse_decoded. wip_beta_height_wpopi_inverse_decoded + S (wip_mate_wpopi_inverse) = S ((S (wip_index_wpopi_inverse)) * v)) /\ exists wip_beta_quotient_wpopi_inverse_decoded. u = wip_beta_quotient_wpopi_inverse_decoded * S ((S (wip_index_wpopi_inverse)) * v) + (wip_mate_wpopi_inverse))) /\ ((exists wip_gap_wpopi_inverse_inverse_index_bound. wip_gap_wpopi_inverse_inverse_index_bound + S wip_index_wpopi_inverse = n) /\ ((exists wip_gap_wpopi_inverse_inverse_mate_bound. wip_gap_wpopi_inverse_inverse_mate_bound + S wip_mate_wpopi_inverse = n) /\ (exists wip_mod_left_wpopi_inverse_inverse_mod wip_mod_right_wpopi_inverse_inverse_mod. ((S wip_index_wpopi_inverse) * S wip_mate_wpopi_inverse) + p * wip_mod_left_wpopi_inverse_inverse_mod = 1 + p * wip_mod_right_wpopi_inverse_inverse_mod))))) -> n = S r -> (exists h. h + S (S (S (m + m))) = n) -> (((forall wpo_position_wpopi_old_state_closed wpo_source_wpopi_old_state_closed wpo_mate_wpopi_old_state_closed. (exists wpo_gap_wpopi_old_state_closed_position_bound. wpo_gap_wpopi_old_state_closed_position_bound + S (wpo_position_wpopi_old_state_closed) = (m + m)) -> (((exists wpo_beta_height_wpopi_old_state_closed_source_entry. wpo_beta_height_wpopi_old_state_closed_source_entry + S (wpo_source_wpopi_old_state_closed) = S ((S (wpo_position_wpopi_old_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_old_state_closed_source_entry. b = wpo_beta_quotient_wpopi_old_state_closed_source_entry * S ((S (wpo_position_wpopi_old_state_closed)) * c) + (wpo_source_wpopi_old_state_closed))) -> (((exists wpo_beta_height_wpopi_old_state_closed_inverse_entry. wpo_beta_height_wpopi_old_state_closed_inverse_entry + S (wpo_mate_wpopi_old_state_closed) = S ((S (wpo_source_wpopi_old_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_old_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_old_state_closed_inverse_entry * S ((S (wpo_source_wpopi_old_state_closed)) * v) + (wpo_mate_wpopi_old_state_closed))) -> exists wpo_mate_position_wpopi_old_state_closed. ((exists wpo_gap_wpopi_old_state_closed_mate_bound. wpo_gap_wpopi_old_state_closed_mate_bound + S (wpo_mate_position_wpopi_old_state_closed) = (m + m)) /\ (((exists wpo_beta_height_wpopi_old_state_closed_mate_entry. wpo_beta_height_wpopi_old_state_closed_mate_entry + S (wpo_mate_wpopi_old_state_closed) = S ((S (wpo_mate_position_wpopi_old_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_old_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_old_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_old_state_closed)) * c) + (wpo_mate_wpopi_old_state_closed))))) /\ ((forall fom_index_wpopi_old_state_bounded. (exists fom_gap_wpopi_old_state_bounded_index_bound. fom_gap_wpopi_old_state_bounded_index_bound + S (fom_index_wpopi_old_state_bounded) = (m + m)) -> exists fom_value_wpopi_old_state_bounded. ((((exists fom_beta_height_wpopi_old_state_bounded_entry. fom_beta_height_wpopi_old_state_bounded_entry + S (fom_value_wpopi_old_state_bounded) = S ((S (fom_index_wpopi_old_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_old_state_bounded_entry. b = fom_beta_quotient_wpopi_old_state_bounded_entry * S ((S (fom_index_wpopi_old_state_bounded)) * c) + (fom_value_wpopi_old_state_bounded))) /\ (exists fom_gap_wpopi_old_state_bounded_value_bound. fom_gap_wpopi_old_state_bounded_value_bound + S (fom_value_wpopi_old_state_bounded) = n))) /\ ((forall wpo_position_wpopi_old_state_nonendpoint wpo_value_wpopi_old_state_nonendpoint. (exists wpo_gap_wpopi_old_state_nonendpoint_position_bound. wpo_gap_wpopi_old_state_nonendpoint_position_bound + S (wpo_position_wpopi_old_state_nonendpoint) = (m + m)) -> (((exists wpo_beta_height_wpopi_old_state_nonendpoint_entry. wpo_beta_height_wpopi_old_state_nonendpoint_entry + S (wpo_value_wpopi_old_state_nonendpoint) = S ((S (wpo_position_wpopi_old_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_old_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_old_state_nonendpoint_entry * S ((S (wpo_position_wpopi_old_state_nonendpoint)) * c) + (wpo_value_wpopi_old_state_nonendpoint))) -> (~(wpo_value_wpopi_old_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_old_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_old_state_injective wpo_injective_right_wpopi_old_state_injective wpo_injective_value_wpopi_old_state_injective. (exists wpo_gap_wpopi_old_state_injective_left_bound. wpo_gap_wpopi_old_state_injective_left_bound + S (wpo_injective_left_wpopi_old_state_injective) = (m + m)) -> (exists wpo_gap_wpopi_old_state_injective_right_bound. wpo_gap_wpopi_old_state_injective_right_bound + S (wpo_injective_right_wpopi_old_state_injective) = (m + m)) -> (((exists wpo_beta_height_wpopi_old_state_injective_left_entry. wpo_beta_height_wpopi_old_state_injective_left_entry + S (wpo_injective_value_wpopi_old_state_injective) = S ((S (wpo_injective_left_wpopi_old_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_old_state_injective_left_entry. b = wpo_beta_quotient_wpopi_old_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_old_state_injective)) * c) + (wpo_injective_value_wpopi_old_state_injective))) -> (((exists wpo_beta_height_wpopi_old_state_injective_right_entry. wpo_beta_height_wpopi_old_state_injective_right_entry + S (wpo_injective_value_wpopi_old_state_injective) = S ((S (wpo_injective_right_wpopi_old_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_old_state_injective_right_entry. b = wpo_beta_quotient_wpopi_old_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_old_state_injective)) * c) + (wpo_injective_value_wpopi_old_state_injective))) -> wpo_injective_left_wpopi_old_state_injective = wpo_injective_right_wpopi_old_state_injective))))) -> (forall wpop_pair_wpop_old_pairs. (exists wpo_gap_wpop_old_pairs_pair_bound. wpo_gap_wpop_old_pairs_pair_bound + S (wpop_pair_wpop_old_pairs) = m) -> exists wpop_left_wpop_old_pairs wpop_right_wpop_old_pairs. ((((exists wpo_beta_height_wpop_old_pairs_left_entry. wpo_beta_height_wpop_old_pairs_left_entry + S (wpop_left_wpop_old_pairs) = S ((S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs)) * c)) /\ exists wpo_beta_quotient_wpop_old_pairs_left_entry. b = wpo_beta_quotient_wpop_old_pairs_left_entry * S ((S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs)) * c) + (wpop_left_wpop_old_pairs))) /\ ((((exists wpo_beta_height_wpop_old_pairs_right_entry. wpo_beta_height_wpop_old_pairs_right_entry + S (wpop_right_wpop_old_pairs) = S ((S (S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs))) * c)) /\ exists wpo_beta_quotient_wpop_old_pairs_right_entry. b = wpo_beta_quotient_wpop_old_pairs_right_entry * S ((S (S (wpop_pair_wpop_old_pairs + wpop_pair_wpop_old_pairs))) * c) + (wpop_right_wpop_old_pairs))) /\ (((exists wpo_beta_height_wpop_old_pairs_inverse_entry. wpo_beta_height_wpop_old_pairs_inverse_entry + S (wpop_right_wpop_old_pairs) = S ((S (wpop_left_wpop_old_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_old_pairs_inverse_entry. u = wpo_beta_quotient_wpop_old_pairs_inverse_entry * S ((S (wpop_left_wpop_old_pairs)) * v) + (wpop_right_wpop_old_pairs)))))) -> (exists z d. ((((forall wpo_position_wpopi_next_state_closed wpo_source_wpopi_next_state_closed wpo_mate_wpopi_next_state_closed. (exists wpo_gap_wpopi_next_state_closed_position_bound. wpo_gap_wpopi_next_state_closed_position_bound + S (wpo_position_wpopi_next_state_closed) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_closed_source_entry. wpo_beta_height_wpopi_next_state_closed_source_entry + S (wpo_source_wpopi_next_state_closed) = S ((S (wpo_position_wpopi_next_state_closed)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_source_entry. z = wpo_beta_quotient_wpopi_next_state_closed_source_entry * S ((S (wpo_position_wpopi_next_state_closed)) * d) + (wpo_source_wpopi_next_state_closed))) -> (((exists wpo_beta_height_wpopi_next_state_closed_inverse_entry. wpo_beta_height_wpopi_next_state_closed_inverse_entry + S (wpo_mate_wpopi_next_state_closed) = S ((S (wpo_source_wpopi_next_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_next_state_closed_inverse_entry * S ((S (wpo_source_wpopi_next_state_closed)) * v) + (wpo_mate_wpopi_next_state_closed))) -> exists wpo_mate_position_wpopi_next_state_closed. ((exists wpo_gap_wpopi_next_state_closed_mate_bound. wpo_gap_wpopi_next_state_closed_mate_bound + S (wpo_mate_position_wpopi_next_state_closed) = S (S (m + m))) /\ (((exists wpo_beta_height_wpopi_next_state_closed_mate_entry. wpo_beta_height_wpopi_next_state_closed_mate_entry + S (wpo_mate_wpopi_next_state_closed) = S ((S (wpo_mate_position_wpopi_next_state_closed)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_closed_mate_entry. z = wpo_beta_quotient_wpopi_next_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_next_state_closed)) * d) + (wpo_mate_wpopi_next_state_closed))))) /\ ((forall fom_index_wpopi_next_state_bounded. (exists fom_gap_wpopi_next_state_bounded_index_bound. fom_gap_wpopi_next_state_bounded_index_bound + S (fom_index_wpopi_next_state_bounded) = S (S (m + m))) -> exists fom_value_wpopi_next_state_bounded. ((((exists fom_beta_height_wpopi_next_state_bounded_entry. fom_beta_height_wpopi_next_state_bounded_entry + S (fom_value_wpopi_next_state_bounded) = S ((S (fom_index_wpopi_next_state_bounded)) * d)) /\ exists fom_beta_quotient_wpopi_next_state_bounded_entry. z = fom_beta_quotient_wpopi_next_state_bounded_entry * S ((S (fom_index_wpopi_next_state_bounded)) * d) + (fom_value_wpopi_next_state_bounded))) /\ (exists fom_gap_wpopi_next_state_bounded_value_bound. fom_gap_wpopi_next_state_bounded_value_bound + S (fom_value_wpopi_next_state_bounded) = n))) /\ ((forall wpo_position_wpopi_next_state_nonendpoint wpo_value_wpopi_next_state_nonendpoint. (exists wpo_gap_wpopi_next_state_nonendpoint_position_bound. wpo_gap_wpopi_next_state_nonendpoint_position_bound + S (wpo_position_wpopi_next_state_nonendpoint) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_nonendpoint_entry. wpo_beta_height_wpopi_next_state_nonendpoint_entry + S (wpo_value_wpopi_next_state_nonendpoint) = S ((S (wpo_position_wpopi_next_state_nonendpoint)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_nonendpoint_entry. z = wpo_beta_quotient_wpopi_next_state_nonendpoint_entry * S ((S (wpo_position_wpopi_next_state_nonendpoint)) * d) + (wpo_value_wpopi_next_state_nonendpoint))) -> (~(wpo_value_wpopi_next_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_next_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_next_state_injective wpo_injective_right_wpopi_next_state_injective wpo_injective_value_wpopi_next_state_injective. (exists wpo_gap_wpopi_next_state_injective_left_bound. wpo_gap_wpopi_next_state_injective_left_bound + S (wpo_injective_left_wpopi_next_state_injective) = S (S (m + m))) -> (exists wpo_gap_wpopi_next_state_injective_right_bound. wpo_gap_wpopi_next_state_injective_right_bound + S (wpo_injective_right_wpopi_next_state_injective) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_next_state_injective_left_entry. wpo_beta_height_wpopi_next_state_injective_left_entry + S (wpo_injective_value_wpopi_next_state_injective) = S ((S (wpo_injective_left_wpopi_next_state_injective)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_injective_left_entry. z = wpo_beta_quotient_wpopi_next_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_next_state_injective)) * d) + (wpo_injective_value_wpopi_next_state_injective))) -> (((exists wpo_beta_height_wpopi_next_state_injective_right_entry. wpo_beta_height_wpopi_next_state_injective_right_entry + S (wpo_injective_value_wpopi_next_state_injective) = S ((S (wpo_injective_right_wpopi_next_state_injective)) * d)) /\ exists wpo_beta_quotient_wpopi_next_state_injective_right_entry. z = wpo_beta_quotient_wpopi_next_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_next_state_injective)) * d) + (wpo_injective_value_wpopi_next_state_injective))) -> wpo_injective_left_wpopi_next_state_injective = wpo_injective_right_wpopi_next_state_injective))))) /\ (forall wpop_pair_wpop_new_pairs. (exists wpo_gap_wpop_new_pairs_pair_bound. wpo_gap_wpop_new_pairs_pair_bound + S (wpop_pair_wpop_new_pairs) = S m) -> exists wpop_left_wpop_new_pairs wpop_right_wpop_new_pairs. ((((exists wpo_beta_height_wpop_new_pairs_left_entry. wpo_beta_height_wpop_new_pairs_left_entry + S (wpop_left_wpop_new_pairs) = S ((S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs)) * d)) /\ exists wpo_beta_quotient_wpop_new_pairs_left_entry. z = wpo_beta_quotient_wpop_new_pairs_left_entry * S ((S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs)) * d) + (wpop_left_wpop_new_pairs))) /\ ((((exists wpo_beta_height_wpop_new_pairs_right_entry. wpo_beta_height_wpop_new_pairs_right_entry + S (wpop_right_wpop_new_pairs) = S ((S (S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs))) * d)) /\ exists wpo_beta_quotient_wpop_new_pairs_right_entry. z = wpo_beta_quotient_wpop_new_pairs_right_entry * S ((S (S (wpop_pair_wpop_new_pairs + wpop_pair_wpop_new_pairs))) * d) + (wpop_right_wpop_new_pairs))) /\ (((exists wpo_beta_height_wpop_new_pairs_inverse_entry. wpo_beta_height_wpop_new_pairs_inverse_entry + S (wpop_right_wpop_new_pairs) = S ((S (wpop_left_wpop_new_pairs)) * v)) /\ exists wpo_beta_quotient_wpop_new_pairs_inverse_entry. u = wpo_beta_quotient_wpop_new_pairs_inverse_entry * S ((S (wpop_left_wpop_new_pairs)) * v) + (wpop_right_wpop_new_pairs))))))))

Structural proof guide

Generated structural guide

Preserve the bounded PairOrder state and every adjacent inverse-pair witness through one append.

Use the direct prerequisites prime_pair_order_choose_append_state, paired_inverse_witness_append as previously established PA formulas.

The proof proceeds by case analysis (20), intermediate claims (3).

Referenced ingredients

PA00AX prime_pair_order_choose_append_state PA00AY paired_inverse_witness_append

Proof neighborhood

Direct dependencies

PA00AX prime_pair_order_choose_append_state PA00AY paired_inverse_witness_append

Direct dependents

PA00B1 prime_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 n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro b
  6. 0006intro c
  7. 0007intro m
  8. 0008intro r
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hprefix
  12. 0012intro hnr
  13. 0013intro hroom
  14. 0014intro hstate
  15. 0015intro hhistory
  16. 0016cases hstate
  17. 0017cases hstate_right
  18. 0018cases hstate_right_right
  19. 0019have hstep : exists z d i j. ((((((((exists wpo_beta_height_wpopi_step_body_trace_first. wpo_beta_height_wpopi_step_body_trace_first + S (i) = S ((S ((m + m))) * d)) /\ exists wpo_beta_quotient_wpopi_step_body_trace_first. z = wpo_beta_quotient_wpopi_step_body_trace_first * S ((S ((m + m))) * d) + (i))) /\ ((((exists wpo_beta_height_wpopi_step_body_trace_second. wpo_beta_height_wpopi_step_body_trace_second + S (j) = S ((S (S ((m + m)))) * d)) /\ exists wpo_beta_quotient_wpopi_step_body_trace_second. z = wpo_beta_quotient_wpopi_step_body_trace_second * S ((S (S ((m + m)))) * d) + (j))) /\ (forall wpo_old_index_wpopi_step_body_trace wpo_old_value_wpopi_step_body_trace. (exists wpo_gap_wpopi_step_body_trace_old_bound. wpo_gap_wpopi_step_body_trace_old_bound + S (wpo_old_index_wpopi_step_body_trace) = (m + m)) -> (((exists wpo_beta_height_wpopi_step_body_trace_old_entry. wpo_beta_height_wpopi_step_body_trace_old_entry + S (wpo_old_value_wpopi_step_body_trace) = S ((S (wpo_old_index_wpopi_step_body_trace)) * c)) /\ exists wpo_beta_quotient_wpopi_step_body_trace_old_entry. b = wpo_beta_quotient_wpopi_step_body_trace_old_entry * S ((S (wpo_old_index_wpopi_step_body_trace)) * c) + (wpo_old_value_wpopi_step_body_trace))) -> (((exists wpo_beta_height_wpopi_step_body_trace_new_entry. wpo_beta_height_wpopi_step_body_trace_new_entry + S (wpo_old_value_wpopi_step_body_trace) = S ((S (wpo_old_index_wpopi_step_body_trace)) * d)) /\ exists wpo_beta_quotient_wpopi_step_body_trace_new_entry. z = wpo_beta_quotient_wpopi_step_body_trace_new_entry * S ((S (wpo_old_index_wpopi_step_body_trace)) * d) + (wpo_old_value_wpopi_step_body_trace))))))) /\ ((exists wpo_gap_wpopi_step_body_source_bound. wpo_gap_wpopi_step_body_source_bound + S (i) = n) /\ ((~(i = 0) /\ ~((S i) = n)) /\ ((~(exists wpo_index_wpopi_step_body_source_omit_contains. ((exists wpo_gap_wpopi_step_body_source_omit_contains_bound. wpo_gap_wpopi_step_body_source_omit_contains_bound + S (wpo_index_wpopi_step_body_source_omit_contains) = (m + m)) /\ (((exists wpo_beta_height_wpopi_step_body_source_omit_contains_entry. wpo_beta_height_wpopi_step_body_source_omit_contains_entry + S (i) = S ((S (wpo_index_wpopi_step_body_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpopi_step_body_source_omit_contains_entry. b = wpo_beta_quotient_wpopi_step_body_source_omit_contains_entry * S ((S (wpo_index_wpopi_step_body_source_omit_contains)) * c) + (i)))))) /\ ((((exists wpo_beta_height_wpopi_step_body_forward. wpo_beta_height_wpopi_step_body_forward + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_wpopi_step_body_forward. u = wpo_beta_quotient_wpopi_step_body_forward * S ((S (i)) * v) + (j))) /\ ((exists wpo_gap_wpopi_step_body_mate_bound. wpo_gap_wpopi_step_body_mate_bound + S (j) = n) /\ ((~(j = 0) /\ ~((S j) = n)) /\ (~(i = j) /\ ((((exists wpo_beta_height_wpopi_step_body_back. wpo_beta_height_wpopi_step_body_back + S (i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_wpopi_step_body_back. u = wpo_beta_quotient_wpopi_step_body_back * S ((S (j)) * v) + (i))) /\ ((~(exists wpo_index_wpopi_step_body_mate_omit_contains. ((exists wpo_gap_wpopi_step_body_mate_omit_contains_bound. wpo_gap_wpopi_step_body_mate_omit_contains_bound + S (wpo_index_wpopi_step_body_mate_omit_contains) = (m + m)) /\ (((exists wpo_beta_height_wpopi_step_body_mate_omit_contains_entry. wpo_beta_height_wpopi_step_body_mate_omit_contains_entry + S (j) = S ((S (wpo_index_wpopi_step_body_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpopi_step_body_mate_omit_contains_entry. b = wpo_beta_quotient_wpopi_step_body_mate_omit_contains_entry * S ((S (wpo_index_wpopi_step_body_mate_omit_contains)) * c) + (j)))))) /\ ((forall wpo_position_wpopi_step_body_closed_after wpo_source_wpopi_step_body_closed_after wpo_mate_wpopi_step_body_closed_after. (exists wpo_gap_wpopi_step_body_closed_after_position_bound. wpo_gap_wpopi_step_body_closed_after_position_bound + S (wpo_position_wpopi_step_body_closed_after) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_step_body_closed_after_source_entry. wpo_beta_height_wpopi_step_body_closed_after_source_entry + S (wpo_source_wpopi_step_body_closed_after) = S ((S (wpo_position_wpopi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpopi_step_body_closed_after_source_entry. z = wpo_beta_quotient_wpopi_step_body_closed_after_source_entry * S ((S (wpo_position_wpopi_step_body_closed_after)) * d) + (wpo_source_wpopi_step_body_closed_after))) -> (((exists wpo_beta_height_wpopi_step_body_closed_after_inverse_entry. wpo_beta_height_wpopi_step_body_closed_after_inverse_entry + S (wpo_mate_wpopi_step_body_closed_after) = S ((S (wpo_source_wpopi_step_body_closed_after)) * v)) /\ exists wpo_beta_quotient_wpopi_step_body_closed_after_inverse_entry. u = wpo_beta_quotient_wpopi_step_body_closed_after_inverse_entry * S ((S (wpo_source_wpopi_step_body_closed_after)) * v) + (wpo_mate_wpopi_step_body_closed_after))) -> exists wpo_mate_position_wpopi_step_body_closed_after. ((exists wpo_gap_wpopi_step_body_closed_after_mate_bound. wpo_gap_wpopi_step_body_closed_after_mate_bound + S (wpo_mate_position_wpopi_step_body_closed_after) = S (S (m + m))) /\ (((exists wpo_beta_height_wpopi_step_body_closed_after_mate_entry. wpo_beta_height_wpopi_step_body_closed_after_mate_entry + S (wpo_mate_wpopi_step_body_closed_after) = S ((S (wpo_mate_position_wpopi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpopi_step_body_closed_after_mate_entry. z = wpo_beta_quotient_wpopi_step_body_closed_after_mate_entry * S ((S (wpo_mate_position_wpopi_step_body_closed_after)) * d) + (wpo_mate_wpopi_step_body_closed_after))))) /\ (forall wpo_position_wpopi_step_body_nonendpoint_after wpo_value_wpopi_step_body_nonendpoint_after. (exists wpo_gap_wpopi_step_body_nonendpoint_after_position_bound. wpo_gap_wpopi_step_body_nonendpoint_after_position_bound + S (wpo_position_wpopi_step_body_nonendpoint_after) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_step_body_nonendpoint_after_entry. wpo_beta_height_wpopi_step_body_nonendpoint_after_entry + S (wpo_value_wpopi_step_body_nonendpoint_after) = S ((S (wpo_position_wpopi_step_body_nonendpoint_after)) * d)) /\ exists wpo_beta_quotient_wpopi_step_body_nonendpoint_after_entry. z = wpo_beta_quotient_wpopi_step_body_nonendpoint_after_entry * S ((S (wpo_position_wpopi_step_body_nonendpoint_after)) * d) + (wpo_value_wpopi_step_body_nonendpoint_after))) -> (~(wpo_value_wpopi_step_body_nonendpoint_after = 0) /\ ~((S wpo_value_wpopi_step_body_nonendpoint_after) = n))))))))))))))) /\ ((forall fom_index_wpopi_bounded_after. (exists fom_gap_wpopi_bounded_after_index_bound. fom_gap_wpopi_bounded_after_index_bound + S (fom_index_wpopi_bounded_after) = S (S (m + m))) -> exists fom_value_wpopi_bounded_after. ((((exists fom_beta_height_wpopi_bounded_after_entry. fom_beta_height_wpopi_bounded_after_entry + S (fom_value_wpopi_bounded_after) = S ((S (fom_index_wpopi_bounded_after)) * d)) /\ exists fom_beta_quotient_wpopi_bounded_after_entry. z = fom_beta_quotient_wpopi_bounded_after_entry * S ((S (fom_index_wpopi_bounded_after)) * d) + (fom_value_wpopi_bounded_after))) /\ (exists fom_gap_wpopi_bounded_after_value_bound. fom_gap_wpopi_bounded_after_value_bound + S (fom_value_wpopi_bounded_after) = n))) /\ (forall wpo_injective_left_wpopi_injective_after wpo_injective_right_wpopi_injective_after wpo_injective_value_wpopi_injective_after. (exists wpo_gap_wpopi_injective_after_left_bound. wpo_gap_wpopi_injective_after_left_bound + S (wpo_injective_left_wpopi_injective_after) = S (S (m + m))) -> (exists wpo_gap_wpopi_injective_after_right_bound. wpo_gap_wpopi_injective_after_right_bound + S (wpo_injective_right_wpopi_injective_after) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_injective_after_left_entry. wpo_beta_height_wpopi_injective_after_left_entry + S (wpo_injective_value_wpopi_injective_after) = S ((S (wpo_injective_left_wpopi_injective_after)) * d)) /\ exists wpo_beta_quotient_wpopi_injective_after_left_entry. z = wpo_beta_quotient_wpopi_injective_after_left_entry * S ((S (wpo_injective_left_wpopi_injective_after)) * d) + (wpo_injective_value_wpopi_injective_after))) -> (((exists wpo_beta_height_wpopi_injective_after_right_entry. wpo_beta_height_wpopi_injective_after_right_entry + S (wpo_injective_value_wpopi_injective_after) = S ((S (wpo_injective_right_wpopi_injective_after)) * d)) /\ exists wpo_beta_quotient_wpopi_injective_after_right_entry. z = wpo_beta_quotient_wpopi_injective_after_right_entry * S ((S (wpo_injective_right_wpopi_injective_after)) * d) + (wpo_injective_value_wpopi_injective_after))) -> wpo_injective_left_wpopi_injective_after = wpo_injective_right_wpopi_injective_after)))
  20. 0020specialize prime_pair_order_choose_append_state p
  21. 0021specialize prime_pair_order_choose_append_state n
  22. 0022specialize prime_pair_order_choose_append_state u
  23. 0023specialize prime_pair_order_choose_append_state v
  24. 0024specialize prime_pair_order_choose_append_state b
  25. 0025specialize prime_pair_order_choose_append_state c
  26. 0026specialize prime_pair_order_choose_append_state (m + m)
  27. 0027specialize prime_pair_order_choose_append_state r
  28. 0028apply prime_pair_order_choose_append_state
  29. 0029exact hpn
  30. 0030exact hp
  31. 0031exact hprefix
  32. 0032exact hnr
  33. 0033exact hroom
  34. 0034exact hstate_left
  35. 0035exact hstate_right_left
  36. 0036exact hstate_right_right_left
  37. 0037exact hstate_right_right_right
  38. 0038cases hstep
  39. 0039cases hstep_witness
  40. 0040cases hstep_witness_witness
  41. 0041cases hstep_witness_witness_witness
  42. 0042have hcombined : ((((((((exists wpo_beta_height_wpopi_step_body_x_trace_first. wpo_beta_height_wpopi_step_body_x_trace_first + S (x2) = S ((S ((m + m))) * x1)) /\ exists wpo_beta_quotient_wpopi_step_body_x_trace_first. x = wpo_beta_quotient_wpopi_step_body_x_trace_first * S ((S ((m + m))) * x1) + (x2))) /\ ((((exists wpo_beta_height_wpopi_step_body_x_trace_second. wpo_beta_height_wpopi_step_body_x_trace_second + S (x3) = S ((S (S ((m + m)))) * x1)) /\ exists wpo_beta_quotient_wpopi_step_body_x_trace_second. x = wpo_beta_quotient_wpopi_step_body_x_trace_second * S ((S (S ((m + m)))) * x1) + (x3))) /\ (forall wpo_old_index_wpopi_step_body_x_trace wpo_old_value_wpopi_step_body_x_trace. (exists wpo_gap_wpopi_step_body_x_trace_old_bound. wpo_gap_wpopi_step_body_x_trace_old_bound + S (wpo_old_index_wpopi_step_body_x_trace) = (m + m)) -> (((exists wpo_beta_height_wpopi_step_body_x_trace_old_entry. wpo_beta_height_wpopi_step_body_x_trace_old_entry + S (wpo_old_value_wpopi_step_body_x_trace) = S ((S (wpo_old_index_wpopi_step_body_x_trace)) * c)) /\ exists wpo_beta_quotient_wpopi_step_body_x_trace_old_entry. b = wpo_beta_quotient_wpopi_step_body_x_trace_old_entry * S ((S (wpo_old_index_wpopi_step_body_x_trace)) * c) + (wpo_old_value_wpopi_step_body_x_trace))) -> (((exists wpo_beta_height_wpopi_step_body_x_trace_new_entry. wpo_beta_height_wpopi_step_body_x_trace_new_entry + S (wpo_old_value_wpopi_step_body_x_trace) = S ((S (wpo_old_index_wpopi_step_body_x_trace)) * x1)) /\ exists wpo_beta_quotient_wpopi_step_body_x_trace_new_entry. x = wpo_beta_quotient_wpopi_step_body_x_trace_new_entry * S ((S (wpo_old_index_wpopi_step_body_x_trace)) * x1) + (wpo_old_value_wpopi_step_body_x_trace))))))) /\ ((exists wpo_gap_wpopi_step_body_x_source_bound. wpo_gap_wpopi_step_body_x_source_bound + S (x2) = n) /\ ((~(x2 = 0) /\ ~((S x2) = n)) /\ ((~(exists wpo_index_wpopi_step_body_x_source_omit_contains. ((exists wpo_gap_wpopi_step_body_x_source_omit_contains_bound. wpo_gap_wpopi_step_body_x_source_omit_contains_bound + S (wpo_index_wpopi_step_body_x_source_omit_contains) = (m + m)) /\ (((exists wpo_beta_height_wpopi_step_body_x_source_omit_contains_entry. wpo_beta_height_wpopi_step_body_x_source_omit_contains_entry + S (x2) = S ((S (wpo_index_wpopi_step_body_x_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpopi_step_body_x_source_omit_contains_entry. b = wpo_beta_quotient_wpopi_step_body_x_source_omit_contains_entry * S ((S (wpo_index_wpopi_step_body_x_source_omit_contains)) * c) + (x2)))))) /\ ((((exists wpo_beta_height_wpopi_step_body_x_forward. wpo_beta_height_wpopi_step_body_x_forward + S (x3) = S ((S (x2)) * v)) /\ exists wpo_beta_quotient_wpopi_step_body_x_forward. u = wpo_beta_quotient_wpopi_step_body_x_forward * S ((S (x2)) * v) + (x3))) /\ ((exists wpo_gap_wpopi_step_body_x_mate_bound. wpo_gap_wpopi_step_body_x_mate_bound + S (x3) = n) /\ ((~(x3 = 0) /\ ~((S x3) = n)) /\ (~(x2 = x3) /\ ((((exists wpo_beta_height_wpopi_step_body_x_back. wpo_beta_height_wpopi_step_body_x_back + S (x2) = S ((S (x3)) * v)) /\ exists wpo_beta_quotient_wpopi_step_body_x_back. u = wpo_beta_quotient_wpopi_step_body_x_back * S ((S (x3)) * v) + (x2))) /\ ((~(exists wpo_index_wpopi_step_body_x_mate_omit_contains. ((exists wpo_gap_wpopi_step_body_x_mate_omit_contains_bound. wpo_gap_wpopi_step_body_x_mate_omit_contains_bound + S (wpo_index_wpopi_step_body_x_mate_omit_contains) = (m + m)) /\ (((exists wpo_beta_height_wpopi_step_body_x_mate_omit_contains_entry. wpo_beta_height_wpopi_step_body_x_mate_omit_contains_entry + S (x3) = S ((S (wpo_index_wpopi_step_body_x_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpopi_step_body_x_mate_omit_contains_entry. b = wpo_beta_quotient_wpopi_step_body_x_mate_omit_contains_entry * S ((S (wpo_index_wpopi_step_body_x_mate_omit_contains)) * c) + (x3)))))) /\ ((forall wpo_position_wpopi_step_body_x_closed_after wpo_source_wpopi_step_body_x_closed_after wpo_mate_wpopi_step_body_x_closed_after. (exists wpo_gap_wpopi_step_body_x_closed_after_position_bound. wpo_gap_wpopi_step_body_x_closed_after_position_bound + S (wpo_position_wpopi_step_body_x_closed_after) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_step_body_x_closed_after_source_entry. wpo_beta_height_wpopi_step_body_x_closed_after_source_entry + S (wpo_source_wpopi_step_body_x_closed_after) = S ((S (wpo_position_wpopi_step_body_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_wpopi_step_body_x_closed_after_source_entry. x = wpo_beta_quotient_wpopi_step_body_x_closed_after_source_entry * S ((S (wpo_position_wpopi_step_body_x_closed_after)) * x1) + (wpo_source_wpopi_step_body_x_closed_after))) -> (((exists wpo_beta_height_wpopi_step_body_x_closed_after_inverse_entry. wpo_beta_height_wpopi_step_body_x_closed_after_inverse_entry + S (wpo_mate_wpopi_step_body_x_closed_after) = S ((S (wpo_source_wpopi_step_body_x_closed_after)) * v)) /\ exists wpo_beta_quotient_wpopi_step_body_x_closed_after_inverse_entry. u = wpo_beta_quotient_wpopi_step_body_x_closed_after_inverse_entry * S ((S (wpo_source_wpopi_step_body_x_closed_after)) * v) + (wpo_mate_wpopi_step_body_x_closed_after))) -> exists wpo_mate_position_wpopi_step_body_x_closed_after. ((exists wpo_gap_wpopi_step_body_x_closed_after_mate_bound. wpo_gap_wpopi_step_body_x_closed_after_mate_bound + S (wpo_mate_position_wpopi_step_body_x_closed_after) = S (S (m + m))) /\ (((exists wpo_beta_height_wpopi_step_body_x_closed_after_mate_entry. wpo_beta_height_wpopi_step_body_x_closed_after_mate_entry + S (wpo_mate_wpopi_step_body_x_closed_after) = S ((S (wpo_mate_position_wpopi_step_body_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_wpopi_step_body_x_closed_after_mate_entry. x = wpo_beta_quotient_wpopi_step_body_x_closed_after_mate_entry * S ((S (wpo_mate_position_wpopi_step_body_x_closed_after)) * x1) + (wpo_mate_wpopi_step_body_x_closed_after))))) /\ (forall wpo_position_wpopi_step_body_x_nonendpoint_after wpo_value_wpopi_step_body_x_nonendpoint_after. (exists wpo_gap_wpopi_step_body_x_nonendpoint_after_position_bound. wpo_gap_wpopi_step_body_x_nonendpoint_after_position_bound + S (wpo_position_wpopi_step_body_x_nonendpoint_after) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_step_body_x_nonendpoint_after_entry. wpo_beta_height_wpopi_step_body_x_nonendpoint_after_entry + S (wpo_value_wpopi_step_body_x_nonendpoint_after) = S ((S (wpo_position_wpopi_step_body_x_nonendpoint_after)) * x1)) /\ exists wpo_beta_quotient_wpopi_step_body_x_nonendpoint_after_entry. x = wpo_beta_quotient_wpopi_step_body_x_nonendpoint_after_entry * S ((S (wpo_position_wpopi_step_body_x_nonendpoint_after)) * x1) + (wpo_value_wpopi_step_body_x_nonendpoint_after))) -> (~(wpo_value_wpopi_step_body_x_nonendpoint_after = 0) /\ ~((S wpo_value_wpopi_step_body_x_nonendpoint_after) = n))))))))))))))) /\ ((forall fom_index_wpopi_bounded_after_x. (exists fom_gap_wpopi_bounded_after_x_index_bound. fom_gap_wpopi_bounded_after_x_index_bound + S (fom_index_wpopi_bounded_after_x) = S (S (m + m))) -> exists fom_value_wpopi_bounded_after_x. ((((exists fom_beta_height_wpopi_bounded_after_x_entry. fom_beta_height_wpopi_bounded_after_x_entry + S (fom_value_wpopi_bounded_after_x) = S ((S (fom_index_wpopi_bounded_after_x)) * x1)) /\ exists fom_beta_quotient_wpopi_bounded_after_x_entry. x = fom_beta_quotient_wpopi_bounded_after_x_entry * S ((S (fom_index_wpopi_bounded_after_x)) * x1) + (fom_value_wpopi_bounded_after_x))) /\ (exists fom_gap_wpopi_bounded_after_x_value_bound. fom_gap_wpopi_bounded_after_x_value_bound + S (fom_value_wpopi_bounded_after_x) = n))) /\ (forall wpo_injective_left_wpopi_injective_after_x wpo_injective_right_wpopi_injective_after_x wpo_injective_value_wpopi_injective_after_x. (exists wpo_gap_wpopi_injective_after_x_left_bound. wpo_gap_wpopi_injective_after_x_left_bound + S (wpo_injective_left_wpopi_injective_after_x) = S (S (m + m))) -> (exists wpo_gap_wpopi_injective_after_x_right_bound. wpo_gap_wpopi_injective_after_x_right_bound + S (wpo_injective_right_wpopi_injective_after_x) = S (S (m + m))) -> (((exists wpo_beta_height_wpopi_injective_after_x_left_entry. wpo_beta_height_wpopi_injective_after_x_left_entry + S (wpo_injective_value_wpopi_injective_after_x) = S ((S (wpo_injective_left_wpopi_injective_after_x)) * x1)) /\ exists wpo_beta_quotient_wpopi_injective_after_x_left_entry. x = wpo_beta_quotient_wpopi_injective_after_x_left_entry * S ((S (wpo_injective_left_wpopi_injective_after_x)) * x1) + (wpo_injective_value_wpopi_injective_after_x))) -> (((exists wpo_beta_height_wpopi_injective_after_x_right_entry. wpo_beta_height_wpopi_injective_after_x_right_entry + S (wpo_injective_value_wpopi_injective_after_x) = S ((S (wpo_injective_right_wpopi_injective_after_x)) * x1)) /\ exists wpo_beta_quotient_wpopi_injective_after_x_right_entry. x = wpo_beta_quotient_wpopi_injective_after_x_right_entry * S ((S (wpo_injective_right_wpopi_injective_after_x)) * x1) + (wpo_injective_value_wpopi_injective_after_x))) -> wpo_injective_left_wpopi_injective_after_x = wpo_injective_right_wpopi_injective_after_x)))
  43. 0043exact hstep_witness_witness_witness_witness
  44. 0044cases hcombined
  45. 0045cases hcombined_right
  46. 0046cases hcombined_left
  47. 0047cases hcombined_left_right
  48. 0048cases hcombined_left_right_right
  49. 0049cases hcombined_left_right_right_right
  50. 0050cases hcombined_left_right_right_right_right
  51. 0051cases hcombined_left_right_right_right_right_right
  52. 0052cases hcombined_left_right_right_right_right_right_right
  53. 0053cases hcombined_left_right_right_right_right_right_right_right
  54. 0054cases hcombined_left_right_right_right_right_right_right_right_right
  55. 0055cases hcombined_left_right_right_right_right_right_right_right_right_right
  56. 0056cases hcombined_left_right_right_right_right_right_right_right_right_right_right
  57. 0057have hnew_history : forall wpop_pair_wpopi_new_history_x. (exists wpo_gap_wpopi_new_history_x_pair_bound. wpo_gap_wpopi_new_history_x_pair_bound + S (wpop_pair_wpopi_new_history_x) = S m) -> exists wpop_left_wpopi_new_history_x wpop_right_wpopi_new_history_x. ((((exists wpo_beta_height_wpopi_new_history_x_left_entry. wpo_beta_height_wpopi_new_history_x_left_entry + S (wpop_left_wpopi_new_history_x) = S ((S (wpop_pair_wpopi_new_history_x + wpop_pair_wpopi_new_history_x)) * x1)) /\ exists wpo_beta_quotient_wpopi_new_history_x_left_entry. x = wpo_beta_quotient_wpopi_new_history_x_left_entry * S ((S (wpop_pair_wpopi_new_history_x + wpop_pair_wpopi_new_history_x)) * x1) + (wpop_left_wpopi_new_history_x))) /\ ((((exists wpo_beta_height_wpopi_new_history_x_right_entry. wpo_beta_height_wpopi_new_history_x_right_entry + S (wpop_right_wpopi_new_history_x) = S ((S (S (wpop_pair_wpopi_new_history_x + wpop_pair_wpopi_new_history_x))) * x1)) /\ exists wpo_beta_quotient_wpopi_new_history_x_right_entry. x = wpo_beta_quotient_wpopi_new_history_x_right_entry * S ((S (S (wpop_pair_wpopi_new_history_x + wpop_pair_wpopi_new_history_x))) * x1) + (wpop_right_wpopi_new_history_x))) /\ (((exists wpo_beta_height_wpopi_new_history_x_inverse_entry. wpo_beta_height_wpopi_new_history_x_inverse_entry + S (wpop_right_wpopi_new_history_x) = S ((S (wpop_left_wpopi_new_history_x)) * v)) /\ exists wpo_beta_quotient_wpopi_new_history_x_inverse_entry. u = wpo_beta_quotient_wpopi_new_history_x_inverse_entry * S ((S (wpop_left_wpopi_new_history_x)) * v) + (wpop_right_wpopi_new_history_x)))))
  58. 0058specialize paired_inverse_witness_append u
  59. 0059specialize paired_inverse_witness_append v
  60. 0060specialize paired_inverse_witness_append b
  61. 0061specialize paired_inverse_witness_append c
  62. 0062specialize paired_inverse_witness_append x
  63. 0063specialize paired_inverse_witness_append x1
  64. 0064specialize paired_inverse_witness_append m
  65. 0065specialize paired_inverse_witness_append x2
  66. 0066specialize paired_inverse_witness_append x3
  67. 0067apply paired_inverse_witness_append
  68. 0068exact hhistory
  69. 0069exact hcombined_left_left
  70. 0070exact hcombined_left_right_right_right_right_left
  71. 0071exists x
  72. 0072exists x1
  73. 0073split
  74. 0074split
  75. 0075exact hcombined_left_right_right_right_right_right_right_right_right_right_right_left
  76. 0076split
  77. 0077exact hcombined_right_left
  78. 0078split
  79. 0079exact hcombined_left_right_right_right_right_right_right_right_right_right_right_right
  80. 0080exact hcombined_right_right
  81. 0081exact hnew_history