CF0005

continued_fraction_trace_exists_up_to

Bounded natural induction terminates Euclid at zero and builds a complete forward quotient list for every divisor below its bound.

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

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 theorem in conservative defined notation

∀ B. ∀ b. b ≤ B → ∀ x. ∃ y. ∃ z. ∃ n. ∃ m. ContinuedFractionTrace(x,b,y,z,n,m)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ContinuedFractionTrace(a,b,s,u,v,ell) · 1

Actual proof prerequisites

le_zero · checked external prerequisitele_eq_or_lt · checked external prerequisitele_of_succ_le_succ · checked external prerequisitedivision_remainder_exists · checked external prerequisitecontinued_fraction_empty_trace_existscontinued_fraction_trace_extend
Original expanded first-order statement 
forall B b. (exists gap. gap + b = B) -> forall a. (exists s h e l. (exists cf_gcd_bounded. ((((exists ff_h_cf_bounded_initial_state. ff_h_cf_bounded_initial_state + S (((cf_gcd_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_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_bounded_initial_state. h = ff_q_cf_bounded_initial_state * S ((S (0)) * e) + (((cf_gcd_bounded) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_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_bounded_terminal_state. ff_h_cf_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_bounded_terminal_state. h = ff_q_cf_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_bounded. (exists ff_lt_cf_bounded_index. ff_lt_cf_bounded_index + S cf_index_bounded = l) -> exists cf_old_a_bounded cf_old_b_bounded cf_tail_bounded cf_new_a_bounded cf_new_b_bounded cf_head_bounded cf_quotient_bounded. ((((exists ff_h_cf_bounded_previous_state. ff_h_cf_bounded_previous_state + S (((cf_old_a_bounded) + (((cf_old_b_bounded) + (cf_tail_bounded)) * S ((cf_old_b_bounded) + (cf_tail_bounded)) + ((cf_tail_bounded) + (cf_tail_bounded)))) * S ((cf_old_a_bounded) + (((cf_old_b_bounded) + (cf_tail_bounded)) * S ((cf_old_b_bounded) + (cf_tail_bounded)) + ((cf_tail_bounded) + (cf_tail_bounded)))) + ((((cf_old_b_bounded) + (cf_tail_bounded)) * S ((cf_old_b_bounded) + (cf_tail_bounded)) + ((cf_tail_bounded) + (cf_tail_bounded))) + (((cf_old_b_bounded) + (cf_tail_bounded)) * S ((cf_old_b_bounded) + (cf_tail_bounded)) + ((cf_tail_bounded) + (cf_tail_bounded))))) = S ((S (cf_index_bounded)) * e)) /\ exists ff_q_cf_bounded_previous_state. h = ff_q_cf_bounded_previous_state * S ((S (cf_index_bounded)) * e) + (((cf_old_a_bounded) + (((cf_old_b_bounded) + (cf_tail_bounded)) * S ((cf_old_b_bounded) + (cf_tail_bounded)) + ((cf_tail_bounded) + (cf_tail_bounded)))) * S ((cf_old_a_bounded) + (((cf_old_b_bounded) + (cf_tail_bounded)) * S ((cf_old_b_bounded) + (cf_tail_bounded)) + ((cf_tail_bounded) + (cf_tail_bounded)))) + ((((cf_old_b_bounded) + (cf_tail_bounded)) * S ((cf_old_b_bounded) + (cf_tail_bounded)) + ((cf_tail_bounded) + (cf_tail_bounded))) + (((cf_old_b_bounded) + (cf_tail_bounded)) * S ((cf_old_b_bounded) + (cf_tail_bounded)) + ((cf_tail_bounded) + (cf_tail_bounded))))))) /\ ((((exists ff_h_cf_bounded_following_state. ff_h_cf_bounded_following_state + S (((cf_new_a_bounded) + (((cf_new_b_bounded) + (cf_head_bounded)) * S ((cf_new_b_bounded) + (cf_head_bounded)) + ((cf_head_bounded) + (cf_head_bounded)))) * S ((cf_new_a_bounded) + (((cf_new_b_bounded) + (cf_head_bounded)) * S ((cf_new_b_bounded) + (cf_head_bounded)) + ((cf_head_bounded) + (cf_head_bounded)))) + ((((cf_new_b_bounded) + (cf_head_bounded)) * S ((cf_new_b_bounded) + (cf_head_bounded)) + ((cf_head_bounded) + (cf_head_bounded))) + (((cf_new_b_bounded) + (cf_head_bounded)) * S ((cf_new_b_bounded) + (cf_head_bounded)) + ((cf_head_bounded) + (cf_head_bounded))))) = S ((S (S cf_index_bounded)) * e)) /\ exists ff_q_cf_bounded_following_state. h = ff_q_cf_bounded_following_state * S ((S (S cf_index_bounded)) * e) + (((cf_new_a_bounded) + (((cf_new_b_bounded) + (cf_head_bounded)) * S ((cf_new_b_bounded) + (cf_head_bounded)) + ((cf_head_bounded) + (cf_head_bounded)))) * S ((cf_new_a_bounded) + (((cf_new_b_bounded) + (cf_head_bounded)) * S ((cf_new_b_bounded) + (cf_head_bounded)) + ((cf_head_bounded) + (cf_head_bounded)))) + ((((cf_new_b_bounded) + (cf_head_bounded)) * S ((cf_new_b_bounded) + (cf_head_bounded)) + ((cf_head_bounded) + (cf_head_bounded))) + (((cf_new_b_bounded) + (cf_head_bounded)) * S ((cf_new_b_bounded) + (cf_head_bounded)) + ((cf_head_bounded) + (cf_head_bounded))))))) /\ (cf_new_b_bounded = cf_old_a_bounded /\ (cf_new_a_bounded = cf_new_b_bounded * cf_quotient_bounded + cf_old_b_bounded /\ ((exists ff_lt_cf_bounded_remainder. ff_lt_cf_bounded_remainder + S cf_old_b_bounded = cf_new_b_bounded) /\ (cf_head_bounded = S ((cf_quotient_bounded + cf_tail_bounded) * S (cf_quotient_bounded + cf_tail_bounded) + (cf_tail_bounded + cf_tail_bounded))))))))))))

Complete unchanged native tactic proof

All 100 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

100 script commands · 26 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.

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 (2)
continued fraction empty trace existscontinued fraction trace extend

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
06Calculate and transport equalitiesL16–25

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

  1. L16
    rewrite hb0
  2. L17
    rewrite hb0
  3. L18
    rewrite hb0
  4. L19
    rewrite hb0
  5. L20
    rewrite hb0
  6. L21
    rewrite hb0
  7. L22
    rewrite hb0
  8. L23
    rewrite hb0
  9. L24
    rewrite hb0
  10. L25
    rewrite hb0
07Calculate and transport equalitiesL26–31

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

  1. L26
    rewrite hb0
  2. L27
    rewrite hb0
  3. L28
    rewrite hb0
  4. L29
    rewrite hb0
  5. L30
    rewrite hb0
  6. L31
    rewrite hb0
08Use earlier factsL32–32

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

  1. L32
    exact continued_fraction_empty_trace_exists_witness_witness
09Fix variables and assumptionsL33–35

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

  1. L33
    intro b
  2. L34
    intro hb
  3. L35
    intro a
10Use earlier factsL36–37

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

  1. L36
    specialize le_eq_or_lt b
  2. L37
    specialize le_eq_or_lt (S B)
11Establish hsplitL38–40

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

  1. L38
    have hsplit : b = S B \/ exists gap. gap + S b = S B
  2. L39
    apply le_eq_or_lt
  3. L40
    exact hb
12Separate the logical casesL41–41

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

  1. L41
    cases hsplit
13Establish hb0L42–48

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

  1. L42
    have hb0 : ~(b = 0)
  2. L43
    intro hzero
  3. L44
    apply PA1
  4. L45
    trans b
  5. L46
    symm
  6. L47
    exact hsplit_left
  7. L48
    exact hzero
14Establish hdivisionL49–51

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

  1. L49
    have hdivision : exists q r. a = b * q + r /\ exists gap. gap + S r = b
  2. L50
    apply division_remainder_exists
  3. L51
    exact hb0
15Separate the logical casesL52–54

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

  1. L52
    cases hdivision
  2. L53
    cases hdivision_witness
  3. L54
    cases hdivision_witness_witness
16Establish hrBL55–58

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

  1. L55
    have hrB : exists gap. gap + x1 = B
  2. L56
    apply le_of_succ_le_succ
  3. L57
    rewrite hsplit_left at hdivision_witness_witness_right
  4. L58
    exact hdivision_witness_witness_right
17Establish hsmallL59–60

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

  1. L59
    have hsmall : ∃ s. ∃ h. ∃ e. ∃ l. ContinuedFractionTrace(b,x1,s,h,e,l)Definitions: ContinuedFractionTraceOriginal native command in the exact edition
  2. L60
    specialize IH x1
18Establish hallL61–65

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

  1. L61
    have hall : ∀ z. ∃ x. ∃ y. ∃ n. ∃ m. ContinuedFractionTrace(z,x1,x,y,n,m)Definitions: ContinuedFractionTraceOriginal native command in the exact edition
  2. L62
    apply IH
  3. L63
    exact hrB
  4. L64
    specialize hall b
  5. L65
    exact hall
19Separate the logical casesL66–69

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

  1. L66
    cases hsmall
  2. L67
    cases hsmall_witness
  3. L68
    cases hsmall_witness_witness
  4. L69
    cases hsmall_witness_witness_witness
20Establish hextendL70–79

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

  1. L70
    have hextend : ∃ s. ∃ z. ∃ c. ListCell(s,x,x2) ∧ ContinuedFractionTrace(a,b,s,z,c,S x5)Definitions: ListCellContinuedFractionTraceOriginal native command in the exact edition
  2. L71
    specialize continued_fraction_trace_extend a
  3. L72
    specialize continued_fraction_trace_extend b
  4. L73
    specialize continued_fraction_trace_extend x
  5. L74
    specialize continued_fraction_trace_extend x1
  6. L75
    specialize continued_fraction_trace_extend x2
  7. L76
    specialize continued_fraction_trace_extend x3
  8. L77
    specialize continued_fraction_trace_extend x4
  9. L78
    specialize continued_fraction_trace_extend x5
  10. L79
    apply continued_fraction_trace_extend
21Use earlier factsL80–82

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

  1. L80
    exact hdivision_witness_witness_left
  2. L81
    exact hdivision_witness_witness_right
  3. L82
    exact hsmall_witness_witness_witness_witness
22Separate the logical casesL83–86

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

  1. L83
    cases hextend
  2. L84
    cases hextend_witness
  3. L85
    cases hextend_witness_witness
  4. L86
    cases hextend_witness_witness_witness
23Construct an explicit witnessL87–90

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

  1. L87
    exists x6
  2. L88
    exists x7
  3. L89
    exists x8
  4. L90
    exists S x5
24Use earlier factsL91–91

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

  1. L91
    exact hextend_witness_witness_witness_right
25Establish hbBL92–95

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

  1. L92
    have hbB : exists gap. gap + b = B
  2. L93
    apply le_of_succ_le_succ
  3. L94
    exact hsplit_right
  4. L95
    specialize IH b
26Establish hallL96–100

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

  1. L96
    have hall : ∀ z. ∃ x. ∃ y. ∃ n. ∃ m. ContinuedFractionTrace(z,b,x,y,n,m)Definitions: ContinuedFractionTraceOriginal native command in the exact edition
  2. L97
    apply IH
  3. L98
    exact hbB
  4. L99
    specialize hall a
  5. L100
    exact hall

Library-wide reading audit

Original defined command ledger · 100 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. 0016rewrite hb0
  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. 0032exact continued_fraction_empty_trace_exists_witness_witness
  33. 0033intro b
  34. 0034intro hb
  35. 0035intro a
  36. 0036specialize le_eq_or_lt b
  37. 0037specialize le_eq_or_lt (S B)
  38. 0038have hsplit : b = S B \/ exists gap. gap + S b = S B
  39. 0039apply le_eq_or_lt
  40. 0040exact hb
  41. 0041cases hsplit
  42. 0042have hb0 : ~(b = 0)
  43. 0043intro hzero
  44. 0044apply PA1
  45. 0045trans b
  46. 0046symm
  47. 0047exact hsplit_left
  48. 0048exact hzero
  49. 0049have hdivision : exists q r. a = b * q + r /\ exists gap. gap + S r = b
  50. 0050apply division_remainder_exists
  51. 0051exact hb0
  52. 0052cases hdivision
  53. 0053cases hdivision_witness
  54. 0054cases hdivision_witness_witness
  55. 0055have hrB : exists gap. gap + x1 = B
  56. 0056apply le_of_succ_le_succ
  57. 0057rewrite hsplit_left at hdivision_witness_witness_right
  58. 0058exact hdivision_witness_witness_right
  59. 0059have hsmall : exists s h e l. (exists cf_gcd_bounded_reduced. ((((exists ff_h_cf_bounded_reduced_initial_state. ff_h_cf_bounded_reduced_initial_state + S (((cf_gcd_bounded_reduced) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bounded_reduced) + (((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_bounded_reduced_initial_state. h = ff_q_cf_bounded_reduced_initial_state * S ((S (0)) * e) + (((cf_gcd_bounded_reduced) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bounded_reduced) + (((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_bounded_reduced_terminal_state. ff_h_cf_bounded_reduced_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_bounded_reduced_terminal_state. h = ff_q_cf_bounded_reduced_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_bounded_reduced. (exists ff_lt_cf_bounded_reduced_index. ff_lt_cf_bounded_reduced_index + S cf_index_bounded_reduced = l) -> exists cf_old_a_bounded_reduced cf_old_b_bounded_reduced cf_tail_bounded_reduced cf_new_a_bounded_reduced cf_new_b_bounded_reduced cf_head_bounded_reduced cf_quotient_bounded_reduced. ((((exists ff_h_cf_bounded_reduced_previous_state. ff_h_cf_bounded_reduced_previous_state + S (((cf_old_a_bounded_reduced) + (((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) * S ((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) + ((cf_tail_bounded_reduced) + (cf_tail_bounded_reduced)))) * S ((cf_old_a_bounded_reduced) + (((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) * S ((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) + ((cf_tail_bounded_reduced) + (cf_tail_bounded_reduced)))) + ((((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) * S ((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) + ((cf_tail_bounded_reduced) + (cf_tail_bounded_reduced))) + (((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) * S ((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) + ((cf_tail_bounded_reduced) + (cf_tail_bounded_reduced))))) = S ((S (cf_index_bounded_reduced)) * e)) /\ exists ff_q_cf_bounded_reduced_previous_state. h = ff_q_cf_bounded_reduced_previous_state * S ((S (cf_index_bounded_reduced)) * e) + (((cf_old_a_bounded_reduced) + (((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) * S ((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) + ((cf_tail_bounded_reduced) + (cf_tail_bounded_reduced)))) * S ((cf_old_a_bounded_reduced) + (((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) * S ((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) + ((cf_tail_bounded_reduced) + (cf_tail_bounded_reduced)))) + ((((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) * S ((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) + ((cf_tail_bounded_reduced) + (cf_tail_bounded_reduced))) + (((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) * S ((cf_old_b_bounded_reduced) + (cf_tail_bounded_reduced)) + ((cf_tail_bounded_reduced) + (cf_tail_bounded_reduced))))))) /\ ((((exists ff_h_cf_bounded_reduced_following_state. ff_h_cf_bounded_reduced_following_state + S (((cf_new_a_bounded_reduced) + (((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) * S ((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) + ((cf_head_bounded_reduced) + (cf_head_bounded_reduced)))) * S ((cf_new_a_bounded_reduced) + (((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) * S ((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) + ((cf_head_bounded_reduced) + (cf_head_bounded_reduced)))) + ((((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) * S ((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) + ((cf_head_bounded_reduced) + (cf_head_bounded_reduced))) + (((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) * S ((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) + ((cf_head_bounded_reduced) + (cf_head_bounded_reduced))))) = S ((S (S cf_index_bounded_reduced)) * e)) /\ exists ff_q_cf_bounded_reduced_following_state. h = ff_q_cf_bounded_reduced_following_state * S ((S (S cf_index_bounded_reduced)) * e) + (((cf_new_a_bounded_reduced) + (((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) * S ((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) + ((cf_head_bounded_reduced) + (cf_head_bounded_reduced)))) * S ((cf_new_a_bounded_reduced) + (((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) * S ((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) + ((cf_head_bounded_reduced) + (cf_head_bounded_reduced)))) + ((((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) * S ((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) + ((cf_head_bounded_reduced) + (cf_head_bounded_reduced))) + (((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) * S ((cf_new_b_bounded_reduced) + (cf_head_bounded_reduced)) + ((cf_head_bounded_reduced) + (cf_head_bounded_reduced))))))) /\ (cf_new_b_bounded_reduced = cf_old_a_bounded_reduced /\ (cf_new_a_bounded_reduced = cf_new_b_bounded_reduced * cf_quotient_bounded_reduced + cf_old_b_bounded_reduced /\ ((exists ff_lt_cf_bounded_reduced_remainder. ff_lt_cf_bounded_reduced_remainder + S cf_old_b_bounded_reduced = cf_new_b_bounded_reduced) /\ (cf_head_bounded_reduced = S ((cf_quotient_bounded_reduced + cf_tail_bounded_reduced) * S (cf_quotient_bounded_reduced + cf_tail_bounded_reduced) + (cf_tail_bounded_reduced + cf_tail_bounded_reduced)))))))))))
  60. 0060specialize IH x1
  61. 0061have hall : forall z. (exists s h e l. (exists cf_gcd_bounded_reduced_all. ((((exists ff_h_cf_bounded_reduced_all_initial_state. ff_h_cf_bounded_reduced_all_initial_state + S (((cf_gcd_bounded_reduced_all) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bounded_reduced_all) + (((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_bounded_reduced_all_initial_state. h = ff_q_cf_bounded_reduced_all_initial_state * S ((S (0)) * e) + (((cf_gcd_bounded_reduced_all) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bounded_reduced_all) + (((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_bounded_reduced_all_terminal_state. ff_h_cf_bounded_reduced_all_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_bounded_reduced_all_terminal_state. h = ff_q_cf_bounded_reduced_all_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_bounded_reduced_all. (exists ff_lt_cf_bounded_reduced_all_index. ff_lt_cf_bounded_reduced_all_index + S cf_index_bounded_reduced_all = l) -> exists cf_old_a_bounded_reduced_all cf_old_b_bounded_reduced_all cf_tail_bounded_reduced_all cf_new_a_bounded_reduced_all cf_new_b_bounded_reduced_all cf_head_bounded_reduced_all cf_quotient_bounded_reduced_all. ((((exists ff_h_cf_bounded_reduced_all_previous_state. ff_h_cf_bounded_reduced_all_previous_state + S (((cf_old_a_bounded_reduced_all) + (((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) * S ((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) + ((cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all)))) * S ((cf_old_a_bounded_reduced_all) + (((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) * S ((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) + ((cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all)))) + ((((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) * S ((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) + ((cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all))) + (((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) * S ((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) + ((cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all))))) = S ((S (cf_index_bounded_reduced_all)) * e)) /\ exists ff_q_cf_bounded_reduced_all_previous_state. h = ff_q_cf_bounded_reduced_all_previous_state * S ((S (cf_index_bounded_reduced_all)) * e) + (((cf_old_a_bounded_reduced_all) + (((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) * S ((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) + ((cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all)))) * S ((cf_old_a_bounded_reduced_all) + (((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) * S ((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) + ((cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all)))) + ((((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) * S ((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) + ((cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all))) + (((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) * S ((cf_old_b_bounded_reduced_all) + (cf_tail_bounded_reduced_all)) + ((cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all))))))) /\ ((((exists ff_h_cf_bounded_reduced_all_following_state. ff_h_cf_bounded_reduced_all_following_state + S (((cf_new_a_bounded_reduced_all) + (((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) * S ((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) + ((cf_head_bounded_reduced_all) + (cf_head_bounded_reduced_all)))) * S ((cf_new_a_bounded_reduced_all) + (((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) * S ((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) + ((cf_head_bounded_reduced_all) + (cf_head_bounded_reduced_all)))) + ((((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) * S ((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) + ((cf_head_bounded_reduced_all) + (cf_head_bounded_reduced_all))) + (((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) * S ((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) + ((cf_head_bounded_reduced_all) + (cf_head_bounded_reduced_all))))) = S ((S (S cf_index_bounded_reduced_all)) * e)) /\ exists ff_q_cf_bounded_reduced_all_following_state. h = ff_q_cf_bounded_reduced_all_following_state * S ((S (S cf_index_bounded_reduced_all)) * e) + (((cf_new_a_bounded_reduced_all) + (((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) * S ((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) + ((cf_head_bounded_reduced_all) + (cf_head_bounded_reduced_all)))) * S ((cf_new_a_bounded_reduced_all) + (((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) * S ((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) + ((cf_head_bounded_reduced_all) + (cf_head_bounded_reduced_all)))) + ((((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) * S ((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) + ((cf_head_bounded_reduced_all) + (cf_head_bounded_reduced_all))) + (((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) * S ((cf_new_b_bounded_reduced_all) + (cf_head_bounded_reduced_all)) + ((cf_head_bounded_reduced_all) + (cf_head_bounded_reduced_all))))))) /\ (cf_new_b_bounded_reduced_all = cf_old_a_bounded_reduced_all /\ (cf_new_a_bounded_reduced_all = cf_new_b_bounded_reduced_all * cf_quotient_bounded_reduced_all + cf_old_b_bounded_reduced_all /\ ((exists ff_lt_cf_bounded_reduced_all_remainder. ff_lt_cf_bounded_reduced_all_remainder + S cf_old_b_bounded_reduced_all = cf_new_b_bounded_reduced_all) /\ (cf_head_bounded_reduced_all = S ((cf_quotient_bounded_reduced_all + cf_tail_bounded_reduced_all) * S (cf_quotient_bounded_reduced_all + cf_tail_bounded_reduced_all) + (cf_tail_bounded_reduced_all + cf_tail_bounded_reduced_all))))))))))))
  62. 0062apply IH
  63. 0063exact hrB
  64. 0064specialize hall b
  65. 0065exact hall
  66. 0066cases hsmall
  67. 0067cases hsmall_witness
  68. 0068cases hsmall_witness_witness
  69. 0069cases hsmall_witness_witness_witness
  70. 0070have hextend : exists s z c. ((s = S ((x + x2) * S (x + x2) + (x2 + x2))) /\ (exists cf_gcd_bounded_extension. ((((exists ff_h_cf_bounded_extension_initial_state. ff_h_cf_bounded_extension_initial_state + S (((cf_gcd_bounded_extension) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bounded_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_bounded_extension_initial_state. z = ff_q_cf_bounded_extension_initial_state * S ((S (0)) * c) + (((cf_gcd_bounded_extension) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bounded_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_bounded_extension_terminal_state. ff_h_cf_bounded_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_bounded_extension_terminal_state. z = ff_q_cf_bounded_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_bounded_extension. (exists ff_lt_cf_bounded_extension_index. ff_lt_cf_bounded_extension_index + S cf_index_bounded_extension = S x5) -> exists cf_old_a_bounded_extension cf_old_b_bounded_extension cf_tail_bounded_extension cf_new_a_bounded_extension cf_new_b_bounded_extension cf_head_bounded_extension cf_quotient_bounded_extension. ((((exists ff_h_cf_bounded_extension_previous_state. ff_h_cf_bounded_extension_previous_state + S (((cf_old_a_bounded_extension) + (((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) * S ((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) + ((cf_tail_bounded_extension) + (cf_tail_bounded_extension)))) * S ((cf_old_a_bounded_extension) + (((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) * S ((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) + ((cf_tail_bounded_extension) + (cf_tail_bounded_extension)))) + ((((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) * S ((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) + ((cf_tail_bounded_extension) + (cf_tail_bounded_extension))) + (((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) * S ((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) + ((cf_tail_bounded_extension) + (cf_tail_bounded_extension))))) = S ((S (cf_index_bounded_extension)) * c)) /\ exists ff_q_cf_bounded_extension_previous_state. z = ff_q_cf_bounded_extension_previous_state * S ((S (cf_index_bounded_extension)) * c) + (((cf_old_a_bounded_extension) + (((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) * S ((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) + ((cf_tail_bounded_extension) + (cf_tail_bounded_extension)))) * S ((cf_old_a_bounded_extension) + (((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) * S ((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) + ((cf_tail_bounded_extension) + (cf_tail_bounded_extension)))) + ((((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) * S ((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) + ((cf_tail_bounded_extension) + (cf_tail_bounded_extension))) + (((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) * S ((cf_old_b_bounded_extension) + (cf_tail_bounded_extension)) + ((cf_tail_bounded_extension) + (cf_tail_bounded_extension))))))) /\ ((((exists ff_h_cf_bounded_extension_following_state. ff_h_cf_bounded_extension_following_state + S (((cf_new_a_bounded_extension) + (((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) * S ((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) + ((cf_head_bounded_extension) + (cf_head_bounded_extension)))) * S ((cf_new_a_bounded_extension) + (((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) * S ((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) + ((cf_head_bounded_extension) + (cf_head_bounded_extension)))) + ((((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) * S ((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) + ((cf_head_bounded_extension) + (cf_head_bounded_extension))) + (((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) * S ((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) + ((cf_head_bounded_extension) + (cf_head_bounded_extension))))) = S ((S (S cf_index_bounded_extension)) * c)) /\ exists ff_q_cf_bounded_extension_following_state. z = ff_q_cf_bounded_extension_following_state * S ((S (S cf_index_bounded_extension)) * c) + (((cf_new_a_bounded_extension) + (((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) * S ((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) + ((cf_head_bounded_extension) + (cf_head_bounded_extension)))) * S ((cf_new_a_bounded_extension) + (((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) * S ((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) + ((cf_head_bounded_extension) + (cf_head_bounded_extension)))) + ((((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) * S ((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) + ((cf_head_bounded_extension) + (cf_head_bounded_extension))) + (((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) * S ((cf_new_b_bounded_extension) + (cf_head_bounded_extension)) + ((cf_head_bounded_extension) + (cf_head_bounded_extension))))))) /\ (cf_new_b_bounded_extension = cf_old_a_bounded_extension /\ (cf_new_a_bounded_extension = cf_new_b_bounded_extension * cf_quotient_bounded_extension + cf_old_b_bounded_extension /\ ((exists ff_lt_cf_bounded_extension_remainder. ff_lt_cf_bounded_extension_remainder + S cf_old_b_bounded_extension = cf_new_b_bounded_extension) /\ (cf_head_bounded_extension = S ((cf_quotient_bounded_extension + cf_tail_bounded_extension) * S (cf_quotient_bounded_extension + cf_tail_bounded_extension) + (cf_tail_bounded_extension + cf_tail_bounded_extension))))))))))))
  71. 0071specialize continued_fraction_trace_extend a
  72. 0072specialize continued_fraction_trace_extend b
  73. 0073specialize continued_fraction_trace_extend x
  74. 0074specialize continued_fraction_trace_extend x1
  75. 0075specialize continued_fraction_trace_extend x2
  76. 0076specialize continued_fraction_trace_extend x3
  77. 0077specialize continued_fraction_trace_extend x4
  78. 0078specialize continued_fraction_trace_extend x5
  79. 0079apply continued_fraction_trace_extend
  80. 0080exact hdivision_witness_witness_left
  81. 0081exact hdivision_witness_witness_right
  82. 0082exact hsmall_witness_witness_witness_witness
  83. 0083cases hextend
  84. 0084cases hextend_witness
  85. 0085cases hextend_witness_witness
  86. 0086cases hextend_witness_witness_witness
  87. 0087exists x6
  88. 0088exists x7
  89. 0089exists x8
  90. 0090exists S x5
  91. 0091exact hextend_witness_witness_witness_right
  92. 0092have hbB : exists gap. gap + b = B
  93. 0093apply le_of_succ_le_succ
  94. 0094exact hsplit_right
  95. 0095specialize IH b
  96. 0096have hall : forall z. (exists s h e l. (exists cf_gcd_bounded_smaller_all. ((((exists ff_h_cf_bounded_smaller_all_initial_state. ff_h_cf_bounded_smaller_all_initial_state + S (((cf_gcd_bounded_smaller_all) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bounded_smaller_all) + (((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_bounded_smaller_all_initial_state. h = ff_q_cf_bounded_smaller_all_initial_state * S ((S (0)) * e) + (((cf_gcd_bounded_smaller_all) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_bounded_smaller_all) + (((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_bounded_smaller_all_terminal_state. ff_h_cf_bounded_smaller_all_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_bounded_smaller_all_terminal_state. h = ff_q_cf_bounded_smaller_all_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_bounded_smaller_all. (exists ff_lt_cf_bounded_smaller_all_index. ff_lt_cf_bounded_smaller_all_index + S cf_index_bounded_smaller_all = l) -> exists cf_old_a_bounded_smaller_all cf_old_b_bounded_smaller_all cf_tail_bounded_smaller_all cf_new_a_bounded_smaller_all cf_new_b_bounded_smaller_all cf_head_bounded_smaller_all cf_quotient_bounded_smaller_all. ((((exists ff_h_cf_bounded_smaller_all_previous_state. ff_h_cf_bounded_smaller_all_previous_state + S (((cf_old_a_bounded_smaller_all) + (((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) * S ((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) + ((cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all)))) * S ((cf_old_a_bounded_smaller_all) + (((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) * S ((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) + ((cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all)))) + ((((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) * S ((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) + ((cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all))) + (((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) * S ((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) + ((cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all))))) = S ((S (cf_index_bounded_smaller_all)) * e)) /\ exists ff_q_cf_bounded_smaller_all_previous_state. h = ff_q_cf_bounded_smaller_all_previous_state * S ((S (cf_index_bounded_smaller_all)) * e) + (((cf_old_a_bounded_smaller_all) + (((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) * S ((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) + ((cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all)))) * S ((cf_old_a_bounded_smaller_all) + (((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) * S ((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) + ((cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all)))) + ((((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) * S ((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) + ((cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all))) + (((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) * S ((cf_old_b_bounded_smaller_all) + (cf_tail_bounded_smaller_all)) + ((cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all))))))) /\ ((((exists ff_h_cf_bounded_smaller_all_following_state. ff_h_cf_bounded_smaller_all_following_state + S (((cf_new_a_bounded_smaller_all) + (((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) * S ((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) + ((cf_head_bounded_smaller_all) + (cf_head_bounded_smaller_all)))) * S ((cf_new_a_bounded_smaller_all) + (((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) * S ((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) + ((cf_head_bounded_smaller_all) + (cf_head_bounded_smaller_all)))) + ((((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) * S ((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) + ((cf_head_bounded_smaller_all) + (cf_head_bounded_smaller_all))) + (((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) * S ((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) + ((cf_head_bounded_smaller_all) + (cf_head_bounded_smaller_all))))) = S ((S (S cf_index_bounded_smaller_all)) * e)) /\ exists ff_q_cf_bounded_smaller_all_following_state. h = ff_q_cf_bounded_smaller_all_following_state * S ((S (S cf_index_bounded_smaller_all)) * e) + (((cf_new_a_bounded_smaller_all) + (((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) * S ((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) + ((cf_head_bounded_smaller_all) + (cf_head_bounded_smaller_all)))) * S ((cf_new_a_bounded_smaller_all) + (((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) * S ((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) + ((cf_head_bounded_smaller_all) + (cf_head_bounded_smaller_all)))) + ((((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) * S ((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) + ((cf_head_bounded_smaller_all) + (cf_head_bounded_smaller_all))) + (((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) * S ((cf_new_b_bounded_smaller_all) + (cf_head_bounded_smaller_all)) + ((cf_head_bounded_smaller_all) + (cf_head_bounded_smaller_all))))))) /\ (cf_new_b_bounded_smaller_all = cf_old_a_bounded_smaller_all /\ (cf_new_a_bounded_smaller_all = cf_new_b_bounded_smaller_all * cf_quotient_bounded_smaller_all + cf_old_b_bounded_smaller_all /\ ((exists ff_lt_cf_bounded_smaller_all_remainder. ff_lt_cf_bounded_smaller_all_remainder + S cf_old_b_bounded_smaller_all = cf_new_b_bounded_smaller_all) /\ (cf_head_bounded_smaller_all = S ((cf_quotient_bounded_smaller_all + cf_tail_bounded_smaller_all) * S (cf_quotient_bounded_smaller_all + cf_tail_bounded_smaller_all) + (cf_tail_bounded_smaller_all + cf_tail_bounded_smaller_all))))))))))))
  97. 0097apply IH
  98. 0098exact hbB
  99. 0099specialize hall a
  100. 0100exact hall