PA004J

beta_prefix_replace_exists

Stable checked-use theorem · independently closed

Recode a finite beta prefix while replacing one interior entry.

Exact expanded PA statement

forall b c i s k. (exists h. h + S i = k) -> exists z d. ((((exists ff_h_replace_entry. ff_h_replace_entry + S (s) = S ((S (i)) * d)) /\ exists ff_q_replace_entry. z = ff_q_replace_entry * S ((S (i)) * d) + (s))) /\ forall j a. (exists h. h + S j = k) -> ~(j = i) -> (((exists ff_h_replace_old. ff_h_replace_old + S (a) = S ((S (j)) * c)) /\ exists ff_q_replace_old. b = ff_q_replace_old * S ((S (j)) * c) + (a))) -> (((exists ff_h_replace_new. ff_h_replace_new + S (a) = S ((S (j)) * d)) /\ exists ff_q_replace_new. z = ff_q_replace_new * S ((S (j)) * d) + (a))))

Structural proof guide

Generated structural guide

Recode a finite beta prefix while replacing one interior entry.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, finite_lt_succ_eq_or_lt, beta_prefix_extend, beta_at_exists, beta_at_unique as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (14), intermediate claims (7), equality transport (8).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA002X beta_prefix_extend PA0029 beta_at_exists PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA002X beta_prefix_extend PA0029 beta_at_exists PA002F beta_at_unique

Direct dependents

PA004K beta_prefix_swap_last_from_entries

Formal native tactic body

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

  1. 0001intro b
  2. 0002intro c
  3. 0003intro i
  4. 0004intro s
  5. 0005induction k
  6. 0006intro hi
  7. 0007exfalso
  8. 0008cases hi
  9. 0009have hsi : S i = 0
  10. 0010specialize add_eq_zero_right x
  11. 0011specialize add_eq_zero_right (S i)
  12. 0012apply add_eq_zero_right
  13. 0013exact hi_witness
  14. 0014specialize succ_ne_zero i
  15. 0015apply succ_ne_zero
  16. 0016exact hsi
  17. 0017intro hi
  18. 0018have hisplit : i = k \/ exists h. h + S i = k
  19. 0019specialize finite_lt_succ_eq_or_lt k
  20. 0020specialize finite_lt_succ_eq_or_lt i
  21. 0021apply finite_lt_succ_eq_or_lt
  22. 0022exact hi
  23. 0023cases hisplit
  24. 0024specialize beta_prefix_extend k
  25. 0025specialize beta_prefix_extend b
  26. 0026specialize beta_prefix_extend c
  27. 0027specialize beta_prefix_extend s
  28. 0028cases beta_prefix_extend
  29. 0029cases beta_prefix_extend_witness
  30. 0030cases beta_prefix_extend_witness_witness
  31. 0031exists x
  32. 0032exists x1
  33. 0033split
  34. 0034rewrite hisplit_left
  35. 0035rewrite hisplit_left
  36. 0036exact beta_prefix_extend_witness_witness_left
  37. 0037intro j
  38. 0038intro a
  39. 0039intro hj
  40. 0040intro hji
  41. 0041intro hold
  42. 0042have hjsplit : j = k \/ exists h. h + S j = k
  43. 0043specialize finite_lt_succ_eq_or_lt k
  44. 0044specialize finite_lt_succ_eq_or_lt j
  45. 0045apply finite_lt_succ_eq_or_lt
  46. 0046exact hj
  47. 0047cases hjsplit
  48. 0048exfalso
  49. 0049apply hji
  50. 0050trans k
  51. 0051exact hjsplit_left
  52. 0052symm
  53. 0053exact hisplit_left
  54. 0054specialize beta_prefix_extend_witness_witness_right j
  55. 0055specialize beta_prefix_extend_witness_witness_right a
  56. 0056apply beta_prefix_extend_witness_witness_right
  57. 0057exact hjsplit_right
  58. 0058exact hold
  59. 0059have hreplaced : exists z d. (((exists h. h + S s = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + s) /\ forall j a. (exists h. h + S j = k) -> ~(j = i) -> ((exists h. h + S a = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + a))
  60. 0060apply IH
  61. 0061exact hisplit_right
  62. 0062cases hreplaced
  63. 0063cases hreplaced_witness
  64. 0064cases hreplaced_witness_witness
  65. 0065specialize beta_at_exists b
  66. 0066specialize beta_at_exists c
  67. 0067specialize beta_at_exists k
  68. 0068cases beta_at_exists
  69. 0069specialize beta_prefix_extend k
  70. 0070specialize beta_prefix_extend x
  71. 0071specialize beta_prefix_extend x1
  72. 0072specialize beta_prefix_extend x2
  73. 0073cases beta_prefix_extend
  74. 0074cases beta_prefix_extend_witness
  75. 0075cases beta_prefix_extend_witness_witness
  76. 0076exists x3
  77. 0077exists x4
  78. 0078split
  79. 0079specialize beta_prefix_extend_witness_witness_right i
  80. 0080specialize beta_prefix_extend_witness_witness_right s
  81. 0081apply beta_prefix_extend_witness_witness_right
  82. 0082exact hisplit_right
  83. 0083exact hreplaced_witness_witness_left
  84. 0084intro j
  85. 0085intro a
  86. 0086intro hj
  87. 0087intro hji
  88. 0088intro hold
  89. 0089have hjsplit : j = k \/ exists h. h + S j = k
  90. 0090specialize finite_lt_succ_eq_or_lt k
  91. 0091specialize finite_lt_succ_eq_or_lt j
  92. 0092apply finite_lt_succ_eq_or_lt
  93. 0093exact hj
  94. 0094cases hjsplit
  95. 0095have hax : a = x2
  96. 0096specialize beta_at_unique b
  97. 0097specialize beta_at_unique c
  98. 0098specialize beta_at_unique k
  99. 0099specialize beta_at_unique a
  100. 0100specialize beta_at_unique x2
  101. 0101apply beta_at_unique
  102. 0102rewrite hjsplit_left at hold
  103. 0103rewrite hjsplit_left at hold
  104. 0104exact hold
  105. 0105exact beta_at_exists_witness
  106. 0106rewrite hjsplit_left
  107. 0107rewrite hjsplit_left
  108. 0108rewrite hax
  109. 0109rewrite hax
  110. 0110exact beta_prefix_extend_witness_witness_left
  111. 0111have hmiddle : ((exists h. h + S a = S ((S j) * x1)) /\ exists q. x = q * S ((S j) * x1) + a)
  112. 0112specialize hreplaced_witness_witness_right j
  113. 0113specialize hreplaced_witness_witness_right a
  114. 0114apply hreplaced_witness_witness_right
  115. 0115exact hjsplit_right
  116. 0116exact hji
  117. 0117exact hold
  118. 0118specialize beta_prefix_extend_witness_witness_right j
  119. 0119specialize beta_prefix_extend_witness_witness_right a
  120. 0120apply beta_prefix_extend_witness_witness_right
  121. 0121exact hjsplit_right
  122. 0122exact hmiddle