PA002I

bounded_beta_exclusive_recode_invariant

Stable checked-use theorem · independently closed

Fold an empty-based, exclusive beta prefix into another base with append readiness.

Exact expanded PA statement

forall N c b e. (forall t. (exists h. S t + S h = S N) -> exists q. c = S t * q) -> forall k. (exists h. h + k = N) -> exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))

Structural proof guide

Generated structural guide

Fold an empty-based, exclusive beta prefix into another base with append readiness.

Use the direct prerequisites succ_ne_zero, add_eq_zero_right, coprime_one_left, le_succ_self, le_trans, beta_exclusive_recode_invariant_step as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (8), intermediate claims (6).

Referenced ingredients

PA0005 succ_ne_zero PA0004 add_eq_zero_right PA000P coprime_one_left PA000Q le_succ_self PA000R le_trans PA002H beta_exclusive_recode_invariant_step

Proof neighborhood

Direct dependencies

PA0005 succ_ne_zero PA0004 add_eq_zero_right PA000P coprime_one_left PA000Q le_succ_self PA000R le_trans PA002H beta_exclusive_recode_invariant_step

Direct dependents

PA002X beta_prefix_extend

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 N
  2. 0002intro c
  3. 0003intro b
  4. 0004intro e
  5. 0005intro hcm
  6. 0006induction k
  7. 0007intro hkN
  8. 0008exists 1
  9. 0009exists 0
  10. 0010split
  11. 0011specialize succ_ne_zero 0
  12. 0012exact succ_ne_zero
  13. 0013split
  14. 0014intro i
  15. 0015intro hi
  16. 0016exfalso
  17. 0017cases hi
  18. 0018have hsi0 : S i = 0
  19. 0019specialize add_eq_zero_right x
  20. 0020specialize add_eq_zero_right (S i)
  21. 0021apply add_eq_zero_right
  22. 0022exact hi_witness
  23. 0023specialize succ_ne_zero i
  24. 0024apply succ_ne_zero
  25. 0025exact hsi0
  26. 0026split
  27. 0027intro i
  28. 0028intro a
  29. 0029intro hi
  30. 0030intro hati
  31. 0031exfalso
  32. 0032cases hi
  33. 0033have hsi0 : S i = 0
  34. 0034specialize add_eq_zero_right x
  35. 0035specialize add_eq_zero_right (S i)
  36. 0036apply add_eq_zero_right
  37. 0037exact hi_witness
  38. 0038specialize succ_ne_zero i
  39. 0039apply succ_ne_zero
  40. 0040exact hsi0
  41. 0041intro j
  42. 0042intro h0j
  43. 0043intro hjN
  44. 0044intro d
  45. 0045intro h1
  46. 0046intro hm
  47. 0047specialize coprime_one_left (S ((S j) * c))
  48. 0048specialize coprime_one_left d
  49. 0049apply coprime_one_left
  50. 0050exact h1
  51. 0051exact hm
  52. 0052intro hkN
  53. 0053have hkprev : exists h. h + k = N
  54. 0054have hkstep : exists h. h + k = S k
  55. 0055specialize le_succ_self k
  56. 0056exact le_succ_self
  57. 0057specialize le_trans k
  58. 0058specialize le_trans (S k)
  59. 0059specialize le_trans N
  60. 0060apply le_trans
  61. 0061exact hkstep
  62. 0062exact hkN
  63. 0063have hprev : exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + k = j) -> (exists h. h + j = N) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))
  64. 0064apply IH
  65. 0065exact hkprev
  66. 0066cases hprev
  67. 0067cases hprev_witness
  68. 0068cases hprev_witness_witness
  69. 0069cases hprev_witness_witness_right
  70. 0070cases hprev_witness_witness_right_right
  71. 0071have hnext : exists z2. (~(x * S ((S k) * c) = 0) /\ ((forall i. (exists h. h + S i = S k) -> exists q. x * S ((S k) * c) = S ((S i) * c) * q) /\ ((forall i a. (exists h. h + S i = S k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z2 + S ((S i) * c) * u = a + S ((S i) * c) * v) /\ forall j. (exists g. g + S k = j) -> (exists h. h + j = N) -> forall d. (exists u. x * S ((S k) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1)))
  72. 0072specialize beta_exclusive_recode_invariant_step N
  73. 0073specialize beta_exclusive_recode_invariant_step c
  74. 0074specialize beta_exclusive_recode_invariant_step b
  75. 0075specialize beta_exclusive_recode_invariant_step e
  76. 0076specialize beta_exclusive_recode_invariant_step k
  77. 0077specialize beta_exclusive_recode_invariant_step x
  78. 0078specialize beta_exclusive_recode_invariant_step x1
  79. 0079apply beta_exclusive_recode_invariant_step
  80. 0080exact hcm
  81. 0081exact hkN
  82. 0082exact hprev_witness_witness_left
  83. 0083exact hprev_witness_witness_right_left
  84. 0084exact hprev_witness_witness_right_right_left
  85. 0085exact hprev_witness_witness_right_right_right
  86. 0086cases hnext
  87. 0087exists x * S ((S k) * c)
  88. 0088exists x2
  89. 0089exact hnext_witness