BT00SM · Bertrand theorem

pow_mul_exp_from_total

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Iterated powers multiply exponents using a supplied totality proof.

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

∀ a. ∀ e. ∀ f. ∀ p. ∀ x. ∀ y. ∀ z. (∀ n. ∀ m. ∃ k. Pow(n,m,k)) → p = e · f → Pow(a,e,x) → Pow(x,f,y) → Pow(a,p,z) → y = z

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0020 Pow

4 occurrences

In local proof propositions

PD0020 Pow

2 occurrences

Exact expanded native-PA statement
forall a e f p x y z. (forall bpt_a_mul_exp bpt_e_mul_exp. exists bpt_x_mul_exp. (exists ff_b_bpt_value_mul_exp ff_c_bpt_value_mul_exp. ((forall ff_i_bpt_value_mul_exp_repeat. (exists ff_lt_bpt_value_mul_exp_repeat_bound. ff_lt_bpt_value_mul_exp_repeat_bound + S ff_i_bpt_value_mul_exp_repeat = bpt_e_mul_exp) -> (((exists ff_h_bpt_value_mul_exp_repeat_decoded. ff_h_bpt_value_mul_exp_repeat_decoded + S (bpt_a_mul_exp) = S ((S (ff_i_bpt_value_mul_exp_repeat)) * ff_c_bpt_value_mul_exp)) /\ exists ff_q_bpt_value_mul_exp_repeat_decoded. ff_b_bpt_value_mul_exp = ff_q_bpt_value_mul_exp_repeat_decoded * S ((S (ff_i_bpt_value_mul_exp_repeat)) * ff_c_bpt_value_mul_exp) + (bpt_a_mul_exp)))) /\ (exists ff_u_bpt_value_mul_exp_product ff_v_bpt_value_mul_exp_product. ((((exists ff_h_bpt_value_mul_exp_product_start. ff_h_bpt_value_mul_exp_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_mul_exp_product)) /\ exists ff_q_bpt_value_mul_exp_product_start. ff_u_bpt_value_mul_exp_product = ff_q_bpt_value_mul_exp_product_start * S ((S (0)) * ff_v_bpt_value_mul_exp_product) + (1))) /\ ((((exists ff_h_bpt_value_mul_exp_product_terminal. ff_h_bpt_value_mul_exp_product_terminal + S (bpt_x_mul_exp) = S ((S (bpt_e_mul_exp)) * ff_v_bpt_value_mul_exp_product)) /\ exists ff_q_bpt_value_mul_exp_product_terminal. ff_u_bpt_value_mul_exp_product = ff_q_bpt_value_mul_exp_product_terminal * S ((S (bpt_e_mul_exp)) * ff_v_bpt_value_mul_exp_product) + (bpt_x_mul_exp))) /\ forall ff_i_bpt_value_mul_exp_product. (exists ff_lt_bpt_value_mul_exp_product_bound. ff_lt_bpt_value_mul_exp_product_bound + S ff_i_bpt_value_mul_exp_product = bpt_e_mul_exp) -> exists ff_p_bpt_value_mul_exp_product ff_r_bpt_value_mul_exp_product ff_s_bpt_value_mul_exp_product. ((((exists ff_h_bpt_value_mul_exp_product_factor. ff_h_bpt_value_mul_exp_product_factor + S (ff_p_bpt_value_mul_exp_product) = S ((S (ff_i_bpt_value_mul_exp_product)) * ff_c_bpt_value_mul_exp)) /\ exists ff_q_bpt_value_mul_exp_product_factor. ff_b_bpt_value_mul_exp = ff_q_bpt_value_mul_exp_product_factor * S ((S (ff_i_bpt_value_mul_exp_product)) * ff_c_bpt_value_mul_exp) + (ff_p_bpt_value_mul_exp_product))) /\ ((((exists ff_h_bpt_value_mul_exp_product_partial. ff_h_bpt_value_mul_exp_product_partial + S (ff_r_bpt_value_mul_exp_product) = S ((S (ff_i_bpt_value_mul_exp_product)) * ff_v_bpt_value_mul_exp_product)) /\ exists ff_q_bpt_value_mul_exp_product_partial. ff_u_bpt_value_mul_exp_product = ff_q_bpt_value_mul_exp_product_partial * S ((S (ff_i_bpt_value_mul_exp_product)) * ff_v_bpt_value_mul_exp_product) + (ff_r_bpt_value_mul_exp_product))) /\ ((((exists ff_h_bpt_value_mul_exp_product_successor. ff_h_bpt_value_mul_exp_product_successor + S (ff_s_bpt_value_mul_exp_product) = S ((S (S ff_i_bpt_value_mul_exp_product)) * ff_v_bpt_value_mul_exp_product)) /\ exists ff_q_bpt_value_mul_exp_product_successor. ff_u_bpt_value_mul_exp_product = ff_q_bpt_value_mul_exp_product_successor * S ((S (S ff_i_bpt_value_mul_exp_product)) * ff_v_bpt_value_mul_exp_product) + (ff_s_bpt_value_mul_exp_product))) /\ ff_s_bpt_value_mul_exp_product = ff_r_bpt_value_mul_exp_product * ff_p_bpt_value_mul_exp_product))))))))) -> p = e * f -> (exists ff_b_bpt_mul_base ff_c_bpt_mul_base. ((forall ff_i_bpt_mul_base_repeat. (exists ff_lt_bpt_mul_base_repeat_bound. ff_lt_bpt_mul_base_repeat_bound + S ff_i_bpt_mul_base_repeat = e) -> (((exists ff_h_bpt_mul_base_repeat_decoded. ff_h_bpt_mul_base_repeat_decoded + S (a) = S ((S (ff_i_bpt_mul_base_repeat)) * ff_c_bpt_mul_base)) /\ exists ff_q_bpt_mul_base_repeat_decoded. ff_b_bpt_mul_base = ff_q_bpt_mul_base_repeat_decoded * S ((S (ff_i_bpt_mul_base_repeat)) * ff_c_bpt_mul_base) + (a)))) /\ (exists ff_u_bpt_mul_base_product ff_v_bpt_mul_base_product. ((((exists ff_h_bpt_mul_base_product_start. ff_h_bpt_mul_base_product_start + S (1) = S ((S (0)) * ff_v_bpt_mul_base_product)) /\ exists ff_q_bpt_mul_base_product_start. ff_u_bpt_mul_base_product = ff_q_bpt_mul_base_product_start * S ((S (0)) * ff_v_bpt_mul_base_product) + (1))) /\ ((((exists ff_h_bpt_mul_base_product_terminal. ff_h_bpt_mul_base_product_terminal + S (x) = S ((S (e)) * ff_v_bpt_mul_base_product)) /\ exists ff_q_bpt_mul_base_product_terminal. ff_u_bpt_mul_base_product = ff_q_bpt_mul_base_product_terminal * S ((S (e)) * ff_v_bpt_mul_base_product) + (x))) /\ forall ff_i_bpt_mul_base_product. (exists ff_lt_bpt_mul_base_product_bound. ff_lt_bpt_mul_base_product_bound + S ff_i_bpt_mul_base_product = e) -> exists ff_p_bpt_mul_base_product ff_r_bpt_mul_base_product ff_s_bpt_mul_base_product. ((((exists ff_h_bpt_mul_base_product_factor. ff_h_bpt_mul_base_product_factor + S (ff_p_bpt_mul_base_product) = S ((S (ff_i_bpt_mul_base_product)) * ff_c_bpt_mul_base)) /\ exists ff_q_bpt_mul_base_product_factor. ff_b_bpt_mul_base = ff_q_bpt_mul_base_product_factor * S ((S (ff_i_bpt_mul_base_product)) * ff_c_bpt_mul_base) + (ff_p_bpt_mul_base_product))) /\ ((((exists ff_h_bpt_mul_base_product_partial. ff_h_bpt_mul_base_product_partial + S (ff_r_bpt_mul_base_product) = S ((S (ff_i_bpt_mul_base_product)) * ff_v_bpt_mul_base_product)) /\ exists ff_q_bpt_mul_base_product_partial. ff_u_bpt_mul_base_product = ff_q_bpt_mul_base_product_partial * S ((S (ff_i_bpt_mul_base_product)) * ff_v_bpt_mul_base_product) + (ff_r_bpt_mul_base_product))) /\ ((((exists ff_h_bpt_mul_base_product_successor. ff_h_bpt_mul_base_product_successor + S (ff_s_bpt_mul_base_product) = S ((S (S ff_i_bpt_mul_base_product)) * ff_v_bpt_mul_base_product)) /\ exists ff_q_bpt_mul_base_product_successor. ff_u_bpt_mul_base_product = ff_q_bpt_mul_base_product_successor * S ((S (S ff_i_bpt_mul_base_product)) * ff_v_bpt_mul_base_product) + (ff_s_bpt_mul_base_product))) /\ ff_s_bpt_mul_base_product = ff_r_bpt_mul_base_product * ff_p_bpt_mul_base_product)))))))) -> (exists ff_b_bpt_mul_outer ff_c_bpt_mul_outer. ((forall ff_i_bpt_mul_outer_repeat. (exists ff_lt_bpt_mul_outer_repeat_bound. ff_lt_bpt_mul_outer_repeat_bound + S ff_i_bpt_mul_outer_repeat = f) -> (((exists ff_h_bpt_mul_outer_repeat_decoded. ff_h_bpt_mul_outer_repeat_decoded + S (x) = S ((S (ff_i_bpt_mul_outer_repeat)) * ff_c_bpt_mul_outer)) /\ exists ff_q_bpt_mul_outer_repeat_decoded. ff_b_bpt_mul_outer = ff_q_bpt_mul_outer_repeat_decoded * S ((S (ff_i_bpt_mul_outer_repeat)) * ff_c_bpt_mul_outer) + (x)))) /\ (exists ff_u_bpt_mul_outer_product ff_v_bpt_mul_outer_product. ((((exists ff_h_bpt_mul_outer_product_start. ff_h_bpt_mul_outer_product_start + S (1) = S ((S (0)) * ff_v_bpt_mul_outer_product)) /\ exists ff_q_bpt_mul_outer_product_start. ff_u_bpt_mul_outer_product = ff_q_bpt_mul_outer_product_start * S ((S (0)) * ff_v_bpt_mul_outer_product) + (1))) /\ ((((exists ff_h_bpt_mul_outer_product_terminal. ff_h_bpt_mul_outer_product_terminal + S (y) = S ((S (f)) * ff_v_bpt_mul_outer_product)) /\ exists ff_q_bpt_mul_outer_product_terminal. ff_u_bpt_mul_outer_product = ff_q_bpt_mul_outer_product_terminal * S ((S (f)) * ff_v_bpt_mul_outer_product) + (y))) /\ forall ff_i_bpt_mul_outer_product. (exists ff_lt_bpt_mul_outer_product_bound. ff_lt_bpt_mul_outer_product_bound + S ff_i_bpt_mul_outer_product = f) -> exists ff_p_bpt_mul_outer_product ff_r_bpt_mul_outer_product ff_s_bpt_mul_outer_product. ((((exists ff_h_bpt_mul_outer_product_factor. ff_h_bpt_mul_outer_product_factor + S (ff_p_bpt_mul_outer_product) = S ((S (ff_i_bpt_mul_outer_product)) * ff_c_bpt_mul_outer)) /\ exists ff_q_bpt_mul_outer_product_factor. ff_b_bpt_mul_outer = ff_q_bpt_mul_outer_product_factor * S ((S (ff_i_bpt_mul_outer_product)) * ff_c_bpt_mul_outer) + (ff_p_bpt_mul_outer_product))) /\ ((((exists ff_h_bpt_mul_outer_product_partial. ff_h_bpt_mul_outer_product_partial + S (ff_r_bpt_mul_outer_product) = S ((S (ff_i_bpt_mul_outer_product)) * ff_v_bpt_mul_outer_product)) /\ exists ff_q_bpt_mul_outer_product_partial. ff_u_bpt_mul_outer_product = ff_q_bpt_mul_outer_product_partial * S ((S (ff_i_bpt_mul_outer_product)) * ff_v_bpt_mul_outer_product) + (ff_r_bpt_mul_outer_product))) /\ ((((exists ff_h_bpt_mul_outer_product_successor. ff_h_bpt_mul_outer_product_successor + S (ff_s_bpt_mul_outer_product) = S ((S (S ff_i_bpt_mul_outer_product)) * ff_v_bpt_mul_outer_product)) /\ exists ff_q_bpt_mul_outer_product_successor. ff_u_bpt_mul_outer_product = ff_q_bpt_mul_outer_product_successor * S ((S (S ff_i_bpt_mul_outer_product)) * ff_v_bpt_mul_outer_product) + (ff_s_bpt_mul_outer_product))) /\ ff_s_bpt_mul_outer_product = ff_r_bpt_mul_outer_product * ff_p_bpt_mul_outer_product)))))))) -> (exists ff_b_bpt_mul_total ff_c_bpt_mul_total. ((forall ff_i_bpt_mul_total_repeat. (exists ff_lt_bpt_mul_total_repeat_bound. ff_lt_bpt_mul_total_repeat_bound + S ff_i_bpt_mul_total_repeat = p) -> (((exists ff_h_bpt_mul_total_repeat_decoded. ff_h_bpt_mul_total_repeat_decoded + S (a) = S ((S (ff_i_bpt_mul_total_repeat)) * ff_c_bpt_mul_total)) /\ exists ff_q_bpt_mul_total_repeat_decoded. ff_b_bpt_mul_total = ff_q_bpt_mul_total_repeat_decoded * S ((S (ff_i_bpt_mul_total_repeat)) * ff_c_bpt_mul_total) + (a)))) /\ (exists ff_u_bpt_mul_total_product ff_v_bpt_mul_total_product. ((((exists ff_h_bpt_mul_total_product_start. ff_h_bpt_mul_total_product_start + S (1) = S ((S (0)) * ff_v_bpt_mul_total_product)) /\ exists ff_q_bpt_mul_total_product_start. ff_u_bpt_mul_total_product = ff_q_bpt_mul_total_product_start * S ((S (0)) * ff_v_bpt_mul_total_product) + (1))) /\ ((((exists ff_h_bpt_mul_total_product_terminal. ff_h_bpt_mul_total_product_terminal + S (z) = S ((S (p)) * ff_v_bpt_mul_total_product)) /\ exists ff_q_bpt_mul_total_product_terminal. ff_u_bpt_mul_total_product = ff_q_bpt_mul_total_product_terminal * S ((S (p)) * ff_v_bpt_mul_total_product) + (z))) /\ forall ff_i_bpt_mul_total_product. (exists ff_lt_bpt_mul_total_product_bound. ff_lt_bpt_mul_total_product_bound + S ff_i_bpt_mul_total_product = p) -> exists ff_p_bpt_mul_total_product ff_r_bpt_mul_total_product ff_s_bpt_mul_total_product. ((((exists ff_h_bpt_mul_total_product_factor. ff_h_bpt_mul_total_product_factor + S (ff_p_bpt_mul_total_product) = S ((S (ff_i_bpt_mul_total_product)) * ff_c_bpt_mul_total)) /\ exists ff_q_bpt_mul_total_product_factor. ff_b_bpt_mul_total = ff_q_bpt_mul_total_product_factor * S ((S (ff_i_bpt_mul_total_product)) * ff_c_bpt_mul_total) + (ff_p_bpt_mul_total_product))) /\ ((((exists ff_h_bpt_mul_total_product_partial. ff_h_bpt_mul_total_product_partial + S (ff_r_bpt_mul_total_product) = S ((S (ff_i_bpt_mul_total_product)) * ff_v_bpt_mul_total_product)) /\ exists ff_q_bpt_mul_total_product_partial. ff_u_bpt_mul_total_product = ff_q_bpt_mul_total_product_partial * S ((S (ff_i_bpt_mul_total_product)) * ff_v_bpt_mul_total_product) + (ff_r_bpt_mul_total_product))) /\ ((((exists ff_h_bpt_mul_total_product_successor. ff_h_bpt_mul_total_product_successor + S (ff_s_bpt_mul_total_product) = S ((S (S ff_i_bpt_mul_total_product)) * ff_v_bpt_mul_total_product)) /\ exists ff_q_bpt_mul_total_product_successor. ff_u_bpt_mul_total_product = ff_q_bpt_mul_total_product_successor * S ((S (S ff_i_bpt_mul_total_product)) * ff_v_bpt_mul_total_product) + (ff_s_bpt_mul_total_product))) /\ ff_s_bpt_mul_total_product = ff_r_bpt_mul_total_product * ff_p_bpt_mul_total_product)))))))) -> y = z

Proof neighborhood

Direct theorem prerequisites

BT0081 pow_zero BT0083 pow_successor_decompose BT009X pow_add

Direct theorem dependents

BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00W3 pow_block_bound_from_total BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WI pow_two_double_eq_pow_four_from_total BT00WO pow_thirty_six_double_block_eq_pow_six_four_block_from_total BT00X4 bertrand_floor_power_product_le_h_from_total

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

95 script commands · 22 reading checkpoints · 7 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 (3)
pow zeropow successor decomposepow add
01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro e
02Induction on fL3–12

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

  1. L3
    induction f
  2. L4
    intro p
  3. L5
    intro x
  4. L6
    intro y
  5. L7
    intro z
  6. L8
    intro htotal
  7. L9
    intro hp
  8. L10
    intro hx
  9. L11
    intro hy
  10. L12
    intro hz
03Calculate and transport equalitiesL13–17

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

  1. L13
    rewrite PA5 at hp
  2. L14
    rewrite hp at hz
  3. L15
    rewrite hp at hz
  4. L16
    rewrite hp at hz
  5. L17
    rewrite hp at hz
04Establish hy1L18–24

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

  1. L18
    have hy1 : y = 1
  2. L19
    specialize pow_zero x
  3. L20
    specialize pow_zero 0
  4. L21
    specialize pow_zero y
  5. L22
    apply pow_zero
  6. L23
    refl
  7. L24
    exact hy
05Establish hz1L25–34

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

  1. L25
    have hz1 : z = 1
  2. L26
    specialize pow_zero a
  3. L27
    specialize pow_zero 0
  4. L28
    specialize pow_zero z
  5. L29
    apply pow_zero
  6. L30
    refl
  7. L31
    exact hz
  8. L32
    trans 1
  9. L33
    exact hy1
  10. L34
    symm
06Use earlier factsL35–35

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

  1. L35
    exact hz1
07Fix variables and assumptionsL36–44

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

  1. L36
    intro p
  2. L37
    intro x
  3. L38
    intro y
  4. L39
    intro z
  5. L40
    intro htotal
  6. L41
    intro hp
  7. L42
    intro hx
  8. L43
    intro hy
  9. L44
    intro hz
08Establish hy_stepL45–52

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

  1. L45
    have hy_step : ∃ r. Pow(x,f,r) ∧ y = r · xDefinitions: Pow(x,f,r)Original native command in the exact edition
  2. L46
    specialize pow_successor_decompose x
  3. L47
    specialize pow_successor_decompose f
  4. L48
    specialize pow_successor_decompose (S f)
  5. L49
    specialize pow_successor_decompose y
  6. L50
    apply pow_successor_decompose
  7. L51
    refl
  8. L52
    exact hy
09Separate the logical casesL53–54

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

  1. L53
    cases hy_step
  2. L54
    cases hy_step_witness
10Establish hqpowL55–58

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

  1. L55
    have hqpow : ∃ r. Pow(a,e · f,r)Definitions: Pow(a,e · f,r)Original native command in the exact edition
  2. L56
    specialize htotal a
  3. L57
    specialize htotal (e * f)
  4. L58
    exact htotal
11Separate the logical casesL59–59

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

  1. L59
    cases hqpow
12Establish hprefixL60–69

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

  1. L60
    have hprefix : x1 = x2
  2. L61
    specialize IH (e * f)
  3. L62
    specialize IH x
  4. L63
    specialize IH x1
  5. L64
    specialize IH x2
  6. L65
    apply IH
  7. L66
    exact htotal
  8. L67
    refl
  9. L68
    exact hx
  10. L69
    exact hy_step_witness_left
13Use earlier factsL70–70

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

  1. L70
    exact hqpow_witness
14Establish hpsumL71–74

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

  1. L71
    have hpsum : p = (e * f) + e
  2. L72
    trans e * S f
  3. L73
    exact hp
  4. L74
    apply PA6
15Establish hproductL75–84

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

  1. L75
    have hproduct : z = x2 * x
  2. L76
    specialize pow_add a
  3. L77
    specialize pow_add (e * f)
  4. L78
    specialize pow_add e
  5. L79
    specialize pow_add p
  6. L80
    specialize pow_add x2
  7. L81
    specialize pow_add x
  8. L82
    specialize pow_add z
  9. L83
    apply pow_add
  10. L84
    exact hpsum
16Use earlier factsL85–87

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

  1. L85
    exact hqpow_witness
  2. L86
    exact hx
  3. L87
    exact hz
17Calculate and transport equalitiesL88–88

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

  1. L88
    trans x1 * x
18Use earlier factsL89–89

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

  1. L89
    exact hy_step_witness_right
19Calculate and transport equalitiesL90–91

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

  1. L90
    trans x2 * x
  2. L91
    congr
20Use earlier factsL92–92

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

  1. L92
    exact hprefix
21Calculate and transport equalitiesL93–94

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

  1. L93
    refl
  2. L94
    symm
22Use earlier factsL95–95

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

  1. L95
    exact hproduct

Library-wide reading audit

Original defined command ledger · 95 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003induction f
  4. 0004intro p
  5. 0005intro x
  6. 0006intro y
  7. 0007intro z
  8. 0008intro htotal
  9. 0009intro hp
  10. 0010intro hx
  11. 0011intro hy
  12. 0012intro hz
  13. 0013rewrite PA5 at hp
  14. 0014rewrite hp at hz
  15. 0015rewrite hp at hz
  16. 0016rewrite hp at hz
  17. 0017rewrite hp at hz
  18. 0018have hy1 : y = 1
  19. 0019specialize pow_zero x
  20. 0020specialize pow_zero 0
  21. 0021specialize pow_zero y
  22. 0022apply pow_zero
  23. 0023refl
  24. 0024exact hy
  25. 0025have hz1 : z = 1
  26. 0026specialize pow_zero a
  27. 0027specialize pow_zero 0
  28. 0028specialize pow_zero z
  29. 0029apply pow_zero
  30. 0030refl
  31. 0031exact hz
  32. 0032trans 1
  33. 0033exact hy1
  34. 0034symm
  35. 0035exact hz1
  36. 0036intro p
  37. 0037intro x
  38. 0038intro y
  39. 0039intro z
  40. 0040intro htotal
  41. 0041intro hp
  42. 0042intro hx
  43. 0043intro hy
  44. 0044intro hz
  45. 0045have hy_step : ∃ r. Pow(x,f,r) ∧ y = r · x
    Exact native replay linehave hy_step : exists r. (exists ff_b_bpt_mul_y_prefix ff_c_bpt_mul_y_prefix. ((forall ff_i_bpt_mul_y_prefix_repeat. (exists ff_lt_bpt_mul_y_prefix_repeat_bound. ff_lt_bpt_mul_y_prefix_repeat_bound + S ff_i_bpt_mul_y_prefix_repeat = f) -> (((exists ff_h_bpt_mul_y_prefix_repeat_decoded. ff_h_bpt_mul_y_prefix_repeat_decoded + S (x) = S ((S (ff_i_bpt_mul_y_prefix_repeat)) * ff_c_bpt_mul_y_prefix)) /\ exists ff_q_bpt_mul_y_prefix_repeat_decoded. ff_b_bpt_mul_y_prefix = ff_q_bpt_mul_y_prefix_repeat_decoded * S ((S (ff_i_bpt_mul_y_prefix_repeat)) * ff_c_bpt_mul_y_prefix) + (x)))) /\ (exists ff_u_bpt_mul_y_prefix_product ff_v_bpt_mul_y_prefix_product. ((((exists ff_h_bpt_mul_y_prefix_product_start. ff_h_bpt_mul_y_prefix_product_start + S (1) = S ((S (0)) * ff_v_bpt_mul_y_prefix_product)) /\ exists ff_q_bpt_mul_y_prefix_product_start. ff_u_bpt_mul_y_prefix_product = ff_q_bpt_mul_y_prefix_product_start * S ((S (0)) * ff_v_bpt_mul_y_prefix_product) + (1))) /\ ((((exists ff_h_bpt_mul_y_prefix_product_terminal. ff_h_bpt_mul_y_prefix_product_terminal + S (r) = S ((S (f)) * ff_v_bpt_mul_y_prefix_product)) /\ exists ff_q_bpt_mul_y_prefix_product_terminal. ff_u_bpt_mul_y_prefix_product = ff_q_bpt_mul_y_prefix_product_terminal * S ((S (f)) * ff_v_bpt_mul_y_prefix_product) + (r))) /\ forall ff_i_bpt_mul_y_prefix_product. (exists ff_lt_bpt_mul_y_prefix_product_bound. ff_lt_bpt_mul_y_prefix_product_bound + S ff_i_bpt_mul_y_prefix_product = f) -> exists ff_p_bpt_mul_y_prefix_product ff_r_bpt_mul_y_prefix_product ff_s_bpt_mul_y_prefix_product. ((((exists ff_h_bpt_mul_y_prefix_product_factor. ff_h_bpt_mul_y_prefix_product_factor + S (ff_p_bpt_mul_y_prefix_product) = S ((S (ff_i_bpt_mul_y_prefix_product)) * ff_c_bpt_mul_y_prefix)) /\ exists ff_q_bpt_mul_y_prefix_product_factor. ff_b_bpt_mul_y_prefix = ff_q_bpt_mul_y_prefix_product_factor * S ((S (ff_i_bpt_mul_y_prefix_product)) * ff_c_bpt_mul_y_prefix) + (ff_p_bpt_mul_y_prefix_product))) /\ ((((exists ff_h_bpt_mul_y_prefix_product_partial. ff_h_bpt_mul_y_prefix_product_partial + S (ff_r_bpt_mul_y_prefix_product) = S ((S (ff_i_bpt_mul_y_prefix_product)) * ff_v_bpt_mul_y_prefix_product)) /\ exists ff_q_bpt_mul_y_prefix_product_partial. ff_u_bpt_mul_y_prefix_product = ff_q_bpt_mul_y_prefix_product_partial * S ((S (ff_i_bpt_mul_y_prefix_product)) * ff_v_bpt_mul_y_prefix_product) + (ff_r_bpt_mul_y_prefix_product))) /\ ((((exists ff_h_bpt_mul_y_prefix_product_successor. ff_h_bpt_mul_y_prefix_product_successor + S (ff_s_bpt_mul_y_prefix_product) = S ((S (S ff_i_bpt_mul_y_prefix_product)) * ff_v_bpt_mul_y_prefix_product)) /\ exists ff_q_bpt_mul_y_prefix_product_successor. ff_u_bpt_mul_y_prefix_product = ff_q_bpt_mul_y_prefix_product_successor * S ((S (S ff_i_bpt_mul_y_prefix_product)) * ff_v_bpt_mul_y_prefix_product) + (ff_s_bpt_mul_y_prefix_product))) /\ ff_s_bpt_mul_y_prefix_product = ff_r_bpt_mul_y_prefix_product * ff_p_bpt_mul_y_prefix_product)))))))) /\ y = r * x
  46. 0046specialize pow_successor_decompose x
  47. 0047specialize pow_successor_decompose f
  48. 0048specialize pow_successor_decompose (S f)
  49. 0049specialize pow_successor_decompose y
  50. 0050apply pow_successor_decompose
  51. 0051refl
  52. 0052exact hy
  53. 0053cases hy_step
  54. 0054cases hy_step_witness
  55. 0055have hqpow : ∃ r. Pow(a,e · f,r)
    Exact native replay linehave hqpow : exists r. (exists pa_b_bpt_mul_total_prefix pa_c_bpt_mul_total_prefix. ((forall pa_i_bpt_mul_total_prefix_repeat. (exists pa_lt_bpt_mul_total_prefix_repeat_bound. pa_lt_bpt_mul_total_prefix_repeat_bound + S pa_i_bpt_mul_total_prefix_repeat = e * f) -> (((exists pa_h_bpt_mul_total_prefix_repeat_decoded. pa_h_bpt_mul_total_prefix_repeat_decoded + S (a) = S ((S (pa_i_bpt_mul_total_prefix_repeat)) * pa_c_bpt_mul_total_prefix)) /\ exists pa_q_bpt_mul_total_prefix_repeat_decoded. pa_b_bpt_mul_total_prefix = pa_q_bpt_mul_total_prefix_repeat_decoded * S ((S (pa_i_bpt_mul_total_prefix_repeat)) * pa_c_bpt_mul_total_prefix) + (a)))) /\ (exists pa_u_bpt_mul_total_prefix_product pa_v_bpt_mul_total_prefix_product. ((((exists pa_h_bpt_mul_total_prefix_product_start. pa_h_bpt_mul_total_prefix_product_start + S (1) = S ((S (0)) * pa_v_bpt_mul_total_prefix_product)) /\ exists pa_q_bpt_mul_total_prefix_product_start. pa_u_bpt_mul_total_prefix_product = pa_q_bpt_mul_total_prefix_product_start * S ((S (0)) * pa_v_bpt_mul_total_prefix_product) + (1))) /\ ((((exists pa_h_bpt_mul_total_prefix_product_terminal. pa_h_bpt_mul_total_prefix_product_terminal + S (r) = S ((S (e * f)) * pa_v_bpt_mul_total_prefix_product)) /\ exists pa_q_bpt_mul_total_prefix_product_terminal. pa_u_bpt_mul_total_prefix_product = pa_q_bpt_mul_total_prefix_product_terminal * S ((S (e * f)) * pa_v_bpt_mul_total_prefix_product) + (r))) /\ forall pa_i_bpt_mul_total_prefix_product. (exists pa_lt_bpt_mul_total_prefix_product_bound. pa_lt_bpt_mul_total_prefix_product_bound + S pa_i_bpt_mul_total_prefix_product = e * f) -> exists pa_p_bpt_mul_total_prefix_product pa_r_bpt_mul_total_prefix_product pa_s_bpt_mul_total_prefix_product. ((((exists pa_h_bpt_mul_total_prefix_product_factor. pa_h_bpt_mul_total_prefix_product_factor + S (pa_p_bpt_mul_total_prefix_product) = S ((S (pa_i_bpt_mul_total_prefix_product)) * pa_c_bpt_mul_total_prefix)) /\ exists pa_q_bpt_mul_total_prefix_product_factor. pa_b_bpt_mul_total_prefix = pa_q_bpt_mul_total_prefix_product_factor * S ((S (pa_i_bpt_mul_total_prefix_product)) * pa_c_bpt_mul_total_prefix) + (pa_p_bpt_mul_total_prefix_product))) /\ ((((exists pa_h_bpt_mul_total_prefix_product_partial. pa_h_bpt_mul_total_prefix_product_partial + S (pa_r_bpt_mul_total_prefix_product) = S ((S (pa_i_bpt_mul_total_prefix_product)) * pa_v_bpt_mul_total_prefix_product)) /\ exists pa_q_bpt_mul_total_prefix_product_partial. pa_u_bpt_mul_total_prefix_product = pa_q_bpt_mul_total_prefix_product_partial * S ((S (pa_i_bpt_mul_total_prefix_product)) * pa_v_bpt_mul_total_prefix_product) + (pa_r_bpt_mul_total_prefix_product))) /\ ((((exists pa_h_bpt_mul_total_prefix_product_successor. pa_h_bpt_mul_total_prefix_product_successor + S (pa_s_bpt_mul_total_prefix_product) = S ((S (S pa_i_bpt_mul_total_prefix_product)) * pa_v_bpt_mul_total_prefix_product)) /\ exists pa_q_bpt_mul_total_prefix_product_successor. pa_u_bpt_mul_total_prefix_product = pa_q_bpt_mul_total_prefix_product_successor * S ((S (S pa_i_bpt_mul_total_prefix_product)) * pa_v_bpt_mul_total_prefix_product) + (pa_s_bpt_mul_total_prefix_product))) /\ pa_s_bpt_mul_total_prefix_product = pa_r_bpt_mul_total_prefix_product * pa_p_bpt_mul_total_prefix_product))))))))
  56. 0056specialize htotal a
  57. 0057specialize htotal (e * f)
  58. 0058exact htotal
  59. 0059cases hqpow
  60. 0060have hprefix : x1 = x2
  61. 0061specialize IH (e * f)
  62. 0062specialize IH x
  63. 0063specialize IH x1
  64. 0064specialize IH x2
  65. 0065apply IH
  66. 0066exact htotal
  67. 0067refl
  68. 0068exact hx
  69. 0069exact hy_step_witness_left
  70. 0070exact hqpow_witness
  71. 0071have hpsum : p = (e * f) + e
  72. 0072trans e * S f
  73. 0073exact hp
  74. 0074apply PA6
  75. 0075have hproduct : z = x2 * x
  76. 0076specialize pow_add a
  77. 0077specialize pow_add (e * f)
  78. 0078specialize pow_add e
  79. 0079specialize pow_add p
  80. 0080specialize pow_add x2
  81. 0081specialize pow_add x
  82. 0082specialize pow_add z
  83. 0083apply pow_add
  84. 0084exact hpsum
  85. 0085exact hqpow_witness
  86. 0086exact hx
  87. 0087exact hz
  88. 0088trans x1 * x
  89. 0089exact hy_step_witness_right
  90. 0090trans x2 * x
  91. 0091congr
  92. 0092exact hprefix
  93. 0093refl
  94. 0094symm
  95. 0095exact hproduct