PA00B2 · theorem

prime_pair_order_paired_terminal_state_exists

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

Specialize the paired iteration to a terminal n-2 prefix with full adjacency history.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ n. ∀ u. ∀ v. ∀ r. ∀ m. p = S n → Prime(p) → InversePrefix(p,n,u,v,n) → n = S r → n = S S (m + m) → ∃ x. ∃ y. (∀ z. ∀ k. ∀ i. Lt(z,m + m) → BetaAt(x,y,z,k) → BetaAt(u,v,k,i) → ContainsPrefix(x,y,m + m,i)) ∧ ((∀ z. Lt(z,m + m) → ∃ k. BetaAt(x,y,z,k) ∧ Lt(k,n)) ∧ ((∀ z. ∀ k. Lt(z,m + m) → BetaAt(x,y,z,k) → ¬k = 0 ∧ ¬S k = n) ∧ InjectivePrefix(x,y,m + m))) ∧ (∀ z. Lt(z,m) → ∃ k. ∃ i. BetaAt(x,y,z + z,k) ∧ (BetaAt(x,y,S (z + z),i) ∧ BetaAt(u,v,k,i)))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0004 Prime PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix PD0037 InversePrefix

16 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

14 occurrences

Exact expanded native-PA statement
forall p n u v r m. 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 -> n = S (S (m + m)) -> (exists b c. ((((forall wpo_position_wpopi_iteration_state_closed wpo_source_wpopi_iteration_state_closed wpo_mate_wpopi_iteration_state_closed. (exists wpo_gap_wpopi_iteration_state_closed_position_bound. wpo_gap_wpopi_iteration_state_closed_position_bound + S (wpo_position_wpopi_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_source_entry. wpo_beta_height_wpopi_iteration_state_closed_source_entry + S (wpo_source_wpopi_iteration_state_closed) = S ((S (wpo_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_source_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_source_entry * S ((S (wpo_position_wpopi_iteration_state_closed)) * c) + (wpo_source_wpopi_iteration_state_closed))) -> (((exists wpo_beta_height_wpopi_iteration_state_closed_inverse_entry. wpo_beta_height_wpopi_iteration_state_closed_inverse_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_source_wpopi_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_state_closed_inverse_entry * S ((S (wpo_source_wpopi_iteration_state_closed)) * v) + (wpo_mate_wpopi_iteration_state_closed))) -> exists wpo_mate_position_wpopi_iteration_state_closed. ((exists wpo_gap_wpopi_iteration_state_closed_mate_bound. wpo_gap_wpopi_iteration_state_closed_mate_bound + S (wpo_mate_position_wpopi_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_wpopi_iteration_state_closed_mate_entry. wpo_beta_height_wpopi_iteration_state_closed_mate_entry + S (wpo_mate_wpopi_iteration_state_closed) = S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_iteration_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_iteration_state_closed)) * c) + (wpo_mate_wpopi_iteration_state_closed))))) /\ ((forall fom_index_wpopi_iteration_state_bounded. (exists fom_gap_wpopi_iteration_state_bounded_index_bound. fom_gap_wpopi_iteration_state_bounded_index_bound + S (fom_index_wpopi_iteration_state_bounded) = m + m) -> exists fom_value_wpopi_iteration_state_bounded. ((((exists fom_beta_height_wpopi_iteration_state_bounded_entry. fom_beta_height_wpopi_iteration_state_bounded_entry + S (fom_value_wpopi_iteration_state_bounded) = S ((S (fom_index_wpopi_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_iteration_state_bounded_entry. b = fom_beta_quotient_wpopi_iteration_state_bounded_entry * S ((S (fom_index_wpopi_iteration_state_bounded)) * c) + (fom_value_wpopi_iteration_state_bounded))) /\ (exists fom_gap_wpopi_iteration_state_bounded_value_bound. fom_gap_wpopi_iteration_state_bounded_value_bound + S (fom_value_wpopi_iteration_state_bounded) = n))) /\ ((forall wpo_position_wpopi_iteration_state_nonendpoint wpo_value_wpopi_iteration_state_nonendpoint. (exists wpo_gap_wpopi_iteration_state_nonendpoint_position_bound. wpo_gap_wpopi_iteration_state_nonendpoint_position_bound + S (wpo_position_wpopi_iteration_state_nonendpoint) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_nonendpoint_entry. wpo_beta_height_wpopi_iteration_state_nonendpoint_entry + S (wpo_value_wpopi_iteration_state_nonendpoint) = S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_iteration_state_nonendpoint_entry * S ((S (wpo_position_wpopi_iteration_state_nonendpoint)) * c) + (wpo_value_wpopi_iteration_state_nonendpoint))) -> (~(wpo_value_wpopi_iteration_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_iteration_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_iteration_state_injective wpo_injective_right_wpopi_iteration_state_injective wpo_injective_value_wpopi_iteration_state_injective. (exists wpo_gap_wpopi_iteration_state_injective_left_bound. wpo_gap_wpopi_iteration_state_injective_left_bound + S (wpo_injective_left_wpopi_iteration_state_injective) = m + m) -> (exists wpo_gap_wpopi_iteration_state_injective_right_bound. wpo_gap_wpopi_iteration_state_injective_right_bound + S (wpo_injective_right_wpopi_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_left_entry. wpo_beta_height_wpopi_iteration_state_injective_left_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_left_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> (((exists wpo_beta_height_wpopi_iteration_state_injective_right_entry. wpo_beta_height_wpopi_iteration_state_injective_right_entry + S (wpo_injective_value_wpopi_iteration_state_injective) = S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_state_injective_right_entry. b = wpo_beta_quotient_wpopi_iteration_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_iteration_state_injective)) * c) + (wpo_injective_value_wpopi_iteration_state_injective))) -> wpo_injective_left_wpopi_iteration_state_injective = wpo_injective_right_wpopi_iteration_state_injective))))) /\ (forall wpop_pair_wpopi_iteration_history. (exists wpo_gap_wpopi_iteration_history_pair_bound. wpo_gap_wpopi_iteration_history_pair_bound + S (wpop_pair_wpopi_iteration_history) = m) -> exists wpop_left_wpopi_iteration_history wpop_right_wpopi_iteration_history. ((((exists wpo_beta_height_wpopi_iteration_history_left_entry. wpo_beta_height_wpopi_iteration_history_left_entry + S (wpop_left_wpopi_iteration_history) = S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_left_entry. b = wpo_beta_quotient_wpopi_iteration_history_left_entry * S ((S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history)) * c) + (wpop_left_wpopi_iteration_history))) /\ ((((exists wpo_beta_height_wpopi_iteration_history_right_entry. wpo_beta_height_wpopi_iteration_history_right_entry + S (wpop_right_wpopi_iteration_history) = S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c)) /\ exists wpo_beta_quotient_wpopi_iteration_history_right_entry. b = wpo_beta_quotient_wpopi_iteration_history_right_entry * S ((S (S (wpop_pair_wpopi_iteration_history + wpop_pair_wpopi_iteration_history))) * c) + (wpop_right_wpopi_iteration_history))) /\ (((exists wpo_beta_height_wpopi_iteration_history_inverse_entry. wpo_beta_height_wpopi_iteration_history_inverse_entry + S (wpop_right_wpopi_iteration_history) = S ((S (wpop_left_wpopi_iteration_history)) * v)) /\ exists wpo_beta_quotient_wpopi_iteration_history_inverse_entry. u = wpo_beta_quotient_wpopi_iteration_history_inverse_entry * S ((S (wpop_left_wpopi_iteration_history)) * v) + (wpop_right_wpopi_iteration_history))))))))

Proof neighborhood

Direct theorem prerequisites

PA00B1 prime_pair_order_paired_iteration PA0001 zero_add

Direct theorem dependents

PA00BE prime_wilson_terminal_product_package_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

29 script commands · 5 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
prime pair order paired iteration
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro r
  6. L6
    intro m
  7. L7
    intro hpn
  8. L8
    intro hp
  9. L9
    intro hprefix
  10. L10
    intro hnr
02Fix variables and assumptionsL11–11

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hterminal
03Establish hbalanceL12–14

Establish this local claim before using it. It is not an additional assumption.

  1. L12
    have hbalance : (0 + 0) + S (S (m + m)) = n
  2. L13
    rewrite hterminal
  3. L14
    simp [zero_add]
04Establish hiterationL15–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime pair order paired iteration.

  1. L15
    have hiteration : ∀ t. ∀ q. q + q + S S (t + t) = n → ∃ x. ∃ y. (∀ z. ∀ m. ∀ k. Lt(z,t + t) → BetaAt(x,y,z,m) → BetaAt(u,v,m,k) → ContainsPrefix(x,y,t + t,k)) ∧ ((∀ z. Lt(z,t + t) → ∃ m. BetaAt(x,y,z,m) ∧ Lt(m,n)) ∧ ((∀ z. ∀ m. Lt(z,t + t) → BetaAt(x,y,z,m) → ¬m = 0 ∧ ¬S m = n) ∧ InjectivePrefix(x,y,t + t))) ∧ (∀ z. Lt(z,t) → ∃ m. ∃ k. BetaAt(x,y,z + z,m) ∧ (BetaAt(x,y,S (z + z),k) ∧ BetaAt(u,v,m,k)))Definitions: Lt(z,t + t)BetaAt(x,y,z,m)BetaAt(u,v,m,k)ContainsPrefix(x,y,t + t,k)Lt(m,n)InjectivePrefix(x,y,t + t)Lt(z,t)BetaAt(x,y,z + z,m)BetaAt(x,y,S (z + z),k)Original native command in the exact edition
  2. L16
    specialize prime_pair_order_paired_iteration p
  3. L17
    specialize prime_pair_order_paired_iteration n
  4. L18
    specialize prime_pair_order_paired_iteration u
  5. L19
    specialize prime_pair_order_paired_iteration v
  6. L20
    specialize prime_pair_order_paired_iteration r
  7. L21
    apply prime_pair_order_paired_iteration
  8. L22
    exact hpn
  9. L23
    exact hp
  10. L24
    exact hprefix
05Use earlier factsL25–29

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L25
    exact hnr
  2. L26
    specialize hiteration m
  3. L27
    specialize hiteration 0
  4. L28
    apply hiteration
  5. L29
    exact hbalance

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro r
  6. 0006intro m
  7. 0007intro hpn
  8. 0008intro hp
  9. 0009intro hprefix
  10. 0010intro hnr
  11. 0011intro hterminal
  12. 0012have hbalance : (0 + 0) + S (S (m + m)) = n
  13. 0013rewrite hterminal
  14. 0014simp [zero_add]
  15. 0015have hiteration : ∀ t. ∀ q. q + q + S S (t + t) = n → ∃ x. ∃ y. (∀ z. ∀ m. ∀ k. Lt(z,t + t) → BetaAt(x,y,z,m) → BetaAt(u,v,m,k) → ContainsPrefix(x,y,t + t,k)) ∧ ((∀ z. Lt(z,t + t) → ∃ m. BetaAt(x,y,z,m) ∧ Lt(m,n)) ∧ ((∀ z. ∀ m. Lt(z,t + t) → BetaAt(x,y,z,m) → ¬m = 0 ∧ ¬S m = n) ∧ InjectivePrefix(x,y,t + t))) ∧ (∀ z. Lt(z,t) → ∃ m. ∃ k. BetaAt(x,y,z + z,m) ∧ (BetaAt(x,y,S (z + z),k) ∧ BetaAt(u,v,m,k)))
    Exact native replay linehave hiteration : forall t q. (q + q) + S (S (t + t)) = n -> exists b c. ((((forall wpo_position_wpopi_family_state_closed wpo_source_wpopi_family_state_closed wpo_mate_wpopi_family_state_closed. (exists wpo_gap_wpopi_family_state_closed_position_bound. wpo_gap_wpopi_family_state_closed_position_bound + S (wpo_position_wpopi_family_state_closed) = t + t) -> (((exists wpo_beta_height_wpopi_family_state_closed_source_entry. wpo_beta_height_wpopi_family_state_closed_source_entry + S (wpo_source_wpopi_family_state_closed) = S ((S (wpo_position_wpopi_family_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_closed_source_entry. b = wpo_beta_quotient_wpopi_family_state_closed_source_entry * S ((S (wpo_position_wpopi_family_state_closed)) * c) + (wpo_source_wpopi_family_state_closed))) -> (((exists wpo_beta_height_wpopi_family_state_closed_inverse_entry. wpo_beta_height_wpopi_family_state_closed_inverse_entry + S (wpo_mate_wpopi_family_state_closed) = S ((S (wpo_source_wpopi_family_state_closed)) * v)) /\ exists wpo_beta_quotient_wpopi_family_state_closed_inverse_entry. u = wpo_beta_quotient_wpopi_family_state_closed_inverse_entry * S ((S (wpo_source_wpopi_family_state_closed)) * v) + (wpo_mate_wpopi_family_state_closed))) -> exists wpo_mate_position_wpopi_family_state_closed. ((exists wpo_gap_wpopi_family_state_closed_mate_bound. wpo_gap_wpopi_family_state_closed_mate_bound + S (wpo_mate_position_wpopi_family_state_closed) = t + t) /\ (((exists wpo_beta_height_wpopi_family_state_closed_mate_entry. wpo_beta_height_wpopi_family_state_closed_mate_entry + S (wpo_mate_wpopi_family_state_closed) = S ((S (wpo_mate_position_wpopi_family_state_closed)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_closed_mate_entry. b = wpo_beta_quotient_wpopi_family_state_closed_mate_entry * S ((S (wpo_mate_position_wpopi_family_state_closed)) * c) + (wpo_mate_wpopi_family_state_closed))))) /\ ((forall fom_index_wpopi_family_state_bounded. (exists fom_gap_wpopi_family_state_bounded_index_bound. fom_gap_wpopi_family_state_bounded_index_bound + S (fom_index_wpopi_family_state_bounded) = t + t) -> exists fom_value_wpopi_family_state_bounded. ((((exists fom_beta_height_wpopi_family_state_bounded_entry. fom_beta_height_wpopi_family_state_bounded_entry + S (fom_value_wpopi_family_state_bounded) = S ((S (fom_index_wpopi_family_state_bounded)) * c)) /\ exists fom_beta_quotient_wpopi_family_state_bounded_entry. b = fom_beta_quotient_wpopi_family_state_bounded_entry * S ((S (fom_index_wpopi_family_state_bounded)) * c) + (fom_value_wpopi_family_state_bounded))) /\ (exists fom_gap_wpopi_family_state_bounded_value_bound. fom_gap_wpopi_family_state_bounded_value_bound + S (fom_value_wpopi_family_state_bounded) = n))) /\ ((forall wpo_position_wpopi_family_state_nonendpoint wpo_value_wpopi_family_state_nonendpoint. (exists wpo_gap_wpopi_family_state_nonendpoint_position_bound. wpo_gap_wpopi_family_state_nonendpoint_position_bound + S (wpo_position_wpopi_family_state_nonendpoint) = t + t) -> (((exists wpo_beta_height_wpopi_family_state_nonendpoint_entry. wpo_beta_height_wpopi_family_state_nonendpoint_entry + S (wpo_value_wpopi_family_state_nonendpoint) = S ((S (wpo_position_wpopi_family_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_nonendpoint_entry. b = wpo_beta_quotient_wpopi_family_state_nonendpoint_entry * S ((S (wpo_position_wpopi_family_state_nonendpoint)) * c) + (wpo_value_wpopi_family_state_nonendpoint))) -> (~(wpo_value_wpopi_family_state_nonendpoint = 0) /\ ~((S wpo_value_wpopi_family_state_nonendpoint) = n))) /\ (forall wpo_injective_left_wpopi_family_state_injective wpo_injective_right_wpopi_family_state_injective wpo_injective_value_wpopi_family_state_injective. (exists wpo_gap_wpopi_family_state_injective_left_bound. wpo_gap_wpopi_family_state_injective_left_bound + S (wpo_injective_left_wpopi_family_state_injective) = t + t) -> (exists wpo_gap_wpopi_family_state_injective_right_bound. wpo_gap_wpopi_family_state_injective_right_bound + S (wpo_injective_right_wpopi_family_state_injective) = t + t) -> (((exists wpo_beta_height_wpopi_family_state_injective_left_entry. wpo_beta_height_wpopi_family_state_injective_left_entry + S (wpo_injective_value_wpopi_family_state_injective) = S ((S (wpo_injective_left_wpopi_family_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_injective_left_entry. b = wpo_beta_quotient_wpopi_family_state_injective_left_entry * S ((S (wpo_injective_left_wpopi_family_state_injective)) * c) + (wpo_injective_value_wpopi_family_state_injective))) -> (((exists wpo_beta_height_wpopi_family_state_injective_right_entry. wpo_beta_height_wpopi_family_state_injective_right_entry + S (wpo_injective_value_wpopi_family_state_injective) = S ((S (wpo_injective_right_wpopi_family_state_injective)) * c)) /\ exists wpo_beta_quotient_wpopi_family_state_injective_right_entry. b = wpo_beta_quotient_wpopi_family_state_injective_right_entry * S ((S (wpo_injective_right_wpopi_family_state_injective)) * c) + (wpo_injective_value_wpopi_family_state_injective))) -> wpo_injective_left_wpopi_family_state_injective = wpo_injective_right_wpopi_family_state_injective))))) /\ (forall wpop_pair_wpopi_family_history. (exists wpo_gap_wpopi_family_history_pair_bound. wpo_gap_wpopi_family_history_pair_bound + S (wpop_pair_wpopi_family_history) = t) -> exists wpop_left_wpopi_family_history wpop_right_wpopi_family_history. ((((exists wpo_beta_height_wpopi_family_history_left_entry. wpo_beta_height_wpopi_family_history_left_entry + S (wpop_left_wpopi_family_history) = S ((S (wpop_pair_wpopi_family_history + wpop_pair_wpopi_family_history)) * c)) /\ exists wpo_beta_quotient_wpopi_family_history_left_entry. b = wpo_beta_quotient_wpopi_family_history_left_entry * S ((S (wpop_pair_wpopi_family_history + wpop_pair_wpopi_family_history)) * c) + (wpop_left_wpopi_family_history))) /\ ((((exists wpo_beta_height_wpopi_family_history_right_entry. wpo_beta_height_wpopi_family_history_right_entry + S (wpop_right_wpopi_family_history) = S ((S (S (wpop_pair_wpopi_family_history + wpop_pair_wpopi_family_history))) * c)) /\ exists wpo_beta_quotient_wpopi_family_history_right_entry. b = wpo_beta_quotient_wpopi_family_history_right_entry * S ((S (S (wpop_pair_wpopi_family_history + wpop_pair_wpopi_family_history))) * c) + (wpop_right_wpopi_family_history))) /\ (((exists wpo_beta_height_wpopi_family_history_inverse_entry. wpo_beta_height_wpopi_family_history_inverse_entry + S (wpop_right_wpopi_family_history) = S ((S (wpop_left_wpopi_family_history)) * v)) /\ exists wpo_beta_quotient_wpopi_family_history_inverse_entry. u = wpo_beta_quotient_wpopi_family_history_inverse_entry * S ((S (wpop_left_wpopi_family_history)) * v) + (wpop_right_wpopi_family_history)))))))
  16. 0016specialize prime_pair_order_paired_iteration p
  17. 0017specialize prime_pair_order_paired_iteration n
  18. 0018specialize prime_pair_order_paired_iteration u
  19. 0019specialize prime_pair_order_paired_iteration v
  20. 0020specialize prime_pair_order_paired_iteration r
  21. 0021apply prime_pair_order_paired_iteration
  22. 0022exact hpn
  23. 0023exact hp
  24. 0024exact hprefix
  25. 0025exact hnr
  26. 0026specialize hiteration m
  27. 0027specialize hiteration 0
  28. 0028apply hiteration
  29. 0029exact hbalance