PA009T · theorem

scaled_inverse_pair_order_paired_state_step

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

Append one fixed-point-free scaled orbit and preserve iterable state plus 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. ∀ a. ∀ n. ∀ u. ∀ v. ∀ b. ∀ c. ∀ m. p = S n → Prime(p) → ¬QRes(p,a) → ScaledInversePrefix(p,a,n,u,v,n) → Lt(m + m,n) → (∀ x. ∀ y. ∀ z. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(u,v,y,S z) → ContainsPrefix(b,c,m + m,z)) ∧ ((∀ x. Lt(x,m + m) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) ∧ InjectivePrefix(b,c,m + m)) → (∀ x. Lt(x,m) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,S z))) → ∃ x. ∃ y. (∀ z. ∀ k. ∀ i. Lt(z,S S (m + m)) → BetaAt(x,y,z,k) → BetaAt(u,v,k,S i) → ContainsPrefix(x,y,S S (m + m),i)) ∧ ((∀ z. Lt(z,S S (m + m)) → ∃ k. BetaAt(x,y,z,k) ∧ Lt(k,n)) ∧ InjectivePrefix(x,y,S S (m + m))) ∧ (∀ z. Lt(z,S m) → ∃ k. ∃ i. BetaAt(x,y,z + z,k) ∧ (BetaAt(x,y,S (z + z),i) ∧ BetaAt(u,v,k,S 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 PD0021 QRes PD0025 InjectivePrefix PD0027 ContainsPrefix PD0039 ScaledInversePrefix

28 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

47 occurrences

Exact expanded native-PA statement
forall p a n u v b c m. 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))))))) -> (exists wpo_gap_iteration_short. wpo_gap_iteration_short + S (m + m) = n) -> (((forall espo_position_step_old_state_closed espo_source_step_old_state_closed espo_mate_step_old_state_closed. (exists wpo_gap_step_old_state_closed_position_bound. wpo_gap_step_old_state_closed_position_bound + S (espo_position_step_old_state_closed) = m + m) -> (((exists wpo_beta_height_step_old_state_closed_source_entry. wpo_beta_height_step_old_state_closed_source_entry + S (espo_source_step_old_state_closed) = S ((S (espo_position_step_old_state_closed)) * c)) /\ exists wpo_beta_quotient_step_old_state_closed_source_entry. b = wpo_beta_quotient_step_old_state_closed_source_entry * S ((S (espo_position_step_old_state_closed)) * c) + (espo_source_step_old_state_closed))) -> (((exists wpo_beta_height_step_old_state_closed_scaled_entry. wpo_beta_height_step_old_state_closed_scaled_entry + S (S espo_mate_step_old_state_closed) = S ((S (espo_source_step_old_state_closed)) * v)) /\ exists wpo_beta_quotient_step_old_state_closed_scaled_entry. u = wpo_beta_quotient_step_old_state_closed_scaled_entry * S ((S (espo_source_step_old_state_closed)) * v) + (S espo_mate_step_old_state_closed))) -> exists espo_mate_position_step_old_state_closed. ((exists wpo_gap_step_old_state_closed_mate_bound. wpo_gap_step_old_state_closed_mate_bound + S (espo_mate_position_step_old_state_closed) = m + m) /\ (((exists wpo_beta_height_step_old_state_closed_mate_entry. wpo_beta_height_step_old_state_closed_mate_entry + S (espo_mate_step_old_state_closed) = S ((S (espo_mate_position_step_old_state_closed)) * c)) /\ exists wpo_beta_quotient_step_old_state_closed_mate_entry. b = wpo_beta_quotient_step_old_state_closed_mate_entry * S ((S (espo_mate_position_step_old_state_closed)) * c) + (espo_mate_step_old_state_closed))))) /\ (((forall fom_index_step_old_state_bounded. (exists fom_gap_step_old_state_bounded_index_bound. fom_gap_step_old_state_bounded_index_bound + S (fom_index_step_old_state_bounded) = m + m) -> exists fom_value_step_old_state_bounded. ((((exists fom_beta_height_step_old_state_bounded_entry. fom_beta_height_step_old_state_bounded_entry + S (fom_value_step_old_state_bounded) = S ((S (fom_index_step_old_state_bounded)) * c)) /\ exists fom_beta_quotient_step_old_state_bounded_entry. b = fom_beta_quotient_step_old_state_bounded_entry * S ((S (fom_index_step_old_state_bounded)) * c) + (fom_value_step_old_state_bounded))) /\ (exists fom_gap_step_old_state_bounded_value_bound. fom_gap_step_old_state_bounded_value_bound + S (fom_value_step_old_state_bounded) = n))) /\ (forall wpo_injective_left_step_old_state_injective wpo_injective_right_step_old_state_injective wpo_injective_value_step_old_state_injective. (exists wpo_gap_step_old_state_injective_left_bound. wpo_gap_step_old_state_injective_left_bound + S (wpo_injective_left_step_old_state_injective) = m + m) -> (exists wpo_gap_step_old_state_injective_right_bound. wpo_gap_step_old_state_injective_right_bound + S (wpo_injective_right_step_old_state_injective) = m + m) -> (((exists wpo_beta_height_step_old_state_injective_left_entry. wpo_beta_height_step_old_state_injective_left_entry + S (wpo_injective_value_step_old_state_injective) = S ((S (wpo_injective_left_step_old_state_injective)) * c)) /\ exists wpo_beta_quotient_step_old_state_injective_left_entry. b = wpo_beta_quotient_step_old_state_injective_left_entry * S ((S (wpo_injective_left_step_old_state_injective)) * c) + (wpo_injective_value_step_old_state_injective))) -> (((exists wpo_beta_height_step_old_state_injective_right_entry. wpo_beta_height_step_old_state_injective_right_entry + S (wpo_injective_value_step_old_state_injective) = S ((S (wpo_injective_right_step_old_state_injective)) * c)) /\ exists wpo_beta_quotient_step_old_state_injective_right_entry. b = wpo_beta_quotient_step_old_state_injective_right_entry * S ((S (wpo_injective_right_step_old_state_injective)) * c) + (wpo_injective_value_step_old_state_injective))) -> wpo_injective_left_step_old_state_injective = wpo_injective_right_step_old_state_injective))))) -> (forall espi_pair_step_old_history. (exists wpo_gap_step_old_history_pair_bound. wpo_gap_step_old_history_pair_bound + S (espi_pair_step_old_history) = m) -> exists espi_left_step_old_history espi_right_step_old_history. (((((exists wpo_beta_height_step_old_history_left_entry. wpo_beta_height_step_old_history_left_entry + S (espi_left_step_old_history) = S ((S (espi_pair_step_old_history + espi_pair_step_old_history)) * c)) /\ exists wpo_beta_quotient_step_old_history_left_entry. b = wpo_beta_quotient_step_old_history_left_entry * S ((S (espi_pair_step_old_history + espi_pair_step_old_history)) * c) + (espi_left_step_old_history))) /\ (((((exists wpo_beta_height_step_old_history_right_entry. wpo_beta_height_step_old_history_right_entry + S (espi_right_step_old_history) = S ((S (S (espi_pair_step_old_history + espi_pair_step_old_history))) * c)) /\ exists wpo_beta_quotient_step_old_history_right_entry. b = wpo_beta_quotient_step_old_history_right_entry * S ((S (S (espi_pair_step_old_history + espi_pair_step_old_history))) * c) + (espi_right_step_old_history))) /\ (((exists wpo_beta_height_step_old_history_scaled_edge. wpo_beta_height_step_old_history_scaled_edge + S (S espi_right_step_old_history) = S ((S (espi_left_step_old_history)) * v)) /\ exists wpo_beta_quotient_step_old_history_scaled_edge. u = wpo_beta_quotient_step_old_history_scaled_edge * S ((S (espi_left_step_old_history)) * v) + (S espi_right_step_old_history)))))))) -> (exists z d. (((((forall espo_position_step_result_state_closed espo_source_step_result_state_closed espo_mate_step_result_state_closed. (exists wpo_gap_step_result_state_closed_position_bound. wpo_gap_step_result_state_closed_position_bound + S (espo_position_step_result_state_closed) = S (S (m + m))) -> (((exists wpo_beta_height_step_result_state_closed_source_entry. wpo_beta_height_step_result_state_closed_source_entry + S (espo_source_step_result_state_closed) = S ((S (espo_position_step_result_state_closed)) * d)) /\ exists wpo_beta_quotient_step_result_state_closed_source_entry. z = wpo_beta_quotient_step_result_state_closed_source_entry * S ((S (espo_position_step_result_state_closed)) * d) + (espo_source_step_result_state_closed))) -> (((exists wpo_beta_height_step_result_state_closed_scaled_entry. wpo_beta_height_step_result_state_closed_scaled_entry + S (S espo_mate_step_result_state_closed) = S ((S (espo_source_step_result_state_closed)) * v)) /\ exists wpo_beta_quotient_step_result_state_closed_scaled_entry. u = wpo_beta_quotient_step_result_state_closed_scaled_entry * S ((S (espo_source_step_result_state_closed)) * v) + (S espo_mate_step_result_state_closed))) -> exists espo_mate_position_step_result_state_closed. ((exists wpo_gap_step_result_state_closed_mate_bound. wpo_gap_step_result_state_closed_mate_bound + S (espo_mate_position_step_result_state_closed) = S (S (m + m))) /\ (((exists wpo_beta_height_step_result_state_closed_mate_entry. wpo_beta_height_step_result_state_closed_mate_entry + S (espo_mate_step_result_state_closed) = S ((S (espo_mate_position_step_result_state_closed)) * d)) /\ exists wpo_beta_quotient_step_result_state_closed_mate_entry. z = wpo_beta_quotient_step_result_state_closed_mate_entry * S ((S (espo_mate_position_step_result_state_closed)) * d) + (espo_mate_step_result_state_closed))))) /\ (((forall fom_index_step_result_state_bounded. (exists fom_gap_step_result_state_bounded_index_bound. fom_gap_step_result_state_bounded_index_bound + S (fom_index_step_result_state_bounded) = S (S (m + m))) -> exists fom_value_step_result_state_bounded. ((((exists fom_beta_height_step_result_state_bounded_entry. fom_beta_height_step_result_state_bounded_entry + S (fom_value_step_result_state_bounded) = S ((S (fom_index_step_result_state_bounded)) * d)) /\ exists fom_beta_quotient_step_result_state_bounded_entry. z = fom_beta_quotient_step_result_state_bounded_entry * S ((S (fom_index_step_result_state_bounded)) * d) + (fom_value_step_result_state_bounded))) /\ (exists fom_gap_step_result_state_bounded_value_bound. fom_gap_step_result_state_bounded_value_bound + S (fom_value_step_result_state_bounded) = n))) /\ (forall wpo_injective_left_step_result_state_injective wpo_injective_right_step_result_state_injective wpo_injective_value_step_result_state_injective. (exists wpo_gap_step_result_state_injective_left_bound. wpo_gap_step_result_state_injective_left_bound + S (wpo_injective_left_step_result_state_injective) = S (S (m + m))) -> (exists wpo_gap_step_result_state_injective_right_bound. wpo_gap_step_result_state_injective_right_bound + S (wpo_injective_right_step_result_state_injective) = S (S (m + m))) -> (((exists wpo_beta_height_step_result_state_injective_left_entry. wpo_beta_height_step_result_state_injective_left_entry + S (wpo_injective_value_step_result_state_injective) = S ((S (wpo_injective_left_step_result_state_injective)) * d)) /\ exists wpo_beta_quotient_step_result_state_injective_left_entry. z = wpo_beta_quotient_step_result_state_injective_left_entry * S ((S (wpo_injective_left_step_result_state_injective)) * d) + (wpo_injective_value_step_result_state_injective))) -> (((exists wpo_beta_height_step_result_state_injective_right_entry. wpo_beta_height_step_result_state_injective_right_entry + S (wpo_injective_value_step_result_state_injective) = S ((S (wpo_injective_right_step_result_state_injective)) * d)) /\ exists wpo_beta_quotient_step_result_state_injective_right_entry. z = wpo_beta_quotient_step_result_state_injective_right_entry * S ((S (wpo_injective_right_step_result_state_injective)) * d) + (wpo_injective_value_step_result_state_injective))) -> wpo_injective_left_step_result_state_injective = wpo_injective_right_step_result_state_injective))))) /\ (forall espi_pair_append_new_history. (exists wpo_gap_append_new_history_pair_bound. wpo_gap_append_new_history_pair_bound + S (espi_pair_append_new_history) = S m) -> exists espi_left_append_new_history espi_right_append_new_history. (((((exists wpo_beta_height_append_new_history_left_entry. wpo_beta_height_append_new_history_left_entry + S (espi_left_append_new_history) = S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d)) /\ exists wpo_beta_quotient_append_new_history_left_entry. z = wpo_beta_quotient_append_new_history_left_entry * S ((S (espi_pair_append_new_history + espi_pair_append_new_history)) * d) + (espi_left_append_new_history))) /\ (((((exists wpo_beta_height_append_new_history_right_entry. wpo_beta_height_append_new_history_right_entry + S (espi_right_append_new_history) = S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d)) /\ exists wpo_beta_quotient_append_new_history_right_entry. z = wpo_beta_quotient_append_new_history_right_entry * S ((S (S (espi_pair_append_new_history + espi_pair_append_new_history))) * d) + (espi_right_append_new_history))) /\ (((exists wpo_beta_height_append_new_history_scaled_edge. wpo_beta_height_append_new_history_scaled_edge + S (S espi_right_append_new_history) = S ((S (espi_left_append_new_history)) * v)) /\ exists wpo_beta_quotient_append_new_history_scaled_edge. u = wpo_beta_quotient_append_new_history_scaled_edge * S ((S (espi_left_append_new_history)) * v) + (S espi_right_append_new_history)))))))))))

Proof neighborhood

Direct theorem prerequisites

PA009O scaled_inverse_pair_order_choose_append PA009P beta_prefix_append_two_bounded_into PA009S adjacent_scaled_orbit_history_append

Direct theorem dependents

PA009V scaled_inverse_pair_order_paired_iteration

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

88 script commands · 20 reading checkpoints · 5 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 (3)
scaled inverse pair order choose appendbeta prefix append two bounded intoadjacent scaled orbit history append
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro hnotqres
  2. L12
    intro hprefix
  3. L13
    intro hshort
  4. L14
    intro hstate
  5. L15
    intro hhistory
03Separate the logical casesL16–17

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    cases hstate
  2. L17
    cases hstate_right
04Establish hrawL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled inverse pair order choose append.

  1. L18
    have hraw : ∃ z. ∃ d. ∃ i. ∃ j. BetaAt(z,d,m + m,i) ∧ (BetaAt(z,d,S (m + m),j) ∧ (∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))) ∧ (Lt(i,n) ∧ (Lt(j,n) ∧ (¬ContainsPrefix(b,c,m + m,i) ∧ (¬ContainsPrefix(b,c,m + m,j) ∧ (¬i = j ∧ (BetaAt(u,v,i,S j) ∧ (BetaAt(u,v,j,S i) ∧ ((∀ x. ∀ y. ∀ k. Lt(x,S S (m + m)) → BetaAt(z,d,x,y) → BetaAt(u,v,y,S k) → ContainsPrefix(z,d,S S (m + m),k)) ∧ InjectivePrefix(z,d,S S (m + m))))))))))Definitions: BetaAt(z,d,m + m,i)BetaAt(z,d,S (m + m),j)Lt(x,m + m)BetaAt(b,c,x,y)BetaAt(z,d,x,y)Lt(i,n)Lt(j,n)ContainsPrefix(b,c,m + m,i)ContainsPrefix(b,c,m + m,j)BetaAt(u,v,i,S j)BetaAt(u,v,j,S i)Lt(x,S S (m + m))BetaAt(u,v,y,S k)ContainsPrefix(z,d,S S (m + m),k)InjectivePrefix(z,d,S S (m + m))Original native command in the exact edition
  2. L19
    specialize scaled_inverse_pair_order_choose_append p
  3. L20
    specialize scaled_inverse_pair_order_choose_append a
  4. L21
    specialize scaled_inverse_pair_order_choose_append n
  5. L22
    specialize scaled_inverse_pair_order_choose_append u
  6. L23
    specialize scaled_inverse_pair_order_choose_append v
  7. L24
    specialize scaled_inverse_pair_order_choose_append b
  8. L25
    specialize scaled_inverse_pair_order_choose_append c
  9. L26
    specialize scaled_inverse_pair_order_choose_append (m + m)
  10. L27
    apply scaled_inverse_pair_order_choose_append
05Use earlier factsL28–34

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

  1. L28
    exact hpn
  2. L29
    exact hp
  3. L30
    exact hnotqres
  4. L31
    exact hprefix
  5. L32
    exact hshort
  6. L33
    exact hstate_left
  7. L34
    exact hstate_right_right
06Separate the logical casesL35–38

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L35
    cases hraw
  2. L36
    cases hraw_witness
  3. L37
    cases hraw_witness_witness
  4. L38
    cases hraw_witness_witness_witness
07Establish hpartsL39–40

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

  1. L39
    have hparts : BetaAt(x,x1,m + m,x2) ∧ (BetaAt(x,x1,S (m + m),x3) ∧ (∀ y. ∀ z. Lt(y,m + m) → BetaAt(b,c,y,z) → BetaAt(x,x1,y,z))) ∧ (Lt(x2,n) ∧ (Lt(x3,n) ∧ (¬ContainsPrefix(b,c,m + m,x2) ∧ (¬ContainsPrefix(b,c,m + m,x3) ∧ (¬x2 = x3 ∧ (BetaAt(u,v,x2,S x3) ∧ (BetaAt(u,v,x3,S x2) ∧ ((∀ y. ∀ z. ∀ k. Lt(y,S S (m + m)) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,S k) → ContainsPrefix(x,x1,S S (m + m),k)) ∧ InjectivePrefix(x,x1,S S (m + m))))))))))Definitions: BetaAt(x,x1,m + m,x2)BetaAt(x,x1,S (m + m),x3)Lt(y,m + m)BetaAt(b,c,y,z)BetaAt(x,x1,y,z)Lt(x2,n)Lt(x3,n)ContainsPrefix(b,c,m + m,x2)ContainsPrefix(b,c,m + m,x3)BetaAt(u,v,x2,S x3)BetaAt(u,v,x3,S x2)Lt(y,S S (m + m))BetaAt(u,v,z,S k)ContainsPrefix(x,x1,S S (m + m),k)InjectivePrefix(x,x1,S S (m + m))Original native command in the exact edition
  2. L40
    exact hraw_witness_witness_witness_witness
08Separate the logical casesL41–49

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L41
    cases hparts
  2. L42
    cases hparts_right
  3. L43
    cases hparts_right_right
  4. L44
    cases hparts_right_right_right
  5. L45
    cases hparts_right_right_right_right
  6. L46
    cases hparts_right_right_right_right_right
  7. L47
    cases hparts_right_right_right_right_right_right
  8. L48
    cases hparts_right_right_right_right_right_right_right
  9. L49
    cases hparts_right_right_right_right_right_right_right_right
09Establish hbounded_afterL50–59

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix append two bounded into.

  1. L50
    have hbounded_after : ∀ fom_index_bounded_after_x. Lt(fom_index_bounded_after_x,S S (m + m)) → ∃ y. BetaAt(x,x1,fom_index_bounded_after_x,y) ∧ Lt(y,n)Definitions: Lt(fom_index_bounded_after_x,S S (m + m))BetaAt(x,x1,fom_index_bounded_after_x,y)Lt(y,n)Original native command in the exact edition
  2. L51
    specialize beta_prefix_append_two_bounded_into b
  3. L52
    specialize beta_prefix_append_two_bounded_into c
  4. L53
    specialize beta_prefix_append_two_bounded_into x
  5. L54
    specialize beta_prefix_append_two_bounded_into x1
  6. L55
    specialize beta_prefix_append_two_bounded_into (m + m)
  7. L56
    specialize beta_prefix_append_two_bounded_into n
  8. L57
    specialize beta_prefix_append_two_bounded_into x2
  9. L58
    specialize beta_prefix_append_two_bounded_into x3
  10. L59
    apply beta_prefix_append_two_bounded_into
10Use earlier factsL60–63

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

  1. L60
    exact hparts_left
  2. L61
    exact hstate_right_left
  3. L62
    exact hparts_right_left
  4. L63
    exact hparts_right_right_left
11Establish hhistory_afterL64–73

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

  1. L64
    have hhistory_after : ∀ espi_pair_history_after_x. Lt(espi_pair_history_after_x,S m) → ∃ y. ∃ z. BetaAt(x,x1,espi_pair_history_after_x + espi_pair_history_after_x,y) ∧ (BetaAt(x,x1,S (espi_pair_history_after_x + espi_pair_history_after_x),z) ∧ BetaAt(u,v,y,S z))Definitions: Lt(espi_pair_history_after_x,S m)BetaAt(x,x1,espi_pair_history_after_x + espi_pair_history_after_x,y)BetaAt(x,x1,S (espi_pair_history_after_x + espi_pair_history_after_x),z)BetaAt(u,v,y,S z)Original native command in the exact edition
  2. L65
    specialize adjacent_scaled_orbit_history_append u
  3. L66
    specialize adjacent_scaled_orbit_history_append v
  4. L67
    specialize adjacent_scaled_orbit_history_append b
  5. L68
    specialize adjacent_scaled_orbit_history_append c
  6. L69
    specialize adjacent_scaled_orbit_history_append x
  7. L70
    specialize adjacent_scaled_orbit_history_append x1
  8. L71
    specialize adjacent_scaled_orbit_history_append m
  9. L72
    specialize adjacent_scaled_orbit_history_append x2
  10. L73
    specialize adjacent_scaled_orbit_history_append x3
12Use earlier factsL74–77

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

  1. L74
    apply adjacent_scaled_orbit_history_append
  2. L75
    exact hhistory
  3. L76
    exact hparts_left
  4. L77
    exact hparts_right_right_right_right_right_right_left
13Establish hstate_afterL78–78

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

  1. L78
    have hstate_after : (∀ y. ∀ z. ∀ k. Lt(y,S S (m + m)) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,S k) → ContainsPrefix(x,x1,S S (m + m),k)) ∧ ((∀ y. Lt(y,S S (m + m)) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,n)) ∧ InjectivePrefix(x,x1,S S (m + m)))Definitions: Lt(y,S S (m + m))BetaAt(x,x1,y,z)BetaAt(u,v,z,S k)ContainsPrefix(x,x1,S S (m + m),k)Lt(z,n)InjectivePrefix(x,x1,S S (m + m))Original native command in the exact edition
14Separate the logical casesL79–79

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L79
    split
15Use earlier factsL80–80

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

  1. L80
    exact hparts_right_right_right_right_right_right_right_right_left
16Separate the logical casesL81–81

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L81
    split
17Use earlier factsL82–83

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

  1. L82
    exact hbounded_after
  2. L83
    exact hparts_right_right_right_right_right_right_right_right_right
18Construct an explicit witnessL84–85

Supply the displayed value, then prove that it has the required property.

  1. L84
    exists x
  2. L85
    exists x1
19Separate the logical casesL86–86

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L86
    split
20Use earlier factsL87–88

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

  1. L87
    exact hstate_after
  2. L88
    exact hhistory_after

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro b
  7. 0007intro c
  8. 0008intro m
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hnotqres
  12. 0012intro hprefix
  13. 0013intro hshort
  14. 0014intro hstate
  15. 0015intro hhistory
  16. 0016cases hstate
  17. 0017cases hstate_right
  18. 0018have hraw : ∃ z. ∃ d. ∃ i. ∃ j. BetaAt(z,d,m + m,i) ∧ (BetaAt(z,d,S (m + m),j) ∧ (∀ x. ∀ y. Lt(x,m + m) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))) ∧ (Lt(i,n) ∧ (Lt(j,n) ∧ (¬ContainsPrefix(b,c,m + m,i) ∧ (¬ContainsPrefix(b,c,m + m,j) ∧ (¬i = j ∧ (BetaAt(u,v,i,S j) ∧ (BetaAt(u,v,j,S i) ∧ ((∀ x. ∀ y. ∀ k. Lt(x,S S (m + m)) → BetaAt(z,d,x,y) → BetaAt(u,v,y,S k) → ContainsPrefix(z,d,S S (m + m),k)) ∧ InjectivePrefix(z,d,S S (m + m))))))))))
    Exact native replay linehave hraw : exists z d i j. (((((((exists wpo_beta_height_step_payload_trace_first. wpo_beta_height_step_payload_trace_first + S (i) = S ((S (m + m)) * d)) /\ exists wpo_beta_quotient_step_payload_trace_first. z = wpo_beta_quotient_step_payload_trace_first * S ((S (m + m)) * d) + (i))) /\ ((((exists wpo_beta_height_step_payload_trace_second. wpo_beta_height_step_payload_trace_second + S (j) = S ((S (S (m + m))) * d)) /\ exists wpo_beta_quotient_step_payload_trace_second. z = wpo_beta_quotient_step_payload_trace_second * S ((S (S (m + m))) * d) + (j))) /\ (forall wpo_old_index_step_payload_trace wpo_old_value_step_payload_trace. (exists wpo_gap_step_payload_trace_old_bound. wpo_gap_step_payload_trace_old_bound + S (wpo_old_index_step_payload_trace) = m + m) -> (((exists wpo_beta_height_step_payload_trace_old_entry. wpo_beta_height_step_payload_trace_old_entry + S (wpo_old_value_step_payload_trace) = S ((S (wpo_old_index_step_payload_trace)) * c)) /\ exists wpo_beta_quotient_step_payload_trace_old_entry. b = wpo_beta_quotient_step_payload_trace_old_entry * S ((S (wpo_old_index_step_payload_trace)) * c) + (wpo_old_value_step_payload_trace))) -> (((exists wpo_beta_height_step_payload_trace_new_entry. wpo_beta_height_step_payload_trace_new_entry + S (wpo_old_value_step_payload_trace) = S ((S (wpo_old_index_step_payload_trace)) * d)) /\ exists wpo_beta_quotient_step_payload_trace_new_entry. z = wpo_beta_quotient_step_payload_trace_new_entry * S ((S (wpo_old_index_step_payload_trace)) * d) + (wpo_old_value_step_payload_trace))))))) /\ (((exists wpo_gap_step_payload_source_bound. wpo_gap_step_payload_source_bound + S (i) = n) /\ (((exists wpo_gap_step_payload_mate_bound. wpo_gap_step_payload_mate_bound + S (j) = n) /\ (((~(exists wpo_index_step_payload_source_omit_contains. ((exists wpo_gap_step_payload_source_omit_contains_bound. wpo_gap_step_payload_source_omit_contains_bound + S (wpo_index_step_payload_source_omit_contains) = m + m) /\ (((exists wpo_beta_height_step_payload_source_omit_contains_entry. wpo_beta_height_step_payload_source_omit_contains_entry + S (i) = S ((S (wpo_index_step_payload_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_payload_source_omit_contains_entry. b = wpo_beta_quotient_step_payload_source_omit_contains_entry * S ((S (wpo_index_step_payload_source_omit_contains)) * c) + (i)))))) /\ (((~(exists wpo_index_step_payload_mate_omit_contains. ((exists wpo_gap_step_payload_mate_omit_contains_bound. wpo_gap_step_payload_mate_omit_contains_bound + S (wpo_index_step_payload_mate_omit_contains) = m + m) /\ (((exists wpo_beta_height_step_payload_mate_omit_contains_entry. wpo_beta_height_step_payload_mate_omit_contains_entry + S (j) = S ((S (wpo_index_step_payload_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_payload_mate_omit_contains_entry. b = wpo_beta_quotient_step_payload_mate_omit_contains_entry * S ((S (wpo_index_step_payload_mate_omit_contains)) * c) + (j)))))) /\ (((~(i = j)) /\ (((((exists wpo_beta_height_step_payload_forward. wpo_beta_height_step_payload_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_step_payload_forward. u = wpo_beta_quotient_step_payload_forward * S ((S (i)) * v) + (S j))) /\ (((((exists wpo_beta_height_step_payload_back. wpo_beta_height_step_payload_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_step_payload_back. u = wpo_beta_quotient_step_payload_back * S ((S (j)) * v) + (S i))) /\ (((forall espo_position_step_payload_closed_after espo_source_step_payload_closed_after espo_mate_step_payload_closed_after. (exists wpo_gap_step_payload_closed_after_position_bound. wpo_gap_step_payload_closed_after_position_bound + S (espo_position_step_payload_closed_after) = S (S (m + m))) -> (((exists wpo_beta_height_step_payload_closed_after_source_entry. wpo_beta_height_step_payload_closed_after_source_entry + S (espo_source_step_payload_closed_after) = S ((S (espo_position_step_payload_closed_after)) * d)) /\ exists wpo_beta_quotient_step_payload_closed_after_source_entry. z = wpo_beta_quotient_step_payload_closed_after_source_entry * S ((S (espo_position_step_payload_closed_after)) * d) + (espo_source_step_payload_closed_after))) -> (((exists wpo_beta_height_step_payload_closed_after_scaled_entry. wpo_beta_height_step_payload_closed_after_scaled_entry + S (S espo_mate_step_payload_closed_after) = S ((S (espo_source_step_payload_closed_after)) * v)) /\ exists wpo_beta_quotient_step_payload_closed_after_scaled_entry. u = wpo_beta_quotient_step_payload_closed_after_scaled_entry * S ((S (espo_source_step_payload_closed_after)) * v) + (S espo_mate_step_payload_closed_after))) -> exists espo_mate_position_step_payload_closed_after. ((exists wpo_gap_step_payload_closed_after_mate_bound. wpo_gap_step_payload_closed_after_mate_bound + S (espo_mate_position_step_payload_closed_after) = S (S (m + m))) /\ (((exists wpo_beta_height_step_payload_closed_after_mate_entry. wpo_beta_height_step_payload_closed_after_mate_entry + S (espo_mate_step_payload_closed_after) = S ((S (espo_mate_position_step_payload_closed_after)) * d)) /\ exists wpo_beta_quotient_step_payload_closed_after_mate_entry. z = wpo_beta_quotient_step_payload_closed_after_mate_entry * S ((S (espo_mate_position_step_payload_closed_after)) * d) + (espo_mate_step_payload_closed_after))))) /\ (forall wpo_injective_left_step_payload_injective_after wpo_injective_right_step_payload_injective_after wpo_injective_value_step_payload_injective_after. (exists wpo_gap_step_payload_injective_after_left_bound. wpo_gap_step_payload_injective_after_left_bound + S (wpo_injective_left_step_payload_injective_after) = S (S (m + m))) -> (exists wpo_gap_step_payload_injective_after_right_bound. wpo_gap_step_payload_injective_after_right_bound + S (wpo_injective_right_step_payload_injective_after) = S (S (m + m))) -> (((exists wpo_beta_height_step_payload_injective_after_left_entry. wpo_beta_height_step_payload_injective_after_left_entry + S (wpo_injective_value_step_payload_injective_after) = S ((S (wpo_injective_left_step_payload_injective_after)) * d)) /\ exists wpo_beta_quotient_step_payload_injective_after_left_entry. z = wpo_beta_quotient_step_payload_injective_after_left_entry * S ((S (wpo_injective_left_step_payload_injective_after)) * d) + (wpo_injective_value_step_payload_injective_after))) -> (((exists wpo_beta_height_step_payload_injective_after_right_entry. wpo_beta_height_step_payload_injective_after_right_entry + S (wpo_injective_value_step_payload_injective_after) = S ((S (wpo_injective_right_step_payload_injective_after)) * d)) /\ exists wpo_beta_quotient_step_payload_injective_after_right_entry. z = wpo_beta_quotient_step_payload_injective_after_right_entry * S ((S (wpo_injective_right_step_payload_injective_after)) * d) + (wpo_injective_value_step_payload_injective_after))) -> wpo_injective_left_step_payload_injective_after = wpo_injective_right_step_payload_injective_after)))))))))))))))))))
  19. 0019specialize scaled_inverse_pair_order_choose_append p
  20. 0020specialize scaled_inverse_pair_order_choose_append a
  21. 0021specialize scaled_inverse_pair_order_choose_append n
  22. 0022specialize scaled_inverse_pair_order_choose_append u
  23. 0023specialize scaled_inverse_pair_order_choose_append v
  24. 0024specialize scaled_inverse_pair_order_choose_append b
  25. 0025specialize scaled_inverse_pair_order_choose_append c
  26. 0026specialize scaled_inverse_pair_order_choose_append (m + m)
  27. 0027apply scaled_inverse_pair_order_choose_append
  28. 0028exact hpn
  29. 0029exact hp
  30. 0030exact hnotqres
  31. 0031exact hprefix
  32. 0032exact hshort
  33. 0033exact hstate_left
  34. 0034exact hstate_right_right
  35. 0035cases hraw
  36. 0036cases hraw_witness
  37. 0037cases hraw_witness_witness
  38. 0038cases hraw_witness_witness_witness
  39. 0039have hparts : BetaAt(x,x1,m + m,x2) ∧ (BetaAt(x,x1,S (m + m),x3) ∧ (∀ y. ∀ z. Lt(y,m + m) → BetaAt(b,c,y,z) → BetaAt(x,x1,y,z))) ∧ (Lt(x2,n) ∧ (Lt(x3,n) ∧ (¬ContainsPrefix(b,c,m + m,x2) ∧ (¬ContainsPrefix(b,c,m + m,x3) ∧ (¬x2 = x3 ∧ (BetaAt(u,v,x2,S x3) ∧ (BetaAt(u,v,x3,S x2) ∧ ((∀ y. ∀ z. ∀ k. Lt(y,S S (m + m)) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,S k) → ContainsPrefix(x,x1,S S (m + m),k)) ∧ InjectivePrefix(x,x1,S S (m + m))))))))))
    Exact native replay linehave hparts : ((((((exists wpo_beta_height_step_payload_x_trace_first. wpo_beta_height_step_payload_x_trace_first + S (x2) = S ((S (m + m)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_trace_first. x = wpo_beta_quotient_step_payload_x_trace_first * S ((S (m + m)) * x1) + (x2))) /\ ((((exists wpo_beta_height_step_payload_x_trace_second. wpo_beta_height_step_payload_x_trace_second + S (x3) = S ((S (S (m + m))) * x1)) /\ exists wpo_beta_quotient_step_payload_x_trace_second. x = wpo_beta_quotient_step_payload_x_trace_second * S ((S (S (m + m))) * x1) + (x3))) /\ (forall wpo_old_index_step_payload_x_trace wpo_old_value_step_payload_x_trace. (exists wpo_gap_step_payload_x_trace_old_bound. wpo_gap_step_payload_x_trace_old_bound + S (wpo_old_index_step_payload_x_trace) = m + m) -> (((exists wpo_beta_height_step_payload_x_trace_old_entry. wpo_beta_height_step_payload_x_trace_old_entry + S (wpo_old_value_step_payload_x_trace) = S ((S (wpo_old_index_step_payload_x_trace)) * c)) /\ exists wpo_beta_quotient_step_payload_x_trace_old_entry. b = wpo_beta_quotient_step_payload_x_trace_old_entry * S ((S (wpo_old_index_step_payload_x_trace)) * c) + (wpo_old_value_step_payload_x_trace))) -> (((exists wpo_beta_height_step_payload_x_trace_new_entry. wpo_beta_height_step_payload_x_trace_new_entry + S (wpo_old_value_step_payload_x_trace) = S ((S (wpo_old_index_step_payload_x_trace)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_trace_new_entry. x = wpo_beta_quotient_step_payload_x_trace_new_entry * S ((S (wpo_old_index_step_payload_x_trace)) * x1) + (wpo_old_value_step_payload_x_trace))))))) /\ (((exists wpo_gap_step_payload_x_source_bound. wpo_gap_step_payload_x_source_bound + S (x2) = n) /\ (((exists wpo_gap_step_payload_x_mate_bound. wpo_gap_step_payload_x_mate_bound + S (x3) = n) /\ (((~(exists wpo_index_step_payload_x_source_omit_contains. ((exists wpo_gap_step_payload_x_source_omit_contains_bound. wpo_gap_step_payload_x_source_omit_contains_bound + S (wpo_index_step_payload_x_source_omit_contains) = m + m) /\ (((exists wpo_beta_height_step_payload_x_source_omit_contains_entry. wpo_beta_height_step_payload_x_source_omit_contains_entry + S (x2) = S ((S (wpo_index_step_payload_x_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_payload_x_source_omit_contains_entry. b = wpo_beta_quotient_step_payload_x_source_omit_contains_entry * S ((S (wpo_index_step_payload_x_source_omit_contains)) * c) + (x2)))))) /\ (((~(exists wpo_index_step_payload_x_mate_omit_contains. ((exists wpo_gap_step_payload_x_mate_omit_contains_bound. wpo_gap_step_payload_x_mate_omit_contains_bound + S (wpo_index_step_payload_x_mate_omit_contains) = m + m) /\ (((exists wpo_beta_height_step_payload_x_mate_omit_contains_entry. wpo_beta_height_step_payload_x_mate_omit_contains_entry + S (x3) = S ((S (wpo_index_step_payload_x_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_step_payload_x_mate_omit_contains_entry. b = wpo_beta_quotient_step_payload_x_mate_omit_contains_entry * S ((S (wpo_index_step_payload_x_mate_omit_contains)) * c) + (x3)))))) /\ (((~(x2 = x3)) /\ (((((exists wpo_beta_height_step_payload_x_forward. wpo_beta_height_step_payload_x_forward + S (S x3) = S ((S (x2)) * v)) /\ exists wpo_beta_quotient_step_payload_x_forward. u = wpo_beta_quotient_step_payload_x_forward * S ((S (x2)) * v) + (S x3))) /\ (((((exists wpo_beta_height_step_payload_x_back. wpo_beta_height_step_payload_x_back + S (S x2) = S ((S (x3)) * v)) /\ exists wpo_beta_quotient_step_payload_x_back. u = wpo_beta_quotient_step_payload_x_back * S ((S (x3)) * v) + (S x2))) /\ (((forall espo_position_step_payload_x_closed_after espo_source_step_payload_x_closed_after espo_mate_step_payload_x_closed_after. (exists wpo_gap_step_payload_x_closed_after_position_bound. wpo_gap_step_payload_x_closed_after_position_bound + S (espo_position_step_payload_x_closed_after) = S (S (m + m))) -> (((exists wpo_beta_height_step_payload_x_closed_after_source_entry. wpo_beta_height_step_payload_x_closed_after_source_entry + S (espo_source_step_payload_x_closed_after) = S ((S (espo_position_step_payload_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_closed_after_source_entry. x = wpo_beta_quotient_step_payload_x_closed_after_source_entry * S ((S (espo_position_step_payload_x_closed_after)) * x1) + (espo_source_step_payload_x_closed_after))) -> (((exists wpo_beta_height_step_payload_x_closed_after_scaled_entry. wpo_beta_height_step_payload_x_closed_after_scaled_entry + S (S espo_mate_step_payload_x_closed_after) = S ((S (espo_source_step_payload_x_closed_after)) * v)) /\ exists wpo_beta_quotient_step_payload_x_closed_after_scaled_entry. u = wpo_beta_quotient_step_payload_x_closed_after_scaled_entry * S ((S (espo_source_step_payload_x_closed_after)) * v) + (S espo_mate_step_payload_x_closed_after))) -> exists espo_mate_position_step_payload_x_closed_after. ((exists wpo_gap_step_payload_x_closed_after_mate_bound. wpo_gap_step_payload_x_closed_after_mate_bound + S (espo_mate_position_step_payload_x_closed_after) = S (S (m + m))) /\ (((exists wpo_beta_height_step_payload_x_closed_after_mate_entry. wpo_beta_height_step_payload_x_closed_after_mate_entry + S (espo_mate_step_payload_x_closed_after) = S ((S (espo_mate_position_step_payload_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_closed_after_mate_entry. x = wpo_beta_quotient_step_payload_x_closed_after_mate_entry * S ((S (espo_mate_position_step_payload_x_closed_after)) * x1) + (espo_mate_step_payload_x_closed_after))))) /\ (forall wpo_injective_left_step_payload_x_injective_after wpo_injective_right_step_payload_x_injective_after wpo_injective_value_step_payload_x_injective_after. (exists wpo_gap_step_payload_x_injective_after_left_bound. wpo_gap_step_payload_x_injective_after_left_bound + S (wpo_injective_left_step_payload_x_injective_after) = S (S (m + m))) -> (exists wpo_gap_step_payload_x_injective_after_right_bound. wpo_gap_step_payload_x_injective_after_right_bound + S (wpo_injective_right_step_payload_x_injective_after) = S (S (m + m))) -> (((exists wpo_beta_height_step_payload_x_injective_after_left_entry. wpo_beta_height_step_payload_x_injective_after_left_entry + S (wpo_injective_value_step_payload_x_injective_after) = S ((S (wpo_injective_left_step_payload_x_injective_after)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_injective_after_left_entry. x = wpo_beta_quotient_step_payload_x_injective_after_left_entry * S ((S (wpo_injective_left_step_payload_x_injective_after)) * x1) + (wpo_injective_value_step_payload_x_injective_after))) -> (((exists wpo_beta_height_step_payload_x_injective_after_right_entry. wpo_beta_height_step_payload_x_injective_after_right_entry + S (wpo_injective_value_step_payload_x_injective_after) = S ((S (wpo_injective_right_step_payload_x_injective_after)) * x1)) /\ exists wpo_beta_quotient_step_payload_x_injective_after_right_entry. x = wpo_beta_quotient_step_payload_x_injective_after_right_entry * S ((S (wpo_injective_right_step_payload_x_injective_after)) * x1) + (wpo_injective_value_step_payload_x_injective_after))) -> wpo_injective_left_step_payload_x_injective_after = wpo_injective_right_step_payload_x_injective_after))))))))))))))))))
  40. 0040exact hraw_witness_witness_witness_witness
  41. 0041cases hparts
  42. 0042cases hparts_right
  43. 0043cases hparts_right_right
  44. 0044cases hparts_right_right_right
  45. 0045cases hparts_right_right_right_right
  46. 0046cases hparts_right_right_right_right_right
  47. 0047cases hparts_right_right_right_right_right_right
  48. 0048cases hparts_right_right_right_right_right_right_right
  49. 0049cases hparts_right_right_right_right_right_right_right_right
  50. 0050have hbounded_after : ∀ fom_index_bounded_after_x. Lt(fom_index_bounded_after_x,S S (m + m)) → ∃ y. BetaAt(x,x1,fom_index_bounded_after_x,y) ∧ Lt(y,n)
    Exact native replay linehave hbounded_after : forall fom_index_bounded_after_x. (exists fom_gap_bounded_after_x_index_bound. fom_gap_bounded_after_x_index_bound + S (fom_index_bounded_after_x) = S (S (m + m))) -> exists fom_value_bounded_after_x. ((((exists fom_beta_height_bounded_after_x_entry. fom_beta_height_bounded_after_x_entry + S (fom_value_bounded_after_x) = S ((S (fom_index_bounded_after_x)) * x1)) /\ exists fom_beta_quotient_bounded_after_x_entry. x = fom_beta_quotient_bounded_after_x_entry * S ((S (fom_index_bounded_after_x)) * x1) + (fom_value_bounded_after_x))) /\ (exists fom_gap_bounded_after_x_value_bound. fom_gap_bounded_after_x_value_bound + S (fom_value_bounded_after_x) = n))
  51. 0051specialize beta_prefix_append_two_bounded_into b
  52. 0052specialize beta_prefix_append_two_bounded_into c
  53. 0053specialize beta_prefix_append_two_bounded_into x
  54. 0054specialize beta_prefix_append_two_bounded_into x1
  55. 0055specialize beta_prefix_append_two_bounded_into (m + m)
  56. 0056specialize beta_prefix_append_two_bounded_into n
  57. 0057specialize beta_prefix_append_two_bounded_into x2
  58. 0058specialize beta_prefix_append_two_bounded_into x3
  59. 0059apply beta_prefix_append_two_bounded_into
  60. 0060exact hparts_left
  61. 0061exact hstate_right_left
  62. 0062exact hparts_right_left
  63. 0063exact hparts_right_right_left
  64. 0064have hhistory_after : ∀ espi_pair_history_after_x. Lt(espi_pair_history_after_x,S m) → ∃ y. ∃ z. BetaAt(x,x1,espi_pair_history_after_x + espi_pair_history_after_x,y) ∧ (BetaAt(x,x1,S (espi_pair_history_after_x + espi_pair_history_after_x),z) ∧ BetaAt(u,v,y,S z))
    Exact native replay linehave hhistory_after : forall espi_pair_history_after_x. (exists wpo_gap_history_after_x_pair_bound. wpo_gap_history_after_x_pair_bound + S (espi_pair_history_after_x) = S m) -> exists espi_left_history_after_x espi_right_history_after_x. (((((exists wpo_beta_height_history_after_x_left_entry. wpo_beta_height_history_after_x_left_entry + S (espi_left_history_after_x) = S ((S (espi_pair_history_after_x + espi_pair_history_after_x)) * x1)) /\ exists wpo_beta_quotient_history_after_x_left_entry. x = wpo_beta_quotient_history_after_x_left_entry * S ((S (espi_pair_history_after_x + espi_pair_history_after_x)) * x1) + (espi_left_history_after_x))) /\ (((((exists wpo_beta_height_history_after_x_right_entry. wpo_beta_height_history_after_x_right_entry + S (espi_right_history_after_x) = S ((S (S (espi_pair_history_after_x + espi_pair_history_after_x))) * x1)) /\ exists wpo_beta_quotient_history_after_x_right_entry. x = wpo_beta_quotient_history_after_x_right_entry * S ((S (S (espi_pair_history_after_x + espi_pair_history_after_x))) * x1) + (espi_right_history_after_x))) /\ (((exists wpo_beta_height_history_after_x_scaled_edge. wpo_beta_height_history_after_x_scaled_edge + S (S espi_right_history_after_x) = S ((S (espi_left_history_after_x)) * v)) /\ exists wpo_beta_quotient_history_after_x_scaled_edge. u = wpo_beta_quotient_history_after_x_scaled_edge * S ((S (espi_left_history_after_x)) * v) + (S espi_right_history_after_x)))))))
  65. 0065specialize adjacent_scaled_orbit_history_append u
  66. 0066specialize adjacent_scaled_orbit_history_append v
  67. 0067specialize adjacent_scaled_orbit_history_append b
  68. 0068specialize adjacent_scaled_orbit_history_append c
  69. 0069specialize adjacent_scaled_orbit_history_append x
  70. 0070specialize adjacent_scaled_orbit_history_append x1
  71. 0071specialize adjacent_scaled_orbit_history_append m
  72. 0072specialize adjacent_scaled_orbit_history_append x2
  73. 0073specialize adjacent_scaled_orbit_history_append x3
  74. 0074apply adjacent_scaled_orbit_history_append
  75. 0075exact hhistory
  76. 0076exact hparts_left
  77. 0077exact hparts_right_right_right_right_right_right_left
  78. 0078have hstate_after : (∀ y. ∀ z. ∀ k. Lt(y,S S (m + m)) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,S k) → ContainsPrefix(x,x1,S S (m + m),k)) ∧ ((∀ y. Lt(y,S S (m + m)) → ∃ z. BetaAt(x,x1,y,z) ∧ Lt(z,n)) ∧ InjectivePrefix(x,x1,S S (m + m)))
    Exact native replay linehave hstate_after : ((forall espo_position_state_after_x_closed espo_source_state_after_x_closed espo_mate_state_after_x_closed. (exists wpo_gap_state_after_x_closed_position_bound. wpo_gap_state_after_x_closed_position_bound + S (espo_position_state_after_x_closed) = S (S (m + m))) -> (((exists wpo_beta_height_state_after_x_closed_source_entry. wpo_beta_height_state_after_x_closed_source_entry + S (espo_source_state_after_x_closed) = S ((S (espo_position_state_after_x_closed)) * x1)) /\ exists wpo_beta_quotient_state_after_x_closed_source_entry. x = wpo_beta_quotient_state_after_x_closed_source_entry * S ((S (espo_position_state_after_x_closed)) * x1) + (espo_source_state_after_x_closed))) -> (((exists wpo_beta_height_state_after_x_closed_scaled_entry. wpo_beta_height_state_after_x_closed_scaled_entry + S (S espo_mate_state_after_x_closed) = S ((S (espo_source_state_after_x_closed)) * v)) /\ exists wpo_beta_quotient_state_after_x_closed_scaled_entry. u = wpo_beta_quotient_state_after_x_closed_scaled_entry * S ((S (espo_source_state_after_x_closed)) * v) + (S espo_mate_state_after_x_closed))) -> exists espo_mate_position_state_after_x_closed. ((exists wpo_gap_state_after_x_closed_mate_bound. wpo_gap_state_after_x_closed_mate_bound + S (espo_mate_position_state_after_x_closed) = S (S (m + m))) /\ (((exists wpo_beta_height_state_after_x_closed_mate_entry. wpo_beta_height_state_after_x_closed_mate_entry + S (espo_mate_state_after_x_closed) = S ((S (espo_mate_position_state_after_x_closed)) * x1)) /\ exists wpo_beta_quotient_state_after_x_closed_mate_entry. x = wpo_beta_quotient_state_after_x_closed_mate_entry * S ((S (espo_mate_position_state_after_x_closed)) * x1) + (espo_mate_state_after_x_closed))))) /\ (((forall fom_index_state_after_x_bounded. (exists fom_gap_state_after_x_bounded_index_bound. fom_gap_state_after_x_bounded_index_bound + S (fom_index_state_after_x_bounded) = S (S (m + m))) -> exists fom_value_state_after_x_bounded. ((((exists fom_beta_height_state_after_x_bounded_entry. fom_beta_height_state_after_x_bounded_entry + S (fom_value_state_after_x_bounded) = S ((S (fom_index_state_after_x_bounded)) * x1)) /\ exists fom_beta_quotient_state_after_x_bounded_entry. x = fom_beta_quotient_state_after_x_bounded_entry * S ((S (fom_index_state_after_x_bounded)) * x1) + (fom_value_state_after_x_bounded))) /\ (exists fom_gap_state_after_x_bounded_value_bound. fom_gap_state_after_x_bounded_value_bound + S (fom_value_state_after_x_bounded) = n))) /\ (forall wpo_injective_left_state_after_x_injective wpo_injective_right_state_after_x_injective wpo_injective_value_state_after_x_injective. (exists wpo_gap_state_after_x_injective_left_bound. wpo_gap_state_after_x_injective_left_bound + S (wpo_injective_left_state_after_x_injective) = S (S (m + m))) -> (exists wpo_gap_state_after_x_injective_right_bound. wpo_gap_state_after_x_injective_right_bound + S (wpo_injective_right_state_after_x_injective) = S (S (m + m))) -> (((exists wpo_beta_height_state_after_x_injective_left_entry. wpo_beta_height_state_after_x_injective_left_entry + S (wpo_injective_value_state_after_x_injective) = S ((S (wpo_injective_left_state_after_x_injective)) * x1)) /\ exists wpo_beta_quotient_state_after_x_injective_left_entry. x = wpo_beta_quotient_state_after_x_injective_left_entry * S ((S (wpo_injective_left_state_after_x_injective)) * x1) + (wpo_injective_value_state_after_x_injective))) -> (((exists wpo_beta_height_state_after_x_injective_right_entry. wpo_beta_height_state_after_x_injective_right_entry + S (wpo_injective_value_state_after_x_injective) = S ((S (wpo_injective_right_state_after_x_injective)) * x1)) /\ exists wpo_beta_quotient_state_after_x_injective_right_entry. x = wpo_beta_quotient_state_after_x_injective_right_entry * S ((S (wpo_injective_right_state_after_x_injective)) * x1) + (wpo_injective_value_state_after_x_injective))) -> wpo_injective_left_state_after_x_injective = wpo_injective_right_state_after_x_injective))))
  79. 0079split
  80. 0080exact hparts_right_right_right_right_right_right_right_right_left
  81. 0081split
  82. 0082exact hbounded_after
  83. 0083exact hparts_right_right_right_right_right_right_right_right_right
  84. 0084exists x
  85. 0085exists x1
  86. 0086split
  87. 0087exact hstate_after
  88. 0088exact hhistory_after