PA007D

beta_magnitude_predecessor_recode_exists

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

Every positive bounded beta prefix can be recoded pointwise by removing one successor from each value.

Exact expanded PA statement

forall mb mc H l. (forall gmp_index_predecessor_recode_range. (exists gsp_lt_gap_predecessor_recode_range_index_bound. gsp_lt_gap_predecessor_recode_range_index_bound + S gmp_index_predecessor_recode_range = l) -> exists gmp_magnitude_predecessor_recode_range. ((((exists ff_h_gmp_predecessor_recode_range_decoded. ff_h_gmp_predecessor_recode_range_decoded + S (gmp_magnitude_predecessor_recode_range) = S ((S (gmp_index_predecessor_recode_range)) * mc)) /\ exists ff_q_gmp_predecessor_recode_range_decoded. mb = ff_q_gmp_predecessor_recode_range_decoded * S ((S (gmp_index_predecessor_recode_range)) * mc) + (gmp_magnitude_predecessor_recode_range))) /\ ((exists gsp_lt_gap_predecessor_recode_range_positive. gsp_lt_gap_predecessor_recode_range_positive + S 0 = gmp_magnitude_predecessor_recode_range) /\ (exists gsp_le_gap_predecessor_recode_range_bounded. gsp_le_gap_predecessor_recode_range_bounded + gmp_magnitude_predecessor_recode_range = H)))) -> (exists rb rc. (forall gmp_index_predecessor_recode_result gmp_predecessor_predecessor_recode_result. (exists gsp_lt_gap_predecessor_recode_result_index_bound. gsp_lt_gap_predecessor_recode_result_index_bound + S gmp_index_predecessor_recode_result = l) -> (((exists gsp_beta_height_gmp_predecessor_recode_result_source. gsp_beta_height_gmp_predecessor_recode_result_source + S (S gmp_predecessor_predecessor_recode_result) = S ((S (gmp_index_predecessor_recode_result)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_recode_result_source. mb = gsp_beta_quotient_gmp_predecessor_recode_result_source * S ((S (gmp_index_predecessor_recode_result)) * mc) + (S gmp_predecessor_predecessor_recode_result))) -> (((exists ff_h_gmp_predecessor_recode_result_target. ff_h_gmp_predecessor_recode_result_target + S (gmp_predecessor_predecessor_recode_result) = S ((S (gmp_index_predecessor_recode_result)) * rc)) /\ exists ff_q_gmp_predecessor_recode_result_target. rb = ff_q_gmp_predecessor_recode_result_target * S ((S (gmp_index_predecessor_recode_result)) * rc) + (gmp_predecessor_predecessor_recode_result)))))

Structural proof guide

Generated structural guide

Every positive bounded beta prefix can be recoded pointwise by removing one successor from each value.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, le_succ, le_refl, ne_zero_of_one_le, nonzero_is_succ, finite_lt_succ_eq_or_lt, beta_at_unique, succ_injective, beta_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (11), intermediate claims (9), equality transport (6).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA003D finite_lt_succ_eq_or_lt PA002F beta_at_unique PA003V succ_injective PA002X beta_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA003D finite_lt_succ_eq_or_lt PA002F beta_at_unique PA003V succ_injective PA002X beta_prefix_extend

Direct dependents

PA007E gauss_signed_half_predecessor_recode_exists PA00B4 finite_bounded_nonendpoint_injective_coverage PA00BE prime_wilson_terminal_product_package_exists

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 mb
  2. 0002intro mc
  3. 0003intro H
  4. 0004induction l
  5. 0005intro hrange
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro r
  10. 0010intro hi
  11. 0011intro hsource
  12. 0012exfalso
  13. 0013cases hi
  14. 0014have hsi : S i = 0
  15. 0015specialize add_eq_zero_right x
  16. 0016specialize add_eq_zero_right (S i)
  17. 0017apply add_eq_zero_right
  18. 0018exact hi_witness
  19. 0019specialize succ_ne_zero i
  20. 0020apply succ_ne_zero
  21. 0021exact hsi
  22. 0022intro hrange
  23. 0023have hprevious_range : forall gmp_index_predecessor_recode_previous_range. (exists gsp_lt_gap_predecessor_recode_previous_range_index_bound. gsp_lt_gap_predecessor_recode_previous_range_index_bound + S gmp_index_predecessor_recode_previous_range = l) -> exists gmp_magnitude_predecessor_recode_previous_range. ((((exists ff_h_gmp_predecessor_recode_previous_range_decoded. ff_h_gmp_predecessor_recode_previous_range_decoded + S (gmp_magnitude_predecessor_recode_previous_range) = S ((S (gmp_index_predecessor_recode_previous_range)) * mc)) /\ exists ff_q_gmp_predecessor_recode_previous_range_decoded. mb = ff_q_gmp_predecessor_recode_previous_range_decoded * S ((S (gmp_index_predecessor_recode_previous_range)) * mc) + (gmp_magnitude_predecessor_recode_previous_range))) /\ ((exists gsp_lt_gap_predecessor_recode_previous_range_positive. gsp_lt_gap_predecessor_recode_previous_range_positive + S 0 = gmp_magnitude_predecessor_recode_previous_range) /\ (exists gsp_le_gap_predecessor_recode_previous_range_bounded. gsp_le_gap_predecessor_recode_previous_range_bounded + gmp_magnitude_predecessor_recode_previous_range = H)))
  24. 0024intro i
  25. 0025intro hi
  26. 0026specialize hrange i
  27. 0027apply hrange
  28. 0028specialize le_succ (S i)
  29. 0029specialize le_succ l
  30. 0030apply le_succ
  31. 0031exact hi
  32. 0032have hprevious : exists rb rc. (forall gmp_index_predecessor_recode_previous_result gmp_predecessor_predecessor_recode_previous_result. (exists gsp_lt_gap_predecessor_recode_previous_result_index_bound. gsp_lt_gap_predecessor_recode_previous_result_index_bound + S gmp_index_predecessor_recode_previous_result = l) -> (((exists gsp_beta_height_gmp_predecessor_recode_previous_result_source. gsp_beta_height_gmp_predecessor_recode_previous_result_source + S (S gmp_predecessor_predecessor_recode_previous_result) = S ((S (gmp_index_predecessor_recode_previous_result)) * mc)) /\ exists gsp_beta_quotient_gmp_predecessor_recode_previous_result_source. mb = gsp_beta_quotient_gmp_predecessor_recode_previous_result_source * S ((S (gmp_index_predecessor_recode_previous_result)) * mc) + (S gmp_predecessor_predecessor_recode_previous_result))) -> (((exists ff_h_gmp_predecessor_recode_previous_result_target. ff_h_gmp_predecessor_recode_previous_result_target + S (gmp_predecessor_predecessor_recode_previous_result) = S ((S (gmp_index_predecessor_recode_previous_result)) * rc)) /\ exists ff_q_gmp_predecessor_recode_previous_result_target. rb = ff_q_gmp_predecessor_recode_previous_result_target * S ((S (gmp_index_predecessor_recode_previous_result)) * rc) + (gmp_predecessor_predecessor_recode_previous_result))))
  33. 0033apply IH
  34. 0034exact hprevious_range
  35. 0035cases hprevious
  36. 0036cases hprevious_witness
  37. 0037have hlast : exists m. (((exists ff_h_gmp_predecessor_recode_last_entry. ff_h_gmp_predecessor_recode_last_entry + S (m) = S ((S (l)) * mc)) /\ exists ff_q_gmp_predecessor_recode_last_entry. mb = ff_q_gmp_predecessor_recode_last_entry * S ((S (l)) * mc) + (m))) /\ ((exists gsp_lt_gap_predecessor_recode_last_positive. gsp_lt_gap_predecessor_recode_last_positive + S 0 = m) /\ (exists gsp_le_gap_predecessor_recode_last_bounded. gsp_le_gap_predecessor_recode_last_bounded + m = H))
  38. 0038specialize hrange l
  39. 0039apply hrange
  40. 0040specialize le_refl (S l)
  41. 0041exact le_refl
  42. 0042cases hlast
  43. 0043cases hlast_witness
  44. 0044cases hlast_witness_right
  45. 0045have hlast0 : ~(x2 = 0)
  46. 0046intro hlastzero
  47. 0047specialize ne_zero_of_one_le x2
  48. 0048apply ne_zero_of_one_le
  49. 0049exact hlast_witness_right_left
  50. 0050exact hlastzero
  51. 0051have hlast_predecessor : exists r. x2 = S r
  52. 0052specialize nonzero_is_succ x2
  53. 0053apply nonzero_is_succ
  54. 0054exact hlast0
  55. 0055cases hlast_predecessor
  56. 0056specialize beta_prefix_extend l
  57. 0057specialize beta_prefix_extend x
  58. 0058specialize beta_prefix_extend x1
  59. 0059specialize beta_prefix_extend x3
  60. 0060cases beta_prefix_extend
  61. 0061cases beta_prefix_extend_witness
  62. 0062cases beta_prefix_extend_witness_witness
  63. 0063exists x4
  64. 0064exists x5
  65. 0065intro i
  66. 0066intro r
  67. 0067intro hi
  68. 0068intro hsource
  69. 0069have hsplit : i = l \/ exists gap. gap + S i = l
  70. 0070specialize finite_lt_succ_eq_or_lt l
  71. 0071specialize finite_lt_succ_eq_or_lt i
  72. 0072apply finite_lt_succ_eq_or_lt
  73. 0073exact hi
  74. 0074cases hsplit
  75. 0075have hsource_value : S r = x2
  76. 0076specialize beta_at_unique mb
  77. 0077specialize beta_at_unique mc
  78. 0078specialize beta_at_unique l
  79. 0079specialize beta_at_unique (S r)
  80. 0080specialize beta_at_unique x2
  81. 0081apply beta_at_unique
  82. 0082rewrite hsplit_left at hsource
  83. 0083rewrite hsplit_left at hsource
  84. 0084exact hsource
  85. 0085exact hlast_witness_left
  86. 0086have hrvalue : r = x3
  87. 0087specialize succ_injective r
  88. 0088specialize succ_injective x3
  89. 0089apply succ_injective
  90. 0090trans x2
  91. 0091exact hsource_value
  92. 0092exact hlast_predecessor_witness
  93. 0093rewrite hsplit_left
  94. 0094rewrite hsplit_left
  95. 0095rewrite hrvalue
  96. 0096rewrite hrvalue
  97. 0097exact beta_prefix_extend_witness_witness_left
  98. 0098specialize beta_prefix_extend_witness_witness_right i
  99. 0099specialize beta_prefix_extend_witness_witness_right r
  100. 0100apply beta_prefix_extend_witness_witness_right
  101. 0101exact hsplit_right
  102. 0102specialize hprevious_witness_witness i
  103. 0103specialize hprevious_witness_witness r
  104. 0104apply hprevious_witness_witness
  105. 0105exact hsplit_right
  106. 0106exact hsource