PA007K

beta_pointwise_mul_prefix_extend

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

Append the product of the two final decoded values and preserve all earlier products.

Exact expanded PA statement

forall mb mc sb sc tb tc l m s. (forall fpmp_index_recode_before fpmp_left_recode_before fpmp_right_recode_before fpmp_target_recode_before. (exists fpmp_gap_recode_before. fpmp_gap_recode_before + S fpmp_index_recode_before = l) -> (((exists ff_h_fpmp_recode_before_left. ff_h_fpmp_recode_before_left + S (fpmp_left_recode_before) = S ((S (fpmp_index_recode_before)) * mc)) /\ exists ff_q_fpmp_recode_before_left. mb = ff_q_fpmp_recode_before_left * S ((S (fpmp_index_recode_before)) * mc) + (fpmp_left_recode_before))) -> (((exists ff_h_fpmp_recode_before_right. ff_h_fpmp_recode_before_right + S (fpmp_right_recode_before) = S ((S (fpmp_index_recode_before)) * sc)) /\ exists ff_q_fpmp_recode_before_right. sb = ff_q_fpmp_recode_before_right * S ((S (fpmp_index_recode_before)) * sc) + (fpmp_right_recode_before))) -> (((exists ff_h_fpmp_recode_before_target. ff_h_fpmp_recode_before_target + S (fpmp_target_recode_before) = S ((S (fpmp_index_recode_before)) * tc)) /\ exists ff_q_fpmp_recode_before_target. tb = ff_q_fpmp_recode_before_target * S ((S (fpmp_index_recode_before)) * tc) + (fpmp_target_recode_before))) -> fpmp_target_recode_before = fpmp_left_recode_before * fpmp_right_recode_before) -> (((exists ff_h_recode_left_last. ff_h_recode_left_last + S (m) = S ((S (l)) * mc)) /\ exists ff_q_recode_left_last. mb = ff_q_recode_left_last * S ((S (l)) * mc) + (m))) -> (((exists ff_h_recode_right_last. ff_h_recode_right_last + S (s) = S ((S (l)) * sc)) /\ exists ff_q_recode_right_last. sb = ff_q_recode_right_last * S ((S (l)) * sc) + (s))) -> exists z d. (forall fpmp_index_recode_after fpmp_left_recode_after fpmp_right_recode_after fpmp_target_recode_after. (exists fpmp_gap_recode_after. fpmp_gap_recode_after + S fpmp_index_recode_after = S l) -> (((exists ff_h_fpmp_recode_after_left. ff_h_fpmp_recode_after_left + S (fpmp_left_recode_after) = S ((S (fpmp_index_recode_after)) * mc)) /\ exists ff_q_fpmp_recode_after_left. mb = ff_q_fpmp_recode_after_left * S ((S (fpmp_index_recode_after)) * mc) + (fpmp_left_recode_after))) -> (((exists ff_h_fpmp_recode_after_right. ff_h_fpmp_recode_after_right + S (fpmp_right_recode_after) = S ((S (fpmp_index_recode_after)) * sc)) /\ exists ff_q_fpmp_recode_after_right. sb = ff_q_fpmp_recode_after_right * S ((S (fpmp_index_recode_after)) * sc) + (fpmp_right_recode_after))) -> (((exists ff_h_fpmp_recode_after_target. ff_h_fpmp_recode_after_target + S (fpmp_target_recode_after) = S ((S (fpmp_index_recode_after)) * d)) /\ exists ff_q_fpmp_recode_after_target. z = ff_q_fpmp_recode_after_target * S ((S (fpmp_index_recode_after)) * d) + (fpmp_target_recode_after))) -> fpmp_target_recode_after = fpmp_left_recode_after * fpmp_right_recode_after)

Structural proof guide

Generated structural guide

Append the product of the two final decoded values and preserve all earlier products.

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

The proof proceeds by case analysis (5), intermediate claims (9), equality transport (6).

Referenced ingredients

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique

Direct dependents

PA007L beta_pointwise_mul_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 mb
  2. 0002intro mc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro tb
  6. 0006intro tc
  7. 0007intro l
  8. 0008intro m
  9. 0009intro s
  10. 0010intro haligned
  11. 0011intro hm_last
  12. 0012intro hs_last
  13. 0013specialize beta_prefix_extend l
  14. 0014specialize beta_prefix_extend tb
  15. 0015specialize beta_prefix_extend tc
  16. 0016specialize beta_prefix_extend (m * s)
  17. 0017cases beta_prefix_extend
  18. 0018cases beta_prefix_extend_witness
  19. 0019cases beta_prefix_extend_witness_witness
  20. 0020exists x
  21. 0021exists x1
  22. 0022intro i
  23. 0023intro a
  24. 0024intro b
  25. 0025intro t
  26. 0026intro hi
  27. 0027intro ha
  28. 0028intro hb
  29. 0029intro ht
  30. 0030have hsplit : i = l \/ exists gap. gap + S i = l
  31. 0031specialize finite_lt_succ_eq_or_lt l
  32. 0032specialize finite_lt_succ_eq_or_lt i
  33. 0033apply finite_lt_succ_eq_or_lt
  34. 0034exact hi
  35. 0035cases hsplit
  36. 0036rewrite hsplit_left at ha
  37. 0037rewrite hsplit_left at ha
  38. 0038rewrite hsplit_left at hb
  39. 0039rewrite hsplit_left at hb
  40. 0040rewrite hsplit_left at ht
  41. 0041rewrite hsplit_left at ht
  42. 0042have hma : m = a
  43. 0043specialize beta_at_unique mb
  44. 0044specialize beta_at_unique mc
  45. 0045specialize beta_at_unique l
  46. 0046specialize beta_at_unique m
  47. 0047specialize beta_at_unique a
  48. 0048apply beta_at_unique
  49. 0049exact hm_last
  50. 0050exact ha
  51. 0051have hsb : s = b
  52. 0052specialize beta_at_unique sb
  53. 0053specialize beta_at_unique sc
  54. 0054specialize beta_at_unique l
  55. 0055specialize beta_at_unique s
  56. 0056specialize beta_at_unique b
  57. 0057apply beta_at_unique
  58. 0058exact hs_last
  59. 0059exact hb
  60. 0060have happended : ((exists fpmr_height_recode_appended_product. fpmr_height_recode_appended_product + S (m * s) = S ((S (l)) * x1)) /\ exists fpmr_quotient_recode_appended_product. x = fpmr_quotient_recode_appended_product * S ((S (l)) * x1) + (m * s))
  61. 0061exact beta_prefix_extend_witness_witness_left
  62. 0062have ht_product : t = m * s
  63. 0063specialize beta_at_unique x
  64. 0064specialize beta_at_unique x1
  65. 0065specialize beta_at_unique l
  66. 0066specialize beta_at_unique t
  67. 0067specialize beta_at_unique (m * s)
  68. 0068apply beta_at_unique
  69. 0069exact ht
  70. 0070exact happended
  71. 0071trans m * s
  72. 0072exact ht_product
  73. 0073congr
  74. 0074exact hma
  75. 0075exact hsb
  76. 0076have hold_exists : exists u. (((exists ff_h_recode_old_target_exists. ff_h_recode_old_target_exists + S (u) = S ((S (i)) * tc)) /\ exists ff_q_recode_old_target_exists. tb = ff_q_recode_old_target_exists * S ((S (i)) * tc) + (u)))
  77. 0077specialize beta_at_exists tb
  78. 0078specialize beta_at_exists tc
  79. 0079specialize beta_at_exists i
  80. 0080exact beta_at_exists
  81. 0081cases hold_exists
  82. 0082have hnew_old : ((exists ff_h_recode_new_old_target_entry. ff_h_recode_new_old_target_entry + S (x2) = S ((S (i)) * x1)) /\ exists ff_q_recode_new_old_target_entry. x = ff_q_recode_new_old_target_entry * S ((S (i)) * x1) + (x2))
  83. 0083specialize beta_prefix_extend_witness_witness_right i
  84. 0084specialize beta_prefix_extend_witness_witness_right x2
  85. 0085apply beta_prefix_extend_witness_witness_right
  86. 0086exact hsplit_right
  87. 0087exact hold_exists_witness
  88. 0088have htx : t = x2
  89. 0089specialize beta_at_unique x
  90. 0090specialize beta_at_unique x1
  91. 0091specialize beta_at_unique i
  92. 0092specialize beta_at_unique t
  93. 0093specialize beta_at_unique x2
  94. 0094apply beta_at_unique
  95. 0095exact ht
  96. 0096exact hnew_old
  97. 0097have hold_product : x2 = a * b
  98. 0098specialize haligned i
  99. 0099specialize haligned a
  100. 0100specialize haligned b
  101. 0101specialize haligned x2
  102. 0102apply haligned
  103. 0103exact hsplit_right
  104. 0104exact ha
  105. 0105exact hb
  106. 0106exact hold_exists_witness
  107. 0107trans x2
  108. 0108exact htx
  109. 0109exact hold_product