PA00A0 · theorem

beta_adjacent_target_pairs_product_power

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

Adjacent fixed-target pairs multiply to the corresponding relational power.

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

∀ p. ∀ a. ∀ b. ∀ c. ∀ m. ∀ Q. ∀ A. (∀ x. ∀ y. ∀ z. Lt(x,m) → BetaAt(b,c,x + x,y) → BetaAt(b,c,S (x + x),z) → ModEq(p,y · z,a)) → Product(b,c,m + m,Q) → Pow(a,m,A) → ModEq(p,Q,A)

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 PD0008 ModEq PD0013 BetaAt PD0014 Product PD0020 Pow

7 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt PD0014 Product PD0020 Pow

15 occurrences

Exact expanded native-PA statement
forall p a b c m Q A. (forall wpp_pair_pairs wpp_left_pairs wpp_right_pairs. (exists wpp_gap_pairs_pair_bound. wpp_gap_pairs_pair_bound + S (wpp_pair_pairs) = m) -> (((exists wpp_beta_height_pairs_left_entry. wpp_beta_height_pairs_left_entry + S (wpp_left_pairs) = S ((S ((wpp_pair_pairs + wpp_pair_pairs))) * c)) /\ exists wpp_beta_quotient_pairs_left_entry. b = wpp_beta_quotient_pairs_left_entry * S ((S ((wpp_pair_pairs + wpp_pair_pairs))) * c) + (wpp_left_pairs))) -> (((exists wpp_beta_height_pairs_right_entry. wpp_beta_height_pairs_right_entry + S (wpp_right_pairs) = S ((S (S (wpp_pair_pairs + wpp_pair_pairs))) * c)) /\ exists wpp_beta_quotient_pairs_right_entry. b = wpp_beta_quotient_pairs_right_entry * S ((S (S (wpp_pair_pairs + wpp_pair_pairs))) * c) + (wpp_right_pairs))) -> (exists wpp_mod_left_pairs_pair_mod wpp_mod_right_pairs_pair_mod. (wpp_left_pairs * wpp_right_pairs) + p * wpp_mod_left_pairs_pair_mod = (a) + p * wpp_mod_right_pairs_pair_mod)) -> (exists wpp_trace_code_target_product wpp_trace_scale_target_product. ((((exists wpp_beta_height_target_product_start. wpp_beta_height_target_product_start + S (1) = S ((S (0)) * wpp_trace_scale_target_product)) /\ exists wpp_beta_quotient_target_product_start. wpp_trace_code_target_product = wpp_beta_quotient_target_product_start * S ((S (0)) * wpp_trace_scale_target_product) + (1))) /\ ((((exists wpp_beta_height_target_product_terminal. wpp_beta_height_target_product_terminal + S (Q) = S ((S (m + m)) * wpp_trace_scale_target_product)) /\ exists wpp_beta_quotient_target_product_terminal. wpp_trace_code_target_product = wpp_beta_quotient_target_product_terminal * S ((S (m + m)) * wpp_trace_scale_target_product) + (Q))) /\ forall wpp_index_target_product. (exists wpp_gap_target_product_bound. wpp_gap_target_product_bound + S (wpp_index_target_product) = m + m) -> exists wpp_factor_target_product wpp_prefix_target_product wpp_successor_target_product. ((((exists wpp_beta_height_target_product_factor. wpp_beta_height_target_product_factor + S (wpp_factor_target_product) = S ((S (wpp_index_target_product)) * c)) /\ exists wpp_beta_quotient_target_product_factor. b = wpp_beta_quotient_target_product_factor * S ((S (wpp_index_target_product)) * c) + (wpp_factor_target_product))) /\ ((((exists wpp_beta_height_target_product_prefix. wpp_beta_height_target_product_prefix + S (wpp_prefix_target_product) = S ((S (wpp_index_target_product)) * wpp_trace_scale_target_product)) /\ exists wpp_beta_quotient_target_product_prefix. wpp_trace_code_target_product = wpp_beta_quotient_target_product_prefix * S ((S (wpp_index_target_product)) * wpp_trace_scale_target_product) + (wpp_prefix_target_product))) /\ ((((exists wpp_beta_height_target_product_successor. wpp_beta_height_target_product_successor + S (wpp_successor_target_product) = S ((S (S (wpp_index_target_product))) * wpp_trace_scale_target_product)) /\ exists wpp_beta_quotient_target_product_successor. wpp_trace_code_target_product = wpp_beta_quotient_target_product_successor * S ((S (S (wpp_index_target_product))) * wpp_trace_scale_target_product) + (wpp_successor_target_product))) /\ wpp_successor_target_product = wpp_prefix_target_product * wpp_factor_target_product)))))) -> (exists ff_b_target_power ff_c_target_power. ((forall ff_i_target_power_repeat. (exists ff_lt_target_power_repeat_bound. ff_lt_target_power_repeat_bound + S ff_i_target_power_repeat = m) -> (((exists ff_h_target_power_repeat_decoded. ff_h_target_power_repeat_decoded + S (a) = S ((S (ff_i_target_power_repeat)) * ff_c_target_power)) /\ exists ff_q_target_power_repeat_decoded. ff_b_target_power = ff_q_target_power_repeat_decoded * S ((S (ff_i_target_power_repeat)) * ff_c_target_power) + (a)))) /\ (exists ff_u_target_power_product ff_v_target_power_product. ((((exists ff_h_target_power_product_start. ff_h_target_power_product_start + S (1) = S ((S (0)) * ff_v_target_power_product)) /\ exists ff_q_target_power_product_start. ff_u_target_power_product = ff_q_target_power_product_start * S ((S (0)) * ff_v_target_power_product) + (1))) /\ ((((exists ff_h_target_power_product_terminal. ff_h_target_power_product_terminal + S (A) = S ((S (m)) * ff_v_target_power_product)) /\ exists ff_q_target_power_product_terminal. ff_u_target_power_product = ff_q_target_power_product_terminal * S ((S (m)) * ff_v_target_power_product) + (A))) /\ forall ff_i_target_power_product. (exists ff_lt_target_power_product_bound. ff_lt_target_power_product_bound + S ff_i_target_power_product = m) -> exists ff_p_target_power_product ff_r_target_power_product ff_s_target_power_product. ((((exists ff_h_target_power_product_factor. ff_h_target_power_product_factor + S (ff_p_target_power_product) = S ((S (ff_i_target_power_product)) * ff_c_target_power)) /\ exists ff_q_target_power_product_factor. ff_b_target_power = ff_q_target_power_product_factor * S ((S (ff_i_target_power_product)) * ff_c_target_power) + (ff_p_target_power_product))) /\ ((((exists ff_h_target_power_product_partial. ff_h_target_power_product_partial + S (ff_r_target_power_product) = S ((S (ff_i_target_power_product)) * ff_v_target_power_product)) /\ exists ff_q_target_power_product_partial. ff_u_target_power_product = ff_q_target_power_product_partial * S ((S (ff_i_target_power_product)) * ff_v_target_power_product) + (ff_r_target_power_product))) /\ ((((exists ff_h_target_power_product_successor. ff_h_target_power_product_successor + S (ff_s_target_power_product) = S ((S (S ff_i_target_power_product)) * ff_v_target_power_product)) /\ exists ff_q_target_power_product_successor. ff_u_target_power_product = ff_q_target_power_product_successor * S ((S (S ff_i_target_power_product)) * ff_v_target_power_product) + (ff_s_target_power_product))) /\ ff_s_target_power_product = ff_r_target_power_product * ff_p_target_power_product)))))))) -> (exists wpp_mod_left_target_result wpp_mod_right_target_result. (Q) + p * wpp_mod_left_target_result = (A) + p * wpp_mod_right_target_result)

Proof neighborhood

Direct theorem prerequisites

PA009Y beta_product_double_succ_decompose PA0049 beta_product_zero PA004B pow_zero PA004D pow_successor_decompose PA002O le_succ PA001A le_refl PA0023 mod_eq_refl PA004E mod_eq_mul PA000E add_succ_left PA000B mul_assoc

Direct theorem dependents

PA00BK scaled_pair_order_terminal_power_mod_predecessor

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

118 script commands · 19 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 (9)
beta product double succ decomposebeta product zeropow zeropow successor decomposele succle reflmod eq reflmod eq mulmul assoc
01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
02Induction on mL5–10

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

  1. L5
    induction m
  2. L6
    intro Q
  3. L7
    intro A
  4. L8
    intro hpairs
  5. L9
    intro hproduct
  6. L10
    intro hpower
03Establish hzeroL11–15

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

  1. L11
    have hzero : 0 + 0 = 0
  2. L12
    simp
  3. L13
    rewrite hzero at hproduct
  4. L14
    rewrite hzero at hproduct
  5. L15
    rewrite hzero at hproduct
04Establish hQL16–21

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

  1. L16
    have hQ : Q = 1
  2. L17
    specialize beta_product_zero b
  3. L18
    specialize beta_product_zero c
  4. L19
    specialize beta_product_zero Q
  5. L20
    apply beta_product_zero
  6. L21
    exact hproduct
05Establish hAL22–31

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

  1. L22
    have hA : A = 1
  2. L23
    specialize pow_zero a
  3. L24
    specialize pow_zero 0
  4. L25
    specialize pow_zero A
  5. L26
    apply pow_zero
  6. L27
    refl
  7. L28
    exact hpower
  8. L29
    rewrite hQ
  9. L30
    rewrite hA
  10. L31
    specialize mod_eq_refl p
06Use earlier factsL32–33

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

  1. L32
    specialize mod_eq_refl 1
  2. L33
    exact mod_eq_refl
07Fix variables and assumptionsL34–38

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

  1. L34
    intro Q
  2. L35
    intro A
  3. L36
    intro hpairs
  4. L37
    intro hproduct
  5. L38
    intro hpower
08Establish hdoubleL39–40

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

  1. L39
    have hdouble : S m + S m = S (S (m + m))
  2. L40
    simp [add_succ_left]
09Establish hdecompositionL41–49

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

  1. L41
    have hdecomposition : ∃ wpp_left_factor_target_successor_decomposition. ∃ wpp_right_factor_target_successor_decomposition. ∃ wpp_prefix_product_target_successor_decomposition. BetaAt(b,c,m + m,wpp_left_factor_target_successor_decomposition) ∧ (BetaAt(b,c,S (m + m),wpp_right_factor_target_successor_decomposition) ∧ (Product(b,c,m + m,wpp_prefix_product_target_successor_decomposition) ∧ Q = wpp_prefix_product_target_successor_decomposition · wpp_left_factor_target_successor_decomposition · wpp_right_factor_target_successor_decomposition))Definitions: BetaAt(b,c,m + m,wpp_left_factor_target_successor_decomposition)BetaAt(b,c,S (m + m),wpp_right_factor_target_successor_decomposition)Product(b,c,m + m,wpp_prefix_product_target_successor_decomposition)Original native command in the exact edition
  2. L42
    specialize beta_product_double_succ_decompose b
  3. L43
    specialize beta_product_double_succ_decompose c
  4. L44
    specialize beta_product_double_succ_decompose (m + m)
  5. L45
    specialize beta_product_double_succ_decompose (S m + S m)
  6. L46
    specialize beta_product_double_succ_decompose Q
  7. L47
    apply beta_product_double_succ_decompose
  8. L48
    exact hdouble
  9. L49
    exact hproduct
10Separate the logical casesL50–55

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

  1. L50
    cases hdecomposition
  2. L51
    cases hdecomposition_witness
  3. L52
    cases hdecomposition_witness_witness
  4. L53
    cases hdecomposition_witness_witness_witness
  5. L54
    cases hdecomposition_witness_witness_witness_right
  6. L55
    cases hdecomposition_witness_witness_witness_right_right
11Establish hpairs_allL56–57

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

  1. L56
    have hpairs_all : ∀ wpp_pair_target_all_successor_pairs. ∀ wpp_left_target_all_successor_pairs. ∀ wpp_right_target_all_successor_pairs. Lt(wpp_pair_target_all_successor_pairs,S m) → BetaAt(b,c,wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs,wpp_left_target_all_successor_pairs) → BetaAt(b,c,S (wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs),wpp_right_target_all_successor_pairs) → ModEq(p,wpp_left_target_all_successor_pairs · wpp_right_target_all_successor_pairs,a)Definitions: Lt(wpp_pair_target_all_successor_pairs,S m)BetaAt(b,c,wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs,wpp_left_target_all_successor_pairs)BetaAt(b,c,S (wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs),wpp_right_target_all_successor_pairs)ModEq(p,wpp_left_target_all_successor_pairs · wpp_right_target_all_successor_pairs,a)Original native command in the exact edition
  2. L57
    exact hpairs
12Establish hpairs_prefixL58–67

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

  1. L58
    have hpairs_prefix : ∀ wpp_pair_target_prefix_pairs. ∀ wpp_left_target_prefix_pairs. ∀ wpp_right_target_prefix_pairs. Lt(wpp_pair_target_prefix_pairs,m) → BetaAt(b,c,wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs,wpp_left_target_prefix_pairs) → BetaAt(b,c,S (wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs),wpp_right_target_prefix_pairs) → ModEq(p,wpp_left_target_prefix_pairs · wpp_right_target_prefix_pairs,a)Definitions: Lt(wpp_pair_target_prefix_pairs,m)BetaAt(b,c,wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs,wpp_left_target_prefix_pairs)BetaAt(b,c,S (wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs),wpp_right_target_prefix_pairs)ModEq(p,wpp_left_target_prefix_pairs · wpp_right_target_prefix_pairs,a)Original native command in the exact edition
  2. L59
    intro t
  3. L60
    intro u
  4. L61
    intro v
  5. L62
    intro ht
  6. L63
    intro hu
  7. L64
    intro hv
  8. L65
    specialize hpairs_all t
  9. L66
    specialize hpairs_all u
  10. L67
    specialize hpairs_all v
13Use earlier factsL68–74

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

  1. L68
    apply hpairs_all
  2. L69
    specialize le_succ (S t)
  3. L70
    specialize le_succ m
  4. L71
    apply le_succ
  5. L72
    exact ht
  6. L73
    exact hu
  7. L74
    exact hv
14Establish hpower_stepL75–82

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

  1. L75
    have hpower_step : ∃ r. Pow(a,m,r) ∧ A = r · aDefinitions: Pow(a,m,r)Original native command in the exact edition
  2. L76
    specialize pow_successor_decompose a
  3. L77
    specialize pow_successor_decompose m
  4. L78
    specialize pow_successor_decompose (S m)
  5. L79
    specialize pow_successor_decompose A
  6. L80
    apply pow_successor_decompose
  7. L81
    refl
  8. L82
    exact hpower
15Separate the logical casesL83–84

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

  1. L83
    cases hpower_step
  2. L84
    cases hpower_step_witness
16Establish hprefixL85–91

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

  1. L85
    have hprefix : ModEq(p,x2,x3)Definitions: ModEq(p,x2,x3)Original native command in the exact edition
  2. L86
    specialize IH x2
  3. L87
    specialize IH x3
  4. L88
    apply IH
  5. L89
    exact hpairs_prefix
  6. L90
    exact hdecomposition_witness_witness_witness_right_right_left
  7. L91
    exact hpower_step_witness_left
17Establish hlastL92–100

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

  1. L92
    have hlast : ModEq(p,x · x1,a)Definitions: ModEq(p,x · x1,a)Original native command in the exact edition
  2. L93
    specialize hpairs m
  3. L94
    specialize hpairs x
  4. L95
    specialize hpairs x1
  5. L96
    apply hpairs
  6. L97
    specialize le_refl (S m)
  7. L98
    exact le_refl
  8. L99
    exact hdecomposition_witness_witness_witness_left
  9. L100
    exact hdecomposition_witness_witness_witness_right_left
18Establish hfoldL101–109

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

  1. L101
    have hfold : ModEq(p,x2 · (x · x1),x3 · a)Definitions: ModEq(p,x2 · (x · x1),x3 · a)Original native command in the exact edition
  2. L102
    specialize mod_eq_mul p
  3. L103
    specialize mod_eq_mul x2
  4. L104
    specialize mod_eq_mul x3
  5. L105
    specialize mod_eq_mul (x * x1)
  6. L106
    specialize mod_eq_mul a
  7. L107
    apply mod_eq_mul
  8. L108
    exact hprefix
  9. L109
    exact hlast
19Establish hassocL110–118

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

  1. L110
    have hassoc : (x2 * x) * x1 = x2 * (x * x1)
  2. L111
    specialize mul_assoc x2
  3. L112
    specialize mul_assoc x
  4. L113
    specialize mul_assoc x1
  5. L114
    exact mul_assoc
  6. L115
    rewrite hdecomposition_witness_witness_witness_right_right_right
  7. L116
    rewrite hassoc
  8. L117
    rewrite hpower_step_witness_right
  9. L118
    exact hfold

Library-wide reading audit

Original defined command ledger · 118 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005induction m
  6. 0006intro Q
  7. 0007intro A
  8. 0008intro hpairs
  9. 0009intro hproduct
  10. 0010intro hpower
  11. 0011have hzero : 0 + 0 = 0
  12. 0012simp
  13. 0013rewrite hzero at hproduct
  14. 0014rewrite hzero at hproduct
  15. 0015rewrite hzero at hproduct
  16. 0016have hQ : Q = 1
  17. 0017specialize beta_product_zero b
  18. 0018specialize beta_product_zero c
  19. 0019specialize beta_product_zero Q
  20. 0020apply beta_product_zero
  21. 0021exact hproduct
  22. 0022have hA : A = 1
  23. 0023specialize pow_zero a
  24. 0024specialize pow_zero 0
  25. 0025specialize pow_zero A
  26. 0026apply pow_zero
  27. 0027refl
  28. 0028exact hpower
  29. 0029rewrite hQ
  30. 0030rewrite hA
  31. 0031specialize mod_eq_refl p
  32. 0032specialize mod_eq_refl 1
  33. 0033exact mod_eq_refl
  34. 0034intro Q
  35. 0035intro A
  36. 0036intro hpairs
  37. 0037intro hproduct
  38. 0038intro hpower
  39. 0039have hdouble : S m + S m = S (S (m + m))
  40. 0040simp [add_succ_left]
  41. 0041have hdecomposition : ∃ wpp_left_factor_target_successor_decomposition. ∃ wpp_right_factor_target_successor_decomposition. ∃ wpp_prefix_product_target_successor_decomposition. BetaAt(b,c,m + m,wpp_left_factor_target_successor_decomposition) ∧ (BetaAt(b,c,S (m + m),wpp_right_factor_target_successor_decomposition) ∧ (Product(b,c,m + m,wpp_prefix_product_target_successor_decomposition) ∧ Q = wpp_prefix_product_target_successor_decomposition · wpp_left_factor_target_successor_decomposition · wpp_right_factor_target_successor_decomposition))
    Exact native replay linehave hdecomposition : exists wpp_left_factor_target_successor_decomposition wpp_right_factor_target_successor_decomposition wpp_prefix_product_target_successor_decomposition. (((exists wpp_beta_height_target_successor_decomposition_left_entry. wpp_beta_height_target_successor_decomposition_left_entry + S (wpp_left_factor_target_successor_decomposition) = S ((S (m + m)) * c)) /\ exists wpp_beta_quotient_target_successor_decomposition_left_entry. b = wpp_beta_quotient_target_successor_decomposition_left_entry * S ((S (m + m)) * c) + (wpp_left_factor_target_successor_decomposition))) /\ ((((exists wpp_beta_height_target_successor_decomposition_right_entry. wpp_beta_height_target_successor_decomposition_right_entry + S (wpp_right_factor_target_successor_decomposition) = S ((S (S (m + m))) * c)) /\ exists wpp_beta_quotient_target_successor_decomposition_right_entry. b = wpp_beta_quotient_target_successor_decomposition_right_entry * S ((S (S (m + m))) * c) + (wpp_right_factor_target_successor_decomposition))) /\ ((exists wpp_trace_code_target_successor_decomposition_prefix wpp_trace_scale_target_successor_decomposition_prefix. ((((exists wpp_beta_height_target_successor_decomposition_prefix_start. wpp_beta_height_target_successor_decomposition_prefix_start + S (1) = S ((S (0)) * wpp_trace_scale_target_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_start. wpp_trace_code_target_successor_decomposition_prefix = wpp_beta_quotient_target_successor_decomposition_prefix_start * S ((S (0)) * wpp_trace_scale_target_successor_decomposition_prefix) + (1))) /\ ((((exists wpp_beta_height_target_successor_decomposition_prefix_terminal. wpp_beta_height_target_successor_decomposition_prefix_terminal + S (wpp_prefix_product_target_successor_decomposition) = S ((S (m + m)) * wpp_trace_scale_target_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_terminal. wpp_trace_code_target_successor_decomposition_prefix = wpp_beta_quotient_target_successor_decomposition_prefix_terminal * S ((S (m + m)) * wpp_trace_scale_target_successor_decomposition_prefix) + (wpp_prefix_product_target_successor_decomposition))) /\ forall wpp_index_target_successor_decomposition_prefix. (exists wpp_gap_target_successor_decomposition_prefix_bound. wpp_gap_target_successor_decomposition_prefix_bound + S (wpp_index_target_successor_decomposition_prefix) = m + m) -> exists wpp_factor_target_successor_decomposition_prefix wpp_prefix_target_successor_decomposition_prefix wpp_successor_target_successor_decomposition_prefix. ((((exists wpp_beta_height_target_successor_decomposition_prefix_factor. wpp_beta_height_target_successor_decomposition_prefix_factor + S (wpp_factor_target_successor_decomposition_prefix) = S ((S (wpp_index_target_successor_decomposition_prefix)) * c)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_factor. b = wpp_beta_quotient_target_successor_decomposition_prefix_factor * S ((S (wpp_index_target_successor_decomposition_prefix)) * c) + (wpp_factor_target_successor_decomposition_prefix))) /\ ((((exists wpp_beta_height_target_successor_decomposition_prefix_prefix. wpp_beta_height_target_successor_decomposition_prefix_prefix + S (wpp_prefix_target_successor_decomposition_prefix) = S ((S (wpp_index_target_successor_decomposition_prefix)) * wpp_trace_scale_target_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_prefix. wpp_trace_code_target_successor_decomposition_prefix = wpp_beta_quotient_target_successor_decomposition_prefix_prefix * S ((S (wpp_index_target_successor_decomposition_prefix)) * wpp_trace_scale_target_successor_decomposition_prefix) + (wpp_prefix_target_successor_decomposition_prefix))) /\ ((((exists wpp_beta_height_target_successor_decomposition_prefix_successor. wpp_beta_height_target_successor_decomposition_prefix_successor + S (wpp_successor_target_successor_decomposition_prefix) = S ((S (S (wpp_index_target_successor_decomposition_prefix))) * wpp_trace_scale_target_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_target_successor_decomposition_prefix_successor. wpp_trace_code_target_successor_decomposition_prefix = wpp_beta_quotient_target_successor_decomposition_prefix_successor * S ((S (S (wpp_index_target_successor_decomposition_prefix))) * wpp_trace_scale_target_successor_decomposition_prefix) + (wpp_successor_target_successor_decomposition_prefix))) /\ wpp_successor_target_successor_decomposition_prefix = wpp_prefix_target_successor_decomposition_prefix * wpp_factor_target_successor_decomposition_prefix)))))) /\ Q = (wpp_prefix_product_target_successor_decomposition * wpp_left_factor_target_successor_decomposition) * wpp_right_factor_target_successor_decomposition))
  42. 0042specialize beta_product_double_succ_decompose b
  43. 0043specialize beta_product_double_succ_decompose c
  44. 0044specialize beta_product_double_succ_decompose (m + m)
  45. 0045specialize beta_product_double_succ_decompose (S m + S m)
  46. 0046specialize beta_product_double_succ_decompose Q
  47. 0047apply beta_product_double_succ_decompose
  48. 0048exact hdouble
  49. 0049exact hproduct
  50. 0050cases hdecomposition
  51. 0051cases hdecomposition_witness
  52. 0052cases hdecomposition_witness_witness
  53. 0053cases hdecomposition_witness_witness_witness
  54. 0054cases hdecomposition_witness_witness_witness_right
  55. 0055cases hdecomposition_witness_witness_witness_right_right
  56. 0056have hpairs_all : ∀ wpp_pair_target_all_successor_pairs. ∀ wpp_left_target_all_successor_pairs. ∀ wpp_right_target_all_successor_pairs. Lt(wpp_pair_target_all_successor_pairs,S m) → BetaAt(b,c,wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs,wpp_left_target_all_successor_pairs) → BetaAt(b,c,S (wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs),wpp_right_target_all_successor_pairs) → ModEq(p,wpp_left_target_all_successor_pairs · wpp_right_target_all_successor_pairs,a)
    Exact native replay linehave hpairs_all : forall wpp_pair_target_all_successor_pairs wpp_left_target_all_successor_pairs wpp_right_target_all_successor_pairs. (exists wpp_gap_target_all_successor_pairs_pair_bound. wpp_gap_target_all_successor_pairs_pair_bound + S (wpp_pair_target_all_successor_pairs) = S m) -> (((exists wpp_beta_height_target_all_successor_pairs_left_entry. wpp_beta_height_target_all_successor_pairs_left_entry + S (wpp_left_target_all_successor_pairs) = S ((S ((wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs))) * c)) /\ exists wpp_beta_quotient_target_all_successor_pairs_left_entry. b = wpp_beta_quotient_target_all_successor_pairs_left_entry * S ((S ((wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs))) * c) + (wpp_left_target_all_successor_pairs))) -> (((exists wpp_beta_height_target_all_successor_pairs_right_entry. wpp_beta_height_target_all_successor_pairs_right_entry + S (wpp_right_target_all_successor_pairs) = S ((S (S (wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs))) * c)) /\ exists wpp_beta_quotient_target_all_successor_pairs_right_entry. b = wpp_beta_quotient_target_all_successor_pairs_right_entry * S ((S (S (wpp_pair_target_all_successor_pairs + wpp_pair_target_all_successor_pairs))) * c) + (wpp_right_target_all_successor_pairs))) -> (exists wpp_mod_left_target_all_successor_pairs_pair_mod wpp_mod_right_target_all_successor_pairs_pair_mod. (wpp_left_target_all_successor_pairs * wpp_right_target_all_successor_pairs) + p * wpp_mod_left_target_all_successor_pairs_pair_mod = (a) + p * wpp_mod_right_target_all_successor_pairs_pair_mod)
  57. 0057exact hpairs
  58. 0058have hpairs_prefix : ∀ wpp_pair_target_prefix_pairs. ∀ wpp_left_target_prefix_pairs. ∀ wpp_right_target_prefix_pairs. Lt(wpp_pair_target_prefix_pairs,m) → BetaAt(b,c,wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs,wpp_left_target_prefix_pairs) → BetaAt(b,c,S (wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs),wpp_right_target_prefix_pairs) → ModEq(p,wpp_left_target_prefix_pairs · wpp_right_target_prefix_pairs,a)
    Exact native replay linehave hpairs_prefix : forall wpp_pair_target_prefix_pairs wpp_left_target_prefix_pairs wpp_right_target_prefix_pairs. (exists wpp_gap_target_prefix_pairs_pair_bound. wpp_gap_target_prefix_pairs_pair_bound + S (wpp_pair_target_prefix_pairs) = m) -> (((exists wpp_beta_height_target_prefix_pairs_left_entry. wpp_beta_height_target_prefix_pairs_left_entry + S (wpp_left_target_prefix_pairs) = S ((S ((wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs))) * c)) /\ exists wpp_beta_quotient_target_prefix_pairs_left_entry. b = wpp_beta_quotient_target_prefix_pairs_left_entry * S ((S ((wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs))) * c) + (wpp_left_target_prefix_pairs))) -> (((exists wpp_beta_height_target_prefix_pairs_right_entry. wpp_beta_height_target_prefix_pairs_right_entry + S (wpp_right_target_prefix_pairs) = S ((S (S (wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs))) * c)) /\ exists wpp_beta_quotient_target_prefix_pairs_right_entry. b = wpp_beta_quotient_target_prefix_pairs_right_entry * S ((S (S (wpp_pair_target_prefix_pairs + wpp_pair_target_prefix_pairs))) * c) + (wpp_right_target_prefix_pairs))) -> (exists wpp_mod_left_target_prefix_pairs_pair_mod wpp_mod_right_target_prefix_pairs_pair_mod. (wpp_left_target_prefix_pairs * wpp_right_target_prefix_pairs) + p * wpp_mod_left_target_prefix_pairs_pair_mod = (a) + p * wpp_mod_right_target_prefix_pairs_pair_mod)
  59. 0059intro t
  60. 0060intro u
  61. 0061intro v
  62. 0062intro ht
  63. 0063intro hu
  64. 0064intro hv
  65. 0065specialize hpairs_all t
  66. 0066specialize hpairs_all u
  67. 0067specialize hpairs_all v
  68. 0068apply hpairs_all
  69. 0069specialize le_succ (S t)
  70. 0070specialize le_succ m
  71. 0071apply le_succ
  72. 0072exact ht
  73. 0073exact hu
  74. 0074exact hv
  75. 0075have hpower_step : ∃ r. Pow(a,m,r) ∧ A = r · a
    Exact native replay linehave hpower_step : exists r. (exists ff_b_target_predecessor_power ff_c_target_predecessor_power. ((forall ff_i_target_predecessor_power_repeat. (exists ff_lt_target_predecessor_power_repeat_bound. ff_lt_target_predecessor_power_repeat_bound + S ff_i_target_predecessor_power_repeat = m) -> (((exists ff_h_target_predecessor_power_repeat_decoded. ff_h_target_predecessor_power_repeat_decoded + S (a) = S ((S (ff_i_target_predecessor_power_repeat)) * ff_c_target_predecessor_power)) /\ exists ff_q_target_predecessor_power_repeat_decoded. ff_b_target_predecessor_power = ff_q_target_predecessor_power_repeat_decoded * S ((S (ff_i_target_predecessor_power_repeat)) * ff_c_target_predecessor_power) + (a)))) /\ (exists ff_u_target_predecessor_power_product ff_v_target_predecessor_power_product. ((((exists ff_h_target_predecessor_power_product_start. ff_h_target_predecessor_power_product_start + S (1) = S ((S (0)) * ff_v_target_predecessor_power_product)) /\ exists ff_q_target_predecessor_power_product_start. ff_u_target_predecessor_power_product = ff_q_target_predecessor_power_product_start * S ((S (0)) * ff_v_target_predecessor_power_product) + (1))) /\ ((((exists ff_h_target_predecessor_power_product_terminal. ff_h_target_predecessor_power_product_terminal + S (r) = S ((S (m)) * ff_v_target_predecessor_power_product)) /\ exists ff_q_target_predecessor_power_product_terminal. ff_u_target_predecessor_power_product = ff_q_target_predecessor_power_product_terminal * S ((S (m)) * ff_v_target_predecessor_power_product) + (r))) /\ forall ff_i_target_predecessor_power_product. (exists ff_lt_target_predecessor_power_product_bound. ff_lt_target_predecessor_power_product_bound + S ff_i_target_predecessor_power_product = m) -> exists ff_p_target_predecessor_power_product ff_r_target_predecessor_power_product ff_s_target_predecessor_power_product. ((((exists ff_h_target_predecessor_power_product_factor. ff_h_target_predecessor_power_product_factor + S (ff_p_target_predecessor_power_product) = S ((S (ff_i_target_predecessor_power_product)) * ff_c_target_predecessor_power)) /\ exists ff_q_target_predecessor_power_product_factor. ff_b_target_predecessor_power = ff_q_target_predecessor_power_product_factor * S ((S (ff_i_target_predecessor_power_product)) * ff_c_target_predecessor_power) + (ff_p_target_predecessor_power_product))) /\ ((((exists ff_h_target_predecessor_power_product_partial. ff_h_target_predecessor_power_product_partial + S (ff_r_target_predecessor_power_product) = S ((S (ff_i_target_predecessor_power_product)) * ff_v_target_predecessor_power_product)) /\ exists ff_q_target_predecessor_power_product_partial. ff_u_target_predecessor_power_product = ff_q_target_predecessor_power_product_partial * S ((S (ff_i_target_predecessor_power_product)) * ff_v_target_predecessor_power_product) + (ff_r_target_predecessor_power_product))) /\ ((((exists ff_h_target_predecessor_power_product_successor. ff_h_target_predecessor_power_product_successor + S (ff_s_target_predecessor_power_product) = S ((S (S ff_i_target_predecessor_power_product)) * ff_v_target_predecessor_power_product)) /\ exists ff_q_target_predecessor_power_product_successor. ff_u_target_predecessor_power_product = ff_q_target_predecessor_power_product_successor * S ((S (S ff_i_target_predecessor_power_product)) * ff_v_target_predecessor_power_product) + (ff_s_target_predecessor_power_product))) /\ ff_s_target_predecessor_power_product = ff_r_target_predecessor_power_product * ff_p_target_predecessor_power_product)))))))) /\ A = r * a
  76. 0076specialize pow_successor_decompose a
  77. 0077specialize pow_successor_decompose m
  78. 0078specialize pow_successor_decompose (S m)
  79. 0079specialize pow_successor_decompose A
  80. 0080apply pow_successor_decompose
  81. 0081refl
  82. 0082exact hpower
  83. 0083cases hpower_step
  84. 0084cases hpower_step_witness
  85. 0085have hprefix : ModEq(p,x2,x3)
    Exact native replay linehave hprefix : exists wpp_mod_left_target_prefix_congruence wpp_mod_right_target_prefix_congruence. (x2) + p * wpp_mod_left_target_prefix_congruence = (x3) + p * wpp_mod_right_target_prefix_congruence
  86. 0086specialize IH x2
  87. 0087specialize IH x3
  88. 0088apply IH
  89. 0089exact hpairs_prefix
  90. 0090exact hdecomposition_witness_witness_witness_right_right_left
  91. 0091exact hpower_step_witness_left
  92. 0092have hlast : ModEq(p,x · x1,a)
    Exact native replay linehave hlast : exists wpp_mod_left_target_last_pair_congruence wpp_mod_right_target_last_pair_congruence. (x * x1) + p * wpp_mod_left_target_last_pair_congruence = (a) + p * wpp_mod_right_target_last_pair_congruence
  93. 0093specialize hpairs m
  94. 0094specialize hpairs x
  95. 0095specialize hpairs x1
  96. 0096apply hpairs
  97. 0097specialize le_refl (S m)
  98. 0098exact le_refl
  99. 0099exact hdecomposition_witness_witness_witness_left
  100. 0100exact hdecomposition_witness_witness_witness_right_left
  101. 0101have hfold : ModEq(p,x2 · (x · x1),x3 · a)
    Exact native replay linehave hfold : exists wpp_mod_left_target_folded_congruence wpp_mod_right_target_folded_congruence. (x2 * (x * x1)) + p * wpp_mod_left_target_folded_congruence = (x3 * a) + p * wpp_mod_right_target_folded_congruence
  102. 0102specialize mod_eq_mul p
  103. 0103specialize mod_eq_mul x2
  104. 0104specialize mod_eq_mul x3
  105. 0105specialize mod_eq_mul (x * x1)
  106. 0106specialize mod_eq_mul a
  107. 0107apply mod_eq_mul
  108. 0108exact hprefix
  109. 0109exact hlast
  110. 0110have hassoc : (x2 * x) * x1 = x2 * (x * x1)
  111. 0111specialize mul_assoc x2
  112. 0112specialize mul_assoc x
  113. 0113specialize mul_assoc x1
  114. 0114exact mul_assoc
  115. 0115rewrite hdecomposition_witness_witness_witness_right_right_right
  116. 0116rewrite hassoc
  117. 0117rewrite hpower_step_witness_right
  118. 0118exact hfold