PA007M · theorem

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.

Statement with defined notation

∀ mb. ∀ mc. ∀ sb. ∀ sc. ∀ tb. ∀ tc. ∀ l. (∀ x. ∀ y. ∀ z. ∀ n. Lt(x,S l) → BetaAt(mb,mc,x,y) → BetaAt(sb,sc,x,z) → BetaAt(tb,tc,x,n) → n = y · z) → ∀ x. ∀ y. ∀ z. ∀ n. Lt(x,l) → BetaAt(mb,mc,x,y) → BetaAt(sb,sc,x,z) → BetaAt(tb,tc,x,n) → n = y · z

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

8 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

PA002O le_succ

Direct theorem dependents

PA007N beta_product_pointwise_mul_exact

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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