EC0008

euclidean_trace_exists_up_to_linear

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

Bounded natural induction constructs an authentic complete Euclidean beta-history using at most B divisions whenever the divisor is at most B.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall B b. (exists gap. gap + b = B) -> forall a. (exists s h e l. ((exists cf_gcd_ec_induction_bounded. ((((exists ff_h_cf_ec_induction_bounded_initial_state. ff_h_cf_ec_induction_bounded_initial_state + S (((cf_gcd_ec_induction_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_induction_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_ec_induction_bounded_initial_state. h = ff_q_cf_ec_induction_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_induction_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_induction_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_ec_induction_bounded_terminal_state. ff_h_cf_ec_induction_bounded_terminal_state + S (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (l)) * e)) /\ exists ff_q_cf_ec_induction_bounded_terminal_state. h = ff_q_cf_ec_induction_bounded_terminal_state * S ((S (l)) * e) + (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_ec_induction_bounded. (exists ff_lt_cf_ec_induction_bounded_index. ff_lt_cf_ec_induction_bounded_index + S cf_index_ec_induction_bounded = l) -> exists cf_old_a_ec_induction_bounded cf_old_b_ec_induction_bounded cf_tail_ec_induction_bounded cf_new_a_ec_induction_bounded cf_new_b_ec_induction_bounded cf_head_ec_induction_bounded cf_quotient_ec_induction_bounded. ((((exists ff_h_cf_ec_induction_bounded_previous_state. ff_h_cf_ec_induction_bounded_previous_state + S (((cf_old_a_ec_induction_bounded) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded)))) * S ((cf_old_a_ec_induction_bounded) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded)))) + ((((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded))) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded))))) = S ((S (cf_index_ec_induction_bounded)) * e)) /\ exists ff_q_cf_ec_induction_bounded_previous_state. h = ff_q_cf_ec_induction_bounded_previous_state * S ((S (cf_index_ec_induction_bounded)) * e) + (((cf_old_a_ec_induction_bounded) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded)))) * S ((cf_old_a_ec_induction_bounded) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded)))) + ((((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded))) + (((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) * S ((cf_old_b_ec_induction_bounded) + (cf_tail_ec_induction_bounded)) + ((cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded))))))) /\ ((((exists ff_h_cf_ec_induction_bounded_following_state. ff_h_cf_ec_induction_bounded_following_state + S (((cf_new_a_ec_induction_bounded) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded)))) * S ((cf_new_a_ec_induction_bounded) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded)))) + ((((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded))) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded))))) = S ((S (S cf_index_ec_induction_bounded)) * e)) /\ exists ff_q_cf_ec_induction_bounded_following_state. h = ff_q_cf_ec_induction_bounded_following_state * S ((S (S cf_index_ec_induction_bounded)) * e) + (((cf_new_a_ec_induction_bounded) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded)))) * S ((cf_new_a_ec_induction_bounded) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded)))) + ((((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded))) + (((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) * S ((cf_new_b_ec_induction_bounded) + (cf_head_ec_induction_bounded)) + ((cf_head_ec_induction_bounded) + (cf_head_ec_induction_bounded))))))) /\ (cf_new_b_ec_induction_bounded = cf_old_a_ec_induction_bounded /\ (cf_new_a_ec_induction_bounded = cf_new_b_ec_induction_bounded * cf_quotient_ec_induction_bounded + cf_old_b_ec_induction_bounded /\ ((exists ff_lt_cf_ec_induction_bounded_remainder. ff_lt_cf_ec_induction_bounded_remainder + S cf_old_b_ec_induction_bounded = cf_new_b_ec_induction_bounded) /\ (cf_head_ec_induction_bounded = S ((cf_quotient_ec_induction_bounded + cf_tail_ec_induction_bounded) * S (cf_quotient_ec_induction_bounded + cf_tail_ec_induction_bounded) + (cf_tail_ec_induction_bounded + cf_tail_ec_induction_bounded))))))))))) /\ (exists ec_bound_gap_induction. ec_bound_gap_induction + l = B)))

Constructive proof overview

Generated structural guide

Bounded natural induction constructs an authentic complete Euclidean beta-history using at most B divisions whenever the divisor is at most B.

The unchanged tactic script uses 9 declared prerequisites and contains 113 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_zero Stable theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized division_remainder_exists Stable theorem; checked-use authorized continued_fraction_empty_trace_exists Alpha theorem; checked-use authorized continued_fraction_trace_extend Alpha theorem; checked-use authorized le_refl Stable theorem; checked-use authorized succ_le_succ Stable theorem; checked-use authorized EC0007 euclidean_trace_bound_weaken

Direct dependents

EC0009 euclidean_trace_exists_linear

Formal native tactic body

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

Read the argument

Proof checkpoints

113 script commands · 28 reading checkpoints · 10 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.

Named ingredients (1)
euclidean trace bound weaken

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–5

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

  1. L2
    induction B
  2. L3
    intro b
  3. L4
    intro hb
  4. L5
    intro a
03Establish hb0L6–9

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

  1. L6
    have hb0 : b = 0
  2. L7
    apply le_zero
  3. L8
    exact hb
  4. L9
    specialize continued_fraction_empty_trace_exists a
04Separate the logical casesL10–11

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

  1. L10
    cases continued_fraction_empty_trace_exists
  2. L11
    cases continued_fraction_empty_trace_exists_witness
05Construct an explicit witnessL12–15

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

  1. L12
    exists 0
  2. L13
    exists x
  3. L14
    exists x1
  4. L15
    exists 0
06Separate the logical casesL16–16

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

  1. L16
    split
07Calculate and transport equalitiesL17–26

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

  1. L17
    rewrite hb0
  2. L18
    rewrite hb0
  3. L19
    rewrite hb0
  4. L20
    rewrite hb0
  5. L21
    rewrite hb0
  6. L22
    rewrite hb0
  7. L23
    rewrite hb0
  8. L24
    rewrite hb0
  9. L25
    rewrite hb0
  10. L26
    rewrite hb0
08Calculate and transport equalitiesL27–32

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

  1. L27
    rewrite hb0
  2. L28
    rewrite hb0
  3. L29
    rewrite hb0
  4. L30
    rewrite hb0
  5. L31
    rewrite hb0
  6. L32
    rewrite hb0
09Use earlier factsL33–35

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

  1. L33
    exact continued_fraction_empty_trace_exists_witness_witness
  2. L34
    specialize le_refl 0
  3. L35
    exact le_refl
10Fix variables and assumptionsL36–38

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

  1. L36
    intro b
  2. L37
    intro hb
  3. L38
    intro a
11Use earlier factsL39–40

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

  1. L39
    specialize le_eq_or_lt b
  2. L40
    specialize le_eq_or_lt (S B)
12Establish hsplitL41–43

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

  1. L41
    have hsplit : b = S B \/ exists gap. gap + S b = S B
  2. L42
    apply le_eq_or_lt
  3. L43
    exact hb
13Separate the logical casesL44–44

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

  1. L44
    cases hsplit
14Establish hb0L45–51

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

  1. L45
    have hb0 : ~(b = 0)
  2. L46
    intro hzero
  3. L47
    apply PA1
  4. L48
    trans b
  5. L49
    symm
  6. L50
    exact hsplit_left
  7. L51
    exact hzero
15Establish hdivisionL52–54

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

  1. L52
    have hdivision : exists q r. a = b * q + r /\ exists gap. gap + S r = b
  2. L53
    apply division_remainder_exists
  3. L54
    exact hb0
16Separate the logical casesL55–57

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

  1. L55
    cases hdivision
  2. L56
    cases hdivision_witness
  3. L57
    cases hdivision_witness_witness
17Establish hrBL58–61

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

  1. L58
    have hrB : exists gap. gap + x1 = B
  2. L59
    apply le_of_succ_le_succ
  3. L60
    rewrite hsplit_left at hdivision_witness_witness_right
  4. L61
    exact hdivision_witness_witness_right
18Establish hsmallL62–63

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

  1. L62
    have hsmall : ∃ s. ∃ h. ∃ e. ∃ l. ContinuedFractionTrace(b,x1,s,h,e,l) ∧ l ≤ BDefinitions: ContinuedFractionTrace
  2. L63
    specialize IH x1
19Establish hallL64–68

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

  1. L64
    have hall : ∀ z. ∃ x. ∃ y. ∃ n. ∃ m. ContinuedFractionTrace(z,x1,x,y,n,m) ∧ m ≤ BDefinitions: ContinuedFractionTrace
  2. L65
    apply IH
  3. L66
    exact hrB
  4. L67
    specialize hall b
  5. L68
    exact hall
20Separate the logical casesL69–73

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

  1. L69
    cases hsmall
  2. L70
    cases hsmall_witness
  3. L71
    cases hsmall_witness_witness
  4. L72
    cases hsmall_witness_witness_witness
  5. L73
    cases hsmall_witness_witness_witness_witness
21Establish hextendL74–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply continued fraction trace extend.

  1. L74
    have hextend : ∃ s. ∃ z. ∃ c. ListCell(s,x,x2) ∧ ContinuedFractionTrace(a,b,s,z,c,S x5)Definitions: ListCellContinuedFractionTrace
  2. L75
    specialize continued_fraction_trace_extend a
  3. L76
    specialize continued_fraction_trace_extend b
  4. L77
    specialize continued_fraction_trace_extend x
  5. L78
    specialize continued_fraction_trace_extend x1
  6. L79
    specialize continued_fraction_trace_extend x2
  7. L80
    specialize continued_fraction_trace_extend x3
  8. L81
    specialize continued_fraction_trace_extend x4
  9. L82
    specialize continued_fraction_trace_extend x5
  10. L83
    apply continued_fraction_trace_extend
22Use earlier factsL84–86

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

  1. L84
    exact hdivision_witness_witness_left
  2. L85
    exact hdivision_witness_witness_right
  3. L86
    exact hsmall_witness_witness_witness_witness_left
23Separate the logical casesL87–90

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

  1. L87
    cases hextend
  2. L88
    cases hextend_witness
  3. L89
    cases hextend_witness_witness
  4. L90
    cases hextend_witness_witness_witness
24Construct an explicit witnessL91–94

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

  1. L91
    exists x6
  2. L92
    exists x7
  3. L93
    exists x8
  4. L94
    exists S x5
25Separate the logical casesL95–95

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

  1. L95
    split
26Use earlier factsL96–100

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

  1. L96
    exact hextend_witness_witness_witness_right
  2. L97
    specialize succ_le_succ x5
  3. L98
    specialize succ_le_succ B
  4. L99
    apply succ_le_succ
  5. L100
    exact hsmall_witness_witness_witness_witness_right
27Establish hbBL101–104

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

  1. L101
    have hbB : exists gap. gap + b = B
  2. L102
    apply le_of_succ_le_succ
  3. L103
    exact hsplit_right
  4. L104
    specialize IH b
28Establish hallL105–113

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

  1. L105
    have hall : ∀ z. ∃ x. ∃ y. ∃ n. ∃ m. ContinuedFractionTrace(z,b,x,y,n,m) ∧ m ≤ BDefinitions: ContinuedFractionTrace
  2. L106
    apply IH
  3. L107
    exact hbB
  4. L108
    specialize hall a
  5. L109
    specialize euclidean_trace_bound_weaken a
  6. L110
    specialize euclidean_trace_bound_weaken b
  7. L111
    specialize euclidean_trace_bound_weaken B
  8. L112
    apply euclidean_trace_bound_weaken
  9. L113
    exact hall

Library-wide reading audit

Original exact command ledger · 113 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro b
  4. 0004intro hb
  5. 0005intro a
  6. 0006have hb0 : b = 0
  7. 0007apply le_zero
  8. 0008exact hb
  9. 0009specialize continued_fraction_empty_trace_exists a
  10. 0010cases continued_fraction_empty_trace_exists
  11. 0011cases continued_fraction_empty_trace_exists_witness
  12. 0012exists 0
  13. 0013exists x
  14. 0014exists x1
  15. 0015exists 0
  16. 0016split
  17. 0017rewrite hb0
  18. 0018rewrite hb0
  19. 0019rewrite hb0
  20. 0020rewrite hb0
  21. 0021rewrite hb0
  22. 0022rewrite hb0
  23. 0023rewrite hb0
  24. 0024rewrite hb0
  25. 0025rewrite hb0
  26. 0026rewrite hb0
  27. 0027rewrite hb0
  28. 0028rewrite hb0
  29. 0029rewrite hb0
  30. 0030rewrite hb0
  31. 0031rewrite hb0
  32. 0032rewrite hb0
  33. 0033exact continued_fraction_empty_trace_exists_witness_witness
  34. 0034specialize le_refl 0
  35. 0035exact le_refl
  36. 0036intro b
  37. 0037intro hb
  38. 0038intro a
  39. 0039specialize le_eq_or_lt b
  40. 0040specialize le_eq_or_lt (S B)
  41. 0041have hsplit : b = S B \/ exists gap. gap + S b = S B
  42. 0042apply le_eq_or_lt
  43. 0043exact hb
  44. 0044cases hsplit
  45. 0045have hb0 : ~(b = 0)
  46. 0046intro hzero
  47. 0047apply PA1
  48. 0048trans b
  49. 0049symm
  50. 0050exact hsplit_left
  51. 0051exact hzero
  52. 0052have hdivision : exists q r. a = b * q + r /\ exists gap. gap + S r = b
  53. 0053apply division_remainder_exists
  54. 0054exact hb0
  55. 0055cases hdivision
  56. 0056cases hdivision_witness
  57. 0057cases hdivision_witness_witness
  58. 0058have hrB : exists gap. gap + x1 = B
  59. 0059apply le_of_succ_le_succ
  60. 0060rewrite hsplit_left at hdivision_witness_witness_right
  61. 0061exact hdivision_witness_witness_right
  62. 0062have hsmall : exists s h e l. ((exists cf_gcd_ec_reduced_bounded. ((((exists ff_h_cf_ec_reduced_bounded_initial_state. ff_h_cf_ec_reduced_bounded_initial_state + S (((cf_gcd_ec_reduced_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_reduced_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_ec_reduced_bounded_initial_state. h = ff_q_cf_ec_reduced_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_reduced_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_reduced_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_ec_reduced_bounded_terminal_state. ff_h_cf_ec_reduced_bounded_terminal_state + S (((b) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s)))) * S ((b) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s)))) + ((((x1) + (s)) * S ((x1) + (s)) + ((s) + (s))) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s))))) = S ((S (l)) * e)) /\ exists ff_q_cf_ec_reduced_bounded_terminal_state. h = ff_q_cf_ec_reduced_bounded_terminal_state * S ((S (l)) * e) + (((b) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s)))) * S ((b) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s)))) + ((((x1) + (s)) * S ((x1) + (s)) + ((s) + (s))) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s))))))) /\ forall cf_index_ec_reduced_bounded. (exists ff_lt_cf_ec_reduced_bounded_index. ff_lt_cf_ec_reduced_bounded_index + S cf_index_ec_reduced_bounded = l) -> exists cf_old_a_ec_reduced_bounded cf_old_b_ec_reduced_bounded cf_tail_ec_reduced_bounded cf_new_a_ec_reduced_bounded cf_new_b_ec_reduced_bounded cf_head_ec_reduced_bounded cf_quotient_ec_reduced_bounded. ((((exists ff_h_cf_ec_reduced_bounded_previous_state. ff_h_cf_ec_reduced_bounded_previous_state + S (((cf_old_a_ec_reduced_bounded) + (((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) * S ((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) + ((cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)))) * S ((cf_old_a_ec_reduced_bounded) + (((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) * S ((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) + ((cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)))) + ((((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) * S ((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) + ((cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded))) + (((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) * S ((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) + ((cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded))))) = S ((S (cf_index_ec_reduced_bounded)) * e)) /\ exists ff_q_cf_ec_reduced_bounded_previous_state. h = ff_q_cf_ec_reduced_bounded_previous_state * S ((S (cf_index_ec_reduced_bounded)) * e) + (((cf_old_a_ec_reduced_bounded) + (((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) * S ((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) + ((cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)))) * S ((cf_old_a_ec_reduced_bounded) + (((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) * S ((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) + ((cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)))) + ((((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) * S ((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) + ((cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded))) + (((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) * S ((cf_old_b_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded)) + ((cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded))))))) /\ ((((exists ff_h_cf_ec_reduced_bounded_following_state. ff_h_cf_ec_reduced_bounded_following_state + S (((cf_new_a_ec_reduced_bounded) + (((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) * S ((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) + ((cf_head_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)))) * S ((cf_new_a_ec_reduced_bounded) + (((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) * S ((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) + ((cf_head_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)))) + ((((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) * S ((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) + ((cf_head_ec_reduced_bounded) + (cf_head_ec_reduced_bounded))) + (((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) * S ((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) + ((cf_head_ec_reduced_bounded) + (cf_head_ec_reduced_bounded))))) = S ((S (S cf_index_ec_reduced_bounded)) * e)) /\ exists ff_q_cf_ec_reduced_bounded_following_state. h = ff_q_cf_ec_reduced_bounded_following_state * S ((S (S cf_index_ec_reduced_bounded)) * e) + (((cf_new_a_ec_reduced_bounded) + (((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) * S ((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) + ((cf_head_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)))) * S ((cf_new_a_ec_reduced_bounded) + (((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) * S ((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) + ((cf_head_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)))) + ((((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) * S ((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) + ((cf_head_ec_reduced_bounded) + (cf_head_ec_reduced_bounded))) + (((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) * S ((cf_new_b_ec_reduced_bounded) + (cf_head_ec_reduced_bounded)) + ((cf_head_ec_reduced_bounded) + (cf_head_ec_reduced_bounded))))))) /\ (cf_new_b_ec_reduced_bounded = cf_old_a_ec_reduced_bounded /\ (cf_new_a_ec_reduced_bounded = cf_new_b_ec_reduced_bounded * cf_quotient_ec_reduced_bounded + cf_old_b_ec_reduced_bounded /\ ((exists ff_lt_cf_ec_reduced_bounded_remainder. ff_lt_cf_ec_reduced_bounded_remainder + S cf_old_b_ec_reduced_bounded = cf_new_b_ec_reduced_bounded) /\ (cf_head_ec_reduced_bounded = S ((cf_quotient_ec_reduced_bounded + cf_tail_ec_reduced_bounded) * S (cf_quotient_ec_reduced_bounded + cf_tail_ec_reduced_bounded) + (cf_tail_ec_reduced_bounded + cf_tail_ec_reduced_bounded))))))))))) /\ (exists ec_bound_gap_reduced. ec_bound_gap_reduced + l = B))
  63. 0063specialize IH x1
  64. 0064have hall : forall z. (exists s h e l. ((exists cf_gcd_ec_reduced_all_bounded. ((((exists ff_h_cf_ec_reduced_all_bounded_initial_state. ff_h_cf_ec_reduced_all_bounded_initial_state + S (((cf_gcd_ec_reduced_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_reduced_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_ec_reduced_all_bounded_initial_state. h = ff_q_cf_ec_reduced_all_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_reduced_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_reduced_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_ec_reduced_all_bounded_terminal_state. ff_h_cf_ec_reduced_all_bounded_terminal_state + S (((z) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s)))) * S ((z) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s)))) + ((((x1) + (s)) * S ((x1) + (s)) + ((s) + (s))) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s))))) = S ((S (l)) * e)) /\ exists ff_q_cf_ec_reduced_all_bounded_terminal_state. h = ff_q_cf_ec_reduced_all_bounded_terminal_state * S ((S (l)) * e) + (((z) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s)))) * S ((z) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s)))) + ((((x1) + (s)) * S ((x1) + (s)) + ((s) + (s))) + (((x1) + (s)) * S ((x1) + (s)) + ((s) + (s))))))) /\ forall cf_index_ec_reduced_all_bounded. (exists ff_lt_cf_ec_reduced_all_bounded_index. ff_lt_cf_ec_reduced_all_bounded_index + S cf_index_ec_reduced_all_bounded = l) -> exists cf_old_a_ec_reduced_all_bounded cf_old_b_ec_reduced_all_bounded cf_tail_ec_reduced_all_bounded cf_new_a_ec_reduced_all_bounded cf_new_b_ec_reduced_all_bounded cf_head_ec_reduced_all_bounded cf_quotient_ec_reduced_all_bounded. ((((exists ff_h_cf_ec_reduced_all_bounded_previous_state. ff_h_cf_ec_reduced_all_bounded_previous_state + S (((cf_old_a_ec_reduced_all_bounded) + (((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) * S ((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) + ((cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)))) * S ((cf_old_a_ec_reduced_all_bounded) + (((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) * S ((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) + ((cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)))) + ((((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) * S ((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) + ((cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded))) + (((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) * S ((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) + ((cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded))))) = S ((S (cf_index_ec_reduced_all_bounded)) * e)) /\ exists ff_q_cf_ec_reduced_all_bounded_previous_state. h = ff_q_cf_ec_reduced_all_bounded_previous_state * S ((S (cf_index_ec_reduced_all_bounded)) * e) + (((cf_old_a_ec_reduced_all_bounded) + (((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) * S ((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) + ((cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)))) * S ((cf_old_a_ec_reduced_all_bounded) + (((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) * S ((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) + ((cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)))) + ((((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) * S ((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) + ((cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded))) + (((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) * S ((cf_old_b_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded)) + ((cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded))))))) /\ ((((exists ff_h_cf_ec_reduced_all_bounded_following_state. ff_h_cf_ec_reduced_all_bounded_following_state + S (((cf_new_a_ec_reduced_all_bounded) + (((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) * S ((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) + ((cf_head_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)))) * S ((cf_new_a_ec_reduced_all_bounded) + (((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) * S ((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) + ((cf_head_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)))) + ((((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) * S ((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) + ((cf_head_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded))) + (((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) * S ((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) + ((cf_head_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded))))) = S ((S (S cf_index_ec_reduced_all_bounded)) * e)) /\ exists ff_q_cf_ec_reduced_all_bounded_following_state. h = ff_q_cf_ec_reduced_all_bounded_following_state * S ((S (S cf_index_ec_reduced_all_bounded)) * e) + (((cf_new_a_ec_reduced_all_bounded) + (((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) * S ((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) + ((cf_head_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)))) * S ((cf_new_a_ec_reduced_all_bounded) + (((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) * S ((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) + ((cf_head_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)))) + ((((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) * S ((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) + ((cf_head_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded))) + (((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) * S ((cf_new_b_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded)) + ((cf_head_ec_reduced_all_bounded) + (cf_head_ec_reduced_all_bounded))))))) /\ (cf_new_b_ec_reduced_all_bounded = cf_old_a_ec_reduced_all_bounded /\ (cf_new_a_ec_reduced_all_bounded = cf_new_b_ec_reduced_all_bounded * cf_quotient_ec_reduced_all_bounded + cf_old_b_ec_reduced_all_bounded /\ ((exists ff_lt_cf_ec_reduced_all_bounded_remainder. ff_lt_cf_ec_reduced_all_bounded_remainder + S cf_old_b_ec_reduced_all_bounded = cf_new_b_ec_reduced_all_bounded) /\ (cf_head_ec_reduced_all_bounded = S ((cf_quotient_ec_reduced_all_bounded + cf_tail_ec_reduced_all_bounded) * S (cf_quotient_ec_reduced_all_bounded + cf_tail_ec_reduced_all_bounded) + (cf_tail_ec_reduced_all_bounded + cf_tail_ec_reduced_all_bounded))))))))))) /\ (exists ec_bound_gap_reduced_all. ec_bound_gap_reduced_all + l = B)))
  65. 0065apply IH
  66. 0066exact hrB
  67. 0067specialize hall b
  68. 0068exact hall
  69. 0069cases hsmall
  70. 0070cases hsmall_witness
  71. 0071cases hsmall_witness_witness
  72. 0072cases hsmall_witness_witness_witness
  73. 0073cases hsmall_witness_witness_witness_witness
  74. 0074have hextend : exists s z c. ((s = S ((x + x2) * S (x + x2) + (x2 + x2))) /\ (exists cf_gcd_ec_induction_extension. ((((exists ff_h_cf_ec_induction_extension_initial_state. ff_h_cf_ec_induction_extension_initial_state + S (((cf_gcd_ec_induction_extension) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_induction_extension) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * c)) /\ exists ff_q_cf_ec_induction_extension_initial_state. z = ff_q_cf_ec_induction_extension_initial_state * S ((S (0)) * c) + (((cf_gcd_ec_induction_extension) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_induction_extension) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_ec_induction_extension_terminal_state. ff_h_cf_ec_induction_extension_terminal_state + S (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (S x5)) * c)) /\ exists ff_q_cf_ec_induction_extension_terminal_state. z = ff_q_cf_ec_induction_extension_terminal_state * S ((S (S x5)) * c) + (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_ec_induction_extension. (exists ff_lt_cf_ec_induction_extension_index. ff_lt_cf_ec_induction_extension_index + S cf_index_ec_induction_extension = S x5) -> exists cf_old_a_ec_induction_extension cf_old_b_ec_induction_extension cf_tail_ec_induction_extension cf_new_a_ec_induction_extension cf_new_b_ec_induction_extension cf_head_ec_induction_extension cf_quotient_ec_induction_extension. ((((exists ff_h_cf_ec_induction_extension_previous_state. ff_h_cf_ec_induction_extension_previous_state + S (((cf_old_a_ec_induction_extension) + (((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) * S ((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) + ((cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension)))) * S ((cf_old_a_ec_induction_extension) + (((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) * S ((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) + ((cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension)))) + ((((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) * S ((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) + ((cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension))) + (((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) * S ((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) + ((cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension))))) = S ((S (cf_index_ec_induction_extension)) * c)) /\ exists ff_q_cf_ec_induction_extension_previous_state. z = ff_q_cf_ec_induction_extension_previous_state * S ((S (cf_index_ec_induction_extension)) * c) + (((cf_old_a_ec_induction_extension) + (((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) * S ((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) + ((cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension)))) * S ((cf_old_a_ec_induction_extension) + (((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) * S ((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) + ((cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension)))) + ((((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) * S ((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) + ((cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension))) + (((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) * S ((cf_old_b_ec_induction_extension) + (cf_tail_ec_induction_extension)) + ((cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension))))))) /\ ((((exists ff_h_cf_ec_induction_extension_following_state. ff_h_cf_ec_induction_extension_following_state + S (((cf_new_a_ec_induction_extension) + (((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) * S ((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) + ((cf_head_ec_induction_extension) + (cf_head_ec_induction_extension)))) * S ((cf_new_a_ec_induction_extension) + (((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) * S ((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) + ((cf_head_ec_induction_extension) + (cf_head_ec_induction_extension)))) + ((((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) * S ((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) + ((cf_head_ec_induction_extension) + (cf_head_ec_induction_extension))) + (((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) * S ((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) + ((cf_head_ec_induction_extension) + (cf_head_ec_induction_extension))))) = S ((S (S cf_index_ec_induction_extension)) * c)) /\ exists ff_q_cf_ec_induction_extension_following_state. z = ff_q_cf_ec_induction_extension_following_state * S ((S (S cf_index_ec_induction_extension)) * c) + (((cf_new_a_ec_induction_extension) + (((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) * S ((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) + ((cf_head_ec_induction_extension) + (cf_head_ec_induction_extension)))) * S ((cf_new_a_ec_induction_extension) + (((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) * S ((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) + ((cf_head_ec_induction_extension) + (cf_head_ec_induction_extension)))) + ((((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) * S ((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) + ((cf_head_ec_induction_extension) + (cf_head_ec_induction_extension))) + (((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) * S ((cf_new_b_ec_induction_extension) + (cf_head_ec_induction_extension)) + ((cf_head_ec_induction_extension) + (cf_head_ec_induction_extension))))))) /\ (cf_new_b_ec_induction_extension = cf_old_a_ec_induction_extension /\ (cf_new_a_ec_induction_extension = cf_new_b_ec_induction_extension * cf_quotient_ec_induction_extension + cf_old_b_ec_induction_extension /\ ((exists ff_lt_cf_ec_induction_extension_remainder. ff_lt_cf_ec_induction_extension_remainder + S cf_old_b_ec_induction_extension = cf_new_b_ec_induction_extension) /\ (cf_head_ec_induction_extension = S ((cf_quotient_ec_induction_extension + cf_tail_ec_induction_extension) * S (cf_quotient_ec_induction_extension + cf_tail_ec_induction_extension) + (cf_tail_ec_induction_extension + cf_tail_ec_induction_extension))))))))))))
  75. 0075specialize continued_fraction_trace_extend a
  76. 0076specialize continued_fraction_trace_extend b
  77. 0077specialize continued_fraction_trace_extend x
  78. 0078specialize continued_fraction_trace_extend x1
  79. 0079specialize continued_fraction_trace_extend x2
  80. 0080specialize continued_fraction_trace_extend x3
  81. 0081specialize continued_fraction_trace_extend x4
  82. 0082specialize continued_fraction_trace_extend x5
  83. 0083apply continued_fraction_trace_extend
  84. 0084exact hdivision_witness_witness_left
  85. 0085exact hdivision_witness_witness_right
  86. 0086exact hsmall_witness_witness_witness_witness_left
  87. 0087cases hextend
  88. 0088cases hextend_witness
  89. 0089cases hextend_witness_witness
  90. 0090cases hextend_witness_witness_witness
  91. 0091exists x6
  92. 0092exists x7
  93. 0093exists x8
  94. 0094exists S x5
  95. 0095split
  96. 0096exact hextend_witness_witness_witness_right
  97. 0097specialize succ_le_succ x5
  98. 0098specialize succ_le_succ B
  99. 0099apply succ_le_succ
  100. 0100exact hsmall_witness_witness_witness_witness_right
  101. 0101have hbB : exists gap. gap + b = B
  102. 0102apply le_of_succ_le_succ
  103. 0103exact hsplit_right
  104. 0104specialize IH b
  105. 0105have hall : forall z. (exists s h e l. ((exists cf_gcd_ec_smaller_all_bounded. ((((exists ff_h_cf_ec_smaller_all_bounded_initial_state. ff_h_cf_ec_smaller_all_bounded_initial_state + S (((cf_gcd_ec_smaller_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_smaller_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_ec_smaller_all_bounded_initial_state. h = ff_q_cf_ec_smaller_all_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_ec_smaller_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_smaller_all_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_ec_smaller_all_bounded_terminal_state. ff_h_cf_ec_smaller_all_bounded_terminal_state + S (((z) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((z) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (l)) * e)) /\ exists ff_q_cf_ec_smaller_all_bounded_terminal_state. h = ff_q_cf_ec_smaller_all_bounded_terminal_state * S ((S (l)) * e) + (((z) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((z) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_ec_smaller_all_bounded. (exists ff_lt_cf_ec_smaller_all_bounded_index. ff_lt_cf_ec_smaller_all_bounded_index + S cf_index_ec_smaller_all_bounded = l) -> exists cf_old_a_ec_smaller_all_bounded cf_old_b_ec_smaller_all_bounded cf_tail_ec_smaller_all_bounded cf_new_a_ec_smaller_all_bounded cf_new_b_ec_smaller_all_bounded cf_head_ec_smaller_all_bounded cf_quotient_ec_smaller_all_bounded. ((((exists ff_h_cf_ec_smaller_all_bounded_previous_state. ff_h_cf_ec_smaller_all_bounded_previous_state + S (((cf_old_a_ec_smaller_all_bounded) + (((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) * S ((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) + ((cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)))) * S ((cf_old_a_ec_smaller_all_bounded) + (((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) * S ((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) + ((cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)))) + ((((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) * S ((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) + ((cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded))) + (((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) * S ((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) + ((cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded))))) = S ((S (cf_index_ec_smaller_all_bounded)) * e)) /\ exists ff_q_cf_ec_smaller_all_bounded_previous_state. h = ff_q_cf_ec_smaller_all_bounded_previous_state * S ((S (cf_index_ec_smaller_all_bounded)) * e) + (((cf_old_a_ec_smaller_all_bounded) + (((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) * S ((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) + ((cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)))) * S ((cf_old_a_ec_smaller_all_bounded) + (((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) * S ((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) + ((cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)))) + ((((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) * S ((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) + ((cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded))) + (((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) * S ((cf_old_b_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded)) + ((cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded))))))) /\ ((((exists ff_h_cf_ec_smaller_all_bounded_following_state. ff_h_cf_ec_smaller_all_bounded_following_state + S (((cf_new_a_ec_smaller_all_bounded) + (((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) * S ((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) + ((cf_head_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)))) * S ((cf_new_a_ec_smaller_all_bounded) + (((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) * S ((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) + ((cf_head_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)))) + ((((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) * S ((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) + ((cf_head_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded))) + (((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) * S ((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) + ((cf_head_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded))))) = S ((S (S cf_index_ec_smaller_all_bounded)) * e)) /\ exists ff_q_cf_ec_smaller_all_bounded_following_state. h = ff_q_cf_ec_smaller_all_bounded_following_state * S ((S (S cf_index_ec_smaller_all_bounded)) * e) + (((cf_new_a_ec_smaller_all_bounded) + (((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) * S ((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) + ((cf_head_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)))) * S ((cf_new_a_ec_smaller_all_bounded) + (((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) * S ((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) + ((cf_head_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)))) + ((((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) * S ((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) + ((cf_head_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded))) + (((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) * S ((cf_new_b_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded)) + ((cf_head_ec_smaller_all_bounded) + (cf_head_ec_smaller_all_bounded))))))) /\ (cf_new_b_ec_smaller_all_bounded = cf_old_a_ec_smaller_all_bounded /\ (cf_new_a_ec_smaller_all_bounded = cf_new_b_ec_smaller_all_bounded * cf_quotient_ec_smaller_all_bounded + cf_old_b_ec_smaller_all_bounded /\ ((exists ff_lt_cf_ec_smaller_all_bounded_remainder. ff_lt_cf_ec_smaller_all_bounded_remainder + S cf_old_b_ec_smaller_all_bounded = cf_new_b_ec_smaller_all_bounded) /\ (cf_head_ec_smaller_all_bounded = S ((cf_quotient_ec_smaller_all_bounded + cf_tail_ec_smaller_all_bounded) * S (cf_quotient_ec_smaller_all_bounded + cf_tail_ec_smaller_all_bounded) + (cf_tail_ec_smaller_all_bounded + cf_tail_ec_smaller_all_bounded))))))))))) /\ (exists ec_bound_gap_smaller_all. ec_bound_gap_smaller_all + l = B)))
  106. 0106apply IH
  107. 0107exact hbB
  108. 0108specialize hall a
  109. 0109specialize euclidean_trace_bound_weaken a
  110. 0110specialize euclidean_trace_bound_weaken b
  111. 0111specialize euclidean_trace_bound_weaken B
  112. 0112apply euclidean_trace_bound_weaken
  113. 0113exact hall