PA0052 · theorem

beta_product_replace_balance

Stable checked-use theorem · independently closed

Replacing one factor balances the old and new finite products by the exchanged values.

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

∀ k. ∀ b. ∀ c. ∀ z. ∀ d. ∀ i. ∀ x. ∀ y. ∀ p. ∀ q. Lt(i,k) → BetaAt(b,c,i,x) → BetaAt(z,d,i,y) → (∀ n. ∀ m. Lt(n,k) → ¬n = i → BetaAt(b,c,n,m) → BetaAt(z,d,n,m)) → Product(b,c,k,p) → Product(z,d,k,q) → q · x = p · y

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 PD0014 Product

8 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0014 Product

10 occurrences

Exact expanded native-PA statement
forall k b c z d i x y p q. (exists h. h + S i = k) -> (((exists ff_h_balance_old_i. ff_h_balance_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_balance_old_i. b = ff_q_balance_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_balance_new_i. ff_h_balance_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_balance_new_i. z = ff_q_balance_new_i * S ((S (i)) * d) + (y))) -> (forall j a. (exists h. h + S j = k) -> ~(j = i) -> (((exists ff_h_balance_old_j. ff_h_balance_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_balance_old_j. b = ff_q_balance_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_balance_new_j. ff_h_balance_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_balance_new_j. z = ff_q_balance_new_j * S ((S (j)) * d) + (a)))) -> (exists ff_u_balance_old ff_v_balance_old. ((((exists ff_h_balance_old_start. ff_h_balance_old_start + S (1) = S ((S (0)) * ff_v_balance_old)) /\ exists ff_q_balance_old_start. ff_u_balance_old = ff_q_balance_old_start * S ((S (0)) * ff_v_balance_old) + (1))) /\ ((((exists ff_h_balance_old_terminal. ff_h_balance_old_terminal + S (p) = S ((S (k)) * ff_v_balance_old)) /\ exists ff_q_balance_old_terminal. ff_u_balance_old = ff_q_balance_old_terminal * S ((S (k)) * ff_v_balance_old) + (p))) /\ forall ff_i_balance_old. (exists ff_lt_balance_old_bound. ff_lt_balance_old_bound + S ff_i_balance_old = k) -> exists ff_p_balance_old ff_r_balance_old ff_s_balance_old. ((((exists ff_h_balance_old_factor. ff_h_balance_old_factor + S (ff_p_balance_old) = S ((S (ff_i_balance_old)) * c)) /\ exists ff_q_balance_old_factor. b = ff_q_balance_old_factor * S ((S (ff_i_balance_old)) * c) + (ff_p_balance_old))) /\ ((((exists ff_h_balance_old_partial. ff_h_balance_old_partial + S (ff_r_balance_old) = S ((S (ff_i_balance_old)) * ff_v_balance_old)) /\ exists ff_q_balance_old_partial. ff_u_balance_old = ff_q_balance_old_partial * S ((S (ff_i_balance_old)) * ff_v_balance_old) + (ff_r_balance_old))) /\ ((((exists ff_h_balance_old_successor. ff_h_balance_old_successor + S (ff_s_balance_old) = S ((S (S ff_i_balance_old)) * ff_v_balance_old)) /\ exists ff_q_balance_old_successor. ff_u_balance_old = ff_q_balance_old_successor * S ((S (S ff_i_balance_old)) * ff_v_balance_old) + (ff_s_balance_old))) /\ ff_s_balance_old = ff_r_balance_old * ff_p_balance_old)))))) -> (exists ff_u_balance_new ff_v_balance_new. ((((exists ff_h_balance_new_start. ff_h_balance_new_start + S (1) = S ((S (0)) * ff_v_balance_new)) /\ exists ff_q_balance_new_start. ff_u_balance_new = ff_q_balance_new_start * S ((S (0)) * ff_v_balance_new) + (1))) /\ ((((exists ff_h_balance_new_terminal. ff_h_balance_new_terminal + S (q) = S ((S (k)) * ff_v_balance_new)) /\ exists ff_q_balance_new_terminal. ff_u_balance_new = ff_q_balance_new_terminal * S ((S (k)) * ff_v_balance_new) + (q))) /\ forall ff_i_balance_new. (exists ff_lt_balance_new_bound. ff_lt_balance_new_bound + S ff_i_balance_new = k) -> exists ff_p_balance_new ff_r_balance_new ff_s_balance_new. ((((exists ff_h_balance_new_factor. ff_h_balance_new_factor + S (ff_p_balance_new) = S ((S (ff_i_balance_new)) * d)) /\ exists ff_q_balance_new_factor. z = ff_q_balance_new_factor * S ((S (ff_i_balance_new)) * d) + (ff_p_balance_new))) /\ ((((exists ff_h_balance_new_partial. ff_h_balance_new_partial + S (ff_r_balance_new) = S ((S (ff_i_balance_new)) * ff_v_balance_new)) /\ exists ff_q_balance_new_partial. ff_u_balance_new = ff_q_balance_new_partial * S ((S (ff_i_balance_new)) * ff_v_balance_new) + (ff_r_balance_new))) /\ ((((exists ff_h_balance_new_successor. ff_h_balance_new_successor + S (ff_s_balance_new) = S ((S (S ff_i_balance_new)) * ff_v_balance_new)) /\ exists ff_q_balance_new_successor. ff_u_balance_new = ff_q_balance_new_successor * S ((S (S ff_i_balance_new)) * ff_v_balance_new) + (ff_s_balance_new))) /\ ff_s_balance_new = ff_r_balance_new * ff_p_balance_new)))))) -> q * x = p * y

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA004A beta_product_succ_decompose PA004Y beta_product_transport_prefix PA0051 beta_product_functional PA002F beta_at_unique PA000B mul_assoc PA000H mul_comm PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Direct theorem dependents

PA0053 beta_product_swap_last_invariant

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

202 script commands · 34 reading checkpoints · 12 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 (10)
add eq zero rightsucc ne zerofinite lt succ eq or ltbeta product succ decomposebeta product transport prefixbeta product functionalbeta at uniquele succle refllt irrefl expanded
01Induction on kL1–10

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

  1. L1
    induction k
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro z
  5. L5
    intro d
  6. L6
    intro i
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro p
  10. L10
    intro q
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hi
03Separate the logical casesL12–13

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

  1. L12
    exfalso
  2. L13
    cases hi
04Establish hsiL14–23

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

  1. L14
    have hsi : S i = 0
  2. L15
    specialize add_eq_zero_right x1
  3. L16
    specialize add_eq_zero_right (S i)
  4. L17
    apply add_eq_zero_right
  5. L18
    exact hi_witness
  6. L19
    specialize succ_ne_zero i
  7. L20
    apply succ_ne_zero
  8. L21
    exact hsi
  9. L22
    intro b
  10. L23
    intro c
05Fix variables and assumptionsL24–33

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

  1. L24
    intro z
  2. L25
    intro d
  3. L26
    intro i
  4. L27
    intro x
  5. L28
    intro y
  6. L29
    intro p
  7. L30
    intro q
  8. L31
    intro hi
  9. L32
    intro hold_i
  10. L33
    intro hnew_i
06Fix variables and assumptionsL34–36

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

  1. L34
    intro hpreserve
  2. L35
    intro hproduct_old
  3. L36
    intro hproduct_new
07Establish hisplitL37–41

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. L37
    have hisplit : i = k ∨ Lt(i,k)Definitions: Lt(i,k)Original native command in the exact edition
  2. L38
    specialize finite_lt_succ_eq_or_lt k
  3. L39
    specialize finite_lt_succ_eq_or_lt i
  4. L40
    apply finite_lt_succ_eq_or_lt
  5. L41
    exact hi
08Establish hold_decompL42–48

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

  1. L42
    have hold_decomp : ∃ a. ∃ r. BetaAt(b,c,k,a) ∧ (Product(b,c,k,r) ∧ p = r · a)Definitions: BetaAt(b,c,k,a)Product(b,c,k,r)Original native command in the exact edition
  2. L43
    specialize beta_product_succ_decompose b
  3. L44
    specialize beta_product_succ_decompose c
  4. L45
    specialize beta_product_succ_decompose k
  5. L46
    specialize beta_product_succ_decompose p
  6. L47
    apply beta_product_succ_decompose
  7. L48
    exact hproduct_old
09Establish hnew_decompL49–55

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

  1. L49
    have hnew_decomp : ∃ a. ∃ r. BetaAt(z,d,k,a) ∧ (Product(z,d,k,r) ∧ q = r · a)Definitions: BetaAt(z,d,k,a)Product(z,d,k,r)Original native command in the exact edition
  2. L50
    specialize beta_product_succ_decompose z
  3. L51
    specialize beta_product_succ_decompose d
  4. L52
    specialize beta_product_succ_decompose k
  5. L53
    specialize beta_product_succ_decompose q
  6. L54
    apply beta_product_succ_decompose
  7. L55
    exact hproduct_new
10Separate the logical casesL56–64

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

  1. L56
    cases hold_decomp
  2. L57
    cases hold_decomp_witness
  3. L58
    cases hold_decomp_witness_witness
  4. L59
    cases hold_decomp_witness_witness_right
  5. L60
    cases hnew_decomp
  6. L61
    cases hnew_decomp_witness
  7. L62
    cases hnew_decomp_witness_witness
  8. L63
    cases hnew_decomp_witness_witness_right
  9. L64
    cases hisplit
11Establish haxL65–74

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

  1. L65
    have hax : x1 = x
  2. L66
    specialize beta_at_unique b
  3. L67
    specialize beta_at_unique c
  4. L68
    specialize beta_at_unique k
  5. L69
    specialize beta_at_unique x1
  6. L70
    specialize beta_at_unique x
  7. L71
    apply beta_at_unique
  8. L72
    exact hold_decomp_witness_witness_left
  9. L73
    rewrite hisplit_left at hold_i
  10. L74
    rewrite hisplit_left at hold_i
12Use earlier factsL75–75

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

  1. L75
    exact hold_i
13Establish hbyL76–85

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

  1. L76
    have hby : x3 = y
  2. L77
    specialize beta_at_unique z
  3. L78
    specialize beta_at_unique d
  4. L79
    specialize beta_at_unique k
  5. L80
    specialize beta_at_unique x3
  6. L81
    specialize beta_at_unique y
  7. L82
    apply beta_at_unique
  8. L83
    exact hnew_decomp_witness_witness_left
  9. L84
    rewrite hisplit_left at hnew_i
  10. L85
    rewrite hisplit_left at hnew_i
14Use earlier factsL86–86

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

  1. L86
    exact hnew_i
15Establish hprefix_transportL87–96

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

  1. L87
    have hprefix_transport : Product(z,d,k,x2)Definitions: Product(z,d,k,x2)Original native command in the exact edition
  2. L88
    specialize beta_product_transport_prefix b
  3. L89
    specialize beta_product_transport_prefix c
  4. L90
    specialize beta_product_transport_prefix z
  5. L91
    specialize beta_product_transport_prefix d
  6. L92
    specialize beta_product_transport_prefix k
  7. L93
    specialize beta_product_transport_prefix x2
  8. L94
    apply beta_product_transport_prefix
  9. L95
    exact hold_decomp_witness_witness_right_left
  10. L96
    intro j
16Fix variables and assumptionsL97–99

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

  1. L97
    intro a
  2. L98
    intro hj
  3. L99
    intro hold
17Use earlier factsL100–106

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

  1. L100
    specialize hpreserve j
  2. L101
    specialize hpreserve a
  3. L102
    apply hpreserve
  4. L103
    specialize le_succ (S j)
  5. L104
    specialize le_succ k
  6. L105
    apply le_succ
  7. L106
    exact hj
18Fix variables and assumptionsL107–107

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

  1. L107
    intro hjk
19Use earlier factsL108–109

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

  1. L108
    specialize lt_irrefl_expanded k
  2. L109
    apply lt_irrefl_expanded
20Calculate and transport equalitiesL110–111

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

  1. L110
    rewrite hjk at hj
  2. L111
    rewrite hisplit_left at hj
21Use earlier factsL112–113

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

  1. L112
    exact hj
  2. L113
    exact hold
22Separate the logical casesL114–117

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

  1. L114
    cases hprefix_transport
  2. L115
    cases hprefix_transport_witness
  3. L116
    cases hnew_decomp_witness_witness_right_left
  4. L117
    cases hnew_decomp_witness_witness_right_left_witness
23Calculate and transport equalitiesL118–126

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

  1. L118
    rewrite hold_decomp_witness_witness_right_right
  2. L119
    rewrite hnew_decomp_witness_witness_right_right
  3. L120
    rewrite hax
  4. L121
    rewrite hby
  5. L122
    trans (x4 * x) * y
  6. L123
    simp [mul_assoc, mul_comm]
  7. L124
    congr
  8. L125
    congr
  9. L126
    symm
24Use earlier factsL127–136

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

  1. L127
    specialize beta_product_functional z
  2. L128
    specialize beta_product_functional d
  3. L129
    specialize beta_product_functional k
  4. L130
    specialize beta_product_functional x2
  5. L131
    specialize beta_product_functional x5
  6. L132
    specialize beta_product_functional x6
  7. L133
    specialize beta_product_functional x4
  8. L134
    specialize beta_product_functional x7
  9. L135
    specialize beta_product_functional x8
  10. L136
    apply beta_product_functional
25Use earlier factsL137–138

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

  1. L137
    exact hprefix_transport_witness_witness
  2. L138
    exact hnew_decomp_witness_witness_right_left_witness_witness
26Calculate and transport equalitiesL139–140

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

  1. L139
    refl
  2. L140
    refl
27Establish hkiL141–146

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

  1. L141
    have hki : ~(k = i)
  2. L142
    intro hki_eq
  3. L143
    specialize lt_irrefl_expanded k
  4. L144
    apply lt_irrefl_expanded
  5. L145
    rewrite <- hki_eq at hisplit_right
  6. L146
    exact hisplit_right
28Establish hlast_newL147–154

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

  1. L147
    have hlast_new : BetaAt(z,d,k,x1)Definitions: BetaAt(z,d,k,x1)Original native command in the exact edition
  2. L148
    specialize hpreserve k
  3. L149
    specialize hpreserve x1
  4. L150
    apply hpreserve
  5. L151
    specialize le_refl (S k)
  6. L152
    exact le_refl
  7. L153
    exact hki
  8. L154
    exact hold_decomp_witness_witness_left
29Establish hlast_eqL155–163

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

  1. L155
    have hlast_eq : x3 = x1
  2. L156
    specialize beta_at_unique z
  3. L157
    specialize beta_at_unique d
  4. L158
    specialize beta_at_unique k
  5. L159
    specialize beta_at_unique x3
  6. L160
    specialize beta_at_unique x1
  7. L161
    apply beta_at_unique
  8. L162
    exact hnew_decomp_witness_witness_left
  9. L163
    exact hlast_new
30Establish hprefix_preserveL164–173

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

  1. L164
    have hprefix_preserve : ∀ j. ∀ a. Lt(j,k) → ¬j = i → BetaAt(b,c,j,a) → BetaAt(z,d,j,a)Definitions: Lt(j,k)BetaAt(b,c,j,a)BetaAt(z,d,j,a)Original native command in the exact edition
  2. L165
    intro j
  3. L166
    intro a
  4. L167
    intro hj
  5. L168
    intro hji
  6. L169
    intro hold
  7. L170
    specialize hpreserve j
  8. L171
    specialize hpreserve a
  9. L172
    apply hpreserve
  10. L173
    specialize le_succ (S j)
31Use earlier factsL174–178

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

  1. L174
    specialize le_succ k
  2. L175
    apply le_succ
  3. L176
    exact hj
  4. L177
    exact hji
  5. L178
    exact hold
32Establish hbalanceL179–188

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

  1. L179
    have hbalance : x4 * x = x2 * y
  2. L180
    specialize IH b
  3. L181
    specialize IH c
  4. L182
    specialize IH z
  5. L183
    specialize IH d
  6. L184
    specialize IH i
  7. L185
    specialize IH x
  8. L186
    specialize IH y
  9. L187
    specialize IH x2
  10. L188
    specialize IH x4
33Use earlier factsL189–195

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

  1. L189
    apply IH
  2. L190
    exact hisplit_right
  3. L191
    exact hold_i
  4. L192
    exact hnew_i
  5. L193
    exact hprefix_preserve
  6. L194
    exact hold_decomp_witness_witness_right_left
  7. L195
    exact hnew_decomp_witness_witness_right_left
34Calculate and transport equalitiesL196–202

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

  1. L196
    rewrite hold_decomp_witness_witness_right_right
  2. L197
    rewrite hnew_decomp_witness_witness_right_right
  3. L198
    rewrite hlast_eq
  4. L199
    trans (x4 * x) * x1
  5. L200
    simp [mul_assoc, mul_comm]
  6. L201
    rewrite hbalance
  7. L202
    simp [mul_assoc, mul_comm]

Library-wide reading audit

Original defined command ledger · 202 lines
  1. 0001induction k
  2. 0002intro b
  3. 0003intro c
  4. 0004intro z
  5. 0005intro d
  6. 0006intro i
  7. 0007intro x
  8. 0008intro y
  9. 0009intro p
  10. 0010intro q
  11. 0011intro hi
  12. 0012exfalso
  13. 0013cases hi
  14. 0014have hsi : S i = 0
  15. 0015specialize add_eq_zero_right x1
  16. 0016specialize add_eq_zero_right (S i)
  17. 0017apply add_eq_zero_right
  18. 0018exact hi_witness
  19. 0019specialize succ_ne_zero i
  20. 0020apply succ_ne_zero
  21. 0021exact hsi
  22. 0022intro b
  23. 0023intro c
  24. 0024intro z
  25. 0025intro d
  26. 0026intro i
  27. 0027intro x
  28. 0028intro y
  29. 0029intro p
  30. 0030intro q
  31. 0031intro hi
  32. 0032intro hold_i
  33. 0033intro hnew_i
  34. 0034intro hpreserve
  35. 0035intro hproduct_old
  36. 0036intro hproduct_new
  37. 0037have hisplit : i = k ∨ Lt(i,k)
    Exact native replay linehave hisplit : i = k \/ exists h. h + S i = k
  38. 0038specialize finite_lt_succ_eq_or_lt k
  39. 0039specialize finite_lt_succ_eq_or_lt i
  40. 0040apply finite_lt_succ_eq_or_lt
  41. 0041exact hi
  42. 0042have hold_decomp : ∃ a. ∃ r. BetaAt(b,c,k,a) ∧ (Product(b,c,k,r) ∧ p = r · a)
    Exact native replay linehave hold_decomp : exists a r. (((exists ff_h_balance_old_last. ff_h_balance_old_last + S (a) = S ((S (k)) * c)) /\ exists ff_q_balance_old_last. b = ff_q_balance_old_last * S ((S (k)) * c) + (a))) /\ ((exists ff_u_balance_old_prefix ff_v_balance_old_prefix. ((((exists ff_h_balance_old_prefix_start. ff_h_balance_old_prefix_start + S (1) = S ((S (0)) * ff_v_balance_old_prefix)) /\ exists ff_q_balance_old_prefix_start. ff_u_balance_old_prefix = ff_q_balance_old_prefix_start * S ((S (0)) * ff_v_balance_old_prefix) + (1))) /\ ((((exists ff_h_balance_old_prefix_terminal. ff_h_balance_old_prefix_terminal + S (r) = S ((S (k)) * ff_v_balance_old_prefix)) /\ exists ff_q_balance_old_prefix_terminal. ff_u_balance_old_prefix = ff_q_balance_old_prefix_terminal * S ((S (k)) * ff_v_balance_old_prefix) + (r))) /\ forall ff_i_balance_old_prefix. (exists ff_lt_balance_old_prefix_bound. ff_lt_balance_old_prefix_bound + S ff_i_balance_old_prefix = k) -> exists ff_p_balance_old_prefix ff_r_balance_old_prefix ff_s_balance_old_prefix. ((((exists ff_h_balance_old_prefix_factor. ff_h_balance_old_prefix_factor + S (ff_p_balance_old_prefix) = S ((S (ff_i_balance_old_prefix)) * c)) /\ exists ff_q_balance_old_prefix_factor. b = ff_q_balance_old_prefix_factor * S ((S (ff_i_balance_old_prefix)) * c) + (ff_p_balance_old_prefix))) /\ ((((exists ff_h_balance_old_prefix_partial. ff_h_balance_old_prefix_partial + S (ff_r_balance_old_prefix) = S ((S (ff_i_balance_old_prefix)) * ff_v_balance_old_prefix)) /\ exists ff_q_balance_old_prefix_partial. ff_u_balance_old_prefix = ff_q_balance_old_prefix_partial * S ((S (ff_i_balance_old_prefix)) * ff_v_balance_old_prefix) + (ff_r_balance_old_prefix))) /\ ((((exists ff_h_balance_old_prefix_successor. ff_h_balance_old_prefix_successor + S (ff_s_balance_old_prefix) = S ((S (S ff_i_balance_old_prefix)) * ff_v_balance_old_prefix)) /\ exists ff_q_balance_old_prefix_successor. ff_u_balance_old_prefix = ff_q_balance_old_prefix_successor * S ((S (S ff_i_balance_old_prefix)) * ff_v_balance_old_prefix) + (ff_s_balance_old_prefix))) /\ ff_s_balance_old_prefix = ff_r_balance_old_prefix * ff_p_balance_old_prefix)))))) /\ p = r * a)
  43. 0043specialize beta_product_succ_decompose b
  44. 0044specialize beta_product_succ_decompose c
  45. 0045specialize beta_product_succ_decompose k
  46. 0046specialize beta_product_succ_decompose p
  47. 0047apply beta_product_succ_decompose
  48. 0048exact hproduct_old
  49. 0049have hnew_decomp : ∃ a. ∃ r. BetaAt(z,d,k,a) ∧ (Product(z,d,k,r) ∧ q = r · a)
    Exact native replay linehave hnew_decomp : exists a r. (((exists ff_h_balance_new_last. ff_h_balance_new_last + S (a) = S ((S (k)) * d)) /\ exists ff_q_balance_new_last. z = ff_q_balance_new_last * S ((S (k)) * d) + (a))) /\ ((exists ff_u_balance_new_prefix ff_v_balance_new_prefix. ((((exists ff_h_balance_new_prefix_start. ff_h_balance_new_prefix_start + S (1) = S ((S (0)) * ff_v_balance_new_prefix)) /\ exists ff_q_balance_new_prefix_start. ff_u_balance_new_prefix = ff_q_balance_new_prefix_start * S ((S (0)) * ff_v_balance_new_prefix) + (1))) /\ ((((exists ff_h_balance_new_prefix_terminal. ff_h_balance_new_prefix_terminal + S (r) = S ((S (k)) * ff_v_balance_new_prefix)) /\ exists ff_q_balance_new_prefix_terminal. ff_u_balance_new_prefix = ff_q_balance_new_prefix_terminal * S ((S (k)) * ff_v_balance_new_prefix) + (r))) /\ forall ff_i_balance_new_prefix. (exists ff_lt_balance_new_prefix_bound. ff_lt_balance_new_prefix_bound + S ff_i_balance_new_prefix = k) -> exists ff_p_balance_new_prefix ff_r_balance_new_prefix ff_s_balance_new_prefix. ((((exists ff_h_balance_new_prefix_factor. ff_h_balance_new_prefix_factor + S (ff_p_balance_new_prefix) = S ((S (ff_i_balance_new_prefix)) * d)) /\ exists ff_q_balance_new_prefix_factor. z = ff_q_balance_new_prefix_factor * S ((S (ff_i_balance_new_prefix)) * d) + (ff_p_balance_new_prefix))) /\ ((((exists ff_h_balance_new_prefix_partial. ff_h_balance_new_prefix_partial + S (ff_r_balance_new_prefix) = S ((S (ff_i_balance_new_prefix)) * ff_v_balance_new_prefix)) /\ exists ff_q_balance_new_prefix_partial. ff_u_balance_new_prefix = ff_q_balance_new_prefix_partial * S ((S (ff_i_balance_new_prefix)) * ff_v_balance_new_prefix) + (ff_r_balance_new_prefix))) /\ ((((exists ff_h_balance_new_prefix_successor. ff_h_balance_new_prefix_successor + S (ff_s_balance_new_prefix) = S ((S (S ff_i_balance_new_prefix)) * ff_v_balance_new_prefix)) /\ exists ff_q_balance_new_prefix_successor. ff_u_balance_new_prefix = ff_q_balance_new_prefix_successor * S ((S (S ff_i_balance_new_prefix)) * ff_v_balance_new_prefix) + (ff_s_balance_new_prefix))) /\ ff_s_balance_new_prefix = ff_r_balance_new_prefix * ff_p_balance_new_prefix)))))) /\ q = r * a)
  50. 0050specialize beta_product_succ_decompose z
  51. 0051specialize beta_product_succ_decompose d
  52. 0052specialize beta_product_succ_decompose k
  53. 0053specialize beta_product_succ_decompose q
  54. 0054apply beta_product_succ_decompose
  55. 0055exact hproduct_new
  56. 0056cases hold_decomp
  57. 0057cases hold_decomp_witness
  58. 0058cases hold_decomp_witness_witness
  59. 0059cases hold_decomp_witness_witness_right
  60. 0060cases hnew_decomp
  61. 0061cases hnew_decomp_witness
  62. 0062cases hnew_decomp_witness_witness
  63. 0063cases hnew_decomp_witness_witness_right
  64. 0064cases hisplit
  65. 0065have hax : x1 = x
  66. 0066specialize beta_at_unique b
  67. 0067specialize beta_at_unique c
  68. 0068specialize beta_at_unique k
  69. 0069specialize beta_at_unique x1
  70. 0070specialize beta_at_unique x
  71. 0071apply beta_at_unique
  72. 0072exact hold_decomp_witness_witness_left
  73. 0073rewrite hisplit_left at hold_i
  74. 0074rewrite hisplit_left at hold_i
  75. 0075exact hold_i
  76. 0076have hby : x3 = y
  77. 0077specialize beta_at_unique z
  78. 0078specialize beta_at_unique d
  79. 0079specialize beta_at_unique k
  80. 0080specialize beta_at_unique x3
  81. 0081specialize beta_at_unique y
  82. 0082apply beta_at_unique
  83. 0083exact hnew_decomp_witness_witness_left
  84. 0084rewrite hisplit_left at hnew_i
  85. 0085rewrite hisplit_left at hnew_i
  86. 0086exact hnew_i
  87. 0087have hprefix_transport : Product(z,d,k,x2)
    Exact native replay linehave hprefix_transport : exists ff_u_balance_transported_prefix ff_v_balance_transported_prefix. ((((exists ff_h_balance_transported_prefix_start. ff_h_balance_transported_prefix_start + S (1) = S ((S (0)) * ff_v_balance_transported_prefix)) /\ exists ff_q_balance_transported_prefix_start. ff_u_balance_transported_prefix = ff_q_balance_transported_prefix_start * S ((S (0)) * ff_v_balance_transported_prefix) + (1))) /\ ((((exists ff_h_balance_transported_prefix_terminal. ff_h_balance_transported_prefix_terminal + S (x2) = S ((S (k)) * ff_v_balance_transported_prefix)) /\ exists ff_q_balance_transported_prefix_terminal. ff_u_balance_transported_prefix = ff_q_balance_transported_prefix_terminal * S ((S (k)) * ff_v_balance_transported_prefix) + (x2))) /\ forall ff_i_balance_transported_prefix. (exists ff_lt_balance_transported_prefix_bound. ff_lt_balance_transported_prefix_bound + S ff_i_balance_transported_prefix = k) -> exists ff_p_balance_transported_prefix ff_r_balance_transported_prefix ff_s_balance_transported_prefix. ((((exists ff_h_balance_transported_prefix_factor. ff_h_balance_transported_prefix_factor + S (ff_p_balance_transported_prefix) = S ((S (ff_i_balance_transported_prefix)) * d)) /\ exists ff_q_balance_transported_prefix_factor. z = ff_q_balance_transported_prefix_factor * S ((S (ff_i_balance_transported_prefix)) * d) + (ff_p_balance_transported_prefix))) /\ ((((exists ff_h_balance_transported_prefix_partial. ff_h_balance_transported_prefix_partial + S (ff_r_balance_transported_prefix) = S ((S (ff_i_balance_transported_prefix)) * ff_v_balance_transported_prefix)) /\ exists ff_q_balance_transported_prefix_partial. ff_u_balance_transported_prefix = ff_q_balance_transported_prefix_partial * S ((S (ff_i_balance_transported_prefix)) * ff_v_balance_transported_prefix) + (ff_r_balance_transported_prefix))) /\ ((((exists ff_h_balance_transported_prefix_successor. ff_h_balance_transported_prefix_successor + S (ff_s_balance_transported_prefix) = S ((S (S ff_i_balance_transported_prefix)) * ff_v_balance_transported_prefix)) /\ exists ff_q_balance_transported_prefix_successor. ff_u_balance_transported_prefix = ff_q_balance_transported_prefix_successor * S ((S (S ff_i_balance_transported_prefix)) * ff_v_balance_transported_prefix) + (ff_s_balance_transported_prefix))) /\ ff_s_balance_transported_prefix = ff_r_balance_transported_prefix * ff_p_balance_transported_prefix)))))
  88. 0088specialize beta_product_transport_prefix b
  89. 0089specialize beta_product_transport_prefix c
  90. 0090specialize beta_product_transport_prefix z
  91. 0091specialize beta_product_transport_prefix d
  92. 0092specialize beta_product_transport_prefix k
  93. 0093specialize beta_product_transport_prefix x2
  94. 0094apply beta_product_transport_prefix
  95. 0095exact hold_decomp_witness_witness_right_left
  96. 0096intro j
  97. 0097intro a
  98. 0098intro hj
  99. 0099intro hold
  100. 0100specialize hpreserve j
  101. 0101specialize hpreserve a
  102. 0102apply hpreserve
  103. 0103specialize le_succ (S j)
  104. 0104specialize le_succ k
  105. 0105apply le_succ
  106. 0106exact hj
  107. 0107intro hjk
  108. 0108specialize lt_irrefl_expanded k
  109. 0109apply lt_irrefl_expanded
  110. 0110rewrite hjk at hj
  111. 0111rewrite hisplit_left at hj
  112. 0112exact hj
  113. 0113exact hold
  114. 0114cases hprefix_transport
  115. 0115cases hprefix_transport_witness
  116. 0116cases hnew_decomp_witness_witness_right_left
  117. 0117cases hnew_decomp_witness_witness_right_left_witness
  118. 0118rewrite hold_decomp_witness_witness_right_right
  119. 0119rewrite hnew_decomp_witness_witness_right_right
  120. 0120rewrite hax
  121. 0121rewrite hby
  122. 0122trans (x4 * x) * y
  123. 0123simp [mul_assoc, mul_comm]
  124. 0124congr
  125. 0125congr
  126. 0126symm
  127. 0127specialize beta_product_functional z
  128. 0128specialize beta_product_functional d
  129. 0129specialize beta_product_functional k
  130. 0130specialize beta_product_functional x2
  131. 0131specialize beta_product_functional x5
  132. 0132specialize beta_product_functional x6
  133. 0133specialize beta_product_functional x4
  134. 0134specialize beta_product_functional x7
  135. 0135specialize beta_product_functional x8
  136. 0136apply beta_product_functional
  137. 0137exact hprefix_transport_witness_witness
  138. 0138exact hnew_decomp_witness_witness_right_left_witness_witness
  139. 0139refl
  140. 0140refl
  141. 0141have hki : ~(k = i)
  142. 0142intro hki_eq
  143. 0143specialize lt_irrefl_expanded k
  144. 0144apply lt_irrefl_expanded
  145. 0145rewrite <- hki_eq at hisplit_right
  146. 0146exact hisplit_right
  147. 0147have hlast_new : BetaAt(z,d,k,x1)
    Exact native replay linehave hlast_new : ((exists h. h + S x1 = S ((S k) * d)) /\ exists w. z = w * S ((S k) * d) + x1)
  148. 0148specialize hpreserve k
  149. 0149specialize hpreserve x1
  150. 0150apply hpreserve
  151. 0151specialize le_refl (S k)
  152. 0152exact le_refl
  153. 0153exact hki
  154. 0154exact hold_decomp_witness_witness_left
  155. 0155have hlast_eq : x3 = x1
  156. 0156specialize beta_at_unique z
  157. 0157specialize beta_at_unique d
  158. 0158specialize beta_at_unique k
  159. 0159specialize beta_at_unique x3
  160. 0160specialize beta_at_unique x1
  161. 0161apply beta_at_unique
  162. 0162exact hnew_decomp_witness_witness_left
  163. 0163exact hlast_new
  164. 0164have hprefix_preserve : ∀ j. ∀ a. Lt(j,k) → ¬j = i → BetaAt(b,c,j,a) → BetaAt(z,d,j,a)
    Exact native replay linehave hprefix_preserve : forall j a. (exists h. h + S j = k) -> ~(j = i) -> ((exists h. h + S a = S ((S j) * c)) /\ exists w. b = w * S ((S j) * c) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists w. z = w * S ((S j) * d) + a)
  165. 0165intro j
  166. 0166intro a
  167. 0167intro hj
  168. 0168intro hji
  169. 0169intro hold
  170. 0170specialize hpreserve j
  171. 0171specialize hpreserve a
  172. 0172apply hpreserve
  173. 0173specialize le_succ (S j)
  174. 0174specialize le_succ k
  175. 0175apply le_succ
  176. 0176exact hj
  177. 0177exact hji
  178. 0178exact hold
  179. 0179have hbalance : x4 * x = x2 * y
  180. 0180specialize IH b
  181. 0181specialize IH c
  182. 0182specialize IH z
  183. 0183specialize IH d
  184. 0184specialize IH i
  185. 0185specialize IH x
  186. 0186specialize IH y
  187. 0187specialize IH x2
  188. 0188specialize IH x4
  189. 0189apply IH
  190. 0190exact hisplit_right
  191. 0191exact hold_i
  192. 0192exact hnew_i
  193. 0193exact hprefix_preserve
  194. 0194exact hold_decomp_witness_witness_right_left
  195. 0195exact hnew_decomp_witness_witness_right_left
  196. 0196rewrite hold_decomp_witness_witness_right_right
  197. 0197rewrite hnew_decomp_witness_witness_right_right
  198. 0198rewrite hlast_eq
  199. 0199trans (x4 * x) * x1
  200. 0200simp [mul_assoc, mul_comm]
  201. 0201rewrite hbalance
  202. 0202simp [mul_assoc, mul_comm]