PA00BX

beta_division_prefix_extend

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

Append one quotient/remainder pair while preserving the decoded prefix.

Exact expanded PA statement

forall p b c qb qc rb rc l. (forall fdp_index_before. (exists gsp_lt_gap_before_index_bound. gsp_lt_gap_before_index_bound + S fdp_index_before = l) -> exists fdp_value_before fdp_quotient_before fdp_remainder_before. (((exists ff_h_fdp_before_source. ff_h_fdp_before_source + S (fdp_value_before) = S ((S (fdp_index_before)) * c)) /\ exists ff_q_fdp_before_source. b = ff_q_fdp_before_source * S ((S (fdp_index_before)) * c) + (fdp_value_before))) /\ ((((exists ff_h_fdp_before_quotient_entry. ff_h_fdp_before_quotient_entry + S (fdp_quotient_before) = S ((S (fdp_index_before)) * qc)) /\ exists ff_q_fdp_before_quotient_entry. qb = ff_q_fdp_before_quotient_entry * S ((S (fdp_index_before)) * qc) + (fdp_quotient_before))) /\ ((((exists ff_h_fdp_before_remainder_entry. ff_h_fdp_before_remainder_entry + S (fdp_remainder_before) = S ((S (fdp_index_before)) * rc)) /\ exists ff_q_fdp_before_remainder_entry. rb = ff_q_fdp_before_remainder_entry * S ((S (fdp_index_before)) * rc) + (fdp_remainder_before))) /\ (fdp_value_before = p * fdp_quotient_before + fdp_remainder_before /\ (exists gsp_lt_gap_before_remainder_bound. gsp_lt_gap_before_remainder_bound + S fdp_remainder_before = p))))) -> (exists x q r. (((exists ff_h_fdp_choice_source. ff_h_fdp_choice_source + S (x) = S ((S (l)) * c)) /\ exists ff_q_fdp_choice_source. b = ff_q_fdp_choice_source * S ((S (l)) * c) + (x))) /\ (x = p * q + r /\ (exists gsp_lt_gap_fdp_choice_remainder_bound. gsp_lt_gap_fdp_choice_remainder_bound + S r = p))) -> exists z d u v. (forall fdp_index_after. (exists gsp_lt_gap_after_index_bound. gsp_lt_gap_after_index_bound + S fdp_index_after = S l) -> exists fdp_value_after fdp_quotient_after fdp_remainder_after. (((exists ff_h_fdp_after_source. ff_h_fdp_after_source + S (fdp_value_after) = S ((S (fdp_index_after)) * c)) /\ exists ff_q_fdp_after_source. b = ff_q_fdp_after_source * S ((S (fdp_index_after)) * c) + (fdp_value_after))) /\ ((((exists ff_h_fdp_after_quotient_entry. ff_h_fdp_after_quotient_entry + S (fdp_quotient_after) = S ((S (fdp_index_after)) * d)) /\ exists ff_q_fdp_after_quotient_entry. z = ff_q_fdp_after_quotient_entry * S ((S (fdp_index_after)) * d) + (fdp_quotient_after))) /\ ((((exists ff_h_fdp_after_remainder_entry. ff_h_fdp_after_remainder_entry + S (fdp_remainder_after) = S ((S (fdp_index_after)) * v)) /\ exists ff_q_fdp_after_remainder_entry. u = ff_q_fdp_after_remainder_entry * S ((S (fdp_index_after)) * v) + (fdp_remainder_after))) /\ (fdp_value_after = p * fdp_quotient_after + fdp_remainder_after /\ (exists gsp_lt_gap_after_remainder_bound. gsp_lt_gap_after_remainder_bound + S fdp_remainder_after = p)))))

Structural proof guide

Generated structural guide

Append one quotient/remainder pair while preserving the decoded prefix.

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

The proof proceeds by case analysis (19), intermediate claims (4), equality transport (6).

Referenced ingredients

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Proof neighborhood

Direct dependencies

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct dependents

PA00BY beta_division_prefix_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 p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro qb
  5. 0005intro qc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro l
  9. 0009intro hprefix
  10. 0010intro hchoice
  11. 0011cases hchoice
  12. 0012cases hchoice_witness
  13. 0013cases hchoice_witness_witness
  14. 0014cases hchoice_witness_witness_witness
  15. 0015cases hchoice_witness_witness_witness_right
  16. 0016have hqextend : exists z d. (((exists ff_h_fdp_quotient_extension_last. ff_h_fdp_quotient_extension_last + S (x1) = S ((S (l)) * d)) /\ exists ff_q_fdp_quotient_extension_last. z = ff_q_fdp_quotient_extension_last * S ((S (l)) * d) + (x1))) /\ forall i q0. (exists gsp_lt_gap_fdp_quotient_extension_old_bound. gsp_lt_gap_fdp_quotient_extension_old_bound + S i = l) -> (((exists ff_h_fdp_quotient_extension_old_source. ff_h_fdp_quotient_extension_old_source + S (q0) = S ((S (i)) * qc)) /\ exists ff_q_fdp_quotient_extension_old_source. qb = ff_q_fdp_quotient_extension_old_source * S ((S (i)) * qc) + (q0))) -> (((exists ff_h_fdp_quotient_extension_old_target_symbolic. ff_h_fdp_quotient_extension_old_target_symbolic + S (q0) = S ((S (i)) * d)) /\ exists ff_q_fdp_quotient_extension_old_target_symbolic. z = ff_q_fdp_quotient_extension_old_target_symbolic * S ((S (i)) * d) + (q0)))
  17. 0017specialize beta_prefix_extend l
  18. 0018specialize beta_prefix_extend qb
  19. 0019specialize beta_prefix_extend qc
  20. 0020specialize beta_prefix_extend x1
  21. 0021exact beta_prefix_extend
  22. 0022cases hqextend
  23. 0023cases hqextend_witness
  24. 0024cases hqextend_witness_witness
  25. 0025have hrextend : exists u v. (((exists ff_h_fdp_remainder_extension_last. ff_h_fdp_remainder_extension_last + S (x2) = S ((S (l)) * v)) /\ exists ff_q_fdp_remainder_extension_last. u = ff_q_fdp_remainder_extension_last * S ((S (l)) * v) + (x2))) /\ forall i r0. (exists gsp_lt_gap_fdp_remainder_extension_old_bound. gsp_lt_gap_fdp_remainder_extension_old_bound + S i = l) -> (((exists ff_h_fdp_remainder_extension_old_source. ff_h_fdp_remainder_extension_old_source + S (r0) = S ((S (i)) * rc)) /\ exists ff_q_fdp_remainder_extension_old_source. rb = ff_q_fdp_remainder_extension_old_source * S ((S (i)) * rc) + (r0))) -> (((exists ff_h_fdp_remainder_extension_old_target. ff_h_fdp_remainder_extension_old_target + S (r0) = S ((S (i)) * v)) /\ exists ff_q_fdp_remainder_extension_old_target. u = ff_q_fdp_remainder_extension_old_target * S ((S (i)) * v) + (r0)))
  26. 0026specialize beta_prefix_extend l
  27. 0027specialize beta_prefix_extend rb
  28. 0028specialize beta_prefix_extend rc
  29. 0029specialize beta_prefix_extend x2
  30. 0030exact beta_prefix_extend
  31. 0031cases hrextend
  32. 0032cases hrextend_witness
  33. 0033cases hrextend_witness_witness
  34. 0034exists x3
  35. 0035exists x4
  36. 0036exists x5
  37. 0037exists x6
  38. 0038intro i
  39. 0039intro hi
  40. 0040have hsplit : i = l \/ exists gap. gap + S i = l
  41. 0041specialize finite_lt_succ_eq_or_lt l
  42. 0042specialize finite_lt_succ_eq_or_lt i
  43. 0043apply finite_lt_succ_eq_or_lt
  44. 0044exact hi
  45. 0045cases hsplit
  46. 0046exists x
  47. 0047exists x1
  48. 0048exists x2
  49. 0049split
  50. 0050rewrite hsplit_left
  51. 0051rewrite hsplit_left
  52. 0052exact hchoice_witness_witness_witness_left
  53. 0053split
  54. 0054rewrite hsplit_left
  55. 0055rewrite hsplit_left
  56. 0056exact hqextend_witness_witness_left
  57. 0057split
  58. 0058rewrite hsplit_left
  59. 0059rewrite hsplit_left
  60. 0060exact hrextend_witness_witness_left
  61. 0061split
  62. 0062exact hchoice_witness_witness_witness_right_left
  63. 0063exact hchoice_witness_witness_witness_right_right
  64. 0064have hold : exists x q r. (((exists ff_h_fdp_previous_source. ff_h_fdp_previous_source + S (x) = S ((S (i)) * c)) /\ exists ff_q_fdp_previous_source. b = ff_q_fdp_previous_source * S ((S (i)) * c) + (x))) /\ ((((exists ff_h_fdp_previous_quotient. ff_h_fdp_previous_quotient + S (q) = S ((S (i)) * qc)) /\ exists ff_q_fdp_previous_quotient. qb = ff_q_fdp_previous_quotient * S ((S (i)) * qc) + (q))) /\ ((((exists ff_h_fdp_previous_remainder. ff_h_fdp_previous_remainder + S (r) = S ((S (i)) * rc)) /\ exists ff_q_fdp_previous_remainder. rb = ff_q_fdp_previous_remainder * S ((S (i)) * rc) + (r))) /\ (x = p * q + r /\ (exists gsp_lt_gap_fdp_previous_remainder_bound. gsp_lt_gap_fdp_previous_remainder_bound + S r = p))))
  65. 0065specialize hprefix i
  66. 0066apply hprefix
  67. 0067exact hsplit_right
  68. 0068cases hold
  69. 0069cases hold_witness
  70. 0070cases hold_witness_witness
  71. 0071cases hold_witness_witness_witness
  72. 0072cases hold_witness_witness_witness_right
  73. 0073cases hold_witness_witness_witness_right_right
  74. 0074cases hold_witness_witness_witness_right_right_right
  75. 0075exists x7
  76. 0076exists x8
  77. 0077exists x9
  78. 0078split
  79. 0079exact hold_witness_witness_witness_left
  80. 0080split
  81. 0081specialize hqextend_witness_witness_right i
  82. 0082specialize hqextend_witness_witness_right x8
  83. 0083apply hqextend_witness_witness_right
  84. 0084exact hsplit_right
  85. 0085exact hold_witness_witness_witness_right_left
  86. 0086split
  87. 0087specialize hrextend_witness_witness_right i
  88. 0088specialize hrextend_witness_witness_right x9
  89. 0089apply hrextend_witness_witness_right
  90. 0090exact hsplit_right
  91. 0091exact hold_witness_witness_witness_right_right_left
  92. 0092split
  93. 0093exact hold_witness_witness_witness_right_right_right_left
  94. 0094exact hold_witness_witness_witness_right_right_right_right