PA00AW

prime_pair_order_choose_append_injective

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

Thread decoded-prefix injectivity through one constructive fresh-orbit append.

Exact expanded PA statement

forall p n u v b c l r. p = S n -> ((~(p = 1) /\ forall wip_prime_left_wpoi_step_prime wip_prime_right_wpoi_step_prime. p = wip_prime_left_wpoi_step_prime * wip_prime_right_wpoi_step_prime -> wip_prime_left_wpoi_step_prime = 1 \/ wip_prime_right_wpoi_step_prime = 1)) -> (forall wip_index_wpoi_step_inverse. (exists wip_gap_wpoi_step_inverse_prefix_bound. wip_gap_wpoi_step_inverse_prefix_bound + S wip_index_wpoi_step_inverse = n) -> exists wip_mate_wpoi_step_inverse. ((((exists wip_beta_height_wpoi_step_inverse_decoded. wip_beta_height_wpoi_step_inverse_decoded + S (wip_mate_wpoi_step_inverse) = S ((S (wip_index_wpoi_step_inverse)) * v)) /\ exists wip_beta_quotient_wpoi_step_inverse_decoded. u = wip_beta_quotient_wpoi_step_inverse_decoded * S ((S (wip_index_wpoi_step_inverse)) * v) + (wip_mate_wpoi_step_inverse))) /\ ((exists wip_gap_wpoi_step_inverse_inverse_index_bound. wip_gap_wpoi_step_inverse_inverse_index_bound + S wip_index_wpoi_step_inverse = n) /\ ((exists wip_gap_wpoi_step_inverse_inverse_mate_bound. wip_gap_wpoi_step_inverse_inverse_mate_bound + S wip_mate_wpoi_step_inverse = n) /\ (exists wip_mod_left_wpoi_step_inverse_inverse_mod wip_mod_right_wpoi_step_inverse_inverse_mod. ((S wip_index_wpoi_step_inverse) * S wip_mate_wpoi_step_inverse) + p * wip_mod_left_wpoi_step_inverse_inverse_mod = 1 + p * wip_mod_right_wpoi_step_inverse_inverse_mod))))) -> n = S r -> (exists h. h + S (S (S l)) = n) -> (forall wpo_position_wpoi_step_closed_before wpo_source_wpoi_step_closed_before wpo_mate_wpoi_step_closed_before. (exists wpo_gap_wpoi_step_closed_before_position_bound. wpo_gap_wpoi_step_closed_before_position_bound + S (wpo_position_wpoi_step_closed_before) = l) -> (((exists wpo_beta_height_wpoi_step_closed_before_source_entry. wpo_beta_height_wpoi_step_closed_before_source_entry + S (wpo_source_wpoi_step_closed_before) = S ((S (wpo_position_wpoi_step_closed_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_closed_before_source_entry. b = wpo_beta_quotient_wpoi_step_closed_before_source_entry * S ((S (wpo_position_wpoi_step_closed_before)) * c) + (wpo_source_wpoi_step_closed_before))) -> (((exists wpo_beta_height_wpoi_step_closed_before_inverse_entry. wpo_beta_height_wpoi_step_closed_before_inverse_entry + S (wpo_mate_wpoi_step_closed_before) = S ((S (wpo_source_wpoi_step_closed_before)) * v)) /\ exists wpo_beta_quotient_wpoi_step_closed_before_inverse_entry. u = wpo_beta_quotient_wpoi_step_closed_before_inverse_entry * S ((S (wpo_source_wpoi_step_closed_before)) * v) + (wpo_mate_wpoi_step_closed_before))) -> exists wpo_mate_position_wpoi_step_closed_before. ((exists wpo_gap_wpoi_step_closed_before_mate_bound. wpo_gap_wpoi_step_closed_before_mate_bound + S (wpo_mate_position_wpoi_step_closed_before) = l) /\ (((exists wpo_beta_height_wpoi_step_closed_before_mate_entry. wpo_beta_height_wpoi_step_closed_before_mate_entry + S (wpo_mate_wpoi_step_closed_before) = S ((S (wpo_mate_position_wpoi_step_closed_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_closed_before_mate_entry. b = wpo_beta_quotient_wpoi_step_closed_before_mate_entry * S ((S (wpo_mate_position_wpoi_step_closed_before)) * c) + (wpo_mate_wpoi_step_closed_before))))) -> (forall wpo_position_wpoi_step_nonendpoint_before wpo_value_wpoi_step_nonendpoint_before. (exists wpo_gap_wpoi_step_nonendpoint_before_position_bound. wpo_gap_wpoi_step_nonendpoint_before_position_bound + S (wpo_position_wpoi_step_nonendpoint_before) = l) -> (((exists wpo_beta_height_wpoi_step_nonendpoint_before_entry. wpo_beta_height_wpoi_step_nonendpoint_before_entry + S (wpo_value_wpoi_step_nonendpoint_before) = S ((S (wpo_position_wpoi_step_nonendpoint_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_nonendpoint_before_entry. b = wpo_beta_quotient_wpoi_step_nonendpoint_before_entry * S ((S (wpo_position_wpoi_step_nonendpoint_before)) * c) + (wpo_value_wpoi_step_nonendpoint_before))) -> (~(wpo_value_wpoi_step_nonendpoint_before = 0) /\ ~((S wpo_value_wpoi_step_nonendpoint_before) = n))) -> (forall wpo_injective_left_wpoi_step_injective_before wpo_injective_right_wpoi_step_injective_before wpo_injective_value_wpoi_step_injective_before. (exists wpo_gap_wpoi_step_injective_before_left_bound. wpo_gap_wpoi_step_injective_before_left_bound + S (wpo_injective_left_wpoi_step_injective_before) = l) -> (exists wpo_gap_wpoi_step_injective_before_right_bound. wpo_gap_wpoi_step_injective_before_right_bound + S (wpo_injective_right_wpoi_step_injective_before) = l) -> (((exists wpo_beta_height_wpoi_step_injective_before_left_entry. wpo_beta_height_wpoi_step_injective_before_left_entry + S (wpo_injective_value_wpoi_step_injective_before) = S ((S (wpo_injective_left_wpoi_step_injective_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_injective_before_left_entry. b = wpo_beta_quotient_wpoi_step_injective_before_left_entry * S ((S (wpo_injective_left_wpoi_step_injective_before)) * c) + (wpo_injective_value_wpoi_step_injective_before))) -> (((exists wpo_beta_height_wpoi_step_injective_before_right_entry. wpo_beta_height_wpoi_step_injective_before_right_entry + S (wpo_injective_value_wpoi_step_injective_before) = S ((S (wpo_injective_right_wpoi_step_injective_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_injective_before_right_entry. b = wpo_beta_quotient_wpoi_step_injective_before_right_entry * S ((S (wpo_injective_right_wpoi_step_injective_before)) * c) + (wpo_injective_value_wpoi_step_injective_before))) -> wpo_injective_left_wpoi_step_injective_before = wpo_injective_right_wpoi_step_injective_before) -> (exists z d i j. ((((((((exists wpo_beta_height_wpoi_step_body_trace_first. wpo_beta_height_wpoi_step_body_trace_first + S (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_first. z = wpo_beta_quotient_wpoi_step_body_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_wpoi_step_body_trace_second. wpo_beta_height_wpoi_step_body_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_second. z = wpo_beta_quotient_wpoi_step_body_trace_second * S ((S (S (l))) * d) + (j))) /\ (forall wpo_old_index_wpoi_step_body_trace wpo_old_value_wpoi_step_body_trace. (exists wpo_gap_wpoi_step_body_trace_old_bound. wpo_gap_wpoi_step_body_trace_old_bound + S (wpo_old_index_wpoi_step_body_trace) = l) -> (((exists wpo_beta_height_wpoi_step_body_trace_old_entry. wpo_beta_height_wpoi_step_body_trace_old_entry + S (wpo_old_value_wpoi_step_body_trace) = S ((S (wpo_old_index_wpoi_step_body_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_old_entry. b = wpo_beta_quotient_wpoi_step_body_trace_old_entry * S ((S (wpo_old_index_wpoi_step_body_trace)) * c) + (wpo_old_value_wpoi_step_body_trace))) -> (((exists wpo_beta_height_wpoi_step_body_trace_new_entry. wpo_beta_height_wpoi_step_body_trace_new_entry + S (wpo_old_value_wpoi_step_body_trace) = S ((S (wpo_old_index_wpoi_step_body_trace)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_new_entry. z = wpo_beta_quotient_wpoi_step_body_trace_new_entry * S ((S (wpo_old_index_wpoi_step_body_trace)) * d) + (wpo_old_value_wpoi_step_body_trace))))))) /\ ((exists wpo_gap_wpoi_step_body_source_bound. wpo_gap_wpoi_step_body_source_bound + S (i) = n) /\ ((~(i = 0) /\ ~((S i) = n)) /\ ((~(exists wpo_index_wpoi_step_body_source_omit_contains. ((exists wpo_gap_wpoi_step_body_source_omit_contains_bound. wpo_gap_wpoi_step_body_source_omit_contains_bound + S (wpo_index_wpoi_step_body_source_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_source_omit_contains_entry. wpo_beta_height_wpoi_step_body_source_omit_contains_entry + S (i) = S ((S (wpo_index_wpoi_step_body_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_source_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_source_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_source_omit_contains)) * c) + (i)))))) /\ ((((exists wpo_beta_height_wpoi_step_body_forward. wpo_beta_height_wpoi_step_body_forward + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_forward. u = wpo_beta_quotient_wpoi_step_body_forward * S ((S (i)) * v) + (j))) /\ ((exists wpo_gap_wpoi_step_body_mate_bound. wpo_gap_wpoi_step_body_mate_bound + S (j) = n) /\ ((~(j = 0) /\ ~((S j) = n)) /\ (~(i = j) /\ ((((exists wpo_beta_height_wpoi_step_body_back. wpo_beta_height_wpoi_step_body_back + S (i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_back. u = wpo_beta_quotient_wpoi_step_body_back * S ((S (j)) * v) + (i))) /\ ((~(exists wpo_index_wpoi_step_body_mate_omit_contains. ((exists wpo_gap_wpoi_step_body_mate_omit_contains_bound. wpo_gap_wpoi_step_body_mate_omit_contains_bound + S (wpo_index_wpoi_step_body_mate_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_mate_omit_contains_entry. wpo_beta_height_wpoi_step_body_mate_omit_contains_entry + S (j) = S ((S (wpo_index_wpoi_step_body_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_mate_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_mate_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_mate_omit_contains)) * c) + (j)))))) /\ ((forall wpo_position_wpoi_step_body_closed_after wpo_source_wpoi_step_body_closed_after wpo_mate_wpoi_step_body_closed_after. (exists wpo_gap_wpoi_step_body_closed_after_position_bound. wpo_gap_wpoi_step_body_closed_after_position_bound + S (wpo_position_wpoi_step_body_closed_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_closed_after_source_entry. wpo_beta_height_wpoi_step_body_closed_after_source_entry + S (wpo_source_wpoi_step_body_closed_after) = S ((S (wpo_position_wpoi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_source_entry. z = wpo_beta_quotient_wpoi_step_body_closed_after_source_entry * S ((S (wpo_position_wpoi_step_body_closed_after)) * d) + (wpo_source_wpoi_step_body_closed_after))) -> (((exists wpo_beta_height_wpoi_step_body_closed_after_inverse_entry. wpo_beta_height_wpoi_step_body_closed_after_inverse_entry + S (wpo_mate_wpoi_step_body_closed_after) = S ((S (wpo_source_wpoi_step_body_closed_after)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_inverse_entry. u = wpo_beta_quotient_wpoi_step_body_closed_after_inverse_entry * S ((S (wpo_source_wpoi_step_body_closed_after)) * v) + (wpo_mate_wpoi_step_body_closed_after))) -> exists wpo_mate_position_wpoi_step_body_closed_after. ((exists wpo_gap_wpoi_step_body_closed_after_mate_bound. wpo_gap_wpoi_step_body_closed_after_mate_bound + S (wpo_mate_position_wpoi_step_body_closed_after) = S (S l)) /\ (((exists wpo_beta_height_wpoi_step_body_closed_after_mate_entry. wpo_beta_height_wpoi_step_body_closed_after_mate_entry + S (wpo_mate_wpoi_step_body_closed_after) = S ((S (wpo_mate_position_wpoi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_mate_entry. z = wpo_beta_quotient_wpoi_step_body_closed_after_mate_entry * S ((S (wpo_mate_position_wpoi_step_body_closed_after)) * d) + (wpo_mate_wpoi_step_body_closed_after))))) /\ (forall wpo_position_wpoi_step_body_nonendpoint_after wpo_value_wpoi_step_body_nonendpoint_after. (exists wpo_gap_wpoi_step_body_nonendpoint_after_position_bound. wpo_gap_wpoi_step_body_nonendpoint_after_position_bound + S (wpo_position_wpoi_step_body_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_nonendpoint_after_entry. wpo_beta_height_wpoi_step_body_nonendpoint_after_entry + S (wpo_value_wpoi_step_body_nonendpoint_after) = S ((S (wpo_position_wpoi_step_body_nonendpoint_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_nonendpoint_after_entry. z = wpo_beta_quotient_wpoi_step_body_nonendpoint_after_entry * S ((S (wpo_position_wpoi_step_body_nonendpoint_after)) * d) + (wpo_value_wpoi_step_body_nonendpoint_after))) -> (~(wpo_value_wpoi_step_body_nonendpoint_after = 0) /\ ~((S wpo_value_wpoi_step_body_nonendpoint_after) = n))))))))))))))) /\ (forall wpo_injective_left_wpoi_step_injective_after wpo_injective_right_wpoi_step_injective_after wpo_injective_value_wpoi_step_injective_after. (exists wpo_gap_wpoi_step_injective_after_left_bound. wpo_gap_wpoi_step_injective_after_left_bound + S (wpo_injective_left_wpoi_step_injective_after) = S (S l)) -> (exists wpo_gap_wpoi_step_injective_after_right_bound. wpo_gap_wpoi_step_injective_after_right_bound + S (wpo_injective_right_wpoi_step_injective_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_injective_after_left_entry. wpo_beta_height_wpoi_step_injective_after_left_entry + S (wpo_injective_value_wpoi_step_injective_after) = S ((S (wpo_injective_left_wpoi_step_injective_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_left_entry. z = wpo_beta_quotient_wpoi_step_injective_after_left_entry * S ((S (wpo_injective_left_wpoi_step_injective_after)) * d) + (wpo_injective_value_wpoi_step_injective_after))) -> (((exists wpo_beta_height_wpoi_step_injective_after_right_entry. wpo_beta_height_wpoi_step_injective_after_right_entry + S (wpo_injective_value_wpoi_step_injective_after) = S ((S (wpo_injective_right_wpoi_step_injective_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_right_entry. z = wpo_beta_quotient_wpoi_step_injective_after_right_entry * S ((S (wpo_injective_right_wpoi_step_injective_after)) * d) + (wpo_injective_value_wpoi_step_injective_after))) -> wpo_injective_left_wpoi_step_injective_after = wpo_injective_right_wpoi_step_injective_after)))

Structural proof guide

Generated structural guide

Thread decoded-prefix injectivity through one constructive fresh-orbit append.

Use the direct prerequisites prime_pair_order_choose_append, beta_prefix_append_two_injective as previously established PA formulas.

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

Referenced ingredients

PA00AV prime_pair_order_choose_append PA009N beta_prefix_append_two_injective

Proof neighborhood

Direct dependencies

PA00AV prime_pair_order_choose_append PA009N beta_prefix_append_two_injective

Direct dependents

PA00AX prime_pair_order_choose_append_state

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 l
  8. 0008intro r
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hprefix
  12. 0012intro hnr
  13. 0013intro hshort
  14. 0014intro hclosed
  15. 0015intro hnonendpoint
  16. 0016intro hinjective
  17. 0017have hstep : exists z d i j. (((((((exists wpo_beta_height_wpoi_step_body_trace_first. wpo_beta_height_wpoi_step_body_trace_first + S (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_first. z = wpo_beta_quotient_wpoi_step_body_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_wpoi_step_body_trace_second. wpo_beta_height_wpoi_step_body_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_second. z = wpo_beta_quotient_wpoi_step_body_trace_second * S ((S (S (l))) * d) + (j))) /\ (forall wpo_old_index_wpoi_step_body_trace wpo_old_value_wpoi_step_body_trace. (exists wpo_gap_wpoi_step_body_trace_old_bound. wpo_gap_wpoi_step_body_trace_old_bound + S (wpo_old_index_wpoi_step_body_trace) = l) -> (((exists wpo_beta_height_wpoi_step_body_trace_old_entry. wpo_beta_height_wpoi_step_body_trace_old_entry + S (wpo_old_value_wpoi_step_body_trace) = S ((S (wpo_old_index_wpoi_step_body_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_old_entry. b = wpo_beta_quotient_wpoi_step_body_trace_old_entry * S ((S (wpo_old_index_wpoi_step_body_trace)) * c) + (wpo_old_value_wpoi_step_body_trace))) -> (((exists wpo_beta_height_wpoi_step_body_trace_new_entry. wpo_beta_height_wpoi_step_body_trace_new_entry + S (wpo_old_value_wpoi_step_body_trace) = S ((S (wpo_old_index_wpoi_step_body_trace)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_new_entry. z = wpo_beta_quotient_wpoi_step_body_trace_new_entry * S ((S (wpo_old_index_wpoi_step_body_trace)) * d) + (wpo_old_value_wpoi_step_body_trace))))))) /\ ((exists wpo_gap_wpoi_step_body_source_bound. wpo_gap_wpoi_step_body_source_bound + S (i) = n) /\ ((~(i = 0) /\ ~((S i) = n)) /\ ((~(exists wpo_index_wpoi_step_body_source_omit_contains. ((exists wpo_gap_wpoi_step_body_source_omit_contains_bound. wpo_gap_wpoi_step_body_source_omit_contains_bound + S (wpo_index_wpoi_step_body_source_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_source_omit_contains_entry. wpo_beta_height_wpoi_step_body_source_omit_contains_entry + S (i) = S ((S (wpo_index_wpoi_step_body_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_source_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_source_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_source_omit_contains)) * c) + (i)))))) /\ ((((exists wpo_beta_height_wpoi_step_body_forward. wpo_beta_height_wpoi_step_body_forward + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_forward. u = wpo_beta_quotient_wpoi_step_body_forward * S ((S (i)) * v) + (j))) /\ ((exists wpo_gap_wpoi_step_body_mate_bound. wpo_gap_wpoi_step_body_mate_bound + S (j) = n) /\ ((~(j = 0) /\ ~((S j) = n)) /\ (~(i = j) /\ ((((exists wpo_beta_height_wpoi_step_body_back. wpo_beta_height_wpoi_step_body_back + S (i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_back. u = wpo_beta_quotient_wpoi_step_body_back * S ((S (j)) * v) + (i))) /\ ((~(exists wpo_index_wpoi_step_body_mate_omit_contains. ((exists wpo_gap_wpoi_step_body_mate_omit_contains_bound. wpo_gap_wpoi_step_body_mate_omit_contains_bound + S (wpo_index_wpoi_step_body_mate_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_mate_omit_contains_entry. wpo_beta_height_wpoi_step_body_mate_omit_contains_entry + S (j) = S ((S (wpo_index_wpoi_step_body_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_mate_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_mate_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_mate_omit_contains)) * c) + (j)))))) /\ ((forall wpo_position_wpoi_step_body_closed_after wpo_source_wpoi_step_body_closed_after wpo_mate_wpoi_step_body_closed_after. (exists wpo_gap_wpoi_step_body_closed_after_position_bound. wpo_gap_wpoi_step_body_closed_after_position_bound + S (wpo_position_wpoi_step_body_closed_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_closed_after_source_entry. wpo_beta_height_wpoi_step_body_closed_after_source_entry + S (wpo_source_wpoi_step_body_closed_after) = S ((S (wpo_position_wpoi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_source_entry. z = wpo_beta_quotient_wpoi_step_body_closed_after_source_entry * S ((S (wpo_position_wpoi_step_body_closed_after)) * d) + (wpo_source_wpoi_step_body_closed_after))) -> (((exists wpo_beta_height_wpoi_step_body_closed_after_inverse_entry. wpo_beta_height_wpoi_step_body_closed_after_inverse_entry + S (wpo_mate_wpoi_step_body_closed_after) = S ((S (wpo_source_wpoi_step_body_closed_after)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_inverse_entry. u = wpo_beta_quotient_wpoi_step_body_closed_after_inverse_entry * S ((S (wpo_source_wpoi_step_body_closed_after)) * v) + (wpo_mate_wpoi_step_body_closed_after))) -> exists wpo_mate_position_wpoi_step_body_closed_after. ((exists wpo_gap_wpoi_step_body_closed_after_mate_bound. wpo_gap_wpoi_step_body_closed_after_mate_bound + S (wpo_mate_position_wpoi_step_body_closed_after) = S (S l)) /\ (((exists wpo_beta_height_wpoi_step_body_closed_after_mate_entry. wpo_beta_height_wpoi_step_body_closed_after_mate_entry + S (wpo_mate_wpoi_step_body_closed_after) = S ((S (wpo_mate_position_wpoi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_mate_entry. z = wpo_beta_quotient_wpoi_step_body_closed_after_mate_entry * S ((S (wpo_mate_position_wpoi_step_body_closed_after)) * d) + (wpo_mate_wpoi_step_body_closed_after))))) /\ (forall wpo_position_wpoi_step_body_nonendpoint_after wpo_value_wpoi_step_body_nonendpoint_after. (exists wpo_gap_wpoi_step_body_nonendpoint_after_position_bound. wpo_gap_wpoi_step_body_nonendpoint_after_position_bound + S (wpo_position_wpoi_step_body_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_nonendpoint_after_entry. wpo_beta_height_wpoi_step_body_nonendpoint_after_entry + S (wpo_value_wpoi_step_body_nonendpoint_after) = S ((S (wpo_position_wpoi_step_body_nonendpoint_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_nonendpoint_after_entry. z = wpo_beta_quotient_wpoi_step_body_nonendpoint_after_entry * S ((S (wpo_position_wpoi_step_body_nonendpoint_after)) * d) + (wpo_value_wpoi_step_body_nonendpoint_after))) -> (~(wpo_value_wpoi_step_body_nonendpoint_after = 0) /\ ~((S wpo_value_wpoi_step_body_nonendpoint_after) = n)))))))))))))))
  18. 0018specialize prime_pair_order_choose_append p
  19. 0019specialize prime_pair_order_choose_append n
  20. 0020specialize prime_pair_order_choose_append u
  21. 0021specialize prime_pair_order_choose_append v
  22. 0022specialize prime_pair_order_choose_append b
  23. 0023specialize prime_pair_order_choose_append c
  24. 0024specialize prime_pair_order_choose_append l
  25. 0025specialize prime_pair_order_choose_append r
  26. 0026apply prime_pair_order_choose_append
  27. 0027exact hpn
  28. 0028exact hp
  29. 0029exact hprefix
  30. 0030exact hnr
  31. 0031exact hshort
  32. 0032exact hclosed
  33. 0033exact hnonendpoint
  34. 0034cases hstep
  35. 0035cases hstep_witness
  36. 0036cases hstep_witness_witness
  37. 0037cases hstep_witness_witness_witness
  38. 0038have hparts : ((((((exists wpo_beta_height_wpoi_step_body_x_trace_first. wpo_beta_height_wpoi_step_body_x_trace_first + S (x2) = S ((S (l)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_first. x = wpo_beta_quotient_wpoi_step_body_x_trace_first * S ((S (l)) * x1) + (x2))) /\ ((((exists wpo_beta_height_wpoi_step_body_x_trace_second. wpo_beta_height_wpoi_step_body_x_trace_second + S (x3) = S ((S (S (l))) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_second. x = wpo_beta_quotient_wpoi_step_body_x_trace_second * S ((S (S (l))) * x1) + (x3))) /\ (forall wpo_old_index_wpoi_step_body_x_trace wpo_old_value_wpoi_step_body_x_trace. (exists wpo_gap_wpoi_step_body_x_trace_old_bound. wpo_gap_wpoi_step_body_x_trace_old_bound + S (wpo_old_index_wpoi_step_body_x_trace) = l) -> (((exists wpo_beta_height_wpoi_step_body_x_trace_old_entry. wpo_beta_height_wpoi_step_body_x_trace_old_entry + S (wpo_old_value_wpoi_step_body_x_trace) = S ((S (wpo_old_index_wpoi_step_body_x_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_old_entry. b = wpo_beta_quotient_wpoi_step_body_x_trace_old_entry * S ((S (wpo_old_index_wpoi_step_body_x_trace)) * c) + (wpo_old_value_wpoi_step_body_x_trace))) -> (((exists wpo_beta_height_wpoi_step_body_x_trace_new_entry. wpo_beta_height_wpoi_step_body_x_trace_new_entry + S (wpo_old_value_wpoi_step_body_x_trace) = S ((S (wpo_old_index_wpoi_step_body_x_trace)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_new_entry. x = wpo_beta_quotient_wpoi_step_body_x_trace_new_entry * S ((S (wpo_old_index_wpoi_step_body_x_trace)) * x1) + (wpo_old_value_wpoi_step_body_x_trace))))))) /\ ((exists wpo_gap_wpoi_step_body_x_source_bound. wpo_gap_wpoi_step_body_x_source_bound + S (x2) = n) /\ ((~(x2 = 0) /\ ~((S x2) = n)) /\ ((~(exists wpo_index_wpoi_step_body_x_source_omit_contains. ((exists wpo_gap_wpoi_step_body_x_source_omit_contains_bound. wpo_gap_wpoi_step_body_x_source_omit_contains_bound + S (wpo_index_wpoi_step_body_x_source_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_x_source_omit_contains_entry. wpo_beta_height_wpoi_step_body_x_source_omit_contains_entry + S (x2) = S ((S (wpo_index_wpoi_step_body_x_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_source_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_x_source_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_x_source_omit_contains)) * c) + (x2)))))) /\ ((((exists wpo_beta_height_wpoi_step_body_x_forward. wpo_beta_height_wpoi_step_body_x_forward + S (x3) = S ((S (x2)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_forward. u = wpo_beta_quotient_wpoi_step_body_x_forward * S ((S (x2)) * v) + (x3))) /\ ((exists wpo_gap_wpoi_step_body_x_mate_bound. wpo_gap_wpoi_step_body_x_mate_bound + S (x3) = n) /\ ((~(x3 = 0) /\ ~((S x3) = n)) /\ (~(x2 = x3) /\ ((((exists wpo_beta_height_wpoi_step_body_x_back. wpo_beta_height_wpoi_step_body_x_back + S (x2) = S ((S (x3)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_back. u = wpo_beta_quotient_wpoi_step_body_x_back * S ((S (x3)) * v) + (x2))) /\ ((~(exists wpo_index_wpoi_step_body_x_mate_omit_contains. ((exists wpo_gap_wpoi_step_body_x_mate_omit_contains_bound. wpo_gap_wpoi_step_body_x_mate_omit_contains_bound + S (wpo_index_wpoi_step_body_x_mate_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_x_mate_omit_contains_entry. wpo_beta_height_wpoi_step_body_x_mate_omit_contains_entry + S (x3) = S ((S (wpo_index_wpoi_step_body_x_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_mate_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_x_mate_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_x_mate_omit_contains)) * c) + (x3)))))) /\ ((forall wpo_position_wpoi_step_body_x_closed_after wpo_source_wpoi_step_body_x_closed_after wpo_mate_wpoi_step_body_x_closed_after. (exists wpo_gap_wpoi_step_body_x_closed_after_position_bound. wpo_gap_wpoi_step_body_x_closed_after_position_bound + S (wpo_position_wpoi_step_body_x_closed_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_x_closed_after_source_entry. wpo_beta_height_wpoi_step_body_x_closed_after_source_entry + S (wpo_source_wpoi_step_body_x_closed_after) = S ((S (wpo_position_wpoi_step_body_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_source_entry. x = wpo_beta_quotient_wpoi_step_body_x_closed_after_source_entry * S ((S (wpo_position_wpoi_step_body_x_closed_after)) * x1) + (wpo_source_wpoi_step_body_x_closed_after))) -> (((exists wpo_beta_height_wpoi_step_body_x_closed_after_inverse_entry. wpo_beta_height_wpoi_step_body_x_closed_after_inverse_entry + S (wpo_mate_wpoi_step_body_x_closed_after) = S ((S (wpo_source_wpoi_step_body_x_closed_after)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_inverse_entry. u = wpo_beta_quotient_wpoi_step_body_x_closed_after_inverse_entry * S ((S (wpo_source_wpoi_step_body_x_closed_after)) * v) + (wpo_mate_wpoi_step_body_x_closed_after))) -> exists wpo_mate_position_wpoi_step_body_x_closed_after. ((exists wpo_gap_wpoi_step_body_x_closed_after_mate_bound. wpo_gap_wpoi_step_body_x_closed_after_mate_bound + S (wpo_mate_position_wpoi_step_body_x_closed_after) = S (S l)) /\ (((exists wpo_beta_height_wpoi_step_body_x_closed_after_mate_entry. wpo_beta_height_wpoi_step_body_x_closed_after_mate_entry + S (wpo_mate_wpoi_step_body_x_closed_after) = S ((S (wpo_mate_position_wpoi_step_body_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_mate_entry. x = wpo_beta_quotient_wpoi_step_body_x_closed_after_mate_entry * S ((S (wpo_mate_position_wpoi_step_body_x_closed_after)) * x1) + (wpo_mate_wpoi_step_body_x_closed_after))))) /\ (forall wpo_position_wpoi_step_body_x_nonendpoint_after wpo_value_wpoi_step_body_x_nonendpoint_after. (exists wpo_gap_wpoi_step_body_x_nonendpoint_after_position_bound. wpo_gap_wpoi_step_body_x_nonendpoint_after_position_bound + S (wpo_position_wpoi_step_body_x_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_x_nonendpoint_after_entry. wpo_beta_height_wpoi_step_body_x_nonendpoint_after_entry + S (wpo_value_wpoi_step_body_x_nonendpoint_after) = S ((S (wpo_position_wpoi_step_body_x_nonendpoint_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_nonendpoint_after_entry. x = wpo_beta_quotient_wpoi_step_body_x_nonendpoint_after_entry * S ((S (wpo_position_wpoi_step_body_x_nonendpoint_after)) * x1) + (wpo_value_wpoi_step_body_x_nonendpoint_after))) -> (~(wpo_value_wpoi_step_body_x_nonendpoint_after = 0) /\ ~((S wpo_value_wpoi_step_body_x_nonendpoint_after) = n))))))))))))))
  39. 0039exact hstep_witness_witness_witness_witness
  40. 0040cases hparts
  41. 0041cases hparts_right
  42. 0042cases hparts_right_right
  43. 0043cases hparts_right_right_right
  44. 0044cases hparts_right_right_right_right
  45. 0045cases hparts_right_right_right_right_right
  46. 0046cases hparts_right_right_right_right_right_right
  47. 0047cases hparts_right_right_right_right_right_right_right
  48. 0048cases hparts_right_right_right_right_right_right_right_right
  49. 0049cases hparts_right_right_right_right_right_right_right_right_right
  50. 0050have hnew_injective : forall wpo_injective_left_wpoi_step_injective_after_x wpo_injective_right_wpoi_step_injective_after_x wpo_injective_value_wpoi_step_injective_after_x. (exists wpo_gap_wpoi_step_injective_after_x_left_bound. wpo_gap_wpoi_step_injective_after_x_left_bound + S (wpo_injective_left_wpoi_step_injective_after_x) = S (S l)) -> (exists wpo_gap_wpoi_step_injective_after_x_right_bound. wpo_gap_wpoi_step_injective_after_x_right_bound + S (wpo_injective_right_wpoi_step_injective_after_x) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_injective_after_x_left_entry. wpo_beta_height_wpoi_step_injective_after_x_left_entry + S (wpo_injective_value_wpoi_step_injective_after_x) = S ((S (wpo_injective_left_wpoi_step_injective_after_x)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_x_left_entry. x = wpo_beta_quotient_wpoi_step_injective_after_x_left_entry * S ((S (wpo_injective_left_wpoi_step_injective_after_x)) * x1) + (wpo_injective_value_wpoi_step_injective_after_x))) -> (((exists wpo_beta_height_wpoi_step_injective_after_x_right_entry. wpo_beta_height_wpoi_step_injective_after_x_right_entry + S (wpo_injective_value_wpoi_step_injective_after_x) = S ((S (wpo_injective_right_wpoi_step_injective_after_x)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_x_right_entry. x = wpo_beta_quotient_wpoi_step_injective_after_x_right_entry * S ((S (wpo_injective_right_wpoi_step_injective_after_x)) * x1) + (wpo_injective_value_wpoi_step_injective_after_x))) -> wpo_injective_left_wpoi_step_injective_after_x = wpo_injective_right_wpoi_step_injective_after_x
  51. 0051specialize beta_prefix_append_two_injective b
  52. 0052specialize beta_prefix_append_two_injective c
  53. 0053specialize beta_prefix_append_two_injective x
  54. 0054specialize beta_prefix_append_two_injective x1
  55. 0055specialize beta_prefix_append_two_injective l
  56. 0056specialize beta_prefix_append_two_injective x2
  57. 0057specialize beta_prefix_append_two_injective x3
  58. 0058apply beta_prefix_append_two_injective
  59. 0059exact hparts_left
  60. 0060exact hinjective
  61. 0061exact hparts_right_right_right_left
  62. 0062exact hparts_right_right_right_right_right_right_right_right_right_left
  63. 0063exact hparts_right_right_right_right_right_right_right_left
  64. 0064exists x
  65. 0065exists x1
  66. 0066exists x2
  67. 0067exists x3
  68. 0068split
  69. 0069exact hstep_witness_witness_witness_witness
  70. 0070exact hnew_injective