Exact expanded 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))))))))Structural proof guide
Generated structural guide
Specialize the paired iteration to a terminal n-2 prefix with full adjacency history.
Use the direct prerequisites prime_pair_order_paired_iteration, zero_add 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 n - 0003
intro u - 0004
intro v - 0005
intro r - 0006
intro m - 0007
intro hpn - 0008
intro hp - 0009
intro hprefix - 0010
intro hnr - 0011
intro hterminal - 0012
have hbalance : (0 + 0) + S (S (m + m)) = n - 0013
rewrite hterminal - 0014
simp [zero_add] - 0015
have 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))))))) - 0016
specialize prime_pair_order_paired_iteration p - 0017
specialize prime_pair_order_paired_iteration n - 0018
specialize prime_pair_order_paired_iteration u - 0019
specialize prime_pair_order_paired_iteration v - 0020
specialize prime_pair_order_paired_iteration r - 0021
apply prime_pair_order_paired_iteration - 0022
exact hpn - 0023
exact hp - 0024
exact hprefix - 0025
exact hnr - 0026
specialize hiteration m - 0027
specialize hiteration 0 - 0028
apply hiteration - 0029
exact hbalance