BT00UQ · Bertrand theorem

beta_product_prefix_suffix_split

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

Split a finite Product into an initial prefix and an aligned suffix.

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

∀ b. ∀ c. ∀ z. ∀ d. ∀ l. ∀ m. ∀ n. (∀ x. ∀ y. Lt(x,m) → BetaAt(b,c,l + x,y) → BetaAt(z,d,x,y)) → Product(b,c,l + m,n) → ∃ x. ∃ y. Product(b,c,l,x) ∧ (Product(z,d,m,y) ∧ n = x · y)

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

PD0002 Lt PD0013 BetaAt PD0014 Product

6 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0014 Product

8 occurrences

Exact expanded native-PA statement
forall b c z d l m n. (forall i a. (exists fps_bound_bps_split_shift. fps_bound_bps_split_shift + S i = m) -> (((exists fps_height_bps_split_shift_source. fps_height_bps_split_shift_source + S (a) = S ((S (l + i)) * c)) /\ exists fps_quotient_bps_split_shift_source. b = fps_quotient_bps_split_shift_source * S ((S (l + i)) * c) + (a))) -> (((exists fps_height_bps_split_shift_suffix. fps_height_bps_split_shift_suffix + S (a) = S ((S (i)) * d)) /\ exists fps_quotient_bps_split_shift_suffix. z = fps_quotient_bps_split_shift_suffix * S ((S (i)) * d) + (a)))) -> (exists fps_accumulator_bps_split_total fps_scale_bps_split_total. ((((exists fps_height_bps_split_total_start. fps_height_bps_split_total_start + S (1) = S ((S (0)) * fps_scale_bps_split_total)) /\ exists fps_quotient_bps_split_total_start. fps_accumulator_bps_split_total = fps_quotient_bps_split_total_start * S ((S (0)) * fps_scale_bps_split_total) + (1))) /\ ((((exists fps_height_bps_split_total_terminal. fps_height_bps_split_total_terminal + S (n) = S ((S (l + m)) * fps_scale_bps_split_total)) /\ exists fps_quotient_bps_split_total_terminal. fps_accumulator_bps_split_total = fps_quotient_bps_split_total_terminal * S ((S (l + m)) * fps_scale_bps_split_total) + (n))) /\ forall fps_index_bps_split_total. (exists fps_gap_bps_split_total_bound. fps_gap_bps_split_total_bound + S fps_index_bps_split_total = l + m) -> exists fps_factor_bps_split_total fps_partial_bps_split_total fps_successor_bps_split_total. ((((exists fps_height_bps_split_total_factor. fps_height_bps_split_total_factor + S (fps_factor_bps_split_total) = S ((S (fps_index_bps_split_total)) * c)) /\ exists fps_quotient_bps_split_total_factor. b = fps_quotient_bps_split_total_factor * S ((S (fps_index_bps_split_total)) * c) + (fps_factor_bps_split_total))) /\ ((((exists fps_height_bps_split_total_partial. fps_height_bps_split_total_partial + S (fps_partial_bps_split_total) = S ((S (fps_index_bps_split_total)) * fps_scale_bps_split_total)) /\ exists fps_quotient_bps_split_total_partial. fps_accumulator_bps_split_total = fps_quotient_bps_split_total_partial * S ((S (fps_index_bps_split_total)) * fps_scale_bps_split_total) + (fps_partial_bps_split_total))) /\ ((((exists fps_height_bps_split_total_successor. fps_height_bps_split_total_successor + S (fps_successor_bps_split_total) = S ((S (S fps_index_bps_split_total)) * fps_scale_bps_split_total)) /\ exists fps_quotient_bps_split_total_successor. fps_accumulator_bps_split_total = fps_quotient_bps_split_total_successor * S ((S (S fps_index_bps_split_total)) * fps_scale_bps_split_total) + (fps_successor_bps_split_total))) /\ fps_successor_bps_split_total = fps_partial_bps_split_total * fps_factor_bps_split_total)))))) -> exists p q. (exists ff_u_bps_split_prefix ff_v_bps_split_prefix. ((((exists ff_h_bps_split_prefix_start. ff_h_bps_split_prefix_start + S (1) = S ((S (0)) * ff_v_bps_split_prefix)) /\ exists ff_q_bps_split_prefix_start. ff_u_bps_split_prefix = ff_q_bps_split_prefix_start * S ((S (0)) * ff_v_bps_split_prefix) + (1))) /\ ((((exists ff_h_bps_split_prefix_terminal. ff_h_bps_split_prefix_terminal + S (p) = S ((S (l)) * ff_v_bps_split_prefix)) /\ exists ff_q_bps_split_prefix_terminal. ff_u_bps_split_prefix = ff_q_bps_split_prefix_terminal * S ((S (l)) * ff_v_bps_split_prefix) + (p))) /\ forall ff_i_bps_split_prefix. (exists ff_lt_bps_split_prefix_bound. ff_lt_bps_split_prefix_bound + S ff_i_bps_split_prefix = l) -> exists ff_p_bps_split_prefix ff_r_bps_split_prefix ff_s_bps_split_prefix. ((((exists ff_h_bps_split_prefix_factor. ff_h_bps_split_prefix_factor + S (ff_p_bps_split_prefix) = S ((S (ff_i_bps_split_prefix)) * c)) /\ exists ff_q_bps_split_prefix_factor. b = ff_q_bps_split_prefix_factor * S ((S (ff_i_bps_split_prefix)) * c) + (ff_p_bps_split_prefix))) /\ ((((exists ff_h_bps_split_prefix_partial. ff_h_bps_split_prefix_partial + S (ff_r_bps_split_prefix) = S ((S (ff_i_bps_split_prefix)) * ff_v_bps_split_prefix)) /\ exists ff_q_bps_split_prefix_partial. ff_u_bps_split_prefix = ff_q_bps_split_prefix_partial * S ((S (ff_i_bps_split_prefix)) * ff_v_bps_split_prefix) + (ff_r_bps_split_prefix))) /\ ((((exists ff_h_bps_split_prefix_successor. ff_h_bps_split_prefix_successor + S (ff_s_bps_split_prefix) = S ((S (S ff_i_bps_split_prefix)) * ff_v_bps_split_prefix)) /\ exists ff_q_bps_split_prefix_successor. ff_u_bps_split_prefix = ff_q_bps_split_prefix_successor * S ((S (S ff_i_bps_split_prefix)) * ff_v_bps_split_prefix) + (ff_s_bps_split_prefix))) /\ ff_s_bps_split_prefix = ff_r_bps_split_prefix * ff_p_bps_split_prefix)))))) /\ ((exists ff_u_bps_split_suffix ff_v_bps_split_suffix. ((((exists ff_h_bps_split_suffix_start. ff_h_bps_split_suffix_start + S (1) = S ((S (0)) * ff_v_bps_split_suffix)) /\ exists ff_q_bps_split_suffix_start. ff_u_bps_split_suffix = ff_q_bps_split_suffix_start * S ((S (0)) * ff_v_bps_split_suffix) + (1))) /\ ((((exists ff_h_bps_split_suffix_terminal. ff_h_bps_split_suffix_terminal + S (q) = S ((S (m)) * ff_v_bps_split_suffix)) /\ exists ff_q_bps_split_suffix_terminal. ff_u_bps_split_suffix = ff_q_bps_split_suffix_terminal * S ((S (m)) * ff_v_bps_split_suffix) + (q))) /\ forall ff_i_bps_split_suffix. (exists ff_lt_bps_split_suffix_bound. ff_lt_bps_split_suffix_bound + S ff_i_bps_split_suffix = m) -> exists ff_p_bps_split_suffix ff_r_bps_split_suffix ff_s_bps_split_suffix. ((((exists ff_h_bps_split_suffix_factor. ff_h_bps_split_suffix_factor + S (ff_p_bps_split_suffix) = S ((S (ff_i_bps_split_suffix)) * d)) /\ exists ff_q_bps_split_suffix_factor. z = ff_q_bps_split_suffix_factor * S ((S (ff_i_bps_split_suffix)) * d) + (ff_p_bps_split_suffix))) /\ ((((exists ff_h_bps_split_suffix_partial. ff_h_bps_split_suffix_partial + S (ff_r_bps_split_suffix) = S ((S (ff_i_bps_split_suffix)) * ff_v_bps_split_suffix)) /\ exists ff_q_bps_split_suffix_partial. ff_u_bps_split_suffix = ff_q_bps_split_suffix_partial * S ((S (ff_i_bps_split_suffix)) * ff_v_bps_split_suffix) + (ff_r_bps_split_suffix))) /\ ((((exists ff_h_bps_split_suffix_successor. ff_h_bps_split_suffix_successor + S (ff_s_bps_split_suffix) = S ((S (S ff_i_bps_split_suffix)) * ff_v_bps_split_suffix)) /\ exists ff_q_bps_split_suffix_successor. ff_u_bps_split_suffix = ff_q_bps_split_suffix_successor * S ((S (S ff_i_bps_split_suffix)) * ff_v_bps_split_suffix) + (ff_s_bps_split_suffix))) /\ ff_s_bps_split_suffix = ff_r_bps_split_suffix * ff_p_bps_split_suffix)))))) /\ n = p * q)

Proof neighborhood

Direct theorem prerequisites

BT005F beta_product_exists BT005I beta_product_zero BT005J beta_product_succ_decompose BT005K beta_product_succ_append BT0018 le_succ BT000E le_refl BT000A mul_one BT0008 mul_assoc

Direct theorem dependents

BT00UY primorial_prefix_interval_split BT010R prime_contribution_prefix_interval_split

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

107 script commands · 32 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 (8)
beta product existsbeta product zerobeta product succ decomposebeta product succ appendle succle reflmul onemul assoc
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 z
  4. L4
    intro d
  5. L5
    intro l
02Induction on mL6–12

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

  1. L6
    induction m
  2. L7
    intro n
  3. L8
    intro hshift
  4. L9
    intro htotal
  5. L10
    specialize beta_product_exists z
  6. L11
    specialize beta_product_exists d
  7. L12
    specialize beta_product_exists 0
03Separate the logical casesL13–15

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

  1. L13
    cases beta_product_exists
  2. L14
    cases beta_product_exists_witness
  3. L15
    cases beta_product_exists_witness_witness
04Establish hqoneL16–20

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

  1. L16
    have hqone : x = 1
  2. L17
    specialize beta_product_zero z
  3. L18
    specialize beta_product_zero d
  4. L19
    specialize beta_product_zero x
  5. L20
    apply beta_product_zero
05Construct an explicit witnessL21–22

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

  1. L21
    exists x1
  2. L22
    exists x2
06Use earlier factsL23–23

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

  1. L23
    exact beta_product_exists_witness_witness_witness
07Construct an explicit witnessL24–25

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

  1. L24
    exists n
  2. L25
    exists x
08Separate the logical casesL26–26

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

  1. L26
    split
09Establish hbaseL27–32

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

  1. L27
    have hbase : l + 0 = l
  2. L28
    apply PA3
  3. L29
    rewrite hbase at htotal
  4. L30
    rewrite hbase at htotal
  5. L31
    rewrite hbase at htotal
  6. L32
    exact htotal
10Separate the logical casesL33–33

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

  1. L33
    split
11Construct an explicit witnessL34–35

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

  1. L34
    exists x1
  2. L35
    exists x2
12Use earlier factsL36–36

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

  1. L36
    exact beta_product_exists_witness_witness_witness
13Calculate and transport equalitiesL37–37

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

  1. L37
    rewrite hqone
14Use earlier factsL38–38

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

  1. L38
    specialize mul_one n
15Calculate and transport equalitiesL39–39

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

  1. L39
    symm
16Use earlier factsL40–40

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

  1. L40
    exact mul_one
17Fix variables and assumptionsL41–43

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

  1. L41
    intro n
  2. L42
    intro hshift
  3. L43
    intro htotal
18Establish hlengthL44–48

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

  1. L44
    have hlength : l + S m = S (l + m)
  2. L45
    apply PA4
  3. L46
    rewrite hlength at htotal
  4. L47
    rewrite hlength at htotal
  5. L48
    rewrite hlength at htotal
19Establish hdecompositionL49–55

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

  1. L49
    have hdecomposition : ∃ a. ∃ r. BetaAt(b,c,l + m,a) ∧ (Product(b,c,l + m,r) ∧ n = r · a)Definitions: BetaAt(b,c,l + m,a)Product(b,c,l + m,r)Original native command in the exact edition
  2. L50
    specialize beta_product_succ_decompose b
  3. L51
    specialize beta_product_succ_decompose c
  4. L52
    specialize beta_product_succ_decompose (l + m)
  5. L53
    specialize beta_product_succ_decompose n
  6. L54
    apply beta_product_succ_decompose
  7. L55
    exact htotal
20Separate the logical casesL56–59

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

  1. L56
    cases hdecomposition
  2. L57
    cases hdecomposition_witness
  3. L58
    cases hdecomposition_witness_witness
  4. L59
    cases hdecomposition_witness_witness_right
21Establish hprefix_shiftL60–69

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

  1. L60
    have hprefix_shift : ∀ i. ∀ a. Lt(i,m) → BetaAt(b,c,l + i,a) → BetaAt(z,d,i,a)Definitions: Lt(i,m)BetaAt(b,c,l + i,a)BetaAt(z,d,i,a)Original native command in the exact edition
  2. L61
    intro i
  3. L62
    intro a
  4. L63
    intro hi
  5. L64
    intro ha
  6. L65
    specialize hshift i
  7. L66
    specialize hshift a
  8. L67
    apply hshift
  9. L68
    specialize le_succ (S i)
  10. L69
    specialize le_succ m
22Use earlier factsL70–72

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

  1. L70
    apply le_succ
  2. L71
    exact hi
  3. L72
    exact ha
23Establish hrecursiveL73–77

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

  1. L73
    have hrecursive : ∃ p. ∃ q. Product(b,c,l,p) ∧ (Product(z,d,m,q) ∧ x1 = p · q)Definitions: Product(b,c,l,p)Product(z,d,m,q)Original native command in the exact edition
  2. L74
    specialize IH x1
  3. L75
    apply IH
  4. L76
    exact hprefix_shift
  5. L77
    exact hdecomposition_witness_witness_right_left
24Separate the logical casesL78–81

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

  1. L78
    cases hrecursive
  2. L79
    cases hrecursive_witness
  3. L80
    cases hrecursive_witness_witness
  4. L81
    cases hrecursive_witness_witness_right
25Establish hsuffix_lastL82–88

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

  1. L82
    have hsuffix_last : BetaAt(z,d,m,x)Definitions: BetaAt(z,d,m,x)Original native command in the exact edition
  2. L83
    specialize hshift m
  3. L84
    specialize hshift x
  4. L85
    apply hshift
  5. L86
    specialize le_refl (S m)
  6. L87
    exact le_refl
  7. L88
    exact hdecomposition_witness_witness_left
26Construct an explicit witnessL89–90

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

  1. L89
    exists x2
  2. L90
    exists x3 * x
27Separate the logical casesL91–91

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

  1. L91
    split
28Use earlier factsL92–92

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

  1. L92
    exact hrecursive_witness_witness_left
29Separate the logical casesL93–93

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

  1. L93
    split
30Use earlier factsL94–101

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

  1. L94
    specialize beta_product_succ_append z
  2. L95
    specialize beta_product_succ_append d
  3. L96
    specialize beta_product_succ_append m
  4. L97
    specialize beta_product_succ_append x3
  5. L98
    specialize beta_product_succ_append x
  6. L99
    apply beta_product_succ_append
  7. L100
    exact hrecursive_witness_witness_right_left
  8. L101
    exact hsuffix_last
31Calculate and transport equalitiesL102–103

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

  1. L102
    rewrite hdecomposition_witness_witness_right_right
  2. L103
    rewrite hrecursive_witness_witness_right_right
32Use earlier factsL104–107

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

  1. L104
    specialize mul_assoc x2
  2. L105
    specialize mul_assoc x3
  3. L106
    specialize mul_assoc x
  4. L107
    exact mul_assoc

Library-wide reading audit

Original defined command ledger · 107 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro l
  6. 0006induction m
  7. 0007intro n
  8. 0008intro hshift
  9. 0009intro htotal
  10. 0010specialize beta_product_exists z
  11. 0011specialize beta_product_exists d
  12. 0012specialize beta_product_exists 0
  13. 0013cases beta_product_exists
  14. 0014cases beta_product_exists_witness
  15. 0015cases beta_product_exists_witness_witness
  16. 0016have hqone : x = 1
  17. 0017specialize beta_product_zero z
  18. 0018specialize beta_product_zero d
  19. 0019specialize beta_product_zero x
  20. 0020apply beta_product_zero
  21. 0021exists x1
  22. 0022exists x2
  23. 0023exact beta_product_exists_witness_witness_witness
  24. 0024exists n
  25. 0025exists x
  26. 0026split
  27. 0027have hbase : l + 0 = l
  28. 0028apply PA3
  29. 0029rewrite hbase at htotal
  30. 0030rewrite hbase at htotal
  31. 0031rewrite hbase at htotal
  32. 0032exact htotal
  33. 0033split
  34. 0034exists x1
  35. 0035exists x2
  36. 0036exact beta_product_exists_witness_witness_witness
  37. 0037rewrite hqone
  38. 0038specialize mul_one n
  39. 0039symm
  40. 0040exact mul_one
  41. 0041intro n
  42. 0042intro hshift
  43. 0043intro htotal
  44. 0044have hlength : l + S m = S (l + m)
  45. 0045apply PA4
  46. 0046rewrite hlength at htotal
  47. 0047rewrite hlength at htotal
  48. 0048rewrite hlength at htotal
  49. 0049have hdecomposition : ∃ a. ∃ r. BetaAt(b,c,l + m,a) ∧ (Product(b,c,l + m,r) ∧ n = r · a)
    Exact native replay linehave hdecomposition : exists a r. (((exists fps_height_bps_split_last. fps_height_bps_split_last + S (a) = S ((S (l + m)) * c)) /\ exists fps_quotient_bps_split_last. b = fps_quotient_bps_split_last * S ((S (l + m)) * c) + (a))) /\ ((exists fps_accumulator_bps_split_previous_total fps_scale_bps_split_previous_total. ((((exists fps_height_bps_split_previous_total_start. fps_height_bps_split_previous_total_start + S (1) = S ((S (0)) * fps_scale_bps_split_previous_total)) /\ exists fps_quotient_bps_split_previous_total_start. fps_accumulator_bps_split_previous_total = fps_quotient_bps_split_previous_total_start * S ((S (0)) * fps_scale_bps_split_previous_total) + (1))) /\ ((((exists fps_height_bps_split_previous_total_terminal. fps_height_bps_split_previous_total_terminal + S (r) = S ((S (l + m)) * fps_scale_bps_split_previous_total)) /\ exists fps_quotient_bps_split_previous_total_terminal. fps_accumulator_bps_split_previous_total = fps_quotient_bps_split_previous_total_terminal * S ((S (l + m)) * fps_scale_bps_split_previous_total) + (r))) /\ forall fps_index_bps_split_previous_total. (exists fps_gap_bps_split_previous_total_bound. fps_gap_bps_split_previous_total_bound + S fps_index_bps_split_previous_total = l + m) -> exists fps_factor_bps_split_previous_total fps_partial_bps_split_previous_total fps_successor_bps_split_previous_total. ((((exists fps_height_bps_split_previous_total_factor. fps_height_bps_split_previous_total_factor + S (fps_factor_bps_split_previous_total) = S ((S (fps_index_bps_split_previous_total)) * c)) /\ exists fps_quotient_bps_split_previous_total_factor. b = fps_quotient_bps_split_previous_total_factor * S ((S (fps_index_bps_split_previous_total)) * c) + (fps_factor_bps_split_previous_total))) /\ ((((exists fps_height_bps_split_previous_total_partial. fps_height_bps_split_previous_total_partial + S (fps_partial_bps_split_previous_total) = S ((S (fps_index_bps_split_previous_total)) * fps_scale_bps_split_previous_total)) /\ exists fps_quotient_bps_split_previous_total_partial. fps_accumulator_bps_split_previous_total = fps_quotient_bps_split_previous_total_partial * S ((S (fps_index_bps_split_previous_total)) * fps_scale_bps_split_previous_total) + (fps_partial_bps_split_previous_total))) /\ ((((exists fps_height_bps_split_previous_total_successor. fps_height_bps_split_previous_total_successor + S (fps_successor_bps_split_previous_total) = S ((S (S fps_index_bps_split_previous_total)) * fps_scale_bps_split_previous_total)) /\ exists fps_quotient_bps_split_previous_total_successor. fps_accumulator_bps_split_previous_total = fps_quotient_bps_split_previous_total_successor * S ((S (S fps_index_bps_split_previous_total)) * fps_scale_bps_split_previous_total) + (fps_successor_bps_split_previous_total))) /\ fps_successor_bps_split_previous_total = fps_partial_bps_split_previous_total * fps_factor_bps_split_previous_total)))))) /\ n = r * a)
  50. 0050specialize beta_product_succ_decompose b
  51. 0051specialize beta_product_succ_decompose c
  52. 0052specialize beta_product_succ_decompose (l + m)
  53. 0053specialize beta_product_succ_decompose n
  54. 0054apply beta_product_succ_decompose
  55. 0055exact htotal
  56. 0056cases hdecomposition
  57. 0057cases hdecomposition_witness
  58. 0058cases hdecomposition_witness_witness
  59. 0059cases hdecomposition_witness_witness_right
  60. 0060have hprefix_shift : ∀ i. ∀ a. Lt(i,m) → BetaAt(b,c,l + i,a) → BetaAt(z,d,i,a)
    Exact native replay linehave hprefix_shift : forall i a. (exists fps_bound_bps_split_previous_shift. fps_bound_bps_split_previous_shift + S i = m) -> (((exists fps_height_bps_split_previous_shift_source. fps_height_bps_split_previous_shift_source + S (a) = S ((S (l + i)) * c)) /\ exists fps_quotient_bps_split_previous_shift_source. b = fps_quotient_bps_split_previous_shift_source * S ((S (l + i)) * c) + (a))) -> (((exists fps_height_bps_split_previous_shift_suffix. fps_height_bps_split_previous_shift_suffix + S (a) = S ((S (i)) * d)) /\ exists fps_quotient_bps_split_previous_shift_suffix. z = fps_quotient_bps_split_previous_shift_suffix * S ((S (i)) * d) + (a)))
  61. 0061intro i
  62. 0062intro a
  63. 0063intro hi
  64. 0064intro ha
  65. 0065specialize hshift i
  66. 0066specialize hshift a
  67. 0067apply hshift
  68. 0068specialize le_succ (S i)
  69. 0069specialize le_succ m
  70. 0070apply le_succ
  71. 0071exact hi
  72. 0072exact ha
  73. 0073have hrecursive : ∃ p. ∃ q. Product(b,c,l,p) ∧ (Product(z,d,m,q) ∧ x1 = p · q)
    Exact native replay linehave hrecursive : exists p q. (exists ff_u_bps_split_recursive_prefix ff_v_bps_split_recursive_prefix. ((((exists ff_h_bps_split_recursive_prefix_start. ff_h_bps_split_recursive_prefix_start + S (1) = S ((S (0)) * ff_v_bps_split_recursive_prefix)) /\ exists ff_q_bps_split_recursive_prefix_start. ff_u_bps_split_recursive_prefix = ff_q_bps_split_recursive_prefix_start * S ((S (0)) * ff_v_bps_split_recursive_prefix) + (1))) /\ ((((exists ff_h_bps_split_recursive_prefix_terminal. ff_h_bps_split_recursive_prefix_terminal + S (p) = S ((S (l)) * ff_v_bps_split_recursive_prefix)) /\ exists ff_q_bps_split_recursive_prefix_terminal. ff_u_bps_split_recursive_prefix = ff_q_bps_split_recursive_prefix_terminal * S ((S (l)) * ff_v_bps_split_recursive_prefix) + (p))) /\ forall ff_i_bps_split_recursive_prefix. (exists ff_lt_bps_split_recursive_prefix_bound. ff_lt_bps_split_recursive_prefix_bound + S ff_i_bps_split_recursive_prefix = l) -> exists ff_p_bps_split_recursive_prefix ff_r_bps_split_recursive_prefix ff_s_bps_split_recursive_prefix. ((((exists ff_h_bps_split_recursive_prefix_factor. ff_h_bps_split_recursive_prefix_factor + S (ff_p_bps_split_recursive_prefix) = S ((S (ff_i_bps_split_recursive_prefix)) * c)) /\ exists ff_q_bps_split_recursive_prefix_factor. b = ff_q_bps_split_recursive_prefix_factor * S ((S (ff_i_bps_split_recursive_prefix)) * c) + (ff_p_bps_split_recursive_prefix))) /\ ((((exists ff_h_bps_split_recursive_prefix_partial. ff_h_bps_split_recursive_prefix_partial + S (ff_r_bps_split_recursive_prefix) = S ((S (ff_i_bps_split_recursive_prefix)) * ff_v_bps_split_recursive_prefix)) /\ exists ff_q_bps_split_recursive_prefix_partial. ff_u_bps_split_recursive_prefix = ff_q_bps_split_recursive_prefix_partial * S ((S (ff_i_bps_split_recursive_prefix)) * ff_v_bps_split_recursive_prefix) + (ff_r_bps_split_recursive_prefix))) /\ ((((exists ff_h_bps_split_recursive_prefix_successor. ff_h_bps_split_recursive_prefix_successor + S (ff_s_bps_split_recursive_prefix) = S ((S (S ff_i_bps_split_recursive_prefix)) * ff_v_bps_split_recursive_prefix)) /\ exists ff_q_bps_split_recursive_prefix_successor. ff_u_bps_split_recursive_prefix = ff_q_bps_split_recursive_prefix_successor * S ((S (S ff_i_bps_split_recursive_prefix)) * ff_v_bps_split_recursive_prefix) + (ff_s_bps_split_recursive_prefix))) /\ ff_s_bps_split_recursive_prefix = ff_r_bps_split_recursive_prefix * ff_p_bps_split_recursive_prefix)))))) /\ ((exists ff_u_bps_split_recursive_suffix ff_v_bps_split_recursive_suffix. ((((exists ff_h_bps_split_recursive_suffix_start. ff_h_bps_split_recursive_suffix_start + S (1) = S ((S (0)) * ff_v_bps_split_recursive_suffix)) /\ exists ff_q_bps_split_recursive_suffix_start. ff_u_bps_split_recursive_suffix = ff_q_bps_split_recursive_suffix_start * S ((S (0)) * ff_v_bps_split_recursive_suffix) + (1))) /\ ((((exists ff_h_bps_split_recursive_suffix_terminal. ff_h_bps_split_recursive_suffix_terminal + S (q) = S ((S (m)) * ff_v_bps_split_recursive_suffix)) /\ exists ff_q_bps_split_recursive_suffix_terminal. ff_u_bps_split_recursive_suffix = ff_q_bps_split_recursive_suffix_terminal * S ((S (m)) * ff_v_bps_split_recursive_suffix) + (q))) /\ forall ff_i_bps_split_recursive_suffix. (exists ff_lt_bps_split_recursive_suffix_bound. ff_lt_bps_split_recursive_suffix_bound + S ff_i_bps_split_recursive_suffix = m) -> exists ff_p_bps_split_recursive_suffix ff_r_bps_split_recursive_suffix ff_s_bps_split_recursive_suffix. ((((exists ff_h_bps_split_recursive_suffix_factor. ff_h_bps_split_recursive_suffix_factor + S (ff_p_bps_split_recursive_suffix) = S ((S (ff_i_bps_split_recursive_suffix)) * d)) /\ exists ff_q_bps_split_recursive_suffix_factor. z = ff_q_bps_split_recursive_suffix_factor * S ((S (ff_i_bps_split_recursive_suffix)) * d) + (ff_p_bps_split_recursive_suffix))) /\ ((((exists ff_h_bps_split_recursive_suffix_partial. ff_h_bps_split_recursive_suffix_partial + S (ff_r_bps_split_recursive_suffix) = S ((S (ff_i_bps_split_recursive_suffix)) * ff_v_bps_split_recursive_suffix)) /\ exists ff_q_bps_split_recursive_suffix_partial. ff_u_bps_split_recursive_suffix = ff_q_bps_split_recursive_suffix_partial * S ((S (ff_i_bps_split_recursive_suffix)) * ff_v_bps_split_recursive_suffix) + (ff_r_bps_split_recursive_suffix))) /\ ((((exists ff_h_bps_split_recursive_suffix_successor. ff_h_bps_split_recursive_suffix_successor + S (ff_s_bps_split_recursive_suffix) = S ((S (S ff_i_bps_split_recursive_suffix)) * ff_v_bps_split_recursive_suffix)) /\ exists ff_q_bps_split_recursive_suffix_successor. ff_u_bps_split_recursive_suffix = ff_q_bps_split_recursive_suffix_successor * S ((S (S ff_i_bps_split_recursive_suffix)) * ff_v_bps_split_recursive_suffix) + (ff_s_bps_split_recursive_suffix))) /\ ff_s_bps_split_recursive_suffix = ff_r_bps_split_recursive_suffix * ff_p_bps_split_recursive_suffix)))))) /\ x1 = p * q)
  74. 0074specialize IH x1
  75. 0075apply IH
  76. 0076exact hprefix_shift
  77. 0077exact hdecomposition_witness_witness_right_left
  78. 0078cases hrecursive
  79. 0079cases hrecursive_witness
  80. 0080cases hrecursive_witness_witness
  81. 0081cases hrecursive_witness_witness_right
  82. 0082have hsuffix_last : BetaAt(z,d,m,x)
    Exact native replay linehave hsuffix_last : ((exists ff_h_bps_split_suffix_last. ff_h_bps_split_suffix_last + S (x) = S ((S (m)) * d)) /\ exists ff_q_bps_split_suffix_last. z = ff_q_bps_split_suffix_last * S ((S (m)) * d) + (x))
  83. 0083specialize hshift m
  84. 0084specialize hshift x
  85. 0085apply hshift
  86. 0086specialize le_refl (S m)
  87. 0087exact le_refl
  88. 0088exact hdecomposition_witness_witness_left
  89. 0089exists x2
  90. 0090exists x3 * x
  91. 0091split
  92. 0092exact hrecursive_witness_witness_left
  93. 0093split
  94. 0094specialize beta_product_succ_append z
  95. 0095specialize beta_product_succ_append d
  96. 0096specialize beta_product_succ_append m
  97. 0097specialize beta_product_succ_append x3
  98. 0098specialize beta_product_succ_append x
  99. 0099apply beta_product_succ_append
  100. 0100exact hrecursive_witness_witness_right_left
  101. 0101exact hsuffix_last
  102. 0102rewrite hdecomposition_witness_witness_right_right
  103. 0103rewrite hrecursive_witness_witness_right_right
  104. 0104specialize mul_assoc x2
  105. 0105specialize mul_assoc x3
  106. 0106specialize mul_assoc x
  107. 0107exact mul_assoc