PA007M

beta_pointwise_mul_prefix_drop_last

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

Pointwise multiplication alignment restricts to the predecessor prefix.

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. (forall fpmp_index_drop_successor fpmp_left_drop_successor fpmp_right_drop_successor fpmp_target_drop_successor. (exists fpmp_gap_drop_successor. fpmp_gap_drop_successor + S fpmp_index_drop_successor = S l) -> (((exists ff_h_fpmp_drop_successor_left. ff_h_fpmp_drop_successor_left + S (fpmp_left_drop_successor) = S ((S (fpmp_index_drop_successor)) * mc)) /\ exists ff_q_fpmp_drop_successor_left. mb = ff_q_fpmp_drop_successor_left * S ((S (fpmp_index_drop_successor)) * mc) + (fpmp_left_drop_successor))) -> (((exists ff_h_fpmp_drop_successor_right. ff_h_fpmp_drop_successor_right + S (fpmp_right_drop_successor) = S ((S (fpmp_index_drop_successor)) * sc)) /\ exists ff_q_fpmp_drop_successor_right. sb = ff_q_fpmp_drop_successor_right * S ((S (fpmp_index_drop_successor)) * sc) + (fpmp_right_drop_successor))) -> (((exists ff_h_fpmp_drop_successor_target. ff_h_fpmp_drop_successor_target + S (fpmp_target_drop_successor) = S ((S (fpmp_index_drop_successor)) * tc)) /\ exists ff_q_fpmp_drop_successor_target. tb = ff_q_fpmp_drop_successor_target * S ((S (fpmp_index_drop_successor)) * tc) + (fpmp_target_drop_successor))) -> fpmp_target_drop_successor = fpmp_left_drop_successor * fpmp_right_drop_successor) -> (forall fpmp_index_drop_prefix fpmp_left_drop_prefix fpmp_right_drop_prefix fpmp_target_drop_prefix. (exists fpmp_gap_drop_prefix. fpmp_gap_drop_prefix + S fpmp_index_drop_prefix = l) -> (((exists ff_h_fpmp_drop_prefix_left. ff_h_fpmp_drop_prefix_left + S (fpmp_left_drop_prefix) = S ((S (fpmp_index_drop_prefix)) * mc)) /\ exists ff_q_fpmp_drop_prefix_left. mb = ff_q_fpmp_drop_prefix_left * S ((S (fpmp_index_drop_prefix)) * mc) + (fpmp_left_drop_prefix))) -> (((exists ff_h_fpmp_drop_prefix_right. ff_h_fpmp_drop_prefix_right + S (fpmp_right_drop_prefix) = S ((S (fpmp_index_drop_prefix)) * sc)) /\ exists ff_q_fpmp_drop_prefix_right. sb = ff_q_fpmp_drop_prefix_right * S ((S (fpmp_index_drop_prefix)) * sc) + (fpmp_right_drop_prefix))) -> (((exists ff_h_fpmp_drop_prefix_target. ff_h_fpmp_drop_prefix_target + S (fpmp_target_drop_prefix) = S ((S (fpmp_index_drop_prefix)) * tc)) /\ exists ff_q_fpmp_drop_prefix_target. tb = ff_q_fpmp_drop_prefix_target * S ((S (fpmp_index_drop_prefix)) * tc) + (fpmp_target_drop_prefix))) -> fpmp_target_drop_prefix = fpmp_left_drop_prefix * fpmp_right_drop_prefix)

Structural proof guide

Generated structural guide

Pointwise multiplication alignment restricts to the predecessor prefix.

Use the direct prerequisites le_succ as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA002O le_succ

Proof neighborhood

Direct dependencies

PA002O le_succ

Direct dependents

PA007N beta_product_pointwise_mul_exact

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

28 script commands · 4 reading checkpoints · 0 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 (1)
le succ
01Fix variables and assumptionsL1–10

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
  7. L7
    intro l
  8. L8
    intro haligned
  9. L9
    intro i
  10. L10
    intro m
02Fix variables and assumptionsL11–16

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

  1. L11
    intro s
  2. L12
    intro t
  3. L13
    intro hi
  4. L14
    intro hm
  5. L15
    intro hs
  6. L16
    intro ht
03Use earlier factsL17–26

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

  1. L17
    specialize haligned i
  2. L18
    specialize haligned m
  3. L19
    specialize haligned s
  4. L20
    specialize haligned t
  5. L21
    apply haligned
  6. L22
    specialize le_succ (S i)
  7. L23
    specialize le_succ l
  8. L24
    apply le_succ
  9. L25
    exact hi
  10. L26
    exact hm
04Use earlier factsL27–28

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

  1. L27
    exact hs
  2. L28
    exact ht

Library-wide reading audit

Original exact command ledger · 28 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro tb
  6. 0006intro tc
  7. 0007intro l
  8. 0008intro haligned
  9. 0009intro i
  10. 0010intro m
  11. 0011intro s
  12. 0012intro t
  13. 0013intro hi
  14. 0014intro hm
  15. 0015intro hs
  16. 0016intro ht
  17. 0017specialize haligned i
  18. 0018specialize haligned m
  19. 0019specialize haligned s
  20. 0020specialize haligned t
  21. 0021apply haligned
  22. 0022specialize le_succ (S i)
  23. 0023specialize le_succ l
  24. 0024apply le_succ
  25. 0025exact hi
  26. 0026exact hm
  27. 0027exact hs
  28. 0028exact ht