Exact expanded PA statement
forall p a n u v h. p = S n -> ((~(p = 1) /\ forall esi_prime_left_iteration_prime esi_prime_right_iteration_prime. p = esi_prime_left_iteration_prime * esi_prime_right_iteration_prime -> esi_prime_left_iteration_prime = 1 \/ esi_prime_right_iteration_prime = 1)) -> ~(exists qr_x_iteration_nonresidue. exists qr_u_iteration_nonresidue qr_v_iteration_nonresidue. qr_x_iteration_nonresidue * qr_x_iteration_nonresidue + p * qr_u_iteration_nonresidue = a + p * qr_v_iteration_nonresidue) -> (forall esip_index_iteration_prefix. (exists esip_gap_iteration_prefix_prefix_bound. esip_gap_iteration_prefix_prefix_bound + S (esip_index_iteration_prefix) = n) -> exists esip_mate_iteration_prefix. ((((exists ff_h_esip_iteration_prefix_entry. ff_h_esip_iteration_prefix_entry + S (esip_mate_iteration_prefix) = S ((S (esip_index_iteration_prefix)) * v)) /\ exists ff_q_esip_iteration_prefix_entry. u = ff_q_esip_iteration_prefix_entry * S ((S (esip_index_iteration_prefix)) * v) + (esip_mate_iteration_prefix))) /\ ((exists esip_gap_iteration_prefix_relation_index_bound. esip_gap_iteration_prefix_relation_index_bound + S (esip_index_iteration_prefix) = n) /\ ((((~((S esip_index_iteration_prefix) = 0) /\ (exists esip_gap_iteration_prefix_relation_scaled_left_bound. esip_gap_iteration_prefix_relation_scaled_left_bound + S (S esip_index_iteration_prefix) = p))) /\ (((~(esip_mate_iteration_prefix = 0) /\ (exists esip_gap_iteration_prefix_relation_scaled_right_bound. esip_gap_iteration_prefix_relation_scaled_right_bound + S (esip_mate_iteration_prefix) = p))) /\ (exists esi_mod_left_iteration_prefix_relation_scaled_mod esi_mod_right_iteration_prefix_relation_scaled_mod. ((S esip_index_iteration_prefix) * esip_mate_iteration_prefix) + p * esi_mod_left_iteration_prefix_relation_scaled_mod = (a) + p * esi_mod_right_iteration_prefix_relation_scaled_mod))))))) -> n = h + h -> (exists b c. (((((forall espo_position_terminal_state_closed espo_source_terminal_state_closed espo_mate_terminal_state_closed. (exists wpo_gap_terminal_state_closed_position_bound. wpo_gap_terminal_state_closed_position_bound + S (espo_position_terminal_state_closed) = h + h) -> (((exists wpo_beta_height_terminal_state_closed_source_entry. wpo_beta_height_terminal_state_closed_source_entry + S (espo_source_terminal_state_closed) = S ((S (espo_position_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_terminal_state_closed_source_entry. b = wpo_beta_quotient_terminal_state_closed_source_entry * S ((S (espo_position_terminal_state_closed)) * c) + (espo_source_terminal_state_closed))) -> (((exists wpo_beta_height_terminal_state_closed_scaled_entry. wpo_beta_height_terminal_state_closed_scaled_entry + S (S espo_mate_terminal_state_closed) = S ((S (espo_source_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_terminal_state_closed_scaled_entry. u = wpo_beta_quotient_terminal_state_closed_scaled_entry * S ((S (espo_source_terminal_state_closed)) * v) + (S espo_mate_terminal_state_closed))) -> exists espo_mate_position_terminal_state_closed. ((exists wpo_gap_terminal_state_closed_mate_bound. wpo_gap_terminal_state_closed_mate_bound + S (espo_mate_position_terminal_state_closed) = h + h) /\ (((exists wpo_beta_height_terminal_state_closed_mate_entry. wpo_beta_height_terminal_state_closed_mate_entry + S (espo_mate_terminal_state_closed) = S ((S (espo_mate_position_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_terminal_state_closed_mate_entry. b = wpo_beta_quotient_terminal_state_closed_mate_entry * S ((S (espo_mate_position_terminal_state_closed)) * c) + (espo_mate_terminal_state_closed))))) /\ (((forall fom_index_terminal_state_bounded. (exists fom_gap_terminal_state_bounded_index_bound. fom_gap_terminal_state_bounded_index_bound + S (fom_index_terminal_state_bounded) = h + h) -> exists fom_value_terminal_state_bounded. ((((exists fom_beta_height_terminal_state_bounded_entry. fom_beta_height_terminal_state_bounded_entry + S (fom_value_terminal_state_bounded) = S ((S (fom_index_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_terminal_state_bounded_entry. b = fom_beta_quotient_terminal_state_bounded_entry * S ((S (fom_index_terminal_state_bounded)) * c) + (fom_value_terminal_state_bounded))) /\ (exists fom_gap_terminal_state_bounded_value_bound. fom_gap_terminal_state_bounded_value_bound + S (fom_value_terminal_state_bounded) = n))) /\ (forall wpo_injective_left_terminal_state_injective wpo_injective_right_terminal_state_injective wpo_injective_value_terminal_state_injective. (exists wpo_gap_terminal_state_injective_left_bound. wpo_gap_terminal_state_injective_left_bound + S (wpo_injective_left_terminal_state_injective) = h + h) -> (exists wpo_gap_terminal_state_injective_right_bound. wpo_gap_terminal_state_injective_right_bound + S (wpo_injective_right_terminal_state_injective) = h + h) -> (((exists wpo_beta_height_terminal_state_injective_left_entry. wpo_beta_height_terminal_state_injective_left_entry + S (wpo_injective_value_terminal_state_injective) = S ((S (wpo_injective_left_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_terminal_state_injective_left_entry. b = wpo_beta_quotient_terminal_state_injective_left_entry * S ((S (wpo_injective_left_terminal_state_injective)) * c) + (wpo_injective_value_terminal_state_injective))) -> (((exists wpo_beta_height_terminal_state_injective_right_entry. wpo_beta_height_terminal_state_injective_right_entry + S (wpo_injective_value_terminal_state_injective) = S ((S (wpo_injective_right_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_terminal_state_injective_right_entry. b = wpo_beta_quotient_terminal_state_injective_right_entry * S ((S (wpo_injective_right_terminal_state_injective)) * c) + (wpo_injective_value_terminal_state_injective))) -> wpo_injective_left_terminal_state_injective = wpo_injective_right_terminal_state_injective))))) /\ (forall espi_pair_terminal_history. (exists wpo_gap_terminal_history_pair_bound. wpo_gap_terminal_history_pair_bound + S (espi_pair_terminal_history) = h) -> exists espi_left_terminal_history espi_right_terminal_history. (((((exists wpo_beta_height_terminal_history_left_entry. wpo_beta_height_terminal_history_left_entry + S (espi_left_terminal_history) = S ((S (espi_pair_terminal_history + espi_pair_terminal_history)) * c)) /\ exists wpo_beta_quotient_terminal_history_left_entry. b = wpo_beta_quotient_terminal_history_left_entry * S ((S (espi_pair_terminal_history + espi_pair_terminal_history)) * c) + (espi_left_terminal_history))) /\ (((((exists wpo_beta_height_terminal_history_right_entry. wpo_beta_height_terminal_history_right_entry + S (espi_right_terminal_history) = S ((S (S (espi_pair_terminal_history + espi_pair_terminal_history))) * c)) /\ exists wpo_beta_quotient_terminal_history_right_entry. b = wpo_beta_quotient_terminal_history_right_entry * S ((S (S (espi_pair_terminal_history + espi_pair_terminal_history))) * c) + (espi_right_terminal_history))) /\ (((exists wpo_beta_height_terminal_history_scaled_edge. wpo_beta_height_terminal_history_scaled_edge + S (S espi_right_terminal_history) = S ((S (espi_left_terminal_history)) * v)) /\ exists wpo_beta_quotient_terminal_history_scaled_edge. u = wpo_beta_quotient_terminal_history_scaled_edge * S ((S (espi_left_terminal_history)) * v) + (S espi_right_terminal_history)))))))))))Structural proof guide
Generated structural guide
At n=h+h, package a complete adjacent scaled-orbit order of length n.
Use the direct prerequisites scaled_inverse_pair_order_paired_iteration as previously established PA formulas.
The proof proceeds by intermediate claims (2), equality transport (1), certified simplification (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
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.
- 0001
intro p - 0002
intro a - 0003
intro n - 0004
intro u - 0005
intro v - 0006
intro h - 0007
intro hpn - 0008
intro hp - 0009
intro hnotqres - 0010
intro hprefix - 0011
intro heven - 0012
have hbalance : (h + h) + (0 + 0) = n - 0013
rewrite heven - 0014
simp - 0015
have hall : forall m k. (m + m) + (k + k) = n -> (exists b c. (((((forall espo_position_iteration_state_closed espo_source_iteration_state_closed espo_mate_iteration_state_closed. (exists wpo_gap_iteration_state_closed_position_bound. wpo_gap_iteration_state_closed_position_bound + S (espo_position_iteration_state_closed) = m + m) -> (((exists wpo_beta_height_iteration_state_closed_source_entry. wpo_beta_height_iteration_state_closed_source_entry + S (espo_source_iteration_state_closed) = S ((S (espo_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_source_entry. b = wpo_beta_quotient_iteration_state_closed_source_entry * S ((S (espo_position_iteration_state_closed)) * c) + (espo_source_iteration_state_closed))) -> (((exists wpo_beta_height_iteration_state_closed_scaled_entry. wpo_beta_height_iteration_state_closed_scaled_entry + S (S espo_mate_iteration_state_closed) = S ((S (espo_source_iteration_state_closed)) * v)) /\ exists wpo_beta_quotient_iteration_state_closed_scaled_entry. u = wpo_beta_quotient_iteration_state_closed_scaled_entry * S ((S (espo_source_iteration_state_closed)) * v) + (S espo_mate_iteration_state_closed))) -> exists espo_mate_position_iteration_state_closed. ((exists wpo_gap_iteration_state_closed_mate_bound. wpo_gap_iteration_state_closed_mate_bound + S (espo_mate_position_iteration_state_closed) = m + m) /\ (((exists wpo_beta_height_iteration_state_closed_mate_entry. wpo_beta_height_iteration_state_closed_mate_entry + S (espo_mate_iteration_state_closed) = S ((S (espo_mate_position_iteration_state_closed)) * c)) /\ exists wpo_beta_quotient_iteration_state_closed_mate_entry. b = wpo_beta_quotient_iteration_state_closed_mate_entry * S ((S (espo_mate_position_iteration_state_closed)) * c) + (espo_mate_iteration_state_closed))))) /\ (((forall fom_index_iteration_state_bounded. (exists fom_gap_iteration_state_bounded_index_bound. fom_gap_iteration_state_bounded_index_bound + S (fom_index_iteration_state_bounded) = m + m) -> exists fom_value_iteration_state_bounded. ((((exists fom_beta_height_iteration_state_bounded_entry. fom_beta_height_iteration_state_bounded_entry + S (fom_value_iteration_state_bounded) = S ((S (fom_index_iteration_state_bounded)) * c)) /\ exists fom_beta_quotient_iteration_state_bounded_entry. b = fom_beta_quotient_iteration_state_bounded_entry * S ((S (fom_index_iteration_state_bounded)) * c) + (fom_value_iteration_state_bounded))) /\ (exists fom_gap_iteration_state_bounded_value_bound. fom_gap_iteration_state_bounded_value_bound + S (fom_value_iteration_state_bounded) = n))) /\ (forall wpo_injective_left_iteration_state_injective wpo_injective_right_iteration_state_injective wpo_injective_value_iteration_state_injective. (exists wpo_gap_iteration_state_injective_left_bound. wpo_gap_iteration_state_injective_left_bound + S (wpo_injective_left_iteration_state_injective) = m + m) -> (exists wpo_gap_iteration_state_injective_right_bound. wpo_gap_iteration_state_injective_right_bound + S (wpo_injective_right_iteration_state_injective) = m + m) -> (((exists wpo_beta_height_iteration_state_injective_left_entry. wpo_beta_height_iteration_state_injective_left_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_left_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_left_entry. b = wpo_beta_quotient_iteration_state_injective_left_entry * S ((S (wpo_injective_left_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> (((exists wpo_beta_height_iteration_state_injective_right_entry. wpo_beta_height_iteration_state_injective_right_entry + S (wpo_injective_value_iteration_state_injective) = S ((S (wpo_injective_right_iteration_state_injective)) * c)) /\ exists wpo_beta_quotient_iteration_state_injective_right_entry. b = wpo_beta_quotient_iteration_state_injective_right_entry * S ((S (wpo_injective_right_iteration_state_injective)) * c) + (wpo_injective_value_iteration_state_injective))) -> wpo_injective_left_iteration_state_injective = wpo_injective_right_iteration_state_injective))))) /\ (forall espi_pair_iteration_history. (exists wpo_gap_iteration_history_pair_bound. wpo_gap_iteration_history_pair_bound + S (espi_pair_iteration_history) = m) -> exists espi_left_iteration_history espi_right_iteration_history. (((((exists wpo_beta_height_iteration_history_left_entry. wpo_beta_height_iteration_history_left_entry + S (espi_left_iteration_history) = S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c)) /\ exists wpo_beta_quotient_iteration_history_left_entry. b = wpo_beta_quotient_iteration_history_left_entry * S ((S (espi_pair_iteration_history + espi_pair_iteration_history)) * c) + (espi_left_iteration_history))) /\ (((((exists wpo_beta_height_iteration_history_right_entry. wpo_beta_height_iteration_history_right_entry + S (espi_right_iteration_history) = S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c)) /\ exists wpo_beta_quotient_iteration_history_right_entry. b = wpo_beta_quotient_iteration_history_right_entry * S ((S (S (espi_pair_iteration_history + espi_pair_iteration_history))) * c) + (espi_right_iteration_history))) /\ (((exists wpo_beta_height_iteration_history_scaled_edge. wpo_beta_height_iteration_history_scaled_edge + S (S espi_right_iteration_history) = S ((S (espi_left_iteration_history)) * v)) /\ exists wpo_beta_quotient_iteration_history_scaled_edge. u = wpo_beta_quotient_iteration_history_scaled_edge * S ((S (espi_left_iteration_history)) * v) + (S espi_right_iteration_history))))))))))) - 0016
specialize scaled_inverse_pair_order_paired_iteration p - 0017
specialize scaled_inverse_pair_order_paired_iteration a - 0018
specialize scaled_inverse_pair_order_paired_iteration n - 0019
specialize scaled_inverse_pair_order_paired_iteration u - 0020
specialize scaled_inverse_pair_order_paired_iteration v - 0021
apply scaled_inverse_pair_order_paired_iteration - 0022
exact hpn - 0023
exact hp - 0024
exact hnotqres - 0025
exact hprefix - 0026
specialize hall h - 0027
specialize hall 0 - 0028
apply hall - 0029
exact hbalance