PA007K · theorem

beta_pointwise_mul_prefix_extend

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

Append the product of the two final decoded values and preserve all earlier 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.

Statement with defined notation

∀ mb. ∀ mc. ∀ sb. ∀ sc. ∀ tb. ∀ tc. ∀ l. ∀ m. ∀ s. (∀ 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) → BetaAt(mb,mc,l,m) → BetaAt(sb,sc,l,s) → ∃ x. ∃ y. ∀ z. ∀ n. ∀ k. ∀ i. Lt(z,S l) → BetaAt(mb,mc,z,n) → BetaAt(sb,sc,z,k) → BetaAt(x,y,z,i) → i = n · k

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

10 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall mb mc sb sc tb tc l m s. (forall fpmp_index_recode_before fpmp_left_recode_before fpmp_right_recode_before fpmp_target_recode_before. (exists fpmp_gap_recode_before. fpmp_gap_recode_before + S fpmp_index_recode_before = l) -> (((exists ff_h_fpmp_recode_before_left. ff_h_fpmp_recode_before_left + S (fpmp_left_recode_before) = S ((S (fpmp_index_recode_before)) * mc)) /\ exists ff_q_fpmp_recode_before_left. mb = ff_q_fpmp_recode_before_left * S ((S (fpmp_index_recode_before)) * mc) + (fpmp_left_recode_before))) -> (((exists ff_h_fpmp_recode_before_right. ff_h_fpmp_recode_before_right + S (fpmp_right_recode_before) = S ((S (fpmp_index_recode_before)) * sc)) /\ exists ff_q_fpmp_recode_before_right. sb = ff_q_fpmp_recode_before_right * S ((S (fpmp_index_recode_before)) * sc) + (fpmp_right_recode_before))) -> (((exists ff_h_fpmp_recode_before_target. ff_h_fpmp_recode_before_target + S (fpmp_target_recode_before) = S ((S (fpmp_index_recode_before)) * tc)) /\ exists ff_q_fpmp_recode_before_target. tb = ff_q_fpmp_recode_before_target * S ((S (fpmp_index_recode_before)) * tc) + (fpmp_target_recode_before))) -> fpmp_target_recode_before = fpmp_left_recode_before * fpmp_right_recode_before) -> (((exists ff_h_recode_left_last. ff_h_recode_left_last + S (m) = S ((S (l)) * mc)) /\ exists ff_q_recode_left_last. mb = ff_q_recode_left_last * S ((S (l)) * mc) + (m))) -> (((exists ff_h_recode_right_last. ff_h_recode_right_last + S (s) = S ((S (l)) * sc)) /\ exists ff_q_recode_right_last. sb = ff_q_recode_right_last * S ((S (l)) * sc) + (s))) -> exists z d. (forall fpmp_index_recode_after fpmp_left_recode_after fpmp_right_recode_after fpmp_target_recode_after. (exists fpmp_gap_recode_after. fpmp_gap_recode_after + S fpmp_index_recode_after = S l) -> (((exists ff_h_fpmp_recode_after_left. ff_h_fpmp_recode_after_left + S (fpmp_left_recode_after) = S ((S (fpmp_index_recode_after)) * mc)) /\ exists ff_q_fpmp_recode_after_left. mb = ff_q_fpmp_recode_after_left * S ((S (fpmp_index_recode_after)) * mc) + (fpmp_left_recode_after))) -> (((exists ff_h_fpmp_recode_after_right. ff_h_fpmp_recode_after_right + S (fpmp_right_recode_after) = S ((S (fpmp_index_recode_after)) * sc)) /\ exists ff_q_fpmp_recode_after_right. sb = ff_q_fpmp_recode_after_right * S ((S (fpmp_index_recode_after)) * sc) + (fpmp_right_recode_after))) -> (((exists ff_h_fpmp_recode_after_target. ff_h_fpmp_recode_after_target + S (fpmp_target_recode_after) = S ((S (fpmp_index_recode_after)) * d)) /\ exists ff_q_fpmp_recode_after_target. z = ff_q_fpmp_recode_after_target * S ((S (fpmp_index_recode_after)) * d) + (fpmp_target_recode_after))) -> fpmp_target_recode_after = fpmp_left_recode_after * fpmp_right_recode_after)

Proof neighborhood

Direct theorem prerequisites

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique

Direct theorem dependents

PA007L beta_pointwise_mul_prefix_exists

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

109 script commands · 23 reading checkpoints · 9 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 (4)
beta prefix extendfinite lt succ eq or ltbeta at existsbeta at unique
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 m
  9. L9
    intro s
  10. L10
    intro haligned
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hm_last
  2. L12
    intro hs_last
03Use earlier factsL13–16

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

  1. L13
    specialize beta_prefix_extend l
  2. L14
    specialize beta_prefix_extend tb
  3. L15
    specialize beta_prefix_extend tc
  4. L16
    specialize beta_prefix_extend (m * s)
04Separate the logical casesL17–19

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

  1. L17
    cases beta_prefix_extend
  2. L18
    cases beta_prefix_extend_witness
  3. L19
    cases beta_prefix_extend_witness_witness
05Construct an explicit witnessL20–21

Supply the displayed value, then prove that it has the required property.

  1. L20
    exists x
  2. L21
    exists x1
06Fix variables and assumptionsL22–29

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

  1. L22
    intro i
  2. L23
    intro a
  3. L24
    intro b
  4. L25
    intro t
  5. L26
    intro hi
  6. L27
    intro ha
  7. L28
    intro hb
  8. L29
    intro ht
07Establish hsplitL30–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L30
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L31
    specialize finite_lt_succ_eq_or_lt l
  3. L32
    specialize finite_lt_succ_eq_or_lt i
  4. L33
    apply finite_lt_succ_eq_or_lt
  5. L34
    exact hi
08Separate the logical casesL35–35

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

  1. L35
    cases hsplit
09Calculate and transport equalitiesL36–41

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

  1. L36
    rewrite hsplit_left at ha
  2. L37
    rewrite hsplit_left at ha
  3. L38
    rewrite hsplit_left at hb
  4. L39
    rewrite hsplit_left at hb
  5. L40
    rewrite hsplit_left at ht
  6. L41
    rewrite hsplit_left at ht
10Establish hmaL42–50

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

  1. L42
    have hma : m = a
  2. L43
    specialize beta_at_unique mb
  3. L44
    specialize beta_at_unique mc
  4. L45
    specialize beta_at_unique l
  5. L46
    specialize beta_at_unique m
  6. L47
    specialize beta_at_unique a
  7. L48
    apply beta_at_unique
  8. L49
    exact hm_last
  9. L50
    exact ha
11Establish hsbL51–59

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

  1. L51
    have hsb : s = b
  2. L52
    specialize beta_at_unique sb
  3. L53
    specialize beta_at_unique sc
  4. L54
    specialize beta_at_unique l
  5. L55
    specialize beta_at_unique s
  6. L56
    specialize beta_at_unique b
  7. L57
    apply beta_at_unique
  8. L58
    exact hs_last
  9. L59
    exact hb
12Establish happendedL60–61

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

  1. L60
    have happended : BetaAt(x,x1,l,m · s)Definitions: BetaAt(x,x1,l,m · s)Original native command in the exact edition
  2. L61
    exact beta_prefix_extend_witness_witness_left
13Establish ht_productL62–71

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

  1. L62
    have ht_product : t = m * s
  2. L63
    specialize beta_at_unique x
  3. L64
    specialize beta_at_unique x1
  4. L65
    specialize beta_at_unique l
  5. L66
    specialize beta_at_unique t
  6. L67
    specialize beta_at_unique (m * s)
  7. L68
    apply beta_at_unique
  8. L69
    exact ht
  9. L70
    exact happended
  10. L71
    trans m * s
14Use earlier factsL72–72

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

  1. L72
    exact ht_product
15Calculate and transport equalitiesL73–73

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

  1. L73
    congr
16Use earlier factsL74–75

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

  1. L74
    exact hma
  2. L75
    exact hsb
17Establish hold_existsL76–80

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

  1. L76
    have hold_exists : ∃ u. BetaAt(tb,tc,i,u)Definitions: BetaAt(tb,tc,i,u)Original native command in the exact edition
  2. L77
    specialize beta_at_exists tb
  3. L78
    specialize beta_at_exists tc
  4. L79
    specialize beta_at_exists i
  5. L80
    exact beta_at_exists
18Separate the logical casesL81–81

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

  1. L81
    cases hold_exists
19Establish hnew_oldL82–87

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix extend witness witness right.

  1. L82
    have hnew_old : BetaAt(x,x1,i,x2)Definitions: BetaAt(x,x1,i,x2)Original native command in the exact edition
  2. L83
    specialize beta_prefix_extend_witness_witness_right i
  3. L84
    specialize beta_prefix_extend_witness_witness_right x2
  4. L85
    apply beta_prefix_extend_witness_witness_right
  5. L86
    exact hsplit_right
  6. L87
    exact hold_exists_witness
20Establish htxL88–96

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

  1. L88
    have htx : t = x2
  2. L89
    specialize beta_at_unique x
  3. L90
    specialize beta_at_unique x1
  4. L91
    specialize beta_at_unique i
  5. L92
    specialize beta_at_unique t
  6. L93
    specialize beta_at_unique x2
  7. L94
    apply beta_at_unique
  8. L95
    exact ht
  9. L96
    exact hnew_old
21Establish hold_productL97–106

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

  1. L97
    have hold_product : x2 = a * b
  2. L98
    specialize haligned i
  3. L99
    specialize haligned a
  4. L100
    specialize haligned b
  5. L101
    specialize haligned x2
  6. L102
    apply haligned
  7. L103
    exact hsplit_right
  8. L104
    exact ha
  9. L105
    exact hb
  10. L106
    exact hold_exists_witness
22Calculate and transport equalitiesL107–107

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

  1. L107
    trans x2
23Use earlier factsL108–109

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

  1. L108
    exact htx
  2. L109
    exact hold_product

Library-wide reading audit

Original defined command ledger · 109 lines
  1. 0001intro mb
  2. 0002intro mc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro tb
  6. 0006intro tc
  7. 0007intro l
  8. 0008intro m
  9. 0009intro s
  10. 0010intro haligned
  11. 0011intro hm_last
  12. 0012intro hs_last
  13. 0013specialize beta_prefix_extend l
  14. 0014specialize beta_prefix_extend tb
  15. 0015specialize beta_prefix_extend tc
  16. 0016specialize beta_prefix_extend (m * s)
  17. 0017cases beta_prefix_extend
  18. 0018cases beta_prefix_extend_witness
  19. 0019cases beta_prefix_extend_witness_witness
  20. 0020exists x
  21. 0021exists x1
  22. 0022intro i
  23. 0023intro a
  24. 0024intro b
  25. 0025intro t
  26. 0026intro hi
  27. 0027intro ha
  28. 0028intro hb
  29. 0029intro ht
  30. 0030have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists gap. gap + S i = l
  31. 0031specialize finite_lt_succ_eq_or_lt l
  32. 0032specialize finite_lt_succ_eq_or_lt i
  33. 0033apply finite_lt_succ_eq_or_lt
  34. 0034exact hi
  35. 0035cases hsplit
  36. 0036rewrite hsplit_left at ha
  37. 0037rewrite hsplit_left at ha
  38. 0038rewrite hsplit_left at hb
  39. 0039rewrite hsplit_left at hb
  40. 0040rewrite hsplit_left at ht
  41. 0041rewrite hsplit_left at ht
  42. 0042have hma : m = a
  43. 0043specialize beta_at_unique mb
  44. 0044specialize beta_at_unique mc
  45. 0045specialize beta_at_unique l
  46. 0046specialize beta_at_unique m
  47. 0047specialize beta_at_unique a
  48. 0048apply beta_at_unique
  49. 0049exact hm_last
  50. 0050exact ha
  51. 0051have hsb : s = b
  52. 0052specialize beta_at_unique sb
  53. 0053specialize beta_at_unique sc
  54. 0054specialize beta_at_unique l
  55. 0055specialize beta_at_unique s
  56. 0056specialize beta_at_unique b
  57. 0057apply beta_at_unique
  58. 0058exact hs_last
  59. 0059exact hb
  60. 0060have happended : BetaAt(x,x1,l,m · s)
    Exact native replay linehave happended : ((exists fpmr_height_recode_appended_product. fpmr_height_recode_appended_product + S (m * s) = S ((S (l)) * x1)) /\ exists fpmr_quotient_recode_appended_product. x = fpmr_quotient_recode_appended_product * S ((S (l)) * x1) + (m * s))
  61. 0061exact beta_prefix_extend_witness_witness_left
  62. 0062have ht_product : t = m * s
  63. 0063specialize beta_at_unique x
  64. 0064specialize beta_at_unique x1
  65. 0065specialize beta_at_unique l
  66. 0066specialize beta_at_unique t
  67. 0067specialize beta_at_unique (m * s)
  68. 0068apply beta_at_unique
  69. 0069exact ht
  70. 0070exact happended
  71. 0071trans m * s
  72. 0072exact ht_product
  73. 0073congr
  74. 0074exact hma
  75. 0075exact hsb
  76. 0076have hold_exists : ∃ u. BetaAt(tb,tc,i,u)
    Exact native replay linehave hold_exists : exists u. (((exists ff_h_recode_old_target_exists. ff_h_recode_old_target_exists + S (u) = S ((S (i)) * tc)) /\ exists ff_q_recode_old_target_exists. tb = ff_q_recode_old_target_exists * S ((S (i)) * tc) + (u)))
  77. 0077specialize beta_at_exists tb
  78. 0078specialize beta_at_exists tc
  79. 0079specialize beta_at_exists i
  80. 0080exact beta_at_exists
  81. 0081cases hold_exists
  82. 0082have hnew_old : BetaAt(x,x1,i,x2)
    Exact native replay linehave hnew_old : ((exists ff_h_recode_new_old_target_entry. ff_h_recode_new_old_target_entry + S (x2) = S ((S (i)) * x1)) /\ exists ff_q_recode_new_old_target_entry. x = ff_q_recode_new_old_target_entry * S ((S (i)) * x1) + (x2))
  83. 0083specialize beta_prefix_extend_witness_witness_right i
  84. 0084specialize beta_prefix_extend_witness_witness_right x2
  85. 0085apply beta_prefix_extend_witness_witness_right
  86. 0086exact hsplit_right
  87. 0087exact hold_exists_witness
  88. 0088have htx : t = x2
  89. 0089specialize beta_at_unique x
  90. 0090specialize beta_at_unique x1
  91. 0091specialize beta_at_unique i
  92. 0092specialize beta_at_unique t
  93. 0093specialize beta_at_unique x2
  94. 0094apply beta_at_unique
  95. 0095exact ht
  96. 0096exact hnew_old
  97. 0097have hold_product : x2 = a * b
  98. 0098specialize haligned i
  99. 0099specialize haligned a
  100. 0100specialize haligned b
  101. 0101specialize haligned x2
  102. 0102apply haligned
  103. 0103exact hsplit_right
  104. 0104exact ha
  105. 0105exact hb
  106. 0106exact hold_exists_witness
  107. 0107trans x2
  108. 0108exact htx
  109. 0109exact hold_product