PA007W

beta_product_reindex_fixed_last

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

A fixed-final reindex reduces successor product equality to equality of the two prefix products.

Exact expanded PA statement

forall r s b c z d n p q. (forall fpr_i_fra fpr_j_fra fpr_x_fra. (exists fpr_h_fra. fpr_h_fra + S fpr_i_fra = S n) -> (((exists ff_h_fra_map. ff_h_fra_map + S (fpr_j_fra) = S ((S (fpr_i_fra)) * s)) /\ exists ff_q_fra_map. r = ff_q_fra_map * S ((S (fpr_i_fra)) * s) + (fpr_j_fra))) -> (((exists ff_h_fra_source. ff_h_fra_source + S (fpr_x_fra) = S ((S (fpr_j_fra)) * c)) /\ exists ff_q_fra_source. b = ff_q_fra_source * S ((S (fpr_j_fra)) * c) + (fpr_x_fra))) -> (((exists ff_h_fra_target. ff_h_fra_target + S (fpr_x_fra) = S ((S (fpr_i_fra)) * d)) /\ exists ff_q_fra_target. z = ff_q_fra_target * S ((S (fpr_i_fra)) * d) + (fpr_x_fra)))) -> (((exists ff_h_frm. ff_h_frm + S (n) = S ((S (n)) * s)) /\ exists ff_q_frm. r = ff_q_frm * S ((S (n)) * s) + (n))) -> (exists ff_u_frs ff_v_frs. ((((exists ff_h_frs_start. ff_h_frs_start + S (1) = S ((S (0)) * ff_v_frs)) /\ exists ff_q_frs_start. ff_u_frs = ff_q_frs_start * S ((S (0)) * ff_v_frs) + (1))) /\ ((((exists ff_h_frs_terminal. ff_h_frs_terminal + S (p) = S ((S (S n)) * ff_v_frs)) /\ exists ff_q_frs_terminal. ff_u_frs = ff_q_frs_terminal * S ((S (S n)) * ff_v_frs) + (p))) /\ forall ff_i_frs. (exists ff_lt_frs_bound. ff_lt_frs_bound + S ff_i_frs = S n) -> exists ff_p_frs ff_r_frs ff_s_frs. ((((exists ff_h_frs_factor. ff_h_frs_factor + S (ff_p_frs) = S ((S (ff_i_frs)) * c)) /\ exists ff_q_frs_factor. b = ff_q_frs_factor * S ((S (ff_i_frs)) * c) + (ff_p_frs))) /\ ((((exists ff_h_frs_partial. ff_h_frs_partial + S (ff_r_frs) = S ((S (ff_i_frs)) * ff_v_frs)) /\ exists ff_q_frs_partial. ff_u_frs = ff_q_frs_partial * S ((S (ff_i_frs)) * ff_v_frs) + (ff_r_frs))) /\ ((((exists ff_h_frs_successor. ff_h_frs_successor + S (ff_s_frs) = S ((S (S ff_i_frs)) * ff_v_frs)) /\ exists ff_q_frs_successor. ff_u_frs = ff_q_frs_successor * S ((S (S ff_i_frs)) * ff_v_frs) + (ff_s_frs))) /\ ff_s_frs = ff_r_frs * ff_p_frs)))))) -> (exists ff_u_frt ff_v_frt. ((((exists ff_h_frt_start. ff_h_frt_start + S (1) = S ((S (0)) * ff_v_frt)) /\ exists ff_q_frt_start. ff_u_frt = ff_q_frt_start * S ((S (0)) * ff_v_frt) + (1))) /\ ((((exists ff_h_frt_terminal. ff_h_frt_terminal + S (q) = S ((S (S n)) * ff_v_frt)) /\ exists ff_q_frt_terminal. ff_u_frt = ff_q_frt_terminal * S ((S (S n)) * ff_v_frt) + (q))) /\ forall ff_i_frt. (exists ff_lt_frt_bound. ff_lt_frt_bound + S ff_i_frt = S n) -> exists ff_p_frt ff_r_frt ff_s_frt. ((((exists ff_h_frt_factor. ff_h_frt_factor + S (ff_p_frt) = S ((S (ff_i_frt)) * d)) /\ exists ff_q_frt_factor. z = ff_q_frt_factor * S ((S (ff_i_frt)) * d) + (ff_p_frt))) /\ ((((exists ff_h_frt_partial. ff_h_frt_partial + S (ff_r_frt) = S ((S (ff_i_frt)) * ff_v_frt)) /\ exists ff_q_frt_partial. ff_u_frt = ff_q_frt_partial * S ((S (ff_i_frt)) * ff_v_frt) + (ff_r_frt))) /\ ((((exists ff_h_frt_successor. ff_h_frt_successor + S (ff_s_frt) = S ((S (S ff_i_frt)) * ff_v_frt)) /\ exists ff_q_frt_successor. ff_u_frt = ff_q_frt_successor * S ((S (S ff_i_frt)) * ff_v_frt) + (ff_s_frt))) /\ ff_s_frt = ff_r_frt * ff_p_frt)))))) -> (forall u v. (exists ff_u_fru ff_v_fru. ((((exists ff_h_fru_start. ff_h_fru_start + S (1) = S ((S (0)) * ff_v_fru)) /\ exists ff_q_fru_start. ff_u_fru = ff_q_fru_start * S ((S (0)) * ff_v_fru) + (1))) /\ ((((exists ff_h_fru_terminal. ff_h_fru_terminal + S (u) = S ((S (n)) * ff_v_fru)) /\ exists ff_q_fru_terminal. ff_u_fru = ff_q_fru_terminal * S ((S (n)) * ff_v_fru) + (u))) /\ forall ff_i_fru. (exists ff_lt_fru_bound. ff_lt_fru_bound + S ff_i_fru = n) -> exists ff_p_fru ff_r_fru ff_s_fru. ((((exists ff_h_fru_factor. ff_h_fru_factor + S (ff_p_fru) = S ((S (ff_i_fru)) * c)) /\ exists ff_q_fru_factor. b = ff_q_fru_factor * S ((S (ff_i_fru)) * c) + (ff_p_fru))) /\ ((((exists ff_h_fru_partial. ff_h_fru_partial + S (ff_r_fru) = S ((S (ff_i_fru)) * ff_v_fru)) /\ exists ff_q_fru_partial. ff_u_fru = ff_q_fru_partial * S ((S (ff_i_fru)) * ff_v_fru) + (ff_r_fru))) /\ ((((exists ff_h_fru_successor. ff_h_fru_successor + S (ff_s_fru) = S ((S (S ff_i_fru)) * ff_v_fru)) /\ exists ff_q_fru_successor. ff_u_fru = ff_q_fru_successor * S ((S (S ff_i_fru)) * ff_v_fru) + (ff_s_fru))) /\ ff_s_fru = ff_r_fru * ff_p_fru)))))) -> (exists ff_u_frv ff_v_frv. ((((exists ff_h_frv_start. ff_h_frv_start + S (1) = S ((S (0)) * ff_v_frv)) /\ exists ff_q_frv_start. ff_u_frv = ff_q_frv_start * S ((S (0)) * ff_v_frv) + (1))) /\ ((((exists ff_h_frv_terminal. ff_h_frv_terminal + S (v) = S ((S (n)) * ff_v_frv)) /\ exists ff_q_frv_terminal. ff_u_frv = ff_q_frv_terminal * S ((S (n)) * ff_v_frv) + (v))) /\ forall ff_i_frv. (exists ff_lt_frv_bound. ff_lt_frv_bound + S ff_i_frv = n) -> exists ff_p_frv ff_r_frv ff_s_frv. ((((exists ff_h_frv_factor. ff_h_frv_factor + S (ff_p_frv) = S ((S (ff_i_frv)) * d)) /\ exists ff_q_frv_factor. z = ff_q_frv_factor * S ((S (ff_i_frv)) * d) + (ff_p_frv))) /\ ((((exists ff_h_frv_partial. ff_h_frv_partial + S (ff_r_frv) = S ((S (ff_i_frv)) * ff_v_frv)) /\ exists ff_q_frv_partial. ff_u_frv = ff_q_frv_partial * S ((S (ff_i_frv)) * ff_v_frv) + (ff_r_frv))) /\ ((((exists ff_h_frv_successor. ff_h_frv_successor + S (ff_s_frv) = S ((S (S ff_i_frv)) * ff_v_frv)) /\ exists ff_q_frv_successor. ff_u_frv = ff_q_frv_successor * S ((S (S ff_i_frv)) * ff_v_frv) + (ff_s_frv))) /\ ff_s_frv = ff_r_frv * ff_p_frv)))))) -> u = v) -> p = q

Structural proof guide

Generated structural guide

A fixed-final reindex reduces successor product equality to equality of the two prefix products.

Use the direct prerequisites beta_product_succ_decompose, beta_at_unique, le_refl as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (5), equality transport (4).

Referenced ingredients

PA004A beta_product_succ_decompose PA002F beta_at_unique PA001A le_refl

Proof neighborhood

Direct dependencies

PA004A beta_product_succ_decompose PA002F beta_at_unique PA001A le_refl

Direct dependents

PA007X beta_product_permutation_invariant

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 r
  2. 0002intro s
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro n
  8. 0008intro p
  9. 0009intro q
  10. 0010intro haligned
  11. 0011intro hmap_last
  12. 0012intro hsource_product
  13. 0013intro htarget_product
  14. 0014intro hprefix_equal
  15. 0015have hsource_decomp : exists a u. (((exists ff_h_fixed_reindex_source_last. ff_h_fixed_reindex_source_last + S (a) = S ((S (n)) * c)) /\ exists ff_q_fixed_reindex_source_last. b = ff_q_fixed_reindex_source_last * S ((S (n)) * c) + (a))) /\ ((exists ff_u_fixed_reindex_source_prefix_witness ff_v_fixed_reindex_source_prefix_witness. ((((exists ff_h_fixed_reindex_source_prefix_witness_start. ff_h_fixed_reindex_source_prefix_witness_start + S (1) = S ((S (0)) * ff_v_fixed_reindex_source_prefix_witness)) /\ exists ff_q_fixed_reindex_source_prefix_witness_start. ff_u_fixed_reindex_source_prefix_witness = ff_q_fixed_reindex_source_prefix_witness_start * S ((S (0)) * ff_v_fixed_reindex_source_prefix_witness) + (1))) /\ ((((exists ff_h_fixed_reindex_source_prefix_witness_terminal. ff_h_fixed_reindex_source_prefix_witness_terminal + S (u) = S ((S (n)) * ff_v_fixed_reindex_source_prefix_witness)) /\ exists ff_q_fixed_reindex_source_prefix_witness_terminal. ff_u_fixed_reindex_source_prefix_witness = ff_q_fixed_reindex_source_prefix_witness_terminal * S ((S (n)) * ff_v_fixed_reindex_source_prefix_witness) + (u))) /\ forall ff_i_fixed_reindex_source_prefix_witness. (exists ff_lt_fixed_reindex_source_prefix_witness_bound. ff_lt_fixed_reindex_source_prefix_witness_bound + S ff_i_fixed_reindex_source_prefix_witness = n) -> exists ff_p_fixed_reindex_source_prefix_witness ff_r_fixed_reindex_source_prefix_witness ff_s_fixed_reindex_source_prefix_witness. ((((exists ff_h_fixed_reindex_source_prefix_witness_factor. ff_h_fixed_reindex_source_prefix_witness_factor + S (ff_p_fixed_reindex_source_prefix_witness) = S ((S (ff_i_fixed_reindex_source_prefix_witness)) * c)) /\ exists ff_q_fixed_reindex_source_prefix_witness_factor. b = ff_q_fixed_reindex_source_prefix_witness_factor * S ((S (ff_i_fixed_reindex_source_prefix_witness)) * c) + (ff_p_fixed_reindex_source_prefix_witness))) /\ ((((exists ff_h_fixed_reindex_source_prefix_witness_partial. ff_h_fixed_reindex_source_prefix_witness_partial + S (ff_r_fixed_reindex_source_prefix_witness) = S ((S (ff_i_fixed_reindex_source_prefix_witness)) * ff_v_fixed_reindex_source_prefix_witness)) /\ exists ff_q_fixed_reindex_source_prefix_witness_partial. ff_u_fixed_reindex_source_prefix_witness = ff_q_fixed_reindex_source_prefix_witness_partial * S ((S (ff_i_fixed_reindex_source_prefix_witness)) * ff_v_fixed_reindex_source_prefix_witness) + (ff_r_fixed_reindex_source_prefix_witness))) /\ ((((exists ff_h_fixed_reindex_source_prefix_witness_successor. ff_h_fixed_reindex_source_prefix_witness_successor + S (ff_s_fixed_reindex_source_prefix_witness) = S ((S (S ff_i_fixed_reindex_source_prefix_witness)) * ff_v_fixed_reindex_source_prefix_witness)) /\ exists ff_q_fixed_reindex_source_prefix_witness_successor. ff_u_fixed_reindex_source_prefix_witness = ff_q_fixed_reindex_source_prefix_witness_successor * S ((S (S ff_i_fixed_reindex_source_prefix_witness)) * ff_v_fixed_reindex_source_prefix_witness) + (ff_s_fixed_reindex_source_prefix_witness))) /\ ff_s_fixed_reindex_source_prefix_witness = ff_r_fixed_reindex_source_prefix_witness * ff_p_fixed_reindex_source_prefix_witness)))))) /\ p = u * a)
  16. 0016specialize beta_product_succ_decompose b
  17. 0017specialize beta_product_succ_decompose c
  18. 0018specialize beta_product_succ_decompose n
  19. 0019specialize beta_product_succ_decompose p
  20. 0020apply beta_product_succ_decompose
  21. 0021exact hsource_product
  22. 0022have htarget_decomp : exists a v. (((exists ff_h_fixed_reindex_target_last. ff_h_fixed_reindex_target_last + S (a) = S ((S (n)) * d)) /\ exists ff_q_fixed_reindex_target_last. z = ff_q_fixed_reindex_target_last * S ((S (n)) * d) + (a))) /\ ((exists ff_u_fixed_reindex_target_prefix_witness ff_v_fixed_reindex_target_prefix_witness. ((((exists ff_h_fixed_reindex_target_prefix_witness_start. ff_h_fixed_reindex_target_prefix_witness_start + S (1) = S ((S (0)) * ff_v_fixed_reindex_target_prefix_witness)) /\ exists ff_q_fixed_reindex_target_prefix_witness_start. ff_u_fixed_reindex_target_prefix_witness = ff_q_fixed_reindex_target_prefix_witness_start * S ((S (0)) * ff_v_fixed_reindex_target_prefix_witness) + (1))) /\ ((((exists ff_h_fixed_reindex_target_prefix_witness_terminal. ff_h_fixed_reindex_target_prefix_witness_terminal + S (v) = S ((S (n)) * ff_v_fixed_reindex_target_prefix_witness)) /\ exists ff_q_fixed_reindex_target_prefix_witness_terminal. ff_u_fixed_reindex_target_prefix_witness = ff_q_fixed_reindex_target_prefix_witness_terminal * S ((S (n)) * ff_v_fixed_reindex_target_prefix_witness) + (v))) /\ forall ff_i_fixed_reindex_target_prefix_witness. (exists ff_lt_fixed_reindex_target_prefix_witness_bound. ff_lt_fixed_reindex_target_prefix_witness_bound + S ff_i_fixed_reindex_target_prefix_witness = n) -> exists ff_p_fixed_reindex_target_prefix_witness ff_r_fixed_reindex_target_prefix_witness ff_s_fixed_reindex_target_prefix_witness. ((((exists ff_h_fixed_reindex_target_prefix_witness_factor. ff_h_fixed_reindex_target_prefix_witness_factor + S (ff_p_fixed_reindex_target_prefix_witness) = S ((S (ff_i_fixed_reindex_target_prefix_witness)) * d)) /\ exists ff_q_fixed_reindex_target_prefix_witness_factor. z = ff_q_fixed_reindex_target_prefix_witness_factor * S ((S (ff_i_fixed_reindex_target_prefix_witness)) * d) + (ff_p_fixed_reindex_target_prefix_witness))) /\ ((((exists ff_h_fixed_reindex_target_prefix_witness_partial. ff_h_fixed_reindex_target_prefix_witness_partial + S (ff_r_fixed_reindex_target_prefix_witness) = S ((S (ff_i_fixed_reindex_target_prefix_witness)) * ff_v_fixed_reindex_target_prefix_witness)) /\ exists ff_q_fixed_reindex_target_prefix_witness_partial. ff_u_fixed_reindex_target_prefix_witness = ff_q_fixed_reindex_target_prefix_witness_partial * S ((S (ff_i_fixed_reindex_target_prefix_witness)) * ff_v_fixed_reindex_target_prefix_witness) + (ff_r_fixed_reindex_target_prefix_witness))) /\ ((((exists ff_h_fixed_reindex_target_prefix_witness_successor. ff_h_fixed_reindex_target_prefix_witness_successor + S (ff_s_fixed_reindex_target_prefix_witness) = S ((S (S ff_i_fixed_reindex_target_prefix_witness)) * ff_v_fixed_reindex_target_prefix_witness)) /\ exists ff_q_fixed_reindex_target_prefix_witness_successor. ff_u_fixed_reindex_target_prefix_witness = ff_q_fixed_reindex_target_prefix_witness_successor * S ((S (S ff_i_fixed_reindex_target_prefix_witness)) * ff_v_fixed_reindex_target_prefix_witness) + (ff_s_fixed_reindex_target_prefix_witness))) /\ ff_s_fixed_reindex_target_prefix_witness = ff_r_fixed_reindex_target_prefix_witness * ff_p_fixed_reindex_target_prefix_witness)))))) /\ q = v * a)
  23. 0023specialize beta_product_succ_decompose z
  24. 0024specialize beta_product_succ_decompose d
  25. 0025specialize beta_product_succ_decompose n
  26. 0026specialize beta_product_succ_decompose q
  27. 0027apply beta_product_succ_decompose
  28. 0028exact htarget_product
  29. 0029cases hsource_decomp
  30. 0030cases hsource_decomp_witness
  31. 0031cases hsource_decomp_witness_witness
  32. 0032cases hsource_decomp_witness_witness_right
  33. 0033cases htarget_decomp
  34. 0034cases htarget_decomp_witness
  35. 0035cases htarget_decomp_witness_witness
  36. 0036cases htarget_decomp_witness_witness_right
  37. 0037have htarget_source_last : ((exists ff_h_fixed_target_source_last. ff_h_fixed_target_source_last + S (x) = S ((S (n)) * d)) /\ exists ff_q_fixed_target_source_last. z = ff_q_fixed_target_source_last * S ((S (n)) * d) + (x))
  38. 0038specialize haligned n
  39. 0039specialize haligned n
  40. 0040specialize haligned x
  41. 0041apply haligned
  42. 0042specialize le_refl (S n)
  43. 0043exact le_refl
  44. 0044exact hmap_last
  45. 0045exact hsource_decomp_witness_witness_left
  46. 0046have hlast_equal : x2 = x
  47. 0047specialize beta_at_unique z
  48. 0048specialize beta_at_unique d
  49. 0049specialize beta_at_unique n
  50. 0050specialize beta_at_unique x2
  51. 0051specialize beta_at_unique x
  52. 0052apply beta_at_unique
  53. 0053exact htarget_decomp_witness_witness_left
  54. 0054exact htarget_source_last
  55. 0055have hprefixes_equal : x1 = x3
  56. 0056specialize hprefix_equal x1
  57. 0057specialize hprefix_equal x3
  58. 0058apply hprefix_equal
  59. 0059exact hsource_decomp_witness_witness_right_left
  60. 0060exact htarget_decomp_witness_witness_right_left
  61. 0061rewrite hsource_decomp_witness_witness_right_right
  62. 0062rewrite htarget_decomp_witness_witness_right_right
  63. 0063rewrite hlast_equal
  64. 0064rewrite hprefixes_equal
  65. 0065refl