PA007N

beta_product_pointwise_mul_exact

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

Pointwise products of synchronized beta prefixes multiply their exact finite products.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall mb mc sb sc tb tc l M Sprod T. (forall fpmp_index_product_alignment fpmp_left_product_alignment fpmp_right_product_alignment fpmp_target_product_alignment. (exists fpmp_gap_product_alignment. fpmp_gap_product_alignment + S fpmp_index_product_alignment = l) -> (((exists ff_h_fpmp_product_alignment_left. ff_h_fpmp_product_alignment_left + S (fpmp_left_product_alignment) = S ((S (fpmp_index_product_alignment)) * mc)) /\ exists ff_q_fpmp_product_alignment_left. mb = ff_q_fpmp_product_alignment_left * S ((S (fpmp_index_product_alignment)) * mc) + (fpmp_left_product_alignment))) -> (((exists ff_h_fpmp_product_alignment_right. ff_h_fpmp_product_alignment_right + S (fpmp_right_product_alignment) = S ((S (fpmp_index_product_alignment)) * sc)) /\ exists ff_q_fpmp_product_alignment_right. sb = ff_q_fpmp_product_alignment_right * S ((S (fpmp_index_product_alignment)) * sc) + (fpmp_right_product_alignment))) -> (((exists ff_h_fpmp_product_alignment_target. ff_h_fpmp_product_alignment_target + S (fpmp_target_product_alignment) = S ((S (fpmp_index_product_alignment)) * tc)) /\ exists ff_q_fpmp_product_alignment_target. tb = ff_q_fpmp_product_alignment_target * S ((S (fpmp_index_product_alignment)) * tc) + (fpmp_target_product_alignment))) -> fpmp_target_product_alignment = fpmp_left_product_alignment * fpmp_right_product_alignment) -> (exists ff_u_product_left ff_v_product_left. ((((exists ff_h_product_left_start. ff_h_product_left_start + S (1) = S ((S (0)) * ff_v_product_left)) /\ exists ff_q_product_left_start. ff_u_product_left = ff_q_product_left_start * S ((S (0)) * ff_v_product_left) + (1))) /\ ((((exists ff_h_product_left_terminal. ff_h_product_left_terminal + S (M) = S ((S (l)) * ff_v_product_left)) /\ exists ff_q_product_left_terminal. ff_u_product_left = ff_q_product_left_terminal * S ((S (l)) * ff_v_product_left) + (M))) /\ forall ff_i_product_left. (exists ff_lt_product_left_bound. ff_lt_product_left_bound + S ff_i_product_left = l) -> exists ff_p_product_left ff_r_product_left ff_s_product_left. ((((exists ff_h_product_left_factor. ff_h_product_left_factor + S (ff_p_product_left) = S ((S (ff_i_product_left)) * mc)) /\ exists ff_q_product_left_factor. mb = ff_q_product_left_factor * S ((S (ff_i_product_left)) * mc) + (ff_p_product_left))) /\ ((((exists ff_h_product_left_partial. ff_h_product_left_partial + S (ff_r_product_left) = S ((S (ff_i_product_left)) * ff_v_product_left)) /\ exists ff_q_product_left_partial. ff_u_product_left = ff_q_product_left_partial * S ((S (ff_i_product_left)) * ff_v_product_left) + (ff_r_product_left))) /\ ((((exists ff_h_product_left_successor. ff_h_product_left_successor + S (ff_s_product_left) = S ((S (S ff_i_product_left)) * ff_v_product_left)) /\ exists ff_q_product_left_successor. ff_u_product_left = ff_q_product_left_successor * S ((S (S ff_i_product_left)) * ff_v_product_left) + (ff_s_product_left))) /\ ff_s_product_left = ff_r_product_left * ff_p_product_left)))))) -> (exists ff_u_product_right ff_v_product_right. ((((exists ff_h_product_right_start. ff_h_product_right_start + S (1) = S ((S (0)) * ff_v_product_right)) /\ exists ff_q_product_right_start. ff_u_product_right = ff_q_product_right_start * S ((S (0)) * ff_v_product_right) + (1))) /\ ((((exists ff_h_product_right_terminal. ff_h_product_right_terminal + S (Sprod) = S ((S (l)) * ff_v_product_right)) /\ exists ff_q_product_right_terminal. ff_u_product_right = ff_q_product_right_terminal * S ((S (l)) * ff_v_product_right) + (Sprod))) /\ forall ff_i_product_right. (exists ff_lt_product_right_bound. ff_lt_product_right_bound + S ff_i_product_right = l) -> exists ff_p_product_right ff_r_product_right ff_s_product_right. ((((exists ff_h_product_right_factor. ff_h_product_right_factor + S (ff_p_product_right) = S ((S (ff_i_product_right)) * sc)) /\ exists ff_q_product_right_factor. sb = ff_q_product_right_factor * S ((S (ff_i_product_right)) * sc) + (ff_p_product_right))) /\ ((((exists ff_h_product_right_partial. ff_h_product_right_partial + S (ff_r_product_right) = S ((S (ff_i_product_right)) * ff_v_product_right)) /\ exists ff_q_product_right_partial. ff_u_product_right = ff_q_product_right_partial * S ((S (ff_i_product_right)) * ff_v_product_right) + (ff_r_product_right))) /\ ((((exists ff_h_product_right_successor. ff_h_product_right_successor + S (ff_s_product_right) = S ((S (S ff_i_product_right)) * ff_v_product_right)) /\ exists ff_q_product_right_successor. ff_u_product_right = ff_q_product_right_successor * S ((S (S ff_i_product_right)) * ff_v_product_right) + (ff_s_product_right))) /\ ff_s_product_right = ff_r_product_right * ff_p_product_right)))))) -> (exists ff_u_product_target ff_v_product_target. ((((exists ff_h_product_target_start. ff_h_product_target_start + S (1) = S ((S (0)) * ff_v_product_target)) /\ exists ff_q_product_target_start. ff_u_product_target = ff_q_product_target_start * S ((S (0)) * ff_v_product_target) + (1))) /\ ((((exists ff_h_product_target_terminal. ff_h_product_target_terminal + S (T) = S ((S (l)) * ff_v_product_target)) /\ exists ff_q_product_target_terminal. ff_u_product_target = ff_q_product_target_terminal * S ((S (l)) * ff_v_product_target) + (T))) /\ forall ff_i_product_target. (exists ff_lt_product_target_bound. ff_lt_product_target_bound + S ff_i_product_target = l) -> exists ff_p_product_target ff_r_product_target ff_s_product_target. ((((exists ff_h_product_target_factor. ff_h_product_target_factor + S (ff_p_product_target) = S ((S (ff_i_product_target)) * tc)) /\ exists ff_q_product_target_factor. tb = ff_q_product_target_factor * S ((S (ff_i_product_target)) * tc) + (ff_p_product_target))) /\ ((((exists ff_h_product_target_partial. ff_h_product_target_partial + S (ff_r_product_target) = S ((S (ff_i_product_target)) * ff_v_product_target)) /\ exists ff_q_product_target_partial. ff_u_product_target = ff_q_product_target_partial * S ((S (ff_i_product_target)) * ff_v_product_target) + (ff_r_product_target))) /\ ((((exists ff_h_product_target_successor. ff_h_product_target_successor + S (ff_s_product_target) = S ((S (S ff_i_product_target)) * ff_v_product_target)) /\ exists ff_q_product_target_successor. ff_u_product_target = ff_q_product_target_successor * S ((S (S ff_i_product_target)) * ff_v_product_target) + (ff_s_product_target))) /\ ff_s_product_target = ff_r_product_target * ff_p_product_target)))))) -> T = M * Sprod

Structural proof guide

Generated structural guide

Pointwise products of synchronized beta prefixes multiply their exact finite products.

Use the direct prerequisites beta_product_zero, beta_product_succ_decompose, beta_pointwise_mul_prefix_drop_last, le_refl, one_mul, mul_assoc, mul_comm as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (12), intermediate claims (10), equality transport (8), certified simplification (1).

Referenced ingredients

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA007M beta_pointwise_mul_prefix_drop_last PA001A le_refl PA000M one_mul PA000B mul_assoc PA000H mul_comm

Proof neighborhood

Direct dependencies

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA007M beta_pointwise_mul_prefix_drop_last PA001A le_refl PA000M one_mul PA000B mul_assoc PA000H mul_comm

Direct dependents

PA007O beta_pointwise_mul_product_exists PA0080 gauss_signed_products_balance_mod

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

116 script commands · 19 reading checkpoints · 10 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (5)
beta product zerobeta product succ decomposebeta pointwise mul prefix drop lastle reflone mul

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro mb
  2. L2
    intro mc
  3. L3
    intro sb
  4. L4
    intro sc
  5. L5
    intro tb
  6. L6
    intro tc
02Induction on lL7–14

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L7
    induction l
  2. L8
    intro M
  3. L9
    intro Sprod
  4. L10
    intro T
  5. L11
    intro haligned
  6. L12
    intro hM
  7. L13
    intro hS
  8. L14
    intro hT
03Establish hM1L15–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product zero.

  1. L15
    have hM1 : M = 1
  2. L16
    specialize beta_product_zero mb
  3. L17
    specialize beta_product_zero mc
  4. L18
    specialize beta_product_zero M
  5. L19
    apply beta_product_zero
  6. L20
    exact hM
04Establish hS1L21–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product zero.

  1. L21
    have hS1 : Sprod = 1
  2. L22
    specialize beta_product_zero sb
  3. L23
    specialize beta_product_zero sc
  4. L24
    specialize beta_product_zero Sprod
  5. L25
    apply beta_product_zero
  6. L26
    exact hS
05Establish hT1L27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product zero.

  1. L27
    have hT1 : T = 1
  2. L28
    specialize beta_product_zero tb
  3. L29
    specialize beta_product_zero tc
  4. L30
    specialize beta_product_zero T
  5. L31
    apply beta_product_zero
  6. L32
    exact hT
  7. L33
    rewrite hM1
  8. L34
    rewrite hS1
  9. L35
    rewrite hT1
  10. L36
    specialize one_mul 1
06Calculate and transport equalitiesL37–37

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L37
    symm
07Use earlier factsL38–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L38
    exact one_mul
08Fix variables and assumptionsL39–45

Work with arbitrary variables or the premises of the current implication.

  1. L39
    intro M
  2. L40
    intro Sprod
  3. L41
    intro T
  4. L42
    intro haligned
  5. L43
    intro hM
  6. L44
    intro hS
  7. L45
    intro hT
09Establish hMdL46–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L46
    have hMd : ∃ fpmp_factor_product_left_decomposition. ∃ fpmp_prefix_product_left_decomposition. BetaAt(mb,mc,l,fpmp_factor_product_left_decomposition) ∧ (Product(mb,mc,l,fpmp_prefix_product_left_decomposition) ∧ M = fpmp_prefix_product_left_decomposition · fpmp_factor_product_left_decomposition)Definitions: BetaAtProduct
  2. L47
    specialize beta_product_succ_decompose mb
  3. L48
    specialize beta_product_succ_decompose mc
  4. L49
    specialize beta_product_succ_decompose l
  5. L50
    specialize beta_product_succ_decompose M
  6. L51
    apply beta_product_succ_decompose
  7. L52
    exact hM
10Separate the logical casesL53–56

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L53
    cases hMd
  2. L54
    cases hMd_witness
  3. L55
    cases hMd_witness_witness
  4. L56
    cases hMd_witness_witness_right
11Establish hSdL57–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L57
    have hSd : ∃ fpmp_factor_product_right_decomposition. ∃ fpmp_prefix_product_right_decomposition. BetaAt(sb,sc,l,fpmp_factor_product_right_decomposition) ∧ (Product(sb,sc,l,fpmp_prefix_product_right_decomposition) ∧ Sprod = fpmp_prefix_product_right_decomposition · fpmp_factor_product_right_decomposition)Definitions: BetaAtProduct
  2. L58
    specialize beta_product_succ_decompose sb
  3. L59
    specialize beta_product_succ_decompose sc
  4. L60
    specialize beta_product_succ_decompose l
  5. L61
    specialize beta_product_succ_decompose Sprod
  6. L62
    apply beta_product_succ_decompose
  7. L63
    exact hS
12Separate the logical casesL64–67

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L64
    cases hSd
  2. L65
    cases hSd_witness
  3. L66
    cases hSd_witness_witness
  4. L67
    cases hSd_witness_witness_right
13Establish hTdL68–74

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L68
    have hTd : ∃ fpmp_factor_product_target_decomposition. ∃ fpmp_prefix_product_target_decomposition. BetaAt(tb,tc,l,fpmp_factor_product_target_decomposition) ∧ (Product(tb,tc,l,fpmp_prefix_product_target_decomposition) ∧ T = fpmp_prefix_product_target_decomposition · fpmp_factor_product_target_decomposition)Definitions: BetaAtProduct
  2. L69
    specialize beta_product_succ_decompose tb
  3. L70
    specialize beta_product_succ_decompose tc
  4. L71
    specialize beta_product_succ_decompose l
  5. L72
    specialize beta_product_succ_decompose T
  6. L73
    apply beta_product_succ_decompose
  7. L74
    exact hT
14Separate the logical casesL75–78

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L75
    cases hTd
  2. L76
    cases hTd_witness
  3. L77
    cases hTd_witness_witness
  4. L78
    cases hTd_witness_witness_right
15Establish hprefix_alignmentL79–88

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta pointwise mul prefix drop last.

  1. L79
    have hprefix_alignment : ∀ fpmp_index_product_restricted. ∀ fpmp_left_product_restricted. ∀ fpmp_right_product_restricted. ∀ fpmp_target_product_restricted. Lt(fpmp_index_product_restricted,l) → BetaAt(mb,mc,fpmp_index_product_restricted,fpmp_left_product_restricted) → BetaAt(sb,sc,fpmp_index_product_restricted,fpmp_right_product_restricted) → BetaAt(tb,tc,fpmp_index_product_restricted,fpmp_target_product_restricted) → fpmp_target_product_restricted = fpmp_left_product_restricted · fpmp_right_product_restrictedDefinitions: LtBetaAt
  2. L80
    specialize beta_pointwise_mul_prefix_drop_last mb
  3. L81
    specialize beta_pointwise_mul_prefix_drop_last mc
  4. L82
    specialize beta_pointwise_mul_prefix_drop_last sb
  5. L83
    specialize beta_pointwise_mul_prefix_drop_last sc
  6. L84
    specialize beta_pointwise_mul_prefix_drop_last tb
  7. L85
    specialize beta_pointwise_mul_prefix_drop_last tc
  8. L86
    specialize beta_pointwise_mul_prefix_drop_last l
  9. L87
    apply beta_pointwise_mul_prefix_drop_last
  10. L88
    exact haligned
16Establish hprefixL89–97

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L89
    have hprefix : x5 = x1 * x3
  2. L90
    specialize IH x1
  3. L91
    specialize IH x3
  4. L92
    specialize IH x5
  5. L93
    apply IH
  6. L94
    exact hprefix_alignment
  7. L95
    exact hMd_witness_witness_right_left
  8. L96
    exact hSd_witness_witness_right_left
  9. L97
    exact hTd_witness_witness_right_left
17Establish hentryL98–107

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply haligned.

  1. L98
    have hentry : x4 = x * x2
  2. L99
    specialize haligned l
  3. L100
    specialize haligned x
  4. L101
    specialize haligned x2
  5. L102
    specialize haligned x4
  6. L103
    apply haligned
  7. L104
    specialize le_refl (S l)
  8. L105
    exact le_refl
  9. L106
    exact hMd_witness_witness_left
  10. L107
    exact hSd_witness_witness_left
18Use earlier factsL108–108

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L108
    exact hTd_witness_witness_left
19Establish hshuffleL109–116

Establish this local claim before using it. It is not an additional assumption.

  1. L109
    have hshuffle : (x1 * x3) * (x * x2) = (x1 * x) * (x3 * x2)
  2. L110
    simp [mul_assoc, mul_comm]
  3. L111
    rewrite hTd_witness_witness_right_right
  4. L112
    rewrite hMd_witness_witness_right_right
  5. L113
    rewrite hSd_witness_witness_right_right
  6. L114
    rewrite hprefix
  7. L115
    rewrite hentry
  8. L116
    exact hshuffle

Library-wide reading audit

Original exact command ledger · 116 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro tb
  6. 0006intro tc
  7. 0007induction l
  8. 0008intro M
  9. 0009intro Sprod
  10. 0010intro T
  11. 0011intro haligned
  12. 0012intro hM
  13. 0013intro hS
  14. 0014intro hT
  15. 0015have hM1 : M = 1
  16. 0016specialize beta_product_zero mb
  17. 0017specialize beta_product_zero mc
  18. 0018specialize beta_product_zero M
  19. 0019apply beta_product_zero
  20. 0020exact hM
  21. 0021have hS1 : Sprod = 1
  22. 0022specialize beta_product_zero sb
  23. 0023specialize beta_product_zero sc
  24. 0024specialize beta_product_zero Sprod
  25. 0025apply beta_product_zero
  26. 0026exact hS
  27. 0027have hT1 : T = 1
  28. 0028specialize beta_product_zero tb
  29. 0029specialize beta_product_zero tc
  30. 0030specialize beta_product_zero T
  31. 0031apply beta_product_zero
  32. 0032exact hT
  33. 0033rewrite hM1
  34. 0034rewrite hS1
  35. 0035rewrite hT1
  36. 0036specialize one_mul 1
  37. 0037symm
  38. 0038exact one_mul
  39. 0039intro M
  40. 0040intro Sprod
  41. 0041intro T
  42. 0042intro haligned
  43. 0043intro hM
  44. 0044intro hS
  45. 0045intro hT
  46. 0046have hMd : exists fpmp_factor_product_left_decomposition fpmp_prefix_product_left_decomposition. (((exists ff_h_product_left_decomposition_entry. ff_h_product_left_decomposition_entry + S (fpmp_factor_product_left_decomposition) = S ((S (l)) * mc)) /\ exists ff_q_product_left_decomposition_entry. mb = ff_q_product_left_decomposition_entry * S ((S (l)) * mc) + (fpmp_factor_product_left_decomposition))) /\ ((exists ff_u_product_left_decomposition_product ff_v_product_left_decomposition_product. ((((exists ff_h_product_left_decomposition_product_start. ff_h_product_left_decomposition_product_start + S (1) = S ((S (0)) * ff_v_product_left_decomposition_product)) /\ exists ff_q_product_left_decomposition_product_start. ff_u_product_left_decomposition_product = ff_q_product_left_decomposition_product_start * S ((S (0)) * ff_v_product_left_decomposition_product) + (1))) /\ ((((exists ff_h_product_left_decomposition_product_terminal. ff_h_product_left_decomposition_product_terminal + S (fpmp_prefix_product_left_decomposition) = S ((S (l)) * ff_v_product_left_decomposition_product)) /\ exists ff_q_product_left_decomposition_product_terminal. ff_u_product_left_decomposition_product = ff_q_product_left_decomposition_product_terminal * S ((S (l)) * ff_v_product_left_decomposition_product) + (fpmp_prefix_product_left_decomposition))) /\ forall ff_i_product_left_decomposition_product. (exists ff_lt_product_left_decomposition_product_bound. ff_lt_product_left_decomposition_product_bound + S ff_i_product_left_decomposition_product = l) -> exists ff_p_product_left_decomposition_product ff_r_product_left_decomposition_product ff_s_product_left_decomposition_product. ((((exists ff_h_product_left_decomposition_product_factor. ff_h_product_left_decomposition_product_factor + S (ff_p_product_left_decomposition_product) = S ((S (ff_i_product_left_decomposition_product)) * mc)) /\ exists ff_q_product_left_decomposition_product_factor. mb = ff_q_product_left_decomposition_product_factor * S ((S (ff_i_product_left_decomposition_product)) * mc) + (ff_p_product_left_decomposition_product))) /\ ((((exists ff_h_product_left_decomposition_product_partial. ff_h_product_left_decomposition_product_partial + S (ff_r_product_left_decomposition_product) = S ((S (ff_i_product_left_decomposition_product)) * ff_v_product_left_decomposition_product)) /\ exists ff_q_product_left_decomposition_product_partial. ff_u_product_left_decomposition_product = ff_q_product_left_decomposition_product_partial * S ((S (ff_i_product_left_decomposition_product)) * ff_v_product_left_decomposition_product) + (ff_r_product_left_decomposition_product))) /\ ((((exists ff_h_product_left_decomposition_product_successor. ff_h_product_left_decomposition_product_successor + S (ff_s_product_left_decomposition_product) = S ((S (S ff_i_product_left_decomposition_product)) * ff_v_product_left_decomposition_product)) /\ exists ff_q_product_left_decomposition_product_successor. ff_u_product_left_decomposition_product = ff_q_product_left_decomposition_product_successor * S ((S (S ff_i_product_left_decomposition_product)) * ff_v_product_left_decomposition_product) + (ff_s_product_left_decomposition_product))) /\ ff_s_product_left_decomposition_product = ff_r_product_left_decomposition_product * ff_p_product_left_decomposition_product)))))) /\ M = fpmp_prefix_product_left_decomposition * fpmp_factor_product_left_decomposition)
  47. 0047specialize beta_product_succ_decompose mb
  48. 0048specialize beta_product_succ_decompose mc
  49. 0049specialize beta_product_succ_decompose l
  50. 0050specialize beta_product_succ_decompose M
  51. 0051apply beta_product_succ_decompose
  52. 0052exact hM
  53. 0053cases hMd
  54. 0054cases hMd_witness
  55. 0055cases hMd_witness_witness
  56. 0056cases hMd_witness_witness_right
  57. 0057have hSd : exists fpmp_factor_product_right_decomposition fpmp_prefix_product_right_decomposition. (((exists ff_h_product_right_decomposition_entry. ff_h_product_right_decomposition_entry + S (fpmp_factor_product_right_decomposition) = S ((S (l)) * sc)) /\ exists ff_q_product_right_decomposition_entry. sb = ff_q_product_right_decomposition_entry * S ((S (l)) * sc) + (fpmp_factor_product_right_decomposition))) /\ ((exists ff_u_product_right_decomposition_product ff_v_product_right_decomposition_product. ((((exists ff_h_product_right_decomposition_product_start. ff_h_product_right_decomposition_product_start + S (1) = S ((S (0)) * ff_v_product_right_decomposition_product)) /\ exists ff_q_product_right_decomposition_product_start. ff_u_product_right_decomposition_product = ff_q_product_right_decomposition_product_start * S ((S (0)) * ff_v_product_right_decomposition_product) + (1))) /\ ((((exists ff_h_product_right_decomposition_product_terminal. ff_h_product_right_decomposition_product_terminal + S (fpmp_prefix_product_right_decomposition) = S ((S (l)) * ff_v_product_right_decomposition_product)) /\ exists ff_q_product_right_decomposition_product_terminal. ff_u_product_right_decomposition_product = ff_q_product_right_decomposition_product_terminal * S ((S (l)) * ff_v_product_right_decomposition_product) + (fpmp_prefix_product_right_decomposition))) /\ forall ff_i_product_right_decomposition_product. (exists ff_lt_product_right_decomposition_product_bound. ff_lt_product_right_decomposition_product_bound + S ff_i_product_right_decomposition_product = l) -> exists ff_p_product_right_decomposition_product ff_r_product_right_decomposition_product ff_s_product_right_decomposition_product. ((((exists ff_h_product_right_decomposition_product_factor. ff_h_product_right_decomposition_product_factor + S (ff_p_product_right_decomposition_product) = S ((S (ff_i_product_right_decomposition_product)) * sc)) /\ exists ff_q_product_right_decomposition_product_factor. sb = ff_q_product_right_decomposition_product_factor * S ((S (ff_i_product_right_decomposition_product)) * sc) + (ff_p_product_right_decomposition_product))) /\ ((((exists ff_h_product_right_decomposition_product_partial. ff_h_product_right_decomposition_product_partial + S (ff_r_product_right_decomposition_product) = S ((S (ff_i_product_right_decomposition_product)) * ff_v_product_right_decomposition_product)) /\ exists ff_q_product_right_decomposition_product_partial. ff_u_product_right_decomposition_product = ff_q_product_right_decomposition_product_partial * S ((S (ff_i_product_right_decomposition_product)) * ff_v_product_right_decomposition_product) + (ff_r_product_right_decomposition_product))) /\ ((((exists ff_h_product_right_decomposition_product_successor. ff_h_product_right_decomposition_product_successor + S (ff_s_product_right_decomposition_product) = S ((S (S ff_i_product_right_decomposition_product)) * ff_v_product_right_decomposition_product)) /\ exists ff_q_product_right_decomposition_product_successor. ff_u_product_right_decomposition_product = ff_q_product_right_decomposition_product_successor * S ((S (S ff_i_product_right_decomposition_product)) * ff_v_product_right_decomposition_product) + (ff_s_product_right_decomposition_product))) /\ ff_s_product_right_decomposition_product = ff_r_product_right_decomposition_product * ff_p_product_right_decomposition_product)))))) /\ Sprod = fpmp_prefix_product_right_decomposition * fpmp_factor_product_right_decomposition)
  58. 0058specialize beta_product_succ_decompose sb
  59. 0059specialize beta_product_succ_decompose sc
  60. 0060specialize beta_product_succ_decompose l
  61. 0061specialize beta_product_succ_decompose Sprod
  62. 0062apply beta_product_succ_decompose
  63. 0063exact hS
  64. 0064cases hSd
  65. 0065cases hSd_witness
  66. 0066cases hSd_witness_witness
  67. 0067cases hSd_witness_witness_right
  68. 0068have hTd : exists fpmp_factor_product_target_decomposition fpmp_prefix_product_target_decomposition. (((exists ff_h_product_target_decomposition_entry. ff_h_product_target_decomposition_entry + S (fpmp_factor_product_target_decomposition) = S ((S (l)) * tc)) /\ exists ff_q_product_target_decomposition_entry. tb = ff_q_product_target_decomposition_entry * S ((S (l)) * tc) + (fpmp_factor_product_target_decomposition))) /\ ((exists ff_u_product_target_decomposition_product ff_v_product_target_decomposition_product. ((((exists ff_h_product_target_decomposition_product_start. ff_h_product_target_decomposition_product_start + S (1) = S ((S (0)) * ff_v_product_target_decomposition_product)) /\ exists ff_q_product_target_decomposition_product_start. ff_u_product_target_decomposition_product = ff_q_product_target_decomposition_product_start * S ((S (0)) * ff_v_product_target_decomposition_product) + (1))) /\ ((((exists ff_h_product_target_decomposition_product_terminal. ff_h_product_target_decomposition_product_terminal + S (fpmp_prefix_product_target_decomposition) = S ((S (l)) * ff_v_product_target_decomposition_product)) /\ exists ff_q_product_target_decomposition_product_terminal. ff_u_product_target_decomposition_product = ff_q_product_target_decomposition_product_terminal * S ((S (l)) * ff_v_product_target_decomposition_product) + (fpmp_prefix_product_target_decomposition))) /\ forall ff_i_product_target_decomposition_product. (exists ff_lt_product_target_decomposition_product_bound. ff_lt_product_target_decomposition_product_bound + S ff_i_product_target_decomposition_product = l) -> exists ff_p_product_target_decomposition_product ff_r_product_target_decomposition_product ff_s_product_target_decomposition_product. ((((exists ff_h_product_target_decomposition_product_factor. ff_h_product_target_decomposition_product_factor + S (ff_p_product_target_decomposition_product) = S ((S (ff_i_product_target_decomposition_product)) * tc)) /\ exists ff_q_product_target_decomposition_product_factor. tb = ff_q_product_target_decomposition_product_factor * S ((S (ff_i_product_target_decomposition_product)) * tc) + (ff_p_product_target_decomposition_product))) /\ ((((exists ff_h_product_target_decomposition_product_partial. ff_h_product_target_decomposition_product_partial + S (ff_r_product_target_decomposition_product) = S ((S (ff_i_product_target_decomposition_product)) * ff_v_product_target_decomposition_product)) /\ exists ff_q_product_target_decomposition_product_partial. ff_u_product_target_decomposition_product = ff_q_product_target_decomposition_product_partial * S ((S (ff_i_product_target_decomposition_product)) * ff_v_product_target_decomposition_product) + (ff_r_product_target_decomposition_product))) /\ ((((exists ff_h_product_target_decomposition_product_successor. ff_h_product_target_decomposition_product_successor + S (ff_s_product_target_decomposition_product) = S ((S (S ff_i_product_target_decomposition_product)) * ff_v_product_target_decomposition_product)) /\ exists ff_q_product_target_decomposition_product_successor. ff_u_product_target_decomposition_product = ff_q_product_target_decomposition_product_successor * S ((S (S ff_i_product_target_decomposition_product)) * ff_v_product_target_decomposition_product) + (ff_s_product_target_decomposition_product))) /\ ff_s_product_target_decomposition_product = ff_r_product_target_decomposition_product * ff_p_product_target_decomposition_product)))))) /\ T = fpmp_prefix_product_target_decomposition * fpmp_factor_product_target_decomposition)
  69. 0069specialize beta_product_succ_decompose tb
  70. 0070specialize beta_product_succ_decompose tc
  71. 0071specialize beta_product_succ_decompose l
  72. 0072specialize beta_product_succ_decompose T
  73. 0073apply beta_product_succ_decompose
  74. 0074exact hT
  75. 0075cases hTd
  76. 0076cases hTd_witness
  77. 0077cases hTd_witness_witness
  78. 0078cases hTd_witness_witness_right
  79. 0079have hprefix_alignment : forall fpmp_index_product_restricted fpmp_left_product_restricted fpmp_right_product_restricted fpmp_target_product_restricted. (exists fpmp_gap_product_restricted. fpmp_gap_product_restricted + S fpmp_index_product_restricted = l) -> (((exists ff_h_fpmp_product_restricted_left. ff_h_fpmp_product_restricted_left + S (fpmp_left_product_restricted) = S ((S (fpmp_index_product_restricted)) * mc)) /\ exists ff_q_fpmp_product_restricted_left. mb = ff_q_fpmp_product_restricted_left * S ((S (fpmp_index_product_restricted)) * mc) + (fpmp_left_product_restricted))) -> (((exists ff_h_fpmp_product_restricted_right. ff_h_fpmp_product_restricted_right + S (fpmp_right_product_restricted) = S ((S (fpmp_index_product_restricted)) * sc)) /\ exists ff_q_fpmp_product_restricted_right. sb = ff_q_fpmp_product_restricted_right * S ((S (fpmp_index_product_restricted)) * sc) + (fpmp_right_product_restricted))) -> (((exists ff_h_fpmp_product_restricted_target. ff_h_fpmp_product_restricted_target + S (fpmp_target_product_restricted) = S ((S (fpmp_index_product_restricted)) * tc)) /\ exists ff_q_fpmp_product_restricted_target. tb = ff_q_fpmp_product_restricted_target * S ((S (fpmp_index_product_restricted)) * tc) + (fpmp_target_product_restricted))) -> fpmp_target_product_restricted = fpmp_left_product_restricted * fpmp_right_product_restricted
  80. 0080specialize beta_pointwise_mul_prefix_drop_last mb
  81. 0081specialize beta_pointwise_mul_prefix_drop_last mc
  82. 0082specialize beta_pointwise_mul_prefix_drop_last sb
  83. 0083specialize beta_pointwise_mul_prefix_drop_last sc
  84. 0084specialize beta_pointwise_mul_prefix_drop_last tb
  85. 0085specialize beta_pointwise_mul_prefix_drop_last tc
  86. 0086specialize beta_pointwise_mul_prefix_drop_last l
  87. 0087apply beta_pointwise_mul_prefix_drop_last
  88. 0088exact haligned
  89. 0089have hprefix : x5 = x1 * x3
  90. 0090specialize IH x1
  91. 0091specialize IH x3
  92. 0092specialize IH x5
  93. 0093apply IH
  94. 0094exact hprefix_alignment
  95. 0095exact hMd_witness_witness_right_left
  96. 0096exact hSd_witness_witness_right_left
  97. 0097exact hTd_witness_witness_right_left
  98. 0098have hentry : x4 = x * x2
  99. 0099specialize haligned l
  100. 0100specialize haligned x
  101. 0101specialize haligned x2
  102. 0102specialize haligned x4
  103. 0103apply haligned
  104. 0104specialize le_refl (S l)
  105. 0105exact le_refl
  106. 0106exact hMd_witness_witness_left
  107. 0107exact hSd_witness_witness_left
  108. 0108exact hTd_witness_witness_left
  109. 0109have hshuffle : (x1 * x3) * (x * x2) = (x1 * x) * (x3 * x2)
  110. 0110simp [mul_assoc, mul_comm]
  111. 0111rewrite hTd_witness_witness_right_right
  112. 0112rewrite hMd_witness_witness_right_right
  113. 0113rewrite hSd_witness_witness_right_right
  114. 0114rewrite hprefix
  115. 0115rewrite hentry
  116. 0116exact hshuffle