PA009K

beta_prefix_append_two_exists

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

Append two values at consecutive beta positions while preserving every old entry.

Exact expanded PA statement

forall b c l a e. exists z d. (((((exists wpo_beta_height_append_result_first. wpo_beta_height_append_result_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_append_result_first. z = wpo_beta_quotient_append_result_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_append_result_second. wpo_beta_height_append_result_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_append_result_second. z = wpo_beta_quotient_append_result_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_append_result wpo_old_value_append_result. (exists wpo_gap_append_result_old_bound. wpo_gap_append_result_old_bound + S (wpo_old_index_append_result) = l) -> (((exists wpo_beta_height_append_result_old_entry. wpo_beta_height_append_result_old_entry + S (wpo_old_value_append_result) = S ((S (wpo_old_index_append_result)) * c)) /\ exists wpo_beta_quotient_append_result_old_entry. b = wpo_beta_quotient_append_result_old_entry * S ((S (wpo_old_index_append_result)) * c) + (wpo_old_value_append_result))) -> (((exists wpo_beta_height_append_result_new_entry. wpo_beta_height_append_result_new_entry + S (wpo_old_value_append_result) = S ((S (wpo_old_index_append_result)) * d)) /\ exists wpo_beta_quotient_append_result_new_entry. z = wpo_beta_quotient_append_result_new_entry * S ((S (wpo_old_index_append_result)) * d) + (wpo_old_value_append_result)))))))

Structural proof guide

Generated structural guide

Append two values at consecutive beta positions while preserving every old entry.

Use the direct prerequisites beta_prefix_extend, le_refl, le_succ as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (3).

Referenced ingredients

PA002X beta_prefix_extend PA001A le_refl PA002O le_succ

Proof neighborhood

Direct dependencies

PA002X beta_prefix_extend PA001A le_refl PA002O le_succ

Direct dependents

PA009O scaled_inverse_pair_order_choose_append PA00AE finite_prefix_choose_unused_nonendpoint PA00AV prime_pair_order_choose_append

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro a
  5. 0005intro e
  6. 0006have hfirst_extend : forall k q s v. exists r t. (((exists h. h + S v = S ((S k) * t)) /\ exists u. r = u * S ((S k) * t) + v) /\ forall i w. (exists h. h + S i = k) -> ((exists h. h + S w = S ((S i) * s)) /\ exists u. q = u * S ((S i) * s) + w) -> ((exists h. h + S w = S ((S i) * t)) /\ exists u. r = u * S ((S i) * t) + w))
  7. 0007exact beta_prefix_extend
  8. 0008have hsecond_extend : forall k q s v. exists r t. (((exists h. h + S v = S ((S k) * t)) /\ exists u. r = u * S ((S k) * t) + v) /\ forall i w. (exists h. h + S i = k) -> ((exists h. h + S w = S ((S i) * s)) /\ exists u. q = u * S ((S i) * s) + w) -> ((exists h. h + S w = S ((S i) * t)) /\ exists u. r = u * S ((S i) * t) + w))
  9. 0009exact beta_prefix_extend
  10. 0010specialize hfirst_extend l
  11. 0011specialize hfirst_extend b
  12. 0012specialize hfirst_extend c
  13. 0013specialize hfirst_extend a
  14. 0014cases hfirst_extend
  15. 0015cases hfirst_extend_witness
  16. 0016cases hfirst_extend_witness_witness
  17. 0017specialize hsecond_extend (S l)
  18. 0018specialize hsecond_extend x
  19. 0019specialize hsecond_extend x1
  20. 0020specialize hsecond_extend e
  21. 0021cases hsecond_extend
  22. 0022cases hsecond_extend_witness
  23. 0023cases hsecond_extend_witness_witness
  24. 0024exists x2
  25. 0025exists x3
  26. 0026split
  27. 0027specialize hsecond_extend_witness_witness_right l
  28. 0028specialize hsecond_extend_witness_witness_right a
  29. 0029apply hsecond_extend_witness_witness_right
  30. 0030specialize le_refl (S l)
  31. 0031exact le_refl
  32. 0032exact hfirst_extend_witness_witness_left
  33. 0033split
  34. 0034exact hsecond_extend_witness_witness_left
  35. 0035intro i
  36. 0036intro v
  37. 0037intro hi
  38. 0038intro hold
  39. 0039have hmiddle : ((exists wpo_beta_height_append_old_middle. wpo_beta_height_append_old_middle + S (v) = S ((S (i)) * x1)) /\ exists wpo_beta_quotient_append_old_middle. x = wpo_beta_quotient_append_old_middle * S ((S (i)) * x1) + (v))
  40. 0040specialize hfirst_extend_witness_witness_right i
  41. 0041specialize hfirst_extend_witness_witness_right v
  42. 0042apply hfirst_extend_witness_witness_right
  43. 0043exact hi
  44. 0044exact hold
  45. 0045specialize hsecond_extend_witness_witness_right i
  46. 0046specialize hsecond_extend_witness_witness_right v
  47. 0047apply hsecond_extend_witness_witness_right
  48. 0048specialize le_succ (S i)
  49. 0049specialize le_succ l
  50. 0050apply le_succ
  51. 0051exact hi
  52. 0052exact hmiddle