PA00B4

finite_bounded_nonendpoint_injective_coverage

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

A bounded injective terminal prefix covers exactly every nonendpoint value below n = l+2.

Exact expanded PA statement

forall b c l. (forall fom_index_wpoi_terminal_bounded. (exists fom_gap_wpoi_terminal_bounded_index_bound. fom_gap_wpoi_terminal_bounded_index_bound + S (fom_index_wpoi_terminal_bounded) = l) -> exists fom_value_wpoi_terminal_bounded. ((((exists fom_beta_height_wpoi_terminal_bounded_entry. fom_beta_height_wpoi_terminal_bounded_entry + S (fom_value_wpoi_terminal_bounded) = S ((S (fom_index_wpoi_terminal_bounded)) * c)) /\ exists fom_beta_quotient_wpoi_terminal_bounded_entry. b = fom_beta_quotient_wpoi_terminal_bounded_entry * S ((S (fom_index_wpoi_terminal_bounded)) * c) + (fom_value_wpoi_terminal_bounded))) /\ (exists fom_gap_wpoi_terminal_bounded_value_bound. fom_gap_wpoi_terminal_bounded_value_bound + S (fom_value_wpoi_terminal_bounded) = S (S l)))) -> (forall wpo_position_wpoi_terminal_nonendpoint wpo_value_wpoi_terminal_nonendpoint. (exists wpo_gap_wpoi_terminal_nonendpoint_position_bound. wpo_gap_wpoi_terminal_nonendpoint_position_bound + S (wpo_position_wpoi_terminal_nonendpoint) = l) -> (((exists wpo_beta_height_wpoi_terminal_nonendpoint_entry. wpo_beta_height_wpoi_terminal_nonendpoint_entry + S (wpo_value_wpoi_terminal_nonendpoint) = S ((S (wpo_position_wpoi_terminal_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_nonendpoint_entry. b = wpo_beta_quotient_wpoi_terminal_nonendpoint_entry * S ((S (wpo_position_wpoi_terminal_nonendpoint)) * c) + (wpo_value_wpoi_terminal_nonendpoint))) -> (~(wpo_value_wpoi_terminal_nonendpoint = 0) /\ ~((S wpo_value_wpoi_terminal_nonendpoint) = S (S l)))) -> (forall wpo_injective_left_wpoi_terminal_injective wpo_injective_right_wpoi_terminal_injective wpo_injective_value_wpoi_terminal_injective. (exists wpo_gap_wpoi_terminal_injective_left_bound. wpo_gap_wpoi_terminal_injective_left_bound + S (wpo_injective_left_wpoi_terminal_injective) = l) -> (exists wpo_gap_wpoi_terminal_injective_right_bound. wpo_gap_wpoi_terminal_injective_right_bound + S (wpo_injective_right_wpoi_terminal_injective) = l) -> (((exists wpo_beta_height_wpoi_terminal_injective_left_entry. wpo_beta_height_wpoi_terminal_injective_left_entry + S (wpo_injective_value_wpoi_terminal_injective) = S ((S (wpo_injective_left_wpoi_terminal_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_injective_left_entry. b = wpo_beta_quotient_wpoi_terminal_injective_left_entry * S ((S (wpo_injective_left_wpoi_terminal_injective)) * c) + (wpo_injective_value_wpoi_terminal_injective))) -> (((exists wpo_beta_height_wpoi_terminal_injective_right_entry. wpo_beta_height_wpoi_terminal_injective_right_entry + S (wpo_injective_value_wpoi_terminal_injective) = S ((S (wpo_injective_right_wpoi_terminal_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_injective_right_entry. b = wpo_beta_quotient_wpoi_terminal_injective_right_entry * S ((S (wpo_injective_right_wpoi_terminal_injective)) * c) + (wpo_injective_value_wpoi_terminal_injective))) -> wpo_injective_left_wpoi_terminal_injective = wpo_injective_right_wpoi_terminal_injective) -> forall s. (exists wpo_gap_wpoi_terminal_value_bound. wpo_gap_wpoi_terminal_value_bound + S (s) = S (S l)) -> (~(s = 0) /\ ~((S s) = S (S l))) -> (exists q. ((exists wpo_gap_wpoi_terminal_index_bound. wpo_gap_wpoi_terminal_index_bound + S (q) = l) /\ (((exists wpo_beta_height_wpoi_terminal_entry. wpo_beta_height_wpoi_terminal_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_entry. b = wpo_beta_quotient_wpoi_terminal_entry * S ((S (q)) * c) + (s)))))

Structural proof guide

Generated structural guide

A bounded injective terminal prefix covers exactly every nonendpoint value below n = l+2.

Use the direct prerequisites one_le_of_ne_zero, le_of_succ_le_succ, le_eq_or_lt, nonzero_is_succ, beta_magnitude_predecessor_recode_exists, beta_magnitude_predecessor_recode_surjective, beta_magnitude_predecessor_recode_reflect as previously established PA formulas.

The proof proceeds by case analysis (11), intermediate claims (14), equality transport (6).

Referenced ingredients

PA002L one_le_of_ne_zero PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA001V nonzero_is_succ PA007D beta_magnitude_predecessor_recode_exists PA00B3 beta_magnitude_predecessor_recode_surjective PA007T beta_magnitude_predecessor_recode_reflect

Proof neighborhood

Direct dependencies

PA002L one_le_of_ne_zero PA000V le_of_succ_le_succ PA000W le_eq_or_lt PA001V nonzero_is_succ PA007D beta_magnitude_predecessor_recode_exists PA00B3 beta_magnitude_predecessor_recode_surjective PA007T beta_magnitude_predecessor_recode_reflect

Direct dependents

PA00B5 pair_order_state_terminal_coverage

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 hbounded
  5. 0005intro hnonendpoint
  6. 0006intro hinjective
  7. 0007have hmagnitude : forall gmp_index_wpoi_terminal_magnitude_range. (exists gsp_lt_gap_wpoi_terminal_magnitude_range_index_bound. gsp_lt_gap_wpoi_terminal_magnitude_range_index_bound + S gmp_index_wpoi_terminal_magnitude_range = l) -> exists gmp_magnitude_wpoi_terminal_magnitude_range. ((((exists ff_h_gmp_wpoi_terminal_magnitude_range_decoded. ff_h_gmp_wpoi_terminal_magnitude_range_decoded + S (gmp_magnitude_wpoi_terminal_magnitude_range) = S ((S (gmp_index_wpoi_terminal_magnitude_range)) * c)) /\ exists ff_q_gmp_wpoi_terminal_magnitude_range_decoded. b = ff_q_gmp_wpoi_terminal_magnitude_range_decoded * S ((S (gmp_index_wpoi_terminal_magnitude_range)) * c) + (gmp_magnitude_wpoi_terminal_magnitude_range))) /\ ((exists gsp_lt_gap_wpoi_terminal_magnitude_range_positive. gsp_lt_gap_wpoi_terminal_magnitude_range_positive + S 0 = gmp_magnitude_wpoi_terminal_magnitude_range) /\ (exists gsp_le_gap_wpoi_terminal_magnitude_range_bounded. gsp_le_gap_wpoi_terminal_magnitude_range_bounded + gmp_magnitude_wpoi_terminal_magnitude_range = l)))
  8. 0008intro q
  9. 0009intro hq
  10. 0010have hbounded_entry : exists x. ((((exists wpo_beta_height_wpoi_terminal_source_entry_x. wpo_beta_height_wpoi_terminal_source_entry_x + S (x) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_source_entry_x. b = wpo_beta_quotient_wpoi_terminal_source_entry_x * S ((S (q)) * c) + (x))) /\ (exists wpo_gap_wpoi_terminal_source_bound_x. wpo_gap_wpoi_terminal_source_bound_x + S (x) = S (S l)))
  11. 0011specialize hbounded q
  12. 0012apply hbounded
  13. 0013exact hq
  14. 0014cases hbounded_entry
  15. 0015cases hbounded_entry_witness
  16. 0016have hxnonendpoint : ~(x = 0) /\ ~((S x) = S (S l))
  17. 0017specialize hnonendpoint q
  18. 0018specialize hnonendpoint x
  19. 0019apply hnonendpoint
  20. 0020exact hq
  21. 0021exact hbounded_entry_witness_left
  22. 0022cases hxnonendpoint
  23. 0023exists x
  24. 0024split
  25. 0025exact hbounded_entry_witness_left
  26. 0026split
  27. 0027specialize one_le_of_ne_zero x
  28. 0028apply one_le_of_ne_zero
  29. 0029exact hxnonendpoint_left
  30. 0030have hxle_succ : exists h. h + x = S l
  31. 0031specialize le_of_succ_le_succ x
  32. 0032specialize le_of_succ_le_succ (S l)
  33. 0033apply le_of_succ_le_succ
  34. 0034exact hbounded_entry_witness_right
  35. 0035have hxsplit : x = S l \/ exists h. h + S x = S l
  36. 0036specialize le_eq_or_lt x
  37. 0037specialize le_eq_or_lt (S l)
  38. 0038apply le_eq_or_lt
  39. 0039exact hxle_succ
  40. 0040cases hxsplit
  41. 0041exfalso
  42. 0042apply hxnonendpoint_right
  43. 0043rewrite hxsplit_left
  44. 0044refl
  45. 0045specialize le_of_succ_le_succ x
  46. 0046specialize le_of_succ_le_succ l
  47. 0047apply le_of_succ_le_succ
  48. 0048exact hxsplit_right
  49. 0049have hrecode_exists : exists rb rc. (forall gmp_index_wpoi_terminal_recode gmp_predecessor_wpoi_terminal_recode. (exists gsp_lt_gap_wpoi_terminal_recode_index_bound. gsp_lt_gap_wpoi_terminal_recode_index_bound + S gmp_index_wpoi_terminal_recode = l) -> (((exists gsp_beta_height_gmp_wpoi_terminal_recode_source. gsp_beta_height_gmp_wpoi_terminal_recode_source + S (S gmp_predecessor_wpoi_terminal_recode) = S ((S (gmp_index_wpoi_terminal_recode)) * c)) /\ exists gsp_beta_quotient_gmp_wpoi_terminal_recode_source. b = gsp_beta_quotient_gmp_wpoi_terminal_recode_source * S ((S (gmp_index_wpoi_terminal_recode)) * c) + (S gmp_predecessor_wpoi_terminal_recode))) -> (((exists ff_h_gmp_wpoi_terminal_recode_target. ff_h_gmp_wpoi_terminal_recode_target + S (gmp_predecessor_wpoi_terminal_recode) = S ((S (gmp_index_wpoi_terminal_recode)) * rc)) /\ exists ff_q_gmp_wpoi_terminal_recode_target. rb = ff_q_gmp_wpoi_terminal_recode_target * S ((S (gmp_index_wpoi_terminal_recode)) * rc) + (gmp_predecessor_wpoi_terminal_recode))))
  50. 0050specialize beta_magnitude_predecessor_recode_exists b
  51. 0051specialize beta_magnitude_predecessor_recode_exists c
  52. 0052specialize beta_magnitude_predecessor_recode_exists l
  53. 0053specialize beta_magnitude_predecessor_recode_exists l
  54. 0054apply beta_magnitude_predecessor_recode_exists
  55. 0055exact hmagnitude
  56. 0056cases hrecode_exists
  57. 0057cases hrecode_exists_witness
  58. 0058have hrecode : forall gmp_index_wpoi_terminal_recode_x gmp_predecessor_wpoi_terminal_recode_x. (exists gsp_lt_gap_wpoi_terminal_recode_x_index_bound. gsp_lt_gap_wpoi_terminal_recode_x_index_bound + S gmp_index_wpoi_terminal_recode_x = l) -> (((exists gsp_beta_height_gmp_wpoi_terminal_recode_x_source. gsp_beta_height_gmp_wpoi_terminal_recode_x_source + S (S gmp_predecessor_wpoi_terminal_recode_x) = S ((S (gmp_index_wpoi_terminal_recode_x)) * c)) /\ exists gsp_beta_quotient_gmp_wpoi_terminal_recode_x_source. b = gsp_beta_quotient_gmp_wpoi_terminal_recode_x_source * S ((S (gmp_index_wpoi_terminal_recode_x)) * c) + (S gmp_predecessor_wpoi_terminal_recode_x))) -> (((exists ff_h_gmp_wpoi_terminal_recode_x_target. ff_h_gmp_wpoi_terminal_recode_x_target + S (gmp_predecessor_wpoi_terminal_recode_x) = S ((S (gmp_index_wpoi_terminal_recode_x)) * x1)) /\ exists ff_q_gmp_wpoi_terminal_recode_x_target. x = ff_q_gmp_wpoi_terminal_recode_x_target * S ((S (gmp_index_wpoi_terminal_recode_x)) * x1) + (gmp_predecessor_wpoi_terminal_recode_x)))
  59. 0059exact hrecode_exists_witness_witness
  60. 0060have hsurjective : forall fp_value_wpoi_terminal_recode_surjective_x. (exists fp_gap_wpoi_terminal_recode_surjective_x_value. fp_gap_wpoi_terminal_recode_surjective_x_value + S fp_value_wpoi_terminal_recode_surjective_x = l) -> exists fp_i_wpoi_terminal_recode_surjective_x. ((exists fp_gap_wpoi_terminal_recode_surjective_x_index. fp_gap_wpoi_terminal_recode_surjective_x_index + S fp_i_wpoi_terminal_recode_surjective_x = l) /\ (((exists ff_h_wpoi_terminal_recode_surjective_x_entry. ff_h_wpoi_terminal_recode_surjective_x_entry + S (fp_value_wpoi_terminal_recode_surjective_x) = S ((S (fp_i_wpoi_terminal_recode_surjective_x)) * x1)) /\ exists ff_q_wpoi_terminal_recode_surjective_x_entry. x = ff_q_wpoi_terminal_recode_surjective_x_entry * S ((S (fp_i_wpoi_terminal_recode_surjective_x)) * x1) + (fp_value_wpoi_terminal_recode_surjective_x))))
  61. 0061specialize beta_magnitude_predecessor_recode_surjective b
  62. 0062specialize beta_magnitude_predecessor_recode_surjective c
  63. 0063specialize beta_magnitude_predecessor_recode_surjective x
  64. 0064specialize beta_magnitude_predecessor_recode_surjective x1
  65. 0065specialize beta_magnitude_predecessor_recode_surjective l
  66. 0066apply beta_magnitude_predecessor_recode_surjective
  67. 0067exact hmagnitude
  68. 0068exact hinjective
  69. 0069exact hrecode
  70. 0070intro s
  71. 0071intro hsbound
  72. 0072intro hsendpoints
  73. 0073cases hsendpoints
  74. 0074have hspred : exists r. s = S r
  75. 0075specialize nonzero_is_succ s
  76. 0076apply nonzero_is_succ
  77. 0077exact hsendpoints_left
  78. 0078cases hspred
  79. 0079have hsle : exists h. h + s = S l
  80. 0080specialize le_of_succ_le_succ s
  81. 0081specialize le_of_succ_le_succ (S l)
  82. 0082apply le_of_succ_le_succ
  83. 0083exact hsbound
  84. 0084rewrite hspred_witness at hsle
  85. 0085have hrle : exists h. h + x2 = l
  86. 0086specialize le_of_succ_le_succ x2
  87. 0087specialize le_of_succ_le_succ l
  88. 0088apply le_of_succ_le_succ
  89. 0089exact hsle
  90. 0090have hrsplit : x2 = l \/ exists h. h + S x2 = l
  91. 0091specialize le_eq_or_lt x2
  92. 0092specialize le_eq_or_lt l
  93. 0093apply le_eq_or_lt
  94. 0094exact hrle
  95. 0095cases hrsplit
  96. 0096exfalso
  97. 0097apply hsendpoints_right
  98. 0098rewrite hspred_witness
  99. 0099rewrite hrsplit_left
  100. 0100refl
  101. 0101have htarget : exists q. ((exists wpo_gap_wpoi_terminal_target_occurrence_bound. wpo_gap_wpoi_terminal_target_occurrence_bound + S (q) = l) /\ (((exists wpo_beta_height_wpoi_terminal_target_occurrence_entry. wpo_beta_height_wpoi_terminal_target_occurrence_entry + S (x2) = S ((S (q)) * x1)) /\ exists wpo_beta_quotient_wpoi_terminal_target_occurrence_entry. x = wpo_beta_quotient_wpoi_terminal_target_occurrence_entry * S ((S (q)) * x1) + (x2))))
  102. 0102specialize hsurjective x2
  103. 0103apply hsurjective
  104. 0104exact hrsplit_right
  105. 0105cases htarget
  106. 0106cases htarget_witness
  107. 0107have hsource : ((exists wpo_beta_height_wpoi_terminal_source_entry_x2_succ_r. wpo_beta_height_wpoi_terminal_source_entry_x2_succ_r + S (S x2) = S ((S (x3)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_source_entry_x2_succ_r. b = wpo_beta_quotient_wpoi_terminal_source_entry_x2_succ_r * S ((S (x3)) * c) + (S x2))
  108. 0108specialize beta_magnitude_predecessor_recode_reflect b
  109. 0109specialize beta_magnitude_predecessor_recode_reflect c
  110. 0110specialize beta_magnitude_predecessor_recode_reflect x
  111. 0111specialize beta_magnitude_predecessor_recode_reflect x1
  112. 0112specialize beta_magnitude_predecessor_recode_reflect l
  113. 0113specialize beta_magnitude_predecessor_recode_reflect l
  114. 0114specialize beta_magnitude_predecessor_recode_reflect x3
  115. 0115specialize beta_magnitude_predecessor_recode_reflect x2
  116. 0116apply beta_magnitude_predecessor_recode_reflect
  117. 0117exact hmagnitude
  118. 0118exact hrecode
  119. 0119exact htarget_witness_left
  120. 0120exact htarget_witness_right
  121. 0121exists x3
  122. 0122split
  123. 0123exact htarget_witness_left
  124. 0124rewrite hspred_witness
  125. 0125rewrite hspred_witness
  126. 0126exact hsource