PC000C

beta_product_bit_weighted_upper_power

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

An actual bit-weighted finite product has the corresponding upper bound by a power of its actual bit sum.

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 first-order arithmetic statement

forall b c d f B l z k Q. (forall pc_index_weight_upper_source pc_factor_weight_upper_source pc_bit_weight_upper_source. (exists pc_lt_weight_upper_source_index. pc_lt_weight_upper_source_index + S (pc_index_weight_upper_source) = (l)) -> (((exists fs_h_pc_weight_upper_source_factor. fs_h_pc_weight_upper_source_factor + S (pc_factor_weight_upper_source) = S ((S (pc_index_weight_upper_source)) * c)) /\ exists fs_q_pc_weight_upper_source_factor. b = fs_q_pc_weight_upper_source_factor * S ((S (pc_index_weight_upper_source)) * c) + (pc_factor_weight_upper_source))) -> (((exists fs_h_pc_weight_upper_source_bit. fs_h_pc_weight_upper_source_bit + S (pc_bit_weight_upper_source) = S ((S (pc_index_weight_upper_source)) * f)) /\ exists fs_q_pc_weight_upper_source_bit. d = fs_q_pc_weight_upper_source_bit * S ((S (pc_index_weight_upper_source)) * f) + (pc_bit_weight_upper_source))) -> ((pc_bit_weight_upper_source = 0 /\ (pc_factor_weight_upper_source = 1)) \/ (pc_bit_weight_upper_source = 1 /\ (exists pc_le_weight_upper_source_one. pc_le_weight_upper_source_one + (pc_factor_weight_upper_source) = (B))))) -> (exists ff_u_pc_weight_upper_product ff_v_pc_weight_upper_product. ((((exists ff_h_pc_weight_upper_product_start. ff_h_pc_weight_upper_product_start + S (1) = S ((S (0)) * ff_v_pc_weight_upper_product)) /\ exists ff_q_pc_weight_upper_product_start. ff_u_pc_weight_upper_product = ff_q_pc_weight_upper_product_start * S ((S (0)) * ff_v_pc_weight_upper_product) + (1))) /\ ((((exists ff_h_pc_weight_upper_product_terminal. ff_h_pc_weight_upper_product_terminal + S (z) = S ((S (l)) * ff_v_pc_weight_upper_product)) /\ exists ff_q_pc_weight_upper_product_terminal. ff_u_pc_weight_upper_product = ff_q_pc_weight_upper_product_terminal * S ((S (l)) * ff_v_pc_weight_upper_product) + (z))) /\ forall ff_i_pc_weight_upper_product. (exists ff_lt_pc_weight_upper_product_bound. ff_lt_pc_weight_upper_product_bound + S ff_i_pc_weight_upper_product = l) -> exists ff_p_pc_weight_upper_product ff_r_pc_weight_upper_product ff_s_pc_weight_upper_product. ((((exists ff_h_pc_weight_upper_product_factor. ff_h_pc_weight_upper_product_factor + S (ff_p_pc_weight_upper_product) = S ((S (ff_i_pc_weight_upper_product)) * c)) /\ exists ff_q_pc_weight_upper_product_factor. b = ff_q_pc_weight_upper_product_factor * S ((S (ff_i_pc_weight_upper_product)) * c) + (ff_p_pc_weight_upper_product))) /\ ((((exists ff_h_pc_weight_upper_product_partial. ff_h_pc_weight_upper_product_partial + S (ff_r_pc_weight_upper_product) = S ((S (ff_i_pc_weight_upper_product)) * ff_v_pc_weight_upper_product)) /\ exists ff_q_pc_weight_upper_product_partial. ff_u_pc_weight_upper_product = ff_q_pc_weight_upper_product_partial * S ((S (ff_i_pc_weight_upper_product)) * ff_v_pc_weight_upper_product) + (ff_r_pc_weight_upper_product))) /\ ((((exists ff_h_pc_weight_upper_product_successor. ff_h_pc_weight_upper_product_successor + S (ff_s_pc_weight_upper_product) = S ((S (S ff_i_pc_weight_upper_product)) * ff_v_pc_weight_upper_product)) /\ exists ff_q_pc_weight_upper_product_successor. ff_u_pc_weight_upper_product = ff_q_pc_weight_upper_product_successor * S ((S (S ff_i_pc_weight_upper_product)) * ff_v_pc_weight_upper_product) + (ff_s_pc_weight_upper_product))) /\ ff_s_pc_weight_upper_product = ff_r_pc_weight_upper_product * ff_p_pc_weight_upper_product)))))) -> (exists fs_u_pc_weight_upper_sum fs_v_pc_weight_upper_sum. ((((exists fs_h_pc_weight_upper_sum_body_start. fs_h_pc_weight_upper_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_weight_upper_sum)) /\ exists fs_q_pc_weight_upper_sum_body_start. fs_u_pc_weight_upper_sum = fs_q_pc_weight_upper_sum_body_start * S ((S (0)) * fs_v_pc_weight_upper_sum) + (0))) /\ ((((exists fs_h_pc_weight_upper_sum_body_terminal. fs_h_pc_weight_upper_sum_body_terminal + S (k) = S ((S (l)) * fs_v_pc_weight_upper_sum)) /\ exists fs_q_pc_weight_upper_sum_body_terminal. fs_u_pc_weight_upper_sum = fs_q_pc_weight_upper_sum_body_terminal * S ((S (l)) * fs_v_pc_weight_upper_sum) + (k))) /\ forall fs_i_pc_weight_upper_sum_body_steps. (exists fs_lt_pc_weight_upper_sum_body_steps_bound. fs_lt_pc_weight_upper_sum_body_steps_bound + S fs_i_pc_weight_upper_sum_body_steps = l) -> exists fs_a_pc_weight_upper_sum_body_steps fs_r_pc_weight_upper_sum_body_steps fs_s_pc_weight_upper_sum_body_steps. ((((exists fs_h_pc_weight_upper_sum_body_steps_summand. fs_h_pc_weight_upper_sum_body_steps_summand + S (fs_a_pc_weight_upper_sum_body_steps) = S ((S (fs_i_pc_weight_upper_sum_body_steps)) * f)) /\ exists fs_q_pc_weight_upper_sum_body_steps_summand. d = fs_q_pc_weight_upper_sum_body_steps_summand * S ((S (fs_i_pc_weight_upper_sum_body_steps)) * f) + (fs_a_pc_weight_upper_sum_body_steps))) /\ ((((exists fs_h_pc_weight_upper_sum_body_steps_partial. fs_h_pc_weight_upper_sum_body_steps_partial + S (fs_r_pc_weight_upper_sum_body_steps) = S ((S (fs_i_pc_weight_upper_sum_body_steps)) * fs_v_pc_weight_upper_sum)) /\ exists fs_q_pc_weight_upper_sum_body_steps_partial. fs_u_pc_weight_upper_sum = fs_q_pc_weight_upper_sum_body_steps_partial * S ((S (fs_i_pc_weight_upper_sum_body_steps)) * fs_v_pc_weight_upper_sum) + (fs_r_pc_weight_upper_sum_body_steps))) /\ ((((exists fs_h_pc_weight_upper_sum_body_steps_successor. fs_h_pc_weight_upper_sum_body_steps_successor + S (fs_s_pc_weight_upper_sum_body_steps) = S ((S (S fs_i_pc_weight_upper_sum_body_steps)) * fs_v_pc_weight_upper_sum)) /\ exists fs_q_pc_weight_upper_sum_body_steps_successor. fs_u_pc_weight_upper_sum = fs_q_pc_weight_upper_sum_body_steps_successor * S ((S (S fs_i_pc_weight_upper_sum_body_steps)) * fs_v_pc_weight_upper_sum) + (fs_s_pc_weight_upper_sum_body_steps))) /\ fs_s_pc_weight_upper_sum_body_steps = fs_r_pc_weight_upper_sum_body_steps + fs_a_pc_weight_upper_sum_body_steps)))))) -> (exists pa_b_pc_weight_upper_power pa_c_pc_weight_upper_power. ((forall pa_i_pc_weight_upper_power_repeat. (exists pa_lt_pc_weight_upper_power_repeat_bound. pa_lt_pc_weight_upper_power_repeat_bound + S pa_i_pc_weight_upper_power_repeat = k) -> (((exists pa_h_pc_weight_upper_power_repeat_decoded. pa_h_pc_weight_upper_power_repeat_decoded + S (B) = S ((S (pa_i_pc_weight_upper_power_repeat)) * pa_c_pc_weight_upper_power)) /\ exists pa_q_pc_weight_upper_power_repeat_decoded. pa_b_pc_weight_upper_power = pa_q_pc_weight_upper_power_repeat_decoded * S ((S (pa_i_pc_weight_upper_power_repeat)) * pa_c_pc_weight_upper_power) + (B)))) /\ (exists pa_u_pc_weight_upper_power_product pa_v_pc_weight_upper_power_product. ((((exists pa_h_pc_weight_upper_power_product_start. pa_h_pc_weight_upper_power_product_start + S (1) = S ((S (0)) * pa_v_pc_weight_upper_power_product)) /\ exists pa_q_pc_weight_upper_power_product_start. pa_u_pc_weight_upper_power_product = pa_q_pc_weight_upper_power_product_start * S ((S (0)) * pa_v_pc_weight_upper_power_product) + (1))) /\ ((((exists pa_h_pc_weight_upper_power_product_terminal. pa_h_pc_weight_upper_power_product_terminal + S (Q) = S ((S (k)) * pa_v_pc_weight_upper_power_product)) /\ exists pa_q_pc_weight_upper_power_product_terminal. pa_u_pc_weight_upper_power_product = pa_q_pc_weight_upper_power_product_terminal * S ((S (k)) * pa_v_pc_weight_upper_power_product) + (Q))) /\ forall pa_i_pc_weight_upper_power_product. (exists pa_lt_pc_weight_upper_power_product_bound. pa_lt_pc_weight_upper_power_product_bound + S pa_i_pc_weight_upper_power_product = k) -> exists pa_p_pc_weight_upper_power_product pa_r_pc_weight_upper_power_product pa_s_pc_weight_upper_power_product. ((((exists pa_h_pc_weight_upper_power_product_factor. pa_h_pc_weight_upper_power_product_factor + S (pa_p_pc_weight_upper_power_product) = S ((S (pa_i_pc_weight_upper_power_product)) * pa_c_pc_weight_upper_power)) /\ exists pa_q_pc_weight_upper_power_product_factor. pa_b_pc_weight_upper_power = pa_q_pc_weight_upper_power_product_factor * S ((S (pa_i_pc_weight_upper_power_product)) * pa_c_pc_weight_upper_power) + (pa_p_pc_weight_upper_power_product))) /\ ((((exists pa_h_pc_weight_upper_power_product_partial. pa_h_pc_weight_upper_power_product_partial + S (pa_r_pc_weight_upper_power_product) = S ((S (pa_i_pc_weight_upper_power_product)) * pa_v_pc_weight_upper_power_product)) /\ exists pa_q_pc_weight_upper_power_product_partial. pa_u_pc_weight_upper_power_product = pa_q_pc_weight_upper_power_product_partial * S ((S (pa_i_pc_weight_upper_power_product)) * pa_v_pc_weight_upper_power_product) + (pa_r_pc_weight_upper_power_product))) /\ ((((exists pa_h_pc_weight_upper_power_product_successor. pa_h_pc_weight_upper_power_product_successor + S (pa_s_pc_weight_upper_power_product) = S ((S (S pa_i_pc_weight_upper_power_product)) * pa_v_pc_weight_upper_power_product)) /\ exists pa_q_pc_weight_upper_power_product_successor. pa_u_pc_weight_upper_power_product = pa_q_pc_weight_upper_power_product_successor * S ((S (S pa_i_pc_weight_upper_power_product)) * pa_v_pc_weight_upper_power_product) + (pa_s_pc_weight_upper_power_product))) /\ pa_s_pc_weight_upper_power_product = pa_r_pc_weight_upper_power_product * pa_p_pc_weight_upper_power_product)))))))) -> (exists pc_le_weight_upper_result. pc_le_weight_upper_result + (z) = (Q))

Constructive proof overview

Generated structural guide

An actual bit-weighted finite product has the corresponding upper bound by a power of its actual bit sum.

The unchanged tactic script uses 12 declared prerequisites and contains 154 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

beta_product_zero Stable theorem; checked-use authorized beta_sum_zero Stable theorem; checked-use authorized pow_zero Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized beta_product_succ_decompose Stable theorem; checked-use authorized beta_sum_succ_decompose Stable theorem; checked-use authorized pow_exists Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized pow_functional Stable theorem; checked-use authorized pow_successor_pair_mul Stable theorem; checked-use authorized mul_le_mul Alpha theorem; checked-use authorized mul_one Stable theorem; checked-use authorized

Direct dependents

PC001F central_binom_prime_count_power_bound

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

154 script commands · 28 reading checkpoints · 13 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.

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–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro f
  5. L5
    intro B
02Induction on lL6–13

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

  1. L6
    induction l
  2. L7
    intro z
  3. L8
    intro k
  4. L9
    intro Q
  5. L10
    intro hw
  6. L11
    intro hz
  7. L12
    intro hk
  8. L13
    intro hQ
03Establish hz1L14–19

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

  1. L14
    have hz1 : z = 1
  2. L15
    specialize beta_product_zero b
  3. L16
    specialize beta_product_zero c
  4. L17
    specialize beta_product_zero z
  5. L18
    apply beta_product_zero
  6. L19
    exact hz
04Establish hk0L20–25

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

  1. L20
    have hk0 : k = 0
  2. L21
    specialize beta_sum_zero d
  3. L22
    specialize beta_sum_zero f
  4. L23
    specialize beta_sum_zero k
  5. L24
    apply beta_sum_zero
  6. L25
    exact hk
05Establish hQ1L26–35

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

  1. L26
    have hQ1 : Q = 1
  2. L27
    specialize pow_zero B
  3. L28
    specialize pow_zero k
  4. L29
    specialize pow_zero Q
  5. L30
    apply pow_zero
  6. L31
    exact hk0
  7. L32
    exact hQ
  8. L33
    rewrite hz1
  9. L34
    rewrite hQ1
  10. L35
    specialize le_refl 1
06Use earlier factsL36–36

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

  1. L36
    apply le_refl
07Fix variables and assumptionsL37–43

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

  1. L37
    intro z
  2. L38
    intro k
  3. L39
    intro Q
  4. L40
    intro hw
  5. L41
    intro hz
  6. L42
    intro hk
  7. L43
    intro hQ
08Establish hprodL44–50

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

  1. L44
    have hprod : ∃ a. ∃ w. BetaAt(b,c,l,a) ∧ (Product(b,c,l,w) ∧ z = w · a)Definitions: BetaAtProduct
  2. L45
    specialize beta_product_succ_decompose b
  3. L46
    specialize beta_product_succ_decompose c
  4. L47
    specialize beta_product_succ_decompose l
  5. L48
    specialize beta_product_succ_decompose z
  6. L49
    apply beta_product_succ_decompose
  7. L50
    exact hz
09Separate the logical casesL51–54

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

  1. L51
    cases hprod
  2. L52
    cases hprod_witness
  3. L53
    cases hprod_witness_witness
  4. L54
    cases hprod_witness_witness_right
10Establish hsumL55–61

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

  1. L55
    have hsum : ∃ e. ∃ K. BetaAt(d,f,l,e) ∧ (Sum(d,f,l,K) ∧ k = K + e)Definitions: BetaAtSum
  2. L56
    specialize beta_sum_succ_decompose d
  3. L57
    specialize beta_sum_succ_decompose f
  4. L58
    specialize beta_sum_succ_decompose l
  5. L59
    specialize beta_sum_succ_decompose k
  6. L60
    apply beta_sum_succ_decompose
  7. L61
    exact hk
11Separate the logical casesL62–65

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

  1. L62
    cases hsum
  2. L63
    cases hsum_witness
  3. L64
    cases hsum_witness_witness
  4. L65
    cases hsum_witness_witness_right
12Establish hpL66–69

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

  1. L66
    have hp : ∃ R. Pow(B,x3,R)Definitions: Pow
  2. L67
    specialize pow_exists B
  3. L68
    specialize pow_exists x3
  4. L69
    apply pow_exists
13Separate the logical casesL70–70

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

  1. L70
    cases hp
14Establish hpreL71–80

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

  1. L71
    have hpre : exists pc_le_weight_previous_bound. pc_le_weight_previous_bound + (x1) = (x4)
  2. L72
    specialize IH x1
  3. L73
    specialize IH x3
  4. L74
    specialize IH x4
  5. L75
    apply IH
  6. L76
    intro i
  7. L77
    intro a
  8. L78
    intro e
  9. L79
    intro hi
  10. L80
    intro ha
15Fix variables and assumptionsL81–81

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

  1. L81
    intro he
16Use earlier factsL82–91

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

  1. L82
    specialize hw i
  2. L83
    specialize hw a
  3. L84
    specialize hw e
  4. L85
    apply hw
  5. L86
    specialize le_succ (S i)
  6. L87
    specialize le_succ l
  7. L88
    apply le_succ
  8. L89
    exact hi
  9. L90
    exact ha
  10. L91
    exact he
17Use earlier factsL92–94

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

  1. L92
    exact hprod_witness_witness_right_left
  2. L93
    exact hsum_witness_witness_right_left
  3. L94
    exact hp_witness
18Establish hlastL95–103

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

  1. L95
    have hlast : (x2 = 0 /\ (x = 1)) \/ (x2 = 1 /\ (exists pc_le_weight_last_one. pc_le_weight_last_one + (x) = (B)))
  2. L96
    specialize hw l
  3. L97
    specialize hw x
  4. L98
    specialize hw x2
  5. L99
    apply hw
  6. L100
    specialize le_refl (S l)
  7. L101
    apply le_refl
  8. L102
    exact hprod_witness_witness_left
  9. L103
    exact hsum_witness_witness_left
19Separate the logical casesL104–105

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

  1. L104
    cases hlast
  2. L105
    cases hlast_left
20Establish hk0L106–114

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

  1. L106
    have hk0 : k = x3
  2. L107
    trans x3 + x2
  3. L108
    exact hsum_witness_witness_right_right
  4. L109
    rewrite hlast_left_left
  5. L110
    apply PA3
  6. L111
    rewrite hk0 at hQ
  7. L112
    rewrite hk0 at hQ
  8. L113
    rewrite hk0 at hQ
  9. L114
    rewrite hk0 at hQ
21Establish hQ0L115–124

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

  1. L115
    have hQ0 : Q = x4
  2. L116
    specialize pow_functional B
  3. L117
    specialize pow_functional x3
  4. L118
    specialize pow_functional Q
  5. L119
    specialize pow_functional x4
  6. L120
    apply pow_functional
  7. L121
    exact hQ
  8. L122
    exact hp_witness
  9. L123
    rewrite hprod_witness_witness_right_right
  10. L124
    rewrite hQ0
22Calculate and transport equalitiesL125–125

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

  1. L125
    rewrite hlast_left_right
23Establish hmL126–129

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

  1. L126
    have hm : x1 * 1 = x1
  2. L127
    apply mul_one
  3. L128
    rewrite hm
  4. L129
    exact hpre
24Separate the logical casesL130–130

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

  1. L130
    cases hlast_right
25Establish hk1L131–135

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

  1. L131
    have hk1 : k = S x3
  2. L132
    trans x3 + x2
  3. L133
    exact hsum_witness_witness_right_right
  4. L134
    rewrite hlast_right_left
  5. L135
    simp
26Establish hQ1L136–145

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor pair mul.

  1. L136
    have hQ1 : Q = x4 * B
  2. L137
    specialize pow_successor_pair_mul B
  3. L138
    specialize pow_successor_pair_mul x3
  4. L139
    specialize pow_successor_pair_mul k
  5. L140
    specialize pow_successor_pair_mul x4
  6. L141
    specialize pow_successor_pair_mul Q
  7. L142
    apply pow_successor_pair_mul
  8. L143
    exact hk1
  9. L144
    exact hp_witness
  10. L145
    exact hQ
27Calculate and transport equalitiesL146–147

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

  1. L146
    rewrite hprod_witness_witness_right_right
  2. L147
    rewrite hQ1
28Use earlier factsL148–154

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

  1. L148
    specialize mul_le_mul x1
  2. L149
    specialize mul_le_mul x4
  3. L150
    specialize mul_le_mul x
  4. L151
    specialize mul_le_mul B
  5. L152
    apply mul_le_mul
  6. L153
    exact hpre
  7. L154
    exact hlast_right_right

Library-wide reading audit

Original exact command ledger · 154 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro f
  5. 0005intro B
  6. 0006induction l
  7. 0007intro z
  8. 0008intro k
  9. 0009intro Q
  10. 0010intro hw
  11. 0011intro hz
  12. 0012intro hk
  13. 0013intro hQ
  14. 0014have hz1 : z = 1
  15. 0015specialize beta_product_zero b
  16. 0016specialize beta_product_zero c
  17. 0017specialize beta_product_zero z
  18. 0018apply beta_product_zero
  19. 0019exact hz
  20. 0020have hk0 : k = 0
  21. 0021specialize beta_sum_zero d
  22. 0022specialize beta_sum_zero f
  23. 0023specialize beta_sum_zero k
  24. 0024apply beta_sum_zero
  25. 0025exact hk
  26. 0026have hQ1 : Q = 1
  27. 0027specialize pow_zero B
  28. 0028specialize pow_zero k
  29. 0029specialize pow_zero Q
  30. 0030apply pow_zero
  31. 0031exact hk0
  32. 0032exact hQ
  33. 0033rewrite hz1
  34. 0034rewrite hQ1
  35. 0035specialize le_refl 1
  36. 0036apply le_refl
  37. 0037intro z
  38. 0038intro k
  39. 0039intro Q
  40. 0040intro hw
  41. 0041intro hz
  42. 0042intro hk
  43. 0043intro hQ
  44. 0044have hprod : exists a w. (((exists fs_h_pc_weight_last_factor. fs_h_pc_weight_last_factor + S (a) = S ((S (l)) * c)) /\ exists fs_q_pc_weight_last_factor. b = fs_q_pc_weight_last_factor * S ((S (l)) * c) + (a))) /\ ((exists ff_u_pc_weight_previous_product ff_v_pc_weight_previous_product. ((((exists ff_h_pc_weight_previous_product_start. ff_h_pc_weight_previous_product_start + S (1) = S ((S (0)) * ff_v_pc_weight_previous_product)) /\ exists ff_q_pc_weight_previous_product_start. ff_u_pc_weight_previous_product = ff_q_pc_weight_previous_product_start * S ((S (0)) * ff_v_pc_weight_previous_product) + (1))) /\ ((((exists ff_h_pc_weight_previous_product_terminal. ff_h_pc_weight_previous_product_terminal + S (w) = S ((S (l)) * ff_v_pc_weight_previous_product)) /\ exists ff_q_pc_weight_previous_product_terminal. ff_u_pc_weight_previous_product = ff_q_pc_weight_previous_product_terminal * S ((S (l)) * ff_v_pc_weight_previous_product) + (w))) /\ forall ff_i_pc_weight_previous_product. (exists ff_lt_pc_weight_previous_product_bound. ff_lt_pc_weight_previous_product_bound + S ff_i_pc_weight_previous_product = l) -> exists ff_p_pc_weight_previous_product ff_r_pc_weight_previous_product ff_s_pc_weight_previous_product. ((((exists ff_h_pc_weight_previous_product_factor. ff_h_pc_weight_previous_product_factor + S (ff_p_pc_weight_previous_product) = S ((S (ff_i_pc_weight_previous_product)) * c)) /\ exists ff_q_pc_weight_previous_product_factor. b = ff_q_pc_weight_previous_product_factor * S ((S (ff_i_pc_weight_previous_product)) * c) + (ff_p_pc_weight_previous_product))) /\ ((((exists ff_h_pc_weight_previous_product_partial. ff_h_pc_weight_previous_product_partial + S (ff_r_pc_weight_previous_product) = S ((S (ff_i_pc_weight_previous_product)) * ff_v_pc_weight_previous_product)) /\ exists ff_q_pc_weight_previous_product_partial. ff_u_pc_weight_previous_product = ff_q_pc_weight_previous_product_partial * S ((S (ff_i_pc_weight_previous_product)) * ff_v_pc_weight_previous_product) + (ff_r_pc_weight_previous_product))) /\ ((((exists ff_h_pc_weight_previous_product_successor. ff_h_pc_weight_previous_product_successor + S (ff_s_pc_weight_previous_product) = S ((S (S ff_i_pc_weight_previous_product)) * ff_v_pc_weight_previous_product)) /\ exists ff_q_pc_weight_previous_product_successor. ff_u_pc_weight_previous_product = ff_q_pc_weight_previous_product_successor * S ((S (S ff_i_pc_weight_previous_product)) * ff_v_pc_weight_previous_product) + (ff_s_pc_weight_previous_product))) /\ ff_s_pc_weight_previous_product = ff_r_pc_weight_previous_product * ff_p_pc_weight_previous_product)))))) /\ z = w * a)
  45. 0045specialize beta_product_succ_decompose b
  46. 0046specialize beta_product_succ_decompose c
  47. 0047specialize beta_product_succ_decompose l
  48. 0048specialize beta_product_succ_decompose z
  49. 0049apply beta_product_succ_decompose
  50. 0050exact hz
  51. 0051cases hprod
  52. 0052cases hprod_witness
  53. 0053cases hprod_witness_witness
  54. 0054cases hprod_witness_witness_right
  55. 0055have hsum : exists e K. (((exists fs_h_pc_weight_last_bit. fs_h_pc_weight_last_bit + S (e) = S ((S (l)) * f)) /\ exists fs_q_pc_weight_last_bit. d = fs_q_pc_weight_last_bit * S ((S (l)) * f) + (e))) /\ ((exists fs_u_pc_weight_previous_sum fs_v_pc_weight_previous_sum. ((((exists fs_h_pc_weight_previous_sum_body_start. fs_h_pc_weight_previous_sum_body_start + S (0) = S ((S (0)) * fs_v_pc_weight_previous_sum)) /\ exists fs_q_pc_weight_previous_sum_body_start. fs_u_pc_weight_previous_sum = fs_q_pc_weight_previous_sum_body_start * S ((S (0)) * fs_v_pc_weight_previous_sum) + (0))) /\ ((((exists fs_h_pc_weight_previous_sum_body_terminal. fs_h_pc_weight_previous_sum_body_terminal + S (K) = S ((S (l)) * fs_v_pc_weight_previous_sum)) /\ exists fs_q_pc_weight_previous_sum_body_terminal. fs_u_pc_weight_previous_sum = fs_q_pc_weight_previous_sum_body_terminal * S ((S (l)) * fs_v_pc_weight_previous_sum) + (K))) /\ forall fs_i_pc_weight_previous_sum_body_steps. (exists fs_lt_pc_weight_previous_sum_body_steps_bound. fs_lt_pc_weight_previous_sum_body_steps_bound + S fs_i_pc_weight_previous_sum_body_steps = l) -> exists fs_a_pc_weight_previous_sum_body_steps fs_r_pc_weight_previous_sum_body_steps fs_s_pc_weight_previous_sum_body_steps. ((((exists fs_h_pc_weight_previous_sum_body_steps_summand. fs_h_pc_weight_previous_sum_body_steps_summand + S (fs_a_pc_weight_previous_sum_body_steps) = S ((S (fs_i_pc_weight_previous_sum_body_steps)) * f)) /\ exists fs_q_pc_weight_previous_sum_body_steps_summand. d = fs_q_pc_weight_previous_sum_body_steps_summand * S ((S (fs_i_pc_weight_previous_sum_body_steps)) * f) + (fs_a_pc_weight_previous_sum_body_steps))) /\ ((((exists fs_h_pc_weight_previous_sum_body_steps_partial. fs_h_pc_weight_previous_sum_body_steps_partial + S (fs_r_pc_weight_previous_sum_body_steps) = S ((S (fs_i_pc_weight_previous_sum_body_steps)) * fs_v_pc_weight_previous_sum)) /\ exists fs_q_pc_weight_previous_sum_body_steps_partial. fs_u_pc_weight_previous_sum = fs_q_pc_weight_previous_sum_body_steps_partial * S ((S (fs_i_pc_weight_previous_sum_body_steps)) * fs_v_pc_weight_previous_sum) + (fs_r_pc_weight_previous_sum_body_steps))) /\ ((((exists fs_h_pc_weight_previous_sum_body_steps_successor. fs_h_pc_weight_previous_sum_body_steps_successor + S (fs_s_pc_weight_previous_sum_body_steps) = S ((S (S fs_i_pc_weight_previous_sum_body_steps)) * fs_v_pc_weight_previous_sum)) /\ exists fs_q_pc_weight_previous_sum_body_steps_successor. fs_u_pc_weight_previous_sum = fs_q_pc_weight_previous_sum_body_steps_successor * S ((S (S fs_i_pc_weight_previous_sum_body_steps)) * fs_v_pc_weight_previous_sum) + (fs_s_pc_weight_previous_sum_body_steps))) /\ fs_s_pc_weight_previous_sum_body_steps = fs_r_pc_weight_previous_sum_body_steps + fs_a_pc_weight_previous_sum_body_steps)))))) /\ k = K + e)
  56. 0056specialize beta_sum_succ_decompose d
  57. 0057specialize beta_sum_succ_decompose f
  58. 0058specialize beta_sum_succ_decompose l
  59. 0059specialize beta_sum_succ_decompose k
  60. 0060apply beta_sum_succ_decompose
  61. 0061exact hk
  62. 0062cases hsum
  63. 0063cases hsum_witness
  64. 0064cases hsum_witness_witness
  65. 0065cases hsum_witness_witness_right
  66. 0066have hp : exists R. exists pa_b_pc_weight_previous_power pa_c_pc_weight_previous_power. ((forall pa_i_pc_weight_previous_power_repeat. (exists pa_lt_pc_weight_previous_power_repeat_bound. pa_lt_pc_weight_previous_power_repeat_bound + S pa_i_pc_weight_previous_power_repeat = x3) -> (((exists pa_h_pc_weight_previous_power_repeat_decoded. pa_h_pc_weight_previous_power_repeat_decoded + S (B) = S ((S (pa_i_pc_weight_previous_power_repeat)) * pa_c_pc_weight_previous_power)) /\ exists pa_q_pc_weight_previous_power_repeat_decoded. pa_b_pc_weight_previous_power = pa_q_pc_weight_previous_power_repeat_decoded * S ((S (pa_i_pc_weight_previous_power_repeat)) * pa_c_pc_weight_previous_power) + (B)))) /\ (exists pa_u_pc_weight_previous_power_product pa_v_pc_weight_previous_power_product. ((((exists pa_h_pc_weight_previous_power_product_start. pa_h_pc_weight_previous_power_product_start + S (1) = S ((S (0)) * pa_v_pc_weight_previous_power_product)) /\ exists pa_q_pc_weight_previous_power_product_start. pa_u_pc_weight_previous_power_product = pa_q_pc_weight_previous_power_product_start * S ((S (0)) * pa_v_pc_weight_previous_power_product) + (1))) /\ ((((exists pa_h_pc_weight_previous_power_product_terminal. pa_h_pc_weight_previous_power_product_terminal + S (R) = S ((S (x3)) * pa_v_pc_weight_previous_power_product)) /\ exists pa_q_pc_weight_previous_power_product_terminal. pa_u_pc_weight_previous_power_product = pa_q_pc_weight_previous_power_product_terminal * S ((S (x3)) * pa_v_pc_weight_previous_power_product) + (R))) /\ forall pa_i_pc_weight_previous_power_product. (exists pa_lt_pc_weight_previous_power_product_bound. pa_lt_pc_weight_previous_power_product_bound + S pa_i_pc_weight_previous_power_product = x3) -> exists pa_p_pc_weight_previous_power_product pa_r_pc_weight_previous_power_product pa_s_pc_weight_previous_power_product. ((((exists pa_h_pc_weight_previous_power_product_factor. pa_h_pc_weight_previous_power_product_factor + S (pa_p_pc_weight_previous_power_product) = S ((S (pa_i_pc_weight_previous_power_product)) * pa_c_pc_weight_previous_power)) /\ exists pa_q_pc_weight_previous_power_product_factor. pa_b_pc_weight_previous_power = pa_q_pc_weight_previous_power_product_factor * S ((S (pa_i_pc_weight_previous_power_product)) * pa_c_pc_weight_previous_power) + (pa_p_pc_weight_previous_power_product))) /\ ((((exists pa_h_pc_weight_previous_power_product_partial. pa_h_pc_weight_previous_power_product_partial + S (pa_r_pc_weight_previous_power_product) = S ((S (pa_i_pc_weight_previous_power_product)) * pa_v_pc_weight_previous_power_product)) /\ exists pa_q_pc_weight_previous_power_product_partial. pa_u_pc_weight_previous_power_product = pa_q_pc_weight_previous_power_product_partial * S ((S (pa_i_pc_weight_previous_power_product)) * pa_v_pc_weight_previous_power_product) + (pa_r_pc_weight_previous_power_product))) /\ ((((exists pa_h_pc_weight_previous_power_product_successor. pa_h_pc_weight_previous_power_product_successor + S (pa_s_pc_weight_previous_power_product) = S ((S (S pa_i_pc_weight_previous_power_product)) * pa_v_pc_weight_previous_power_product)) /\ exists pa_q_pc_weight_previous_power_product_successor. pa_u_pc_weight_previous_power_product = pa_q_pc_weight_previous_power_product_successor * S ((S (S pa_i_pc_weight_previous_power_product)) * pa_v_pc_weight_previous_power_product) + (pa_s_pc_weight_previous_power_product))) /\ pa_s_pc_weight_previous_power_product = pa_r_pc_weight_previous_power_product * pa_p_pc_weight_previous_power_product)))))))
  67. 0067specialize pow_exists B
  68. 0068specialize pow_exists x3
  69. 0069apply pow_exists
  70. 0070cases hp
  71. 0071have hpre : exists pc_le_weight_previous_bound. pc_le_weight_previous_bound + (x1) = (x4)
  72. 0072specialize IH x1
  73. 0073specialize IH x3
  74. 0074specialize IH x4
  75. 0075apply IH
  76. 0076intro i
  77. 0077intro a
  78. 0078intro e
  79. 0079intro hi
  80. 0080intro ha
  81. 0081intro he
  82. 0082specialize hw i
  83. 0083specialize hw a
  84. 0084specialize hw e
  85. 0085apply hw
  86. 0086specialize le_succ (S i)
  87. 0087specialize le_succ l
  88. 0088apply le_succ
  89. 0089exact hi
  90. 0090exact ha
  91. 0091exact he
  92. 0092exact hprod_witness_witness_right_left
  93. 0093exact hsum_witness_witness_right_left
  94. 0094exact hp_witness
  95. 0095have hlast : (x2 = 0 /\ (x = 1)) \/ (x2 = 1 /\ (exists pc_le_weight_last_one. pc_le_weight_last_one + (x) = (B)))
  96. 0096specialize hw l
  97. 0097specialize hw x
  98. 0098specialize hw x2
  99. 0099apply hw
  100. 0100specialize le_refl (S l)
  101. 0101apply le_refl
  102. 0102exact hprod_witness_witness_left
  103. 0103exact hsum_witness_witness_left
  104. 0104cases hlast
  105. 0105cases hlast_left
  106. 0106have hk0 : k = x3
  107. 0107trans x3 + x2
  108. 0108exact hsum_witness_witness_right_right
  109. 0109rewrite hlast_left_left
  110. 0110apply PA3
  111. 0111rewrite hk0 at hQ
  112. 0112rewrite hk0 at hQ
  113. 0113rewrite hk0 at hQ
  114. 0114rewrite hk0 at hQ
  115. 0115have hQ0 : Q = x4
  116. 0116specialize pow_functional B
  117. 0117specialize pow_functional x3
  118. 0118specialize pow_functional Q
  119. 0119specialize pow_functional x4
  120. 0120apply pow_functional
  121. 0121exact hQ
  122. 0122exact hp_witness
  123. 0123rewrite hprod_witness_witness_right_right
  124. 0124rewrite hQ0
  125. 0125rewrite hlast_left_right
  126. 0126have hm : x1 * 1 = x1
  127. 0127apply mul_one
  128. 0128rewrite hm
  129. 0129exact hpre
  130. 0130cases hlast_right
  131. 0131have hk1 : k = S x3
  132. 0132trans x3 + x2
  133. 0133exact hsum_witness_witness_right_right
  134. 0134rewrite hlast_right_left
  135. 0135simp
  136. 0136have hQ1 : Q = x4 * B
  137. 0137specialize pow_successor_pair_mul B
  138. 0138specialize pow_successor_pair_mul x3
  139. 0139specialize pow_successor_pair_mul k
  140. 0140specialize pow_successor_pair_mul x4
  141. 0141specialize pow_successor_pair_mul Q
  142. 0142apply pow_successor_pair_mul
  143. 0143exact hk1
  144. 0144exact hp_witness
  145. 0145exact hQ
  146. 0146rewrite hprod_witness_witness_right_right
  147. 0147rewrite hQ1
  148. 0148specialize mul_le_mul x1
  149. 0149specialize mul_le_mul x4
  150. 0150specialize mul_le_mul x
  151. 0151specialize mul_le_mul B
  152. 0152apply mul_le_mul
  153. 0153exact hpre
  154. 0154exact hlast_right_right