PA00AX · theorem

prime_pair_order_choose_append_state

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

Thread the complete bounded PairOrder state through one fresh inverse-orbit append.

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. ∀ b. ∀ c. ∀ l. ∀ r. p = S n → Prime(p) → InversePrefix(p,n,u,v,n) → n = S r → Lt(S S l,n) → (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,y,z) → ContainsPrefix(b,c,l,z)) → (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → ¬y = 0 ∧ ¬S y = n) → InjectivePrefix(b,c,l) → ∃ x. ∃ y. ∃ z. ∃ m. BetaAt(x,y,l,z) ∧ (BetaAt(x,y,S l,m) ∧ (∀ k. ∀ i. Lt(k,l) → BetaAt(b,c,k,i) → BetaAt(x,y,k,i))) ∧ (Lt(z,n) ∧ (¬z = 0 ∧ ¬S z = n ∧ (¬ContainsPrefix(b,c,l,z) ∧ (BetaAt(u,v,z,m) ∧ (Lt(m,n) ∧ (¬m = 0 ∧ ¬S m = n ∧ (¬z = m ∧ (BetaAt(u,v,m,z) ∧ (¬ContainsPrefix(b,c,l,m) ∧ ((∀ k. ∀ i. ∀ j. Lt(k,S S l) → BetaAt(x,y,k,i) → BetaAt(u,v,i,j) → ContainsPrefix(x,y,S S l,j)) ∧ (∀ k. ∀ i. Lt(k,S S l) → BetaAt(x,y,k,i) → ¬i = 0 ∧ ¬S i = n))))))))))) ∧ ((∀ k. Lt(k,S S l) → ∃ i. BetaAt(x,y,k,i) ∧ Lt(i,n)) ∧ InjectivePrefix(x,y,S S l))

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

34 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

56 occurrences

Exact expanded native-PA statement
forall p n u v b c l r. p = S n -> ((~(p = 1) /\ forall wip_prime_left_wpoi_step_prime wip_prime_right_wpoi_step_prime. p = wip_prime_left_wpoi_step_prime * wip_prime_right_wpoi_step_prime -> wip_prime_left_wpoi_step_prime = 1 \/ wip_prime_right_wpoi_step_prime = 1)) -> (forall wip_index_wpoi_step_inverse. (exists wip_gap_wpoi_step_inverse_prefix_bound. wip_gap_wpoi_step_inverse_prefix_bound + S wip_index_wpoi_step_inverse = n) -> exists wip_mate_wpoi_step_inverse. ((((exists wip_beta_height_wpoi_step_inverse_decoded. wip_beta_height_wpoi_step_inverse_decoded + S (wip_mate_wpoi_step_inverse) = S ((S (wip_index_wpoi_step_inverse)) * v)) /\ exists wip_beta_quotient_wpoi_step_inverse_decoded. u = wip_beta_quotient_wpoi_step_inverse_decoded * S ((S (wip_index_wpoi_step_inverse)) * v) + (wip_mate_wpoi_step_inverse))) /\ ((exists wip_gap_wpoi_step_inverse_inverse_index_bound. wip_gap_wpoi_step_inverse_inverse_index_bound + S wip_index_wpoi_step_inverse = n) /\ ((exists wip_gap_wpoi_step_inverse_inverse_mate_bound. wip_gap_wpoi_step_inverse_inverse_mate_bound + S wip_mate_wpoi_step_inverse = n) /\ (exists wip_mod_left_wpoi_step_inverse_inverse_mod wip_mod_right_wpoi_step_inverse_inverse_mod. ((S wip_index_wpoi_step_inverse) * S wip_mate_wpoi_step_inverse) + p * wip_mod_left_wpoi_step_inverse_inverse_mod = 1 + p * wip_mod_right_wpoi_step_inverse_inverse_mod))))) -> n = S r -> (exists h. h + S (S (S l)) = n) -> (forall wpo_position_wpoi_step_closed_before wpo_source_wpoi_step_closed_before wpo_mate_wpoi_step_closed_before. (exists wpo_gap_wpoi_step_closed_before_position_bound. wpo_gap_wpoi_step_closed_before_position_bound + S (wpo_position_wpoi_step_closed_before) = l) -> (((exists wpo_beta_height_wpoi_step_closed_before_source_entry. wpo_beta_height_wpoi_step_closed_before_source_entry + S (wpo_source_wpoi_step_closed_before) = S ((S (wpo_position_wpoi_step_closed_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_closed_before_source_entry. b = wpo_beta_quotient_wpoi_step_closed_before_source_entry * S ((S (wpo_position_wpoi_step_closed_before)) * c) + (wpo_source_wpoi_step_closed_before))) -> (((exists wpo_beta_height_wpoi_step_closed_before_inverse_entry. wpo_beta_height_wpoi_step_closed_before_inverse_entry + S (wpo_mate_wpoi_step_closed_before) = S ((S (wpo_source_wpoi_step_closed_before)) * v)) /\ exists wpo_beta_quotient_wpoi_step_closed_before_inverse_entry. u = wpo_beta_quotient_wpoi_step_closed_before_inverse_entry * S ((S (wpo_source_wpoi_step_closed_before)) * v) + (wpo_mate_wpoi_step_closed_before))) -> exists wpo_mate_position_wpoi_step_closed_before. ((exists wpo_gap_wpoi_step_closed_before_mate_bound. wpo_gap_wpoi_step_closed_before_mate_bound + S (wpo_mate_position_wpoi_step_closed_before) = l) /\ (((exists wpo_beta_height_wpoi_step_closed_before_mate_entry. wpo_beta_height_wpoi_step_closed_before_mate_entry + S (wpo_mate_wpoi_step_closed_before) = S ((S (wpo_mate_position_wpoi_step_closed_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_closed_before_mate_entry. b = wpo_beta_quotient_wpoi_step_closed_before_mate_entry * S ((S (wpo_mate_position_wpoi_step_closed_before)) * c) + (wpo_mate_wpoi_step_closed_before))))) -> (forall fom_index_wpoi_step_bounded_before. (exists fom_gap_wpoi_step_bounded_before_index_bound. fom_gap_wpoi_step_bounded_before_index_bound + S (fom_index_wpoi_step_bounded_before) = l) -> exists fom_value_wpoi_step_bounded_before. ((((exists fom_beta_height_wpoi_step_bounded_before_entry. fom_beta_height_wpoi_step_bounded_before_entry + S (fom_value_wpoi_step_bounded_before) = S ((S (fom_index_wpoi_step_bounded_before)) * c)) /\ exists fom_beta_quotient_wpoi_step_bounded_before_entry. b = fom_beta_quotient_wpoi_step_bounded_before_entry * S ((S (fom_index_wpoi_step_bounded_before)) * c) + (fom_value_wpoi_step_bounded_before))) /\ (exists fom_gap_wpoi_step_bounded_before_value_bound. fom_gap_wpoi_step_bounded_before_value_bound + S (fom_value_wpoi_step_bounded_before) = n))) -> (forall wpo_position_wpoi_step_nonendpoint_before wpo_value_wpoi_step_nonendpoint_before. (exists wpo_gap_wpoi_step_nonendpoint_before_position_bound. wpo_gap_wpoi_step_nonendpoint_before_position_bound + S (wpo_position_wpoi_step_nonendpoint_before) = l) -> (((exists wpo_beta_height_wpoi_step_nonendpoint_before_entry. wpo_beta_height_wpoi_step_nonendpoint_before_entry + S (wpo_value_wpoi_step_nonendpoint_before) = S ((S (wpo_position_wpoi_step_nonendpoint_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_nonendpoint_before_entry. b = wpo_beta_quotient_wpoi_step_nonendpoint_before_entry * S ((S (wpo_position_wpoi_step_nonendpoint_before)) * c) + (wpo_value_wpoi_step_nonendpoint_before))) -> (~(wpo_value_wpoi_step_nonendpoint_before = 0) /\ ~((S wpo_value_wpoi_step_nonendpoint_before) = n))) -> (forall wpo_injective_left_wpoi_step_injective_before wpo_injective_right_wpoi_step_injective_before wpo_injective_value_wpoi_step_injective_before. (exists wpo_gap_wpoi_step_injective_before_left_bound. wpo_gap_wpoi_step_injective_before_left_bound + S (wpo_injective_left_wpoi_step_injective_before) = l) -> (exists wpo_gap_wpoi_step_injective_before_right_bound. wpo_gap_wpoi_step_injective_before_right_bound + S (wpo_injective_right_wpoi_step_injective_before) = l) -> (((exists wpo_beta_height_wpoi_step_injective_before_left_entry. wpo_beta_height_wpoi_step_injective_before_left_entry + S (wpo_injective_value_wpoi_step_injective_before) = S ((S (wpo_injective_left_wpoi_step_injective_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_injective_before_left_entry. b = wpo_beta_quotient_wpoi_step_injective_before_left_entry * S ((S (wpo_injective_left_wpoi_step_injective_before)) * c) + (wpo_injective_value_wpoi_step_injective_before))) -> (((exists wpo_beta_height_wpoi_step_injective_before_right_entry. wpo_beta_height_wpoi_step_injective_before_right_entry + S (wpo_injective_value_wpoi_step_injective_before) = S ((S (wpo_injective_right_wpoi_step_injective_before)) * c)) /\ exists wpo_beta_quotient_wpoi_step_injective_before_right_entry. b = wpo_beta_quotient_wpoi_step_injective_before_right_entry * S ((S (wpo_injective_right_wpoi_step_injective_before)) * c) + (wpo_injective_value_wpoi_step_injective_before))) -> wpo_injective_left_wpoi_step_injective_before = wpo_injective_right_wpoi_step_injective_before) -> (exists z d i j. ((((((((exists wpo_beta_height_wpoi_step_body_trace_first. wpo_beta_height_wpoi_step_body_trace_first + S (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_first. z = wpo_beta_quotient_wpoi_step_body_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_wpoi_step_body_trace_second. wpo_beta_height_wpoi_step_body_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_second. z = wpo_beta_quotient_wpoi_step_body_trace_second * S ((S (S (l))) * d) + (j))) /\ (forall wpo_old_index_wpoi_step_body_trace wpo_old_value_wpoi_step_body_trace. (exists wpo_gap_wpoi_step_body_trace_old_bound. wpo_gap_wpoi_step_body_trace_old_bound + S (wpo_old_index_wpoi_step_body_trace) = l) -> (((exists wpo_beta_height_wpoi_step_body_trace_old_entry. wpo_beta_height_wpoi_step_body_trace_old_entry + S (wpo_old_value_wpoi_step_body_trace) = S ((S (wpo_old_index_wpoi_step_body_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_old_entry. b = wpo_beta_quotient_wpoi_step_body_trace_old_entry * S ((S (wpo_old_index_wpoi_step_body_trace)) * c) + (wpo_old_value_wpoi_step_body_trace))) -> (((exists wpo_beta_height_wpoi_step_body_trace_new_entry. wpo_beta_height_wpoi_step_body_trace_new_entry + S (wpo_old_value_wpoi_step_body_trace) = S ((S (wpo_old_index_wpoi_step_body_trace)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_new_entry. z = wpo_beta_quotient_wpoi_step_body_trace_new_entry * S ((S (wpo_old_index_wpoi_step_body_trace)) * d) + (wpo_old_value_wpoi_step_body_trace))))))) /\ ((exists wpo_gap_wpoi_step_body_source_bound. wpo_gap_wpoi_step_body_source_bound + S (i) = n) /\ ((~(i = 0) /\ ~((S i) = n)) /\ ((~(exists wpo_index_wpoi_step_body_source_omit_contains. ((exists wpo_gap_wpoi_step_body_source_omit_contains_bound. wpo_gap_wpoi_step_body_source_omit_contains_bound + S (wpo_index_wpoi_step_body_source_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_source_omit_contains_entry. wpo_beta_height_wpoi_step_body_source_omit_contains_entry + S (i) = S ((S (wpo_index_wpoi_step_body_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_source_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_source_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_source_omit_contains)) * c) + (i)))))) /\ ((((exists wpo_beta_height_wpoi_step_body_forward. wpo_beta_height_wpoi_step_body_forward + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_forward. u = wpo_beta_quotient_wpoi_step_body_forward * S ((S (i)) * v) + (j))) /\ ((exists wpo_gap_wpoi_step_body_mate_bound. wpo_gap_wpoi_step_body_mate_bound + S (j) = n) /\ ((~(j = 0) /\ ~((S j) = n)) /\ (~(i = j) /\ ((((exists wpo_beta_height_wpoi_step_body_back. wpo_beta_height_wpoi_step_body_back + S (i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_back. u = wpo_beta_quotient_wpoi_step_body_back * S ((S (j)) * v) + (i))) /\ ((~(exists wpo_index_wpoi_step_body_mate_omit_contains. ((exists wpo_gap_wpoi_step_body_mate_omit_contains_bound. wpo_gap_wpoi_step_body_mate_omit_contains_bound + S (wpo_index_wpoi_step_body_mate_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_mate_omit_contains_entry. wpo_beta_height_wpoi_step_body_mate_omit_contains_entry + S (j) = S ((S (wpo_index_wpoi_step_body_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_mate_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_mate_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_mate_omit_contains)) * c) + (j)))))) /\ ((forall wpo_position_wpoi_step_body_closed_after wpo_source_wpoi_step_body_closed_after wpo_mate_wpoi_step_body_closed_after. (exists wpo_gap_wpoi_step_body_closed_after_position_bound. wpo_gap_wpoi_step_body_closed_after_position_bound + S (wpo_position_wpoi_step_body_closed_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_closed_after_source_entry. wpo_beta_height_wpoi_step_body_closed_after_source_entry + S (wpo_source_wpoi_step_body_closed_after) = S ((S (wpo_position_wpoi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_source_entry. z = wpo_beta_quotient_wpoi_step_body_closed_after_source_entry * S ((S (wpo_position_wpoi_step_body_closed_after)) * d) + (wpo_source_wpoi_step_body_closed_after))) -> (((exists wpo_beta_height_wpoi_step_body_closed_after_inverse_entry. wpo_beta_height_wpoi_step_body_closed_after_inverse_entry + S (wpo_mate_wpoi_step_body_closed_after) = S ((S (wpo_source_wpoi_step_body_closed_after)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_inverse_entry. u = wpo_beta_quotient_wpoi_step_body_closed_after_inverse_entry * S ((S (wpo_source_wpoi_step_body_closed_after)) * v) + (wpo_mate_wpoi_step_body_closed_after))) -> exists wpo_mate_position_wpoi_step_body_closed_after. ((exists wpo_gap_wpoi_step_body_closed_after_mate_bound. wpo_gap_wpoi_step_body_closed_after_mate_bound + S (wpo_mate_position_wpoi_step_body_closed_after) = S (S l)) /\ (((exists wpo_beta_height_wpoi_step_body_closed_after_mate_entry. wpo_beta_height_wpoi_step_body_closed_after_mate_entry + S (wpo_mate_wpoi_step_body_closed_after) = S ((S (wpo_mate_position_wpoi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_mate_entry. z = wpo_beta_quotient_wpoi_step_body_closed_after_mate_entry * S ((S (wpo_mate_position_wpoi_step_body_closed_after)) * d) + (wpo_mate_wpoi_step_body_closed_after))))) /\ (forall wpo_position_wpoi_step_body_nonendpoint_after wpo_value_wpoi_step_body_nonendpoint_after. (exists wpo_gap_wpoi_step_body_nonendpoint_after_position_bound. wpo_gap_wpoi_step_body_nonendpoint_after_position_bound + S (wpo_position_wpoi_step_body_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_nonendpoint_after_entry. wpo_beta_height_wpoi_step_body_nonendpoint_after_entry + S (wpo_value_wpoi_step_body_nonendpoint_after) = S ((S (wpo_position_wpoi_step_body_nonendpoint_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_nonendpoint_after_entry. z = wpo_beta_quotient_wpoi_step_body_nonendpoint_after_entry * S ((S (wpo_position_wpoi_step_body_nonendpoint_after)) * d) + (wpo_value_wpoi_step_body_nonendpoint_after))) -> (~(wpo_value_wpoi_step_body_nonendpoint_after = 0) /\ ~((S wpo_value_wpoi_step_body_nonendpoint_after) = n))))))))))))))) /\ ((forall fom_index_wpoi_step_bounded_after. (exists fom_gap_wpoi_step_bounded_after_index_bound. fom_gap_wpoi_step_bounded_after_index_bound + S (fom_index_wpoi_step_bounded_after) = S (S l)) -> exists fom_value_wpoi_step_bounded_after. ((((exists fom_beta_height_wpoi_step_bounded_after_entry. fom_beta_height_wpoi_step_bounded_after_entry + S (fom_value_wpoi_step_bounded_after) = S ((S (fom_index_wpoi_step_bounded_after)) * d)) /\ exists fom_beta_quotient_wpoi_step_bounded_after_entry. z = fom_beta_quotient_wpoi_step_bounded_after_entry * S ((S (fom_index_wpoi_step_bounded_after)) * d) + (fom_value_wpoi_step_bounded_after))) /\ (exists fom_gap_wpoi_step_bounded_after_value_bound. fom_gap_wpoi_step_bounded_after_value_bound + S (fom_value_wpoi_step_bounded_after) = n))) /\ (forall wpo_injective_left_wpoi_step_injective_after wpo_injective_right_wpoi_step_injective_after wpo_injective_value_wpoi_step_injective_after. (exists wpo_gap_wpoi_step_injective_after_left_bound. wpo_gap_wpoi_step_injective_after_left_bound + S (wpo_injective_left_wpoi_step_injective_after) = S (S l)) -> (exists wpo_gap_wpoi_step_injective_after_right_bound. wpo_gap_wpoi_step_injective_after_right_bound + S (wpo_injective_right_wpoi_step_injective_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_injective_after_left_entry. wpo_beta_height_wpoi_step_injective_after_left_entry + S (wpo_injective_value_wpoi_step_injective_after) = S ((S (wpo_injective_left_wpoi_step_injective_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_left_entry. z = wpo_beta_quotient_wpoi_step_injective_after_left_entry * S ((S (wpo_injective_left_wpoi_step_injective_after)) * d) + (wpo_injective_value_wpoi_step_injective_after))) -> (((exists wpo_beta_height_wpoi_step_injective_after_right_entry. wpo_beta_height_wpoi_step_injective_after_right_entry + S (wpo_injective_value_wpoi_step_injective_after) = S ((S (wpo_injective_right_wpoi_step_injective_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_right_entry. z = wpo_beta_quotient_wpoi_step_injective_after_right_entry * S ((S (wpo_injective_right_wpoi_step_injective_after)) * d) + (wpo_injective_value_wpoi_step_injective_after))) -> wpo_injective_left_wpoi_step_injective_after = wpo_injective_right_wpoi_step_injective_after))))

Proof neighborhood

Direct theorem prerequisites

PA00AW prime_pair_order_choose_append_injective PA009P beta_prefix_append_two_bounded_into

Direct theorem dependents

PA00B0 prime_pair_order_paired_state_step

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

73 script commands · 16 reading checkpoints · 4 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 (2)
prime pair order choose append injectivebeta prefix append two bounded into
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 b
  6. L6
    intro c
  7. L7
    intro l
  8. L8
    intro r
  9. L9
    intro hpn
  10. L10
    intro hp
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hprefix
  2. L12
    intro hnr
  3. L13
    intro hshort
  4. L14
    intro hclosed
  5. L15
    intro hbounded
  6. L16
    intro hnonendpoint
  7. L17
    intro hinjective
03Establish hstepL18–27

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

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

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

  1. L28
    exact hpn
  2. L29
    exact hp
  3. L30
    exact hprefix
  4. L31
    exact hnr
  5. L32
    exact hshort
  6. L33
    exact hclosed
  7. L34
    exact hnonendpoint
  8. L35
    exact hinjective
05Separate the logical casesL36–39

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

  1. L36
    cases hstep
  2. L37
    cases hstep_witness
  3. L38
    cases hstep_witness_witness
  4. L39
    cases hstep_witness_witness_witness
06Establish hcombinedL40–41

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

  1. L40
    have hcombined : BetaAt(x,x1,l,x2) ∧ (BetaAt(x,x1,S l,x3) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(b,c,y,z) → BetaAt(x,x1,y,z))) ∧ (Lt(x2,n) ∧ (¬x2 = 0 ∧ ¬S x2 = n ∧ (¬ContainsPrefix(b,c,l,x2) ∧ (BetaAt(u,v,x2,x3) ∧ (Lt(x3,n) ∧ (¬x3 = 0 ∧ ¬S x3 = n ∧ (¬x2 = x3 ∧ (BetaAt(u,v,x3,x2) ∧ (¬ContainsPrefix(b,c,l,x3) ∧ ((∀ y. ∀ z. ∀ m. Lt(y,S S l) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,m) → ContainsPrefix(x,x1,S S l,m)) ∧ (∀ y. ∀ z. Lt(y,S S l) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = n))))))))))) ∧ InjectivePrefix(x,x1,S S l)Definitions: BetaAt(x,x1,l,x2)BetaAt(x,x1,S l,x3)Lt(y,l)BetaAt(b,c,y,z)BetaAt(x,x1,y,z)Lt(x2,n)ContainsPrefix(b,c,l,x2)BetaAt(u,v,x2,x3)Lt(x3,n)BetaAt(u,v,x3,x2)ContainsPrefix(b,c,l,x3)Lt(y,S S l)BetaAt(u,v,z,m)ContainsPrefix(x,x1,S S l,m)InjectivePrefix(x,x1,S S l)Original native command in the exact edition
  2. L41
    exact hstep_witness_witness_witness_witness
07Separate the logical casesL42–42

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

  1. L42
    cases hcombined
08Establish hpartsL43–44

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

  1. L43
    have hparts : BetaAt(x,x1,l,x2) ∧ (BetaAt(x,x1,S l,x3) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(b,c,y,z) → BetaAt(x,x1,y,z))) ∧ (Lt(x2,n) ∧ (¬x2 = 0 ∧ ¬S x2 = n ∧ (¬ContainsPrefix(b,c,l,x2) ∧ (BetaAt(u,v,x2,x3) ∧ (Lt(x3,n) ∧ (¬x3 = 0 ∧ ¬S x3 = n ∧ (¬x2 = x3 ∧ (BetaAt(u,v,x3,x2) ∧ (¬ContainsPrefix(b,c,l,x3) ∧ ((∀ y. ∀ z. ∀ m. Lt(y,S S l) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,m) → ContainsPrefix(x,x1,S S l,m)) ∧ (∀ y. ∀ z. Lt(y,S S l) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = n)))))))))))Definitions: BetaAt(x,x1,l,x2)BetaAt(x,x1,S l,x3)Lt(y,l)BetaAt(b,c,y,z)BetaAt(x,x1,y,z)Lt(x2,n)ContainsPrefix(b,c,l,x2)BetaAt(u,v,x2,x3)Lt(x3,n)BetaAt(u,v,x3,x2)ContainsPrefix(b,c,l,x3)Lt(y,S S l)BetaAt(u,v,z,m)ContainsPrefix(x,x1,S S l,m)Original native command in the exact edition
  2. L44
    exact hcombined_left
09Separate the logical casesL45–50

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

  1. L45
    cases hparts
  2. L46
    cases hparts_right
  3. L47
    cases hparts_right_right
  4. L48
    cases hparts_right_right_right
  5. L49
    cases hparts_right_right_right_right
  6. L50
    cases hparts_right_right_right_right_right
10Establish hnew_boundedL51–60

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. L51
    have hnew_bounded : ∀ fom_index_wpoi_step_bounded_after_x. Lt(fom_index_wpoi_step_bounded_after_x,S S l) → ∃ y. BetaAt(x,x1,fom_index_wpoi_step_bounded_after_x,y) ∧ Lt(y,n)Definitions: Lt(fom_index_wpoi_step_bounded_after_x,S S l)BetaAt(x,x1,fom_index_wpoi_step_bounded_after_x,y)Lt(y,n)Original native command in the exact edition
  2. L52
    specialize beta_prefix_append_two_bounded_into b
  3. L53
    specialize beta_prefix_append_two_bounded_into c
  4. L54
    specialize beta_prefix_append_two_bounded_into x
  5. L55
    specialize beta_prefix_append_two_bounded_into x1
  6. L56
    specialize beta_prefix_append_two_bounded_into l
  7. L57
    specialize beta_prefix_append_two_bounded_into n
  8. L58
    specialize beta_prefix_append_two_bounded_into x2
  9. L59
    specialize beta_prefix_append_two_bounded_into x3
  10. L60
    apply beta_prefix_append_two_bounded_into
11Use earlier factsL61–64

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

  1. L61
    exact hparts_left
  2. L62
    exact hbounded
  3. L63
    exact hparts_right_left
  4. L64
    exact hparts_right_right_right_right_right_left
12Construct an explicit witnessL65–68

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

  1. L65
    exists x
  2. L66
    exists x1
  3. L67
    exists x2
  4. L68
    exists x3
13Separate the logical casesL69–69

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

  1. L69
    split
14Use earlier factsL70–70

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

  1. L70
    exact hcombined_left
15Separate the logical casesL71–71

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

  1. L71
    split
16Use earlier factsL72–73

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

  1. L72
    exact hnew_bounded
  2. L73
    exact hcombined_right

Library-wide reading audit

Original defined command ledger · 73 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro b
  6. 0006intro c
  7. 0007intro l
  8. 0008intro r
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hprefix
  12. 0012intro hnr
  13. 0013intro hshort
  14. 0014intro hclosed
  15. 0015intro hbounded
  16. 0016intro hnonendpoint
  17. 0017intro hinjective
  18. 0018have hstep : ∃ z. ∃ d. ∃ i. ∃ j. BetaAt(z,d,l,i) ∧ (BetaAt(z,d,S l,j) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y))) ∧ (Lt(i,n) ∧ (¬i = 0 ∧ ¬S i = n ∧ (¬ContainsPrefix(b,c,l,i) ∧ (BetaAt(u,v,i,j) ∧ (Lt(j,n) ∧ (¬j = 0 ∧ ¬S j = n ∧ (¬i = j ∧ (BetaAt(u,v,j,i) ∧ (¬ContainsPrefix(b,c,l,j) ∧ ((∀ x. ∀ y. ∀ m. Lt(x,S S l) → BetaAt(z,d,x,y) → BetaAt(u,v,y,m) → ContainsPrefix(z,d,S S l,m)) ∧ (∀ x. ∀ y. Lt(x,S S l) → BetaAt(z,d,x,y) → ¬y = 0 ∧ ¬S y = n))))))))))) ∧ InjectivePrefix(z,d,S S l)
    Exact native replay linehave hstep : exists z d i j. ((((((((exists wpo_beta_height_wpoi_step_body_trace_first. wpo_beta_height_wpoi_step_body_trace_first + S (i) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_first. z = wpo_beta_quotient_wpoi_step_body_trace_first * S ((S (l)) * d) + (i))) /\ ((((exists wpo_beta_height_wpoi_step_body_trace_second. wpo_beta_height_wpoi_step_body_trace_second + S (j) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_second. z = wpo_beta_quotient_wpoi_step_body_trace_second * S ((S (S (l))) * d) + (j))) /\ (forall wpo_old_index_wpoi_step_body_trace wpo_old_value_wpoi_step_body_trace. (exists wpo_gap_wpoi_step_body_trace_old_bound. wpo_gap_wpoi_step_body_trace_old_bound + S (wpo_old_index_wpoi_step_body_trace) = l) -> (((exists wpo_beta_height_wpoi_step_body_trace_old_entry. wpo_beta_height_wpoi_step_body_trace_old_entry + S (wpo_old_value_wpoi_step_body_trace) = S ((S (wpo_old_index_wpoi_step_body_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_old_entry. b = wpo_beta_quotient_wpoi_step_body_trace_old_entry * S ((S (wpo_old_index_wpoi_step_body_trace)) * c) + (wpo_old_value_wpoi_step_body_trace))) -> (((exists wpo_beta_height_wpoi_step_body_trace_new_entry. wpo_beta_height_wpoi_step_body_trace_new_entry + S (wpo_old_value_wpoi_step_body_trace) = S ((S (wpo_old_index_wpoi_step_body_trace)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_trace_new_entry. z = wpo_beta_quotient_wpoi_step_body_trace_new_entry * S ((S (wpo_old_index_wpoi_step_body_trace)) * d) + (wpo_old_value_wpoi_step_body_trace))))))) /\ ((exists wpo_gap_wpoi_step_body_source_bound. wpo_gap_wpoi_step_body_source_bound + S (i) = n) /\ ((~(i = 0) /\ ~((S i) = n)) /\ ((~(exists wpo_index_wpoi_step_body_source_omit_contains. ((exists wpo_gap_wpoi_step_body_source_omit_contains_bound. wpo_gap_wpoi_step_body_source_omit_contains_bound + S (wpo_index_wpoi_step_body_source_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_source_omit_contains_entry. wpo_beta_height_wpoi_step_body_source_omit_contains_entry + S (i) = S ((S (wpo_index_wpoi_step_body_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_source_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_source_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_source_omit_contains)) * c) + (i)))))) /\ ((((exists wpo_beta_height_wpoi_step_body_forward. wpo_beta_height_wpoi_step_body_forward + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_forward. u = wpo_beta_quotient_wpoi_step_body_forward * S ((S (i)) * v) + (j))) /\ ((exists wpo_gap_wpoi_step_body_mate_bound. wpo_gap_wpoi_step_body_mate_bound + S (j) = n) /\ ((~(j = 0) /\ ~((S j) = n)) /\ (~(i = j) /\ ((((exists wpo_beta_height_wpoi_step_body_back. wpo_beta_height_wpoi_step_body_back + S (i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_back. u = wpo_beta_quotient_wpoi_step_body_back * S ((S (j)) * v) + (i))) /\ ((~(exists wpo_index_wpoi_step_body_mate_omit_contains. ((exists wpo_gap_wpoi_step_body_mate_omit_contains_bound. wpo_gap_wpoi_step_body_mate_omit_contains_bound + S (wpo_index_wpoi_step_body_mate_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_mate_omit_contains_entry. wpo_beta_height_wpoi_step_body_mate_omit_contains_entry + S (j) = S ((S (wpo_index_wpoi_step_body_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_mate_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_mate_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_mate_omit_contains)) * c) + (j)))))) /\ ((forall wpo_position_wpoi_step_body_closed_after wpo_source_wpoi_step_body_closed_after wpo_mate_wpoi_step_body_closed_after. (exists wpo_gap_wpoi_step_body_closed_after_position_bound. wpo_gap_wpoi_step_body_closed_after_position_bound + S (wpo_position_wpoi_step_body_closed_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_closed_after_source_entry. wpo_beta_height_wpoi_step_body_closed_after_source_entry + S (wpo_source_wpoi_step_body_closed_after) = S ((S (wpo_position_wpoi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_source_entry. z = wpo_beta_quotient_wpoi_step_body_closed_after_source_entry * S ((S (wpo_position_wpoi_step_body_closed_after)) * d) + (wpo_source_wpoi_step_body_closed_after))) -> (((exists wpo_beta_height_wpoi_step_body_closed_after_inverse_entry. wpo_beta_height_wpoi_step_body_closed_after_inverse_entry + S (wpo_mate_wpoi_step_body_closed_after) = S ((S (wpo_source_wpoi_step_body_closed_after)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_inverse_entry. u = wpo_beta_quotient_wpoi_step_body_closed_after_inverse_entry * S ((S (wpo_source_wpoi_step_body_closed_after)) * v) + (wpo_mate_wpoi_step_body_closed_after))) -> exists wpo_mate_position_wpoi_step_body_closed_after. ((exists wpo_gap_wpoi_step_body_closed_after_mate_bound. wpo_gap_wpoi_step_body_closed_after_mate_bound + S (wpo_mate_position_wpoi_step_body_closed_after) = S (S l)) /\ (((exists wpo_beta_height_wpoi_step_body_closed_after_mate_entry. wpo_beta_height_wpoi_step_body_closed_after_mate_entry + S (wpo_mate_wpoi_step_body_closed_after) = S ((S (wpo_mate_position_wpoi_step_body_closed_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_closed_after_mate_entry. z = wpo_beta_quotient_wpoi_step_body_closed_after_mate_entry * S ((S (wpo_mate_position_wpoi_step_body_closed_after)) * d) + (wpo_mate_wpoi_step_body_closed_after))))) /\ (forall wpo_position_wpoi_step_body_nonendpoint_after wpo_value_wpoi_step_body_nonendpoint_after. (exists wpo_gap_wpoi_step_body_nonendpoint_after_position_bound. wpo_gap_wpoi_step_body_nonendpoint_after_position_bound + S (wpo_position_wpoi_step_body_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_nonendpoint_after_entry. wpo_beta_height_wpoi_step_body_nonendpoint_after_entry + S (wpo_value_wpoi_step_body_nonendpoint_after) = S ((S (wpo_position_wpoi_step_body_nonendpoint_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_body_nonendpoint_after_entry. z = wpo_beta_quotient_wpoi_step_body_nonendpoint_after_entry * S ((S (wpo_position_wpoi_step_body_nonendpoint_after)) * d) + (wpo_value_wpoi_step_body_nonendpoint_after))) -> (~(wpo_value_wpoi_step_body_nonendpoint_after = 0) /\ ~((S wpo_value_wpoi_step_body_nonendpoint_after) = n))))))))))))))) /\ (forall wpo_injective_left_wpoi_step_injective_after wpo_injective_right_wpoi_step_injective_after wpo_injective_value_wpoi_step_injective_after. (exists wpo_gap_wpoi_step_injective_after_left_bound. wpo_gap_wpoi_step_injective_after_left_bound + S (wpo_injective_left_wpoi_step_injective_after) = S (S l)) -> (exists wpo_gap_wpoi_step_injective_after_right_bound. wpo_gap_wpoi_step_injective_after_right_bound + S (wpo_injective_right_wpoi_step_injective_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_injective_after_left_entry. wpo_beta_height_wpoi_step_injective_after_left_entry + S (wpo_injective_value_wpoi_step_injective_after) = S ((S (wpo_injective_left_wpoi_step_injective_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_left_entry. z = wpo_beta_quotient_wpoi_step_injective_after_left_entry * S ((S (wpo_injective_left_wpoi_step_injective_after)) * d) + (wpo_injective_value_wpoi_step_injective_after))) -> (((exists wpo_beta_height_wpoi_step_injective_after_right_entry. wpo_beta_height_wpoi_step_injective_after_right_entry + S (wpo_injective_value_wpoi_step_injective_after) = S ((S (wpo_injective_right_wpoi_step_injective_after)) * d)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_right_entry. z = wpo_beta_quotient_wpoi_step_injective_after_right_entry * S ((S (wpo_injective_right_wpoi_step_injective_after)) * d) + (wpo_injective_value_wpoi_step_injective_after))) -> wpo_injective_left_wpoi_step_injective_after = wpo_injective_right_wpoi_step_injective_after))
  19. 0019specialize prime_pair_order_choose_append_injective p
  20. 0020specialize prime_pair_order_choose_append_injective n
  21. 0021specialize prime_pair_order_choose_append_injective u
  22. 0022specialize prime_pair_order_choose_append_injective v
  23. 0023specialize prime_pair_order_choose_append_injective b
  24. 0024specialize prime_pair_order_choose_append_injective c
  25. 0025specialize prime_pair_order_choose_append_injective l
  26. 0026specialize prime_pair_order_choose_append_injective r
  27. 0027apply prime_pair_order_choose_append_injective
  28. 0028exact hpn
  29. 0029exact hp
  30. 0030exact hprefix
  31. 0031exact hnr
  32. 0032exact hshort
  33. 0033exact hclosed
  34. 0034exact hnonendpoint
  35. 0035exact hinjective
  36. 0036cases hstep
  37. 0037cases hstep_witness
  38. 0038cases hstep_witness_witness
  39. 0039cases hstep_witness_witness_witness
  40. 0040have hcombined : BetaAt(x,x1,l,x2) ∧ (BetaAt(x,x1,S l,x3) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(b,c,y,z) → BetaAt(x,x1,y,z))) ∧ (Lt(x2,n) ∧ (¬x2 = 0 ∧ ¬S x2 = n ∧ (¬ContainsPrefix(b,c,l,x2) ∧ (BetaAt(u,v,x2,x3) ∧ (Lt(x3,n) ∧ (¬x3 = 0 ∧ ¬S x3 = n ∧ (¬x2 = x3 ∧ (BetaAt(u,v,x3,x2) ∧ (¬ContainsPrefix(b,c,l,x3) ∧ ((∀ y. ∀ z. ∀ m. Lt(y,S S l) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,m) → ContainsPrefix(x,x1,S S l,m)) ∧ (∀ y. ∀ z. Lt(y,S S l) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = n))))))))))) ∧ InjectivePrefix(x,x1,S S l)
    Exact native replay linehave hcombined : ((((((((exists wpo_beta_height_wpoi_step_body_x_trace_first. wpo_beta_height_wpoi_step_body_x_trace_first + S (x2) = S ((S (l)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_first. x = wpo_beta_quotient_wpoi_step_body_x_trace_first * S ((S (l)) * x1) + (x2))) /\ ((((exists wpo_beta_height_wpoi_step_body_x_trace_second. wpo_beta_height_wpoi_step_body_x_trace_second + S (x3) = S ((S (S (l))) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_second. x = wpo_beta_quotient_wpoi_step_body_x_trace_second * S ((S (S (l))) * x1) + (x3))) /\ (forall wpo_old_index_wpoi_step_body_x_trace wpo_old_value_wpoi_step_body_x_trace. (exists wpo_gap_wpoi_step_body_x_trace_old_bound. wpo_gap_wpoi_step_body_x_trace_old_bound + S (wpo_old_index_wpoi_step_body_x_trace) = l) -> (((exists wpo_beta_height_wpoi_step_body_x_trace_old_entry. wpo_beta_height_wpoi_step_body_x_trace_old_entry + S (wpo_old_value_wpoi_step_body_x_trace) = S ((S (wpo_old_index_wpoi_step_body_x_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_old_entry. b = wpo_beta_quotient_wpoi_step_body_x_trace_old_entry * S ((S (wpo_old_index_wpoi_step_body_x_trace)) * c) + (wpo_old_value_wpoi_step_body_x_trace))) -> (((exists wpo_beta_height_wpoi_step_body_x_trace_new_entry. wpo_beta_height_wpoi_step_body_x_trace_new_entry + S (wpo_old_value_wpoi_step_body_x_trace) = S ((S (wpo_old_index_wpoi_step_body_x_trace)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_new_entry. x = wpo_beta_quotient_wpoi_step_body_x_trace_new_entry * S ((S (wpo_old_index_wpoi_step_body_x_trace)) * x1) + (wpo_old_value_wpoi_step_body_x_trace))))))) /\ ((exists wpo_gap_wpoi_step_body_x_source_bound. wpo_gap_wpoi_step_body_x_source_bound + S (x2) = n) /\ ((~(x2 = 0) /\ ~((S x2) = n)) /\ ((~(exists wpo_index_wpoi_step_body_x_source_omit_contains. ((exists wpo_gap_wpoi_step_body_x_source_omit_contains_bound. wpo_gap_wpoi_step_body_x_source_omit_contains_bound + S (wpo_index_wpoi_step_body_x_source_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_x_source_omit_contains_entry. wpo_beta_height_wpoi_step_body_x_source_omit_contains_entry + S (x2) = S ((S (wpo_index_wpoi_step_body_x_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_source_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_x_source_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_x_source_omit_contains)) * c) + (x2)))))) /\ ((((exists wpo_beta_height_wpoi_step_body_x_forward. wpo_beta_height_wpoi_step_body_x_forward + S (x3) = S ((S (x2)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_forward. u = wpo_beta_quotient_wpoi_step_body_x_forward * S ((S (x2)) * v) + (x3))) /\ ((exists wpo_gap_wpoi_step_body_x_mate_bound. wpo_gap_wpoi_step_body_x_mate_bound + S (x3) = n) /\ ((~(x3 = 0) /\ ~((S x3) = n)) /\ (~(x2 = x3) /\ ((((exists wpo_beta_height_wpoi_step_body_x_back. wpo_beta_height_wpoi_step_body_x_back + S (x2) = S ((S (x3)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_back. u = wpo_beta_quotient_wpoi_step_body_x_back * S ((S (x3)) * v) + (x2))) /\ ((~(exists wpo_index_wpoi_step_body_x_mate_omit_contains. ((exists wpo_gap_wpoi_step_body_x_mate_omit_contains_bound. wpo_gap_wpoi_step_body_x_mate_omit_contains_bound + S (wpo_index_wpoi_step_body_x_mate_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_x_mate_omit_contains_entry. wpo_beta_height_wpoi_step_body_x_mate_omit_contains_entry + S (x3) = S ((S (wpo_index_wpoi_step_body_x_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_mate_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_x_mate_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_x_mate_omit_contains)) * c) + (x3)))))) /\ ((forall wpo_position_wpoi_step_body_x_closed_after wpo_source_wpoi_step_body_x_closed_after wpo_mate_wpoi_step_body_x_closed_after. (exists wpo_gap_wpoi_step_body_x_closed_after_position_bound. wpo_gap_wpoi_step_body_x_closed_after_position_bound + S (wpo_position_wpoi_step_body_x_closed_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_x_closed_after_source_entry. wpo_beta_height_wpoi_step_body_x_closed_after_source_entry + S (wpo_source_wpoi_step_body_x_closed_after) = S ((S (wpo_position_wpoi_step_body_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_source_entry. x = wpo_beta_quotient_wpoi_step_body_x_closed_after_source_entry * S ((S (wpo_position_wpoi_step_body_x_closed_after)) * x1) + (wpo_source_wpoi_step_body_x_closed_after))) -> (((exists wpo_beta_height_wpoi_step_body_x_closed_after_inverse_entry. wpo_beta_height_wpoi_step_body_x_closed_after_inverse_entry + S (wpo_mate_wpoi_step_body_x_closed_after) = S ((S (wpo_source_wpoi_step_body_x_closed_after)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_inverse_entry. u = wpo_beta_quotient_wpoi_step_body_x_closed_after_inverse_entry * S ((S (wpo_source_wpoi_step_body_x_closed_after)) * v) + (wpo_mate_wpoi_step_body_x_closed_after))) -> exists wpo_mate_position_wpoi_step_body_x_closed_after. ((exists wpo_gap_wpoi_step_body_x_closed_after_mate_bound. wpo_gap_wpoi_step_body_x_closed_after_mate_bound + S (wpo_mate_position_wpoi_step_body_x_closed_after) = S (S l)) /\ (((exists wpo_beta_height_wpoi_step_body_x_closed_after_mate_entry. wpo_beta_height_wpoi_step_body_x_closed_after_mate_entry + S (wpo_mate_wpoi_step_body_x_closed_after) = S ((S (wpo_mate_position_wpoi_step_body_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_mate_entry. x = wpo_beta_quotient_wpoi_step_body_x_closed_after_mate_entry * S ((S (wpo_mate_position_wpoi_step_body_x_closed_after)) * x1) + (wpo_mate_wpoi_step_body_x_closed_after))))) /\ (forall wpo_position_wpoi_step_body_x_nonendpoint_after wpo_value_wpoi_step_body_x_nonendpoint_after. (exists wpo_gap_wpoi_step_body_x_nonendpoint_after_position_bound. wpo_gap_wpoi_step_body_x_nonendpoint_after_position_bound + S (wpo_position_wpoi_step_body_x_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_x_nonendpoint_after_entry. wpo_beta_height_wpoi_step_body_x_nonendpoint_after_entry + S (wpo_value_wpoi_step_body_x_nonendpoint_after) = S ((S (wpo_position_wpoi_step_body_x_nonendpoint_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_nonendpoint_after_entry. x = wpo_beta_quotient_wpoi_step_body_x_nonendpoint_after_entry * S ((S (wpo_position_wpoi_step_body_x_nonendpoint_after)) * x1) + (wpo_value_wpoi_step_body_x_nonendpoint_after))) -> (~(wpo_value_wpoi_step_body_x_nonendpoint_after = 0) /\ ~((S wpo_value_wpoi_step_body_x_nonendpoint_after) = n))))))))))))))) /\ (forall wpo_injective_left_wpoi_step_injective_after_x wpo_injective_right_wpoi_step_injective_after_x wpo_injective_value_wpoi_step_injective_after_x. (exists wpo_gap_wpoi_step_injective_after_x_left_bound. wpo_gap_wpoi_step_injective_after_x_left_bound + S (wpo_injective_left_wpoi_step_injective_after_x) = S (S l)) -> (exists wpo_gap_wpoi_step_injective_after_x_right_bound. wpo_gap_wpoi_step_injective_after_x_right_bound + S (wpo_injective_right_wpoi_step_injective_after_x) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_injective_after_x_left_entry. wpo_beta_height_wpoi_step_injective_after_x_left_entry + S (wpo_injective_value_wpoi_step_injective_after_x) = S ((S (wpo_injective_left_wpoi_step_injective_after_x)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_x_left_entry. x = wpo_beta_quotient_wpoi_step_injective_after_x_left_entry * S ((S (wpo_injective_left_wpoi_step_injective_after_x)) * x1) + (wpo_injective_value_wpoi_step_injective_after_x))) -> (((exists wpo_beta_height_wpoi_step_injective_after_x_right_entry. wpo_beta_height_wpoi_step_injective_after_x_right_entry + S (wpo_injective_value_wpoi_step_injective_after_x) = S ((S (wpo_injective_right_wpoi_step_injective_after_x)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_injective_after_x_right_entry. x = wpo_beta_quotient_wpoi_step_injective_after_x_right_entry * S ((S (wpo_injective_right_wpoi_step_injective_after_x)) * x1) + (wpo_injective_value_wpoi_step_injective_after_x))) -> wpo_injective_left_wpoi_step_injective_after_x = wpo_injective_right_wpoi_step_injective_after_x))
  41. 0041exact hstep_witness_witness_witness_witness
  42. 0042cases hcombined
  43. 0043have hparts : BetaAt(x,x1,l,x2) ∧ (BetaAt(x,x1,S l,x3) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(b,c,y,z) → BetaAt(x,x1,y,z))) ∧ (Lt(x2,n) ∧ (¬x2 = 0 ∧ ¬S x2 = n ∧ (¬ContainsPrefix(b,c,l,x2) ∧ (BetaAt(u,v,x2,x3) ∧ (Lt(x3,n) ∧ (¬x3 = 0 ∧ ¬S x3 = n ∧ (¬x2 = x3 ∧ (BetaAt(u,v,x3,x2) ∧ (¬ContainsPrefix(b,c,l,x3) ∧ ((∀ y. ∀ z. ∀ m. Lt(y,S S l) → BetaAt(x,x1,y,z) → BetaAt(u,v,z,m) → ContainsPrefix(x,x1,S S l,m)) ∧ (∀ y. ∀ z. Lt(y,S S l) → BetaAt(x,x1,y,z) → ¬z = 0 ∧ ¬S z = n)))))))))))
    Exact native replay linehave hparts : ((((((exists wpo_beta_height_wpoi_step_body_x_trace_first. wpo_beta_height_wpoi_step_body_x_trace_first + S (x2) = S ((S (l)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_first. x = wpo_beta_quotient_wpoi_step_body_x_trace_first * S ((S (l)) * x1) + (x2))) /\ ((((exists wpo_beta_height_wpoi_step_body_x_trace_second. wpo_beta_height_wpoi_step_body_x_trace_second + S (x3) = S ((S (S (l))) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_second. x = wpo_beta_quotient_wpoi_step_body_x_trace_second * S ((S (S (l))) * x1) + (x3))) /\ (forall wpo_old_index_wpoi_step_body_x_trace wpo_old_value_wpoi_step_body_x_trace. (exists wpo_gap_wpoi_step_body_x_trace_old_bound. wpo_gap_wpoi_step_body_x_trace_old_bound + S (wpo_old_index_wpoi_step_body_x_trace) = l) -> (((exists wpo_beta_height_wpoi_step_body_x_trace_old_entry. wpo_beta_height_wpoi_step_body_x_trace_old_entry + S (wpo_old_value_wpoi_step_body_x_trace) = S ((S (wpo_old_index_wpoi_step_body_x_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_old_entry. b = wpo_beta_quotient_wpoi_step_body_x_trace_old_entry * S ((S (wpo_old_index_wpoi_step_body_x_trace)) * c) + (wpo_old_value_wpoi_step_body_x_trace))) -> (((exists wpo_beta_height_wpoi_step_body_x_trace_new_entry. wpo_beta_height_wpoi_step_body_x_trace_new_entry + S (wpo_old_value_wpoi_step_body_x_trace) = S ((S (wpo_old_index_wpoi_step_body_x_trace)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_trace_new_entry. x = wpo_beta_quotient_wpoi_step_body_x_trace_new_entry * S ((S (wpo_old_index_wpoi_step_body_x_trace)) * x1) + (wpo_old_value_wpoi_step_body_x_trace))))))) /\ ((exists wpo_gap_wpoi_step_body_x_source_bound. wpo_gap_wpoi_step_body_x_source_bound + S (x2) = n) /\ ((~(x2 = 0) /\ ~((S x2) = n)) /\ ((~(exists wpo_index_wpoi_step_body_x_source_omit_contains. ((exists wpo_gap_wpoi_step_body_x_source_omit_contains_bound. wpo_gap_wpoi_step_body_x_source_omit_contains_bound + S (wpo_index_wpoi_step_body_x_source_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_x_source_omit_contains_entry. wpo_beta_height_wpoi_step_body_x_source_omit_contains_entry + S (x2) = S ((S (wpo_index_wpoi_step_body_x_source_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_source_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_x_source_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_x_source_omit_contains)) * c) + (x2)))))) /\ ((((exists wpo_beta_height_wpoi_step_body_x_forward. wpo_beta_height_wpoi_step_body_x_forward + S (x3) = S ((S (x2)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_forward. u = wpo_beta_quotient_wpoi_step_body_x_forward * S ((S (x2)) * v) + (x3))) /\ ((exists wpo_gap_wpoi_step_body_x_mate_bound. wpo_gap_wpoi_step_body_x_mate_bound + S (x3) = n) /\ ((~(x3 = 0) /\ ~((S x3) = n)) /\ (~(x2 = x3) /\ ((((exists wpo_beta_height_wpoi_step_body_x_back. wpo_beta_height_wpoi_step_body_x_back + S (x2) = S ((S (x3)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_back. u = wpo_beta_quotient_wpoi_step_body_x_back * S ((S (x3)) * v) + (x2))) /\ ((~(exists wpo_index_wpoi_step_body_x_mate_omit_contains. ((exists wpo_gap_wpoi_step_body_x_mate_omit_contains_bound. wpo_gap_wpoi_step_body_x_mate_omit_contains_bound + S (wpo_index_wpoi_step_body_x_mate_omit_contains) = l) /\ (((exists wpo_beta_height_wpoi_step_body_x_mate_omit_contains_entry. wpo_beta_height_wpoi_step_body_x_mate_omit_contains_entry + S (x3) = S ((S (wpo_index_wpoi_step_body_x_mate_omit_contains)) * c)) /\ exists wpo_beta_quotient_wpoi_step_body_x_mate_omit_contains_entry. b = wpo_beta_quotient_wpoi_step_body_x_mate_omit_contains_entry * S ((S (wpo_index_wpoi_step_body_x_mate_omit_contains)) * c) + (x3)))))) /\ ((forall wpo_position_wpoi_step_body_x_closed_after wpo_source_wpoi_step_body_x_closed_after wpo_mate_wpoi_step_body_x_closed_after. (exists wpo_gap_wpoi_step_body_x_closed_after_position_bound. wpo_gap_wpoi_step_body_x_closed_after_position_bound + S (wpo_position_wpoi_step_body_x_closed_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_x_closed_after_source_entry. wpo_beta_height_wpoi_step_body_x_closed_after_source_entry + S (wpo_source_wpoi_step_body_x_closed_after) = S ((S (wpo_position_wpoi_step_body_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_source_entry. x = wpo_beta_quotient_wpoi_step_body_x_closed_after_source_entry * S ((S (wpo_position_wpoi_step_body_x_closed_after)) * x1) + (wpo_source_wpoi_step_body_x_closed_after))) -> (((exists wpo_beta_height_wpoi_step_body_x_closed_after_inverse_entry. wpo_beta_height_wpoi_step_body_x_closed_after_inverse_entry + S (wpo_mate_wpoi_step_body_x_closed_after) = S ((S (wpo_source_wpoi_step_body_x_closed_after)) * v)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_inverse_entry. u = wpo_beta_quotient_wpoi_step_body_x_closed_after_inverse_entry * S ((S (wpo_source_wpoi_step_body_x_closed_after)) * v) + (wpo_mate_wpoi_step_body_x_closed_after))) -> exists wpo_mate_position_wpoi_step_body_x_closed_after. ((exists wpo_gap_wpoi_step_body_x_closed_after_mate_bound. wpo_gap_wpoi_step_body_x_closed_after_mate_bound + S (wpo_mate_position_wpoi_step_body_x_closed_after) = S (S l)) /\ (((exists wpo_beta_height_wpoi_step_body_x_closed_after_mate_entry. wpo_beta_height_wpoi_step_body_x_closed_after_mate_entry + S (wpo_mate_wpoi_step_body_x_closed_after) = S ((S (wpo_mate_position_wpoi_step_body_x_closed_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_closed_after_mate_entry. x = wpo_beta_quotient_wpoi_step_body_x_closed_after_mate_entry * S ((S (wpo_mate_position_wpoi_step_body_x_closed_after)) * x1) + (wpo_mate_wpoi_step_body_x_closed_after))))) /\ (forall wpo_position_wpoi_step_body_x_nonendpoint_after wpo_value_wpoi_step_body_x_nonendpoint_after. (exists wpo_gap_wpoi_step_body_x_nonendpoint_after_position_bound. wpo_gap_wpoi_step_body_x_nonendpoint_after_position_bound + S (wpo_position_wpoi_step_body_x_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_wpoi_step_body_x_nonendpoint_after_entry. wpo_beta_height_wpoi_step_body_x_nonendpoint_after_entry + S (wpo_value_wpoi_step_body_x_nonendpoint_after) = S ((S (wpo_position_wpoi_step_body_x_nonendpoint_after)) * x1)) /\ exists wpo_beta_quotient_wpoi_step_body_x_nonendpoint_after_entry. x = wpo_beta_quotient_wpoi_step_body_x_nonendpoint_after_entry * S ((S (wpo_position_wpoi_step_body_x_nonendpoint_after)) * x1) + (wpo_value_wpoi_step_body_x_nonendpoint_after))) -> (~(wpo_value_wpoi_step_body_x_nonendpoint_after = 0) /\ ~((S wpo_value_wpoi_step_body_x_nonendpoint_after) = n))))))))))))))
  44. 0044exact hcombined_left
  45. 0045cases hparts
  46. 0046cases hparts_right
  47. 0047cases hparts_right_right
  48. 0048cases hparts_right_right_right
  49. 0049cases hparts_right_right_right_right
  50. 0050cases hparts_right_right_right_right_right
  51. 0051have hnew_bounded : ∀ fom_index_wpoi_step_bounded_after_x. Lt(fom_index_wpoi_step_bounded_after_x,S S l) → ∃ y. BetaAt(x,x1,fom_index_wpoi_step_bounded_after_x,y) ∧ Lt(y,n)
    Exact native replay linehave hnew_bounded : forall fom_index_wpoi_step_bounded_after_x. (exists fom_gap_wpoi_step_bounded_after_x_index_bound. fom_gap_wpoi_step_bounded_after_x_index_bound + S (fom_index_wpoi_step_bounded_after_x) = S (S l)) -> exists fom_value_wpoi_step_bounded_after_x. ((((exists fom_beta_height_wpoi_step_bounded_after_x_entry. fom_beta_height_wpoi_step_bounded_after_x_entry + S (fom_value_wpoi_step_bounded_after_x) = S ((S (fom_index_wpoi_step_bounded_after_x)) * x1)) /\ exists fom_beta_quotient_wpoi_step_bounded_after_x_entry. x = fom_beta_quotient_wpoi_step_bounded_after_x_entry * S ((S (fom_index_wpoi_step_bounded_after_x)) * x1) + (fom_value_wpoi_step_bounded_after_x))) /\ (exists fom_gap_wpoi_step_bounded_after_x_value_bound. fom_gap_wpoi_step_bounded_after_x_value_bound + S (fom_value_wpoi_step_bounded_after_x) = n))
  52. 0052specialize beta_prefix_append_two_bounded_into b
  53. 0053specialize beta_prefix_append_two_bounded_into c
  54. 0054specialize beta_prefix_append_two_bounded_into x
  55. 0055specialize beta_prefix_append_two_bounded_into x1
  56. 0056specialize beta_prefix_append_two_bounded_into l
  57. 0057specialize beta_prefix_append_two_bounded_into n
  58. 0058specialize beta_prefix_append_two_bounded_into x2
  59. 0059specialize beta_prefix_append_two_bounded_into x3
  60. 0060apply beta_prefix_append_two_bounded_into
  61. 0061exact hparts_left
  62. 0062exact hbounded
  63. 0063exact hparts_right_left
  64. 0064exact hparts_right_right_right_right_right_left
  65. 0065exists x
  66. 0066exists x1
  67. 0067exists x2
  68. 0068exists x3
  69. 0069split
  70. 0070exact hcombined_left
  71. 0071split
  72. 0072exact hnew_bounded
  73. 0073exact hcombined_right