PA00AW · theorem

prime_pair_order_choose_append_injective

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

Thread decoded-prefix injectivity through one constructive fresh-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. ∀ 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))))))))))) ∧ 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

28 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0025 InjectivePrefix PD0027 ContainsPrefix

35 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 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 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

PA00AV prime_pair_order_choose_append PA009N beta_prefix_append_two_injective

Direct theorem dependents

PA00AX prime_pair_order_choose_append_state

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

70 script commands · 12 reading checkpoints · 3 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 appendbeta prefix append two injective
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–16

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 hnonendpoint
  6. L16
    intro hinjective
03Establish hstepL17–26

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

  1. L17
    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)))))))))))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)Original native command in the exact edition
  2. L18
    specialize prime_pair_order_choose_append p
  3. L19
    specialize prime_pair_order_choose_append n
  4. L20
    specialize prime_pair_order_choose_append u
  5. L21
    specialize prime_pair_order_choose_append v
  6. L22
    specialize prime_pair_order_choose_append b
  7. L23
    specialize prime_pair_order_choose_append c
  8. L24
    specialize prime_pair_order_choose_append l
  9. L25
    specialize prime_pair_order_choose_append r
  10. L26
    apply prime_pair_order_choose_append
04Use earlier factsL27–33

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

  1. L27
    exact hpn
  2. L28
    exact hp
  3. L29
    exact hprefix
  4. L30
    exact hnr
  5. L31
    exact hshort
  6. L32
    exact hclosed
  7. L33
    exact hnonendpoint
05Separate the logical casesL34–37

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

  1. L34
    cases hstep
  2. L35
    cases hstep_witness
  3. L36
    cases hstep_witness_witness
  4. L37
    cases hstep_witness_witness_witness
06Establish hpartsL38–39

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

  1. L38
    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. L39
    exact hstep_witness_witness_witness_witness
07Separate the logical casesL40–49

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

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

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

  1. L50
    have hnew_injective : InjectivePrefix(x,x1,S S l)Definitions: InjectivePrefix(x,x1,S S l)Original native command in the exact edition
  2. L51
    specialize beta_prefix_append_two_injective b
  3. L52
    specialize beta_prefix_append_two_injective c
  4. L53
    specialize beta_prefix_append_two_injective x
  5. L54
    specialize beta_prefix_append_two_injective x1
  6. L55
    specialize beta_prefix_append_two_injective l
  7. L56
    specialize beta_prefix_append_two_injective x2
  8. L57
    specialize beta_prefix_append_two_injective x3
  9. L58
    apply beta_prefix_append_two_injective
  10. L59
    exact hparts_left
09Use earlier factsL60–63

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

  1. L60
    exact hinjective
  2. L61
    exact hparts_right_right_right_left
  3. L62
    exact hparts_right_right_right_right_right_right_right_right_right_left
  4. L63
    exact hparts_right_right_right_right_right_right_right_left
10Construct an explicit witnessL64–67

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

  1. L64
    exists x
  2. L65
    exists x1
  3. L66
    exists x2
  4. L67
    exists x3
11Separate the logical casesL68–68

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

  1. L68
    split
12Use earlier factsL69–70

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

  1. L69
    exact hstep_witness_witness_witness_witness
  2. L70
    exact hnew_injective

Library-wide reading audit

Original defined command ledger · 70 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 hnonendpoint
  16. 0016intro hinjective
  17. 0017have 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)))))))))))
    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)))))))))))))))
  18. 0018specialize prime_pair_order_choose_append p
  19. 0019specialize prime_pair_order_choose_append n
  20. 0020specialize prime_pair_order_choose_append u
  21. 0021specialize prime_pair_order_choose_append v
  22. 0022specialize prime_pair_order_choose_append b
  23. 0023specialize prime_pair_order_choose_append c
  24. 0024specialize prime_pair_order_choose_append l
  25. 0025specialize prime_pair_order_choose_append r
  26. 0026apply prime_pair_order_choose_append
  27. 0027exact hpn
  28. 0028exact hp
  29. 0029exact hprefix
  30. 0030exact hnr
  31. 0031exact hshort
  32. 0032exact hclosed
  33. 0033exact hnonendpoint
  34. 0034cases hstep
  35. 0035cases hstep_witness
  36. 0036cases hstep_witness_witness
  37. 0037cases hstep_witness_witness_witness
  38. 0038have 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))))))))))))))
  39. 0039exact hstep_witness_witness_witness_witness
  40. 0040cases hparts
  41. 0041cases hparts_right
  42. 0042cases hparts_right_right
  43. 0043cases hparts_right_right_right
  44. 0044cases hparts_right_right_right_right
  45. 0045cases hparts_right_right_right_right_right
  46. 0046cases hparts_right_right_right_right_right_right
  47. 0047cases hparts_right_right_right_right_right_right_right
  48. 0048cases hparts_right_right_right_right_right_right_right_right
  49. 0049cases hparts_right_right_right_right_right_right_right_right_right
  50. 0050have hnew_injective : InjectivePrefix(x,x1,S S l)
    Exact native replay linehave hnew_injective : 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
  51. 0051specialize beta_prefix_append_two_injective b
  52. 0052specialize beta_prefix_append_two_injective c
  53. 0053specialize beta_prefix_append_two_injective x
  54. 0054specialize beta_prefix_append_two_injective x1
  55. 0055specialize beta_prefix_append_two_injective l
  56. 0056specialize beta_prefix_append_two_injective x2
  57. 0057specialize beta_prefix_append_two_injective x3
  58. 0058apply beta_prefix_append_two_injective
  59. 0059exact hparts_left
  60. 0060exact hinjective
  61. 0061exact hparts_right_right_right_left
  62. 0062exact hparts_right_right_right_right_right_right_right_right_right_left
  63. 0063exact hparts_right_right_right_right_right_right_right_left
  64. 0064exists x
  65. 0065exists x1
  66. 0066exists x2
  67. 0067exists x3
  68. 0068split
  69. 0069exact hstep_witness_witness_witness_witness
  70. 0070exact hnew_injective