PA00AX

prime_pair_order_choose_append_state

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

Thread the complete bounded PairOrder state through one fresh inverse-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 fom_index_wpoi_step_bounded_before. (exists fom_gap_wpoi_step_bounded_before_index_bound. fom_gap_wpoi_step_bounded_before_index_bound + S (fom_index_wpoi_step_bounded_before) = l) -> exists fom_value_wpoi_step_bounded_before. ((((exists fom_beta_height_wpoi_step_bounded_before_entry. fom_beta_height_wpoi_step_bounded_before_entry + S (fom_value_wpoi_step_bounded_before) = S ((S (fom_index_wpoi_step_bounded_before)) * c)) /\ exists fom_beta_quotient_wpoi_step_bounded_before_entry. b = fom_beta_quotient_wpoi_step_bounded_before_entry * S ((S (fom_index_wpoi_step_bounded_before)) * c) + (fom_value_wpoi_step_bounded_before))) /\ (exists fom_gap_wpoi_step_bounded_before_value_bound. fom_gap_wpoi_step_bounded_before_value_bound + S (fom_value_wpoi_step_bounded_before) = n))) -> (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 fom_index_wpoi_step_bounded_after. (exists fom_gap_wpoi_step_bounded_after_index_bound. fom_gap_wpoi_step_bounded_after_index_bound + S (fom_index_wpoi_step_bounded_after) = S (S l)) -> exists fom_value_wpoi_step_bounded_after. ((((exists fom_beta_height_wpoi_step_bounded_after_entry. fom_beta_height_wpoi_step_bounded_after_entry + S (fom_value_wpoi_step_bounded_after) = S ((S (fom_index_wpoi_step_bounded_after)) * d)) /\ exists fom_beta_quotient_wpoi_step_bounded_after_entry. z = fom_beta_quotient_wpoi_step_bounded_after_entry * S ((S (fom_index_wpoi_step_bounded_after)) * d) + (fom_value_wpoi_step_bounded_after))) /\ (exists fom_gap_wpoi_step_bounded_after_value_bound. fom_gap_wpoi_step_bounded_after_value_bound + S (fom_value_wpoi_step_bounded_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 the complete bounded PairOrder state through one fresh inverse-orbit append.

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

The proof proceeds by case analysis (11), intermediate claims (4).

Referenced ingredients

PA00AW prime_pair_order_choose_append_injective PA009P beta_prefix_append_two_bounded_into

Proof neighborhood

Direct dependencies

PA00AW prime_pair_order_choose_append_injective PA009P beta_prefix_append_two_bounded_into

Direct dependents

PA00B0 prime_pair_order_paired_state_step

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 hbounded
  16. 0016intro hnonendpoint
  17. 0017intro hinjective
  18. 0018have 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))))))))))))))) /\ (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))
  19. 0019specialize prime_pair_order_choose_append_injective p
  20. 0020specialize prime_pair_order_choose_append_injective n
  21. 0021specialize prime_pair_order_choose_append_injective u
  22. 0022specialize prime_pair_order_choose_append_injective v
  23. 0023specialize prime_pair_order_choose_append_injective b
  24. 0024specialize prime_pair_order_choose_append_injective c
  25. 0025specialize prime_pair_order_choose_append_injective l
  26. 0026specialize prime_pair_order_choose_append_injective r
  27. 0027apply prime_pair_order_choose_append_injective
  28. 0028exact hpn
  29. 0029exact hp
  30. 0030exact hprefix
  31. 0031exact hnr
  32. 0032exact hshort
  33. 0033exact hclosed
  34. 0034exact hnonendpoint
  35. 0035exact hinjective
  36. 0036cases hstep
  37. 0037cases hstep_witness
  38. 0038cases hstep_witness_witness
  39. 0039cases hstep_witness_witness_witness
  40. 0040have hcombined : ((((((((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))))))))))))))) /\ (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))
  41. 0041exact hstep_witness_witness_witness_witness
  42. 0042cases hcombined
  43. 0043have 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))))))))))))))
  44. 0044exact hcombined_left
  45. 0045cases hparts
  46. 0046cases hparts_right
  47. 0047cases hparts_right_right
  48. 0048cases hparts_right_right_right
  49. 0049cases hparts_right_right_right_right
  50. 0050cases hparts_right_right_right_right_right
  51. 0051have hnew_bounded : forall fom_index_wpoi_step_bounded_after_x. (exists fom_gap_wpoi_step_bounded_after_x_index_bound. fom_gap_wpoi_step_bounded_after_x_index_bound + S (fom_index_wpoi_step_bounded_after_x) = S (S l)) -> exists fom_value_wpoi_step_bounded_after_x. ((((exists fom_beta_height_wpoi_step_bounded_after_x_entry. fom_beta_height_wpoi_step_bounded_after_x_entry + S (fom_value_wpoi_step_bounded_after_x) = S ((S (fom_index_wpoi_step_bounded_after_x)) * x1)) /\ exists fom_beta_quotient_wpoi_step_bounded_after_x_entry. x = fom_beta_quotient_wpoi_step_bounded_after_x_entry * S ((S (fom_index_wpoi_step_bounded_after_x)) * x1) + (fom_value_wpoi_step_bounded_after_x))) /\ (exists fom_gap_wpoi_step_bounded_after_x_value_bound. fom_gap_wpoi_step_bounded_after_x_value_bound + S (fom_value_wpoi_step_bounded_after_x) = n))
  52. 0052specialize beta_prefix_append_two_bounded_into b
  53. 0053specialize beta_prefix_append_two_bounded_into c
  54. 0054specialize beta_prefix_append_two_bounded_into x
  55. 0055specialize beta_prefix_append_two_bounded_into x1
  56. 0056specialize beta_prefix_append_two_bounded_into l
  57. 0057specialize beta_prefix_append_two_bounded_into n
  58. 0058specialize beta_prefix_append_two_bounded_into x2
  59. 0059specialize beta_prefix_append_two_bounded_into x3
  60. 0060apply beta_prefix_append_two_bounded_into
  61. 0061exact hparts_left
  62. 0062exact hbounded
  63. 0063exact hparts_right_left
  64. 0064exact hparts_right_right_right_right_right_left
  65. 0065exists x
  66. 0066exists x1
  67. 0067exists x2
  68. 0068exists x3
  69. 0069split
  70. 0070exact hcombined_left
  71. 0071split
  72. 0072exact hnew_bounded
  73. 0073exact hcombined_right