PA007L

beta_pointwise_mul_prefix_exists

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

Two beta prefixes admit a third beta prefix of their pointwise products.

Exact expanded PA statement

forall mb mc sb sc l. exists tb tc. (forall fpmp_index_recode_exists_result fpmp_left_recode_exists_result fpmp_right_recode_exists_result fpmp_target_recode_exists_result. (exists fpmp_gap_recode_exists_result. fpmp_gap_recode_exists_result + S fpmp_index_recode_exists_result = l) -> (((exists ff_h_fpmp_recode_exists_result_left. ff_h_fpmp_recode_exists_result_left + S (fpmp_left_recode_exists_result) = S ((S (fpmp_index_recode_exists_result)) * mc)) /\ exists ff_q_fpmp_recode_exists_result_left. mb = ff_q_fpmp_recode_exists_result_left * S ((S (fpmp_index_recode_exists_result)) * mc) + (fpmp_left_recode_exists_result))) -> (((exists ff_h_fpmp_recode_exists_result_right. ff_h_fpmp_recode_exists_result_right + S (fpmp_right_recode_exists_result) = S ((S (fpmp_index_recode_exists_result)) * sc)) /\ exists ff_q_fpmp_recode_exists_result_right. sb = ff_q_fpmp_recode_exists_result_right * S ((S (fpmp_index_recode_exists_result)) * sc) + (fpmp_right_recode_exists_result))) -> (((exists ff_h_fpmp_recode_exists_result_target. ff_h_fpmp_recode_exists_result_target + S (fpmp_target_recode_exists_result) = S ((S (fpmp_index_recode_exists_result)) * tc)) /\ exists ff_q_fpmp_recode_exists_result_target. tb = ff_q_fpmp_recode_exists_result_target * S ((S (fpmp_index_recode_exists_result)) * tc) + (fpmp_target_recode_exists_result))) -> fpmp_target_recode_exists_result = fpmp_left_recode_exists_result * fpmp_right_recode_exists_result)

Structural proof guide

Generated structural guide

Two beta prefixes admit a third beta prefix of their pointwise products.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, beta_at_exists, beta_pointwise_mul_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (5), intermediate claims (4).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0029 beta_at_exists PA007K beta_pointwise_mul_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0029 beta_at_exists PA007K beta_pointwise_mul_prefix_extend

Direct dependents

PA007O beta_pointwise_mul_product_exists PA00C0 prime_scaled_half_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 mb
  2. 0002intro mc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005induction l
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro i
  9. 0009intro a
  10. 0010intro b
  11. 0011intro t
  12. 0012intro hi
  13. 0013intro ha
  14. 0014intro hb
  15. 0015intro ht
  16. 0016exfalso
  17. 0017cases hi
  18. 0018have hsi : 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 hsi
  26. 0026have hprevious : exists tb tc. (forall fpmp_index_recode_exists_previous fpmp_left_recode_exists_previous fpmp_right_recode_exists_previous fpmp_target_recode_exists_previous. (exists fpmp_gap_recode_exists_previous. fpmp_gap_recode_exists_previous + S fpmp_index_recode_exists_previous = l) -> (((exists ff_h_fpmp_recode_exists_previous_left. ff_h_fpmp_recode_exists_previous_left + S (fpmp_left_recode_exists_previous) = S ((S (fpmp_index_recode_exists_previous)) * mc)) /\ exists ff_q_fpmp_recode_exists_previous_left. mb = ff_q_fpmp_recode_exists_previous_left * S ((S (fpmp_index_recode_exists_previous)) * mc) + (fpmp_left_recode_exists_previous))) -> (((exists ff_h_fpmp_recode_exists_previous_right. ff_h_fpmp_recode_exists_previous_right + S (fpmp_right_recode_exists_previous) = S ((S (fpmp_index_recode_exists_previous)) * sc)) /\ exists ff_q_fpmp_recode_exists_previous_right. sb = ff_q_fpmp_recode_exists_previous_right * S ((S (fpmp_index_recode_exists_previous)) * sc) + (fpmp_right_recode_exists_previous))) -> (((exists ff_h_fpmp_recode_exists_previous_target. ff_h_fpmp_recode_exists_previous_target + S (fpmp_target_recode_exists_previous) = S ((S (fpmp_index_recode_exists_previous)) * tc)) /\ exists ff_q_fpmp_recode_exists_previous_target. tb = ff_q_fpmp_recode_exists_previous_target * S ((S (fpmp_index_recode_exists_previous)) * tc) + (fpmp_target_recode_exists_previous))) -> fpmp_target_recode_exists_previous = fpmp_left_recode_exists_previous * fpmp_right_recode_exists_previous)
  27. 0027exact IH
  28. 0028cases hprevious
  29. 0029cases hprevious_witness
  30. 0030have hleft : exists m. (((exists ff_h_recode_exists_left_last. ff_h_recode_exists_left_last + S (m) = S ((S (l)) * mc)) /\ exists ff_q_recode_exists_left_last. mb = ff_q_recode_exists_left_last * S ((S (l)) * mc) + (m)))
  31. 0031specialize beta_at_exists mb
  32. 0032specialize beta_at_exists mc
  33. 0033specialize beta_at_exists l
  34. 0034exact beta_at_exists
  35. 0035cases hleft
  36. 0036have hright : exists s. (((exists ff_h_recode_exists_right_last. ff_h_recode_exists_right_last + S (s) = S ((S (l)) * sc)) /\ exists ff_q_recode_exists_right_last. sb = ff_q_recode_exists_right_last * S ((S (l)) * sc) + (s)))
  37. 0037specialize beta_at_exists sb
  38. 0038specialize beta_at_exists sc
  39. 0039specialize beta_at_exists l
  40. 0040exact beta_at_exists
  41. 0041cases hright
  42. 0042specialize beta_pointwise_mul_prefix_extend mb
  43. 0043specialize beta_pointwise_mul_prefix_extend mc
  44. 0044specialize beta_pointwise_mul_prefix_extend sb
  45. 0045specialize beta_pointwise_mul_prefix_extend sc
  46. 0046specialize beta_pointwise_mul_prefix_extend x
  47. 0047specialize beta_pointwise_mul_prefix_extend x1
  48. 0048specialize beta_pointwise_mul_prefix_extend l
  49. 0049specialize beta_pointwise_mul_prefix_extend x2
  50. 0050specialize beta_pointwise_mul_prefix_extend x3
  51. 0051apply beta_pointwise_mul_prefix_extend
  52. 0052exact hprevious_witness_witness
  53. 0053exact hleft_witness
  54. 0054exact hright_witness