CF0007

continued_fraction_nonzero_divisor_exists

Every nonzero divisor produces a strictly positive trace length and a genuinely nonempty forward quotient list.

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

∀ a. ∀ b. ¬b = 0 → ∃ x. ∃ y. ∃ z. ∃ n. ¬x = 0 ∧ ContinuedFractionTrace(a,b,x,y,z,S n)

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

Definition DAG

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

Actual proof prerequisites

division_remainder_exists · checked external prerequisitecontinued_fraction_trace_existscontinued_fraction_trace_extendcell_nonzero · checked external prerequisite
Original expanded first-order statement 
forall a b. ~(b = 0) -> exists s h e k. (~(s = 0) /\ (exists cf_gcd_nonzero_result. ((((exists ff_h_cf_nonzero_result_initial_state. ff_h_cf_nonzero_result_initial_state + S (((cf_gcd_nonzero_result) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_nonzero_result) + (((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_nonzero_result_initial_state. h = ff_q_cf_nonzero_result_initial_state * S ((S (0)) * e) + (((cf_gcd_nonzero_result) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_nonzero_result) + (((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_nonzero_result_terminal_state. ff_h_cf_nonzero_result_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 k)) * e)) /\ exists ff_q_cf_nonzero_result_terminal_state. h = ff_q_cf_nonzero_result_terminal_state * S ((S (S k)) * 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_nonzero_result. (exists ff_lt_cf_nonzero_result_index. ff_lt_cf_nonzero_result_index + S cf_index_nonzero_result = S k) -> exists cf_old_a_nonzero_result cf_old_b_nonzero_result cf_tail_nonzero_result cf_new_a_nonzero_result cf_new_b_nonzero_result cf_head_nonzero_result cf_quotient_nonzero_result. ((((exists ff_h_cf_nonzero_result_previous_state. ff_h_cf_nonzero_result_previous_state + S (((cf_old_a_nonzero_result) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result)))) * S ((cf_old_a_nonzero_result) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result)))) + ((((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result))) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result))))) = S ((S (cf_index_nonzero_result)) * e)) /\ exists ff_q_cf_nonzero_result_previous_state. h = ff_q_cf_nonzero_result_previous_state * S ((S (cf_index_nonzero_result)) * e) + (((cf_old_a_nonzero_result) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result)))) * S ((cf_old_a_nonzero_result) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result)))) + ((((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result))) + (((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) * S ((cf_old_b_nonzero_result) + (cf_tail_nonzero_result)) + ((cf_tail_nonzero_result) + (cf_tail_nonzero_result))))))) /\ ((((exists ff_h_cf_nonzero_result_following_state. ff_h_cf_nonzero_result_following_state + S (((cf_new_a_nonzero_result) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result)))) * S ((cf_new_a_nonzero_result) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result)))) + ((((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result))) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result))))) = S ((S (S cf_index_nonzero_result)) * e)) /\ exists ff_q_cf_nonzero_result_following_state. h = ff_q_cf_nonzero_result_following_state * S ((S (S cf_index_nonzero_result)) * e) + (((cf_new_a_nonzero_result) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result)))) * S ((cf_new_a_nonzero_result) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result)))) + ((((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result))) + (((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) * S ((cf_new_b_nonzero_result) + (cf_head_nonzero_result)) + ((cf_head_nonzero_result) + (cf_head_nonzero_result))))))) /\ (cf_new_b_nonzero_result = cf_old_a_nonzero_result /\ (cf_new_a_nonzero_result = cf_new_b_nonzero_result * cf_quotient_nonzero_result + cf_old_b_nonzero_result /\ ((exists ff_lt_cf_nonzero_result_remainder. ff_lt_cf_nonzero_result_remainder + S cf_old_b_nonzero_result = cf_new_b_nonzero_result) /\ (cf_head_nonzero_result = S ((cf_quotient_nonzero_result + cf_tail_nonzero_result) * S (cf_quotient_nonzero_result + cf_tail_nonzero_result) + (cf_tail_nonzero_result + cf_tail_nonzero_result))))))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

49 script commands · 12 reading checkpoints · 3 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 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–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hb
02Establish hdivisionL4–8

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

  1. L4
    have hdivision : exists q r. a = b * q + r /\ exists gap. gap + S r = b
  2. L5
    specialize division_remainder_exists b
  3. L6
    specialize division_remainder_exists a
  4. L7
    apply division_remainder_exists
  5. L8
    exact hb
03Separate the logical casesL9–11

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

  1. L9
    cases hdivision
  2. L10
    cases hdivision_witness
  3. L11
    cases hdivision_witness_witness
04Establish htailL12–15

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

  1. L12
    have htail : ∃ s. ∃ h. ∃ e. ∃ l. ContinuedFractionTrace(b,x1,s,h,e,l)Definitions: ContinuedFractionTraceOriginal native command in the exact edition
  2. L13
    specialize continued_fraction_trace_exists b
  3. L14
    specialize continued_fraction_trace_exists x1
  4. L15
    exact continued_fraction_trace_exists
05Separate the logical casesL16–19

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

  1. L16
    cases htail
  2. L17
    cases htail_witness
  3. L18
    cases htail_witness_witness
  4. L19
    cases htail_witness_witness_witness
06Establish hextendL20–29

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

  1. L20
    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. L21
    specialize continued_fraction_trace_extend a
  3. L22
    specialize continued_fraction_trace_extend b
  4. L23
    specialize continued_fraction_trace_extend x
  5. L24
    specialize continued_fraction_trace_extend x1
  6. L25
    specialize continued_fraction_trace_extend x2
  7. L26
    specialize continued_fraction_trace_extend x3
  8. L27
    specialize continued_fraction_trace_extend x4
  9. L28
    specialize continued_fraction_trace_extend x5
  10. L29
    apply continued_fraction_trace_extend
07Use earlier factsL30–32

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

  1. L30
    exact hdivision_witness_witness_left
  2. L31
    exact hdivision_witness_witness_right
  3. L32
    exact htail_witness_witness_witness_witness
08Separate the logical casesL33–36

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

  1. L33
    cases hextend
  2. L34
    cases hextend_witness
  3. L35
    cases hextend_witness_witness
  4. L36
    cases hextend_witness_witness_witness
09Construct an explicit witnessL37–40

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

  1. L37
    exists x6
  2. L38
    exists x7
  3. L39
    exists x8
  4. L40
    exists x5
10Separate the logical casesL41–41

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

  1. L41
    split
11Fix variables and assumptionsL42–42

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

  1. L42
    intro hzero
12Use earlier factsL43–49

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

  1. L43
    specialize cell_nonzero x6
  2. L44
    specialize cell_nonzero x
  3. L45
    specialize cell_nonzero x2
  4. L46
    apply cell_nonzero
  5. L47
    exact hextend_witness_witness_witness_left
  6. L48
    exact hzero
  7. L49
    exact hextend_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hb
  4. 0004have hdivision : exists q r. a = b * q + r /\ exists gap. gap + S r = b
  5. 0005specialize division_remainder_exists b
  6. 0006specialize division_remainder_exists a
  7. 0007apply division_remainder_exists
  8. 0008exact hb
  9. 0009cases hdivision
  10. 0010cases hdivision_witness
  11. 0011cases hdivision_witness_witness
  12. 0012have htail : exists s h e l. (exists cf_gcd_nonzero_tail. ((((exists ff_h_cf_nonzero_tail_initial_state. ff_h_cf_nonzero_tail_initial_state + S (((cf_gcd_nonzero_tail) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_nonzero_tail) + (((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_nonzero_tail_initial_state. h = ff_q_cf_nonzero_tail_initial_state * S ((S (0)) * e) + (((cf_gcd_nonzero_tail) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_nonzero_tail) + (((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_nonzero_tail_terminal_state. ff_h_cf_nonzero_tail_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_nonzero_tail_terminal_state. h = ff_q_cf_nonzero_tail_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_nonzero_tail. (exists ff_lt_cf_nonzero_tail_index. ff_lt_cf_nonzero_tail_index + S cf_index_nonzero_tail = l) -> exists cf_old_a_nonzero_tail cf_old_b_nonzero_tail cf_tail_nonzero_tail cf_new_a_nonzero_tail cf_new_b_nonzero_tail cf_head_nonzero_tail cf_quotient_nonzero_tail. ((((exists ff_h_cf_nonzero_tail_previous_state. ff_h_cf_nonzero_tail_previous_state + S (((cf_old_a_nonzero_tail) + (((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) * S ((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) + ((cf_tail_nonzero_tail) + (cf_tail_nonzero_tail)))) * S ((cf_old_a_nonzero_tail) + (((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) * S ((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) + ((cf_tail_nonzero_tail) + (cf_tail_nonzero_tail)))) + ((((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) * S ((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) + ((cf_tail_nonzero_tail) + (cf_tail_nonzero_tail))) + (((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) * S ((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) + ((cf_tail_nonzero_tail) + (cf_tail_nonzero_tail))))) = S ((S (cf_index_nonzero_tail)) * e)) /\ exists ff_q_cf_nonzero_tail_previous_state. h = ff_q_cf_nonzero_tail_previous_state * S ((S (cf_index_nonzero_tail)) * e) + (((cf_old_a_nonzero_tail) + (((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) * S ((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) + ((cf_tail_nonzero_tail) + (cf_tail_nonzero_tail)))) * S ((cf_old_a_nonzero_tail) + (((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) * S ((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) + ((cf_tail_nonzero_tail) + (cf_tail_nonzero_tail)))) + ((((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) * S ((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) + ((cf_tail_nonzero_tail) + (cf_tail_nonzero_tail))) + (((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) * S ((cf_old_b_nonzero_tail) + (cf_tail_nonzero_tail)) + ((cf_tail_nonzero_tail) + (cf_tail_nonzero_tail))))))) /\ ((((exists ff_h_cf_nonzero_tail_following_state. ff_h_cf_nonzero_tail_following_state + S (((cf_new_a_nonzero_tail) + (((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) * S ((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) + ((cf_head_nonzero_tail) + (cf_head_nonzero_tail)))) * S ((cf_new_a_nonzero_tail) + (((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) * S ((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) + ((cf_head_nonzero_tail) + (cf_head_nonzero_tail)))) + ((((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) * S ((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) + ((cf_head_nonzero_tail) + (cf_head_nonzero_tail))) + (((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) * S ((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) + ((cf_head_nonzero_tail) + (cf_head_nonzero_tail))))) = S ((S (S cf_index_nonzero_tail)) * e)) /\ exists ff_q_cf_nonzero_tail_following_state. h = ff_q_cf_nonzero_tail_following_state * S ((S (S cf_index_nonzero_tail)) * e) + (((cf_new_a_nonzero_tail) + (((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) * S ((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) + ((cf_head_nonzero_tail) + (cf_head_nonzero_tail)))) * S ((cf_new_a_nonzero_tail) + (((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) * S ((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) + ((cf_head_nonzero_tail) + (cf_head_nonzero_tail)))) + ((((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) * S ((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) + ((cf_head_nonzero_tail) + (cf_head_nonzero_tail))) + (((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) * S ((cf_new_b_nonzero_tail) + (cf_head_nonzero_tail)) + ((cf_head_nonzero_tail) + (cf_head_nonzero_tail))))))) /\ (cf_new_b_nonzero_tail = cf_old_a_nonzero_tail /\ (cf_new_a_nonzero_tail = cf_new_b_nonzero_tail * cf_quotient_nonzero_tail + cf_old_b_nonzero_tail /\ ((exists ff_lt_cf_nonzero_tail_remainder. ff_lt_cf_nonzero_tail_remainder + S cf_old_b_nonzero_tail = cf_new_b_nonzero_tail) /\ (cf_head_nonzero_tail = S ((cf_quotient_nonzero_tail + cf_tail_nonzero_tail) * S (cf_quotient_nonzero_tail + cf_tail_nonzero_tail) + (cf_tail_nonzero_tail + cf_tail_nonzero_tail)))))))))))
  13. 0013specialize continued_fraction_trace_exists b
  14. 0014specialize continued_fraction_trace_exists x1
  15. 0015exact continued_fraction_trace_exists
  16. 0016cases htail
  17. 0017cases htail_witness
  18. 0018cases htail_witness_witness
  19. 0019cases htail_witness_witness_witness
  20. 0020have hextend : exists s z c. ((s = S ((x + x2) * S (x + x2) + (x2 + x2))) /\ (exists cf_gcd_nonzero_extension. ((((exists ff_h_cf_nonzero_extension_initial_state. ff_h_cf_nonzero_extension_initial_state + S (((cf_gcd_nonzero_extension) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_nonzero_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_nonzero_extension_initial_state. z = ff_q_cf_nonzero_extension_initial_state * S ((S (0)) * c) + (((cf_gcd_nonzero_extension) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_nonzero_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_nonzero_extension_terminal_state. ff_h_cf_nonzero_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_nonzero_extension_terminal_state. z = ff_q_cf_nonzero_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_nonzero_extension. (exists ff_lt_cf_nonzero_extension_index. ff_lt_cf_nonzero_extension_index + S cf_index_nonzero_extension = S x5) -> exists cf_old_a_nonzero_extension cf_old_b_nonzero_extension cf_tail_nonzero_extension cf_new_a_nonzero_extension cf_new_b_nonzero_extension cf_head_nonzero_extension cf_quotient_nonzero_extension. ((((exists ff_h_cf_nonzero_extension_previous_state. ff_h_cf_nonzero_extension_previous_state + S (((cf_old_a_nonzero_extension) + (((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) * S ((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) + ((cf_tail_nonzero_extension) + (cf_tail_nonzero_extension)))) * S ((cf_old_a_nonzero_extension) + (((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) * S ((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) + ((cf_tail_nonzero_extension) + (cf_tail_nonzero_extension)))) + ((((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) * S ((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) + ((cf_tail_nonzero_extension) + (cf_tail_nonzero_extension))) + (((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) * S ((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) + ((cf_tail_nonzero_extension) + (cf_tail_nonzero_extension))))) = S ((S (cf_index_nonzero_extension)) * c)) /\ exists ff_q_cf_nonzero_extension_previous_state. z = ff_q_cf_nonzero_extension_previous_state * S ((S (cf_index_nonzero_extension)) * c) + (((cf_old_a_nonzero_extension) + (((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) * S ((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) + ((cf_tail_nonzero_extension) + (cf_tail_nonzero_extension)))) * S ((cf_old_a_nonzero_extension) + (((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) * S ((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) + ((cf_tail_nonzero_extension) + (cf_tail_nonzero_extension)))) + ((((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) * S ((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) + ((cf_tail_nonzero_extension) + (cf_tail_nonzero_extension))) + (((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) * S ((cf_old_b_nonzero_extension) + (cf_tail_nonzero_extension)) + ((cf_tail_nonzero_extension) + (cf_tail_nonzero_extension))))))) /\ ((((exists ff_h_cf_nonzero_extension_following_state. ff_h_cf_nonzero_extension_following_state + S (((cf_new_a_nonzero_extension) + (((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) * S ((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) + ((cf_head_nonzero_extension) + (cf_head_nonzero_extension)))) * S ((cf_new_a_nonzero_extension) + (((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) * S ((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) + ((cf_head_nonzero_extension) + (cf_head_nonzero_extension)))) + ((((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) * S ((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) + ((cf_head_nonzero_extension) + (cf_head_nonzero_extension))) + (((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) * S ((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) + ((cf_head_nonzero_extension) + (cf_head_nonzero_extension))))) = S ((S (S cf_index_nonzero_extension)) * c)) /\ exists ff_q_cf_nonzero_extension_following_state. z = ff_q_cf_nonzero_extension_following_state * S ((S (S cf_index_nonzero_extension)) * c) + (((cf_new_a_nonzero_extension) + (((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) * S ((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) + ((cf_head_nonzero_extension) + (cf_head_nonzero_extension)))) * S ((cf_new_a_nonzero_extension) + (((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) * S ((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) + ((cf_head_nonzero_extension) + (cf_head_nonzero_extension)))) + ((((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) * S ((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) + ((cf_head_nonzero_extension) + (cf_head_nonzero_extension))) + (((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) * S ((cf_new_b_nonzero_extension) + (cf_head_nonzero_extension)) + ((cf_head_nonzero_extension) + (cf_head_nonzero_extension))))))) /\ (cf_new_b_nonzero_extension = cf_old_a_nonzero_extension /\ (cf_new_a_nonzero_extension = cf_new_b_nonzero_extension * cf_quotient_nonzero_extension + cf_old_b_nonzero_extension /\ ((exists ff_lt_cf_nonzero_extension_remainder. ff_lt_cf_nonzero_extension_remainder + S cf_old_b_nonzero_extension = cf_new_b_nonzero_extension) /\ (cf_head_nonzero_extension = S ((cf_quotient_nonzero_extension + cf_tail_nonzero_extension) * S (cf_quotient_nonzero_extension + cf_tail_nonzero_extension) + (cf_tail_nonzero_extension + cf_tail_nonzero_extension))))))))))))
  21. 0021specialize continued_fraction_trace_extend a
  22. 0022specialize continued_fraction_trace_extend b
  23. 0023specialize continued_fraction_trace_extend x
  24. 0024specialize continued_fraction_trace_extend x1
  25. 0025specialize continued_fraction_trace_extend x2
  26. 0026specialize continued_fraction_trace_extend x3
  27. 0027specialize continued_fraction_trace_extend x4
  28. 0028specialize continued_fraction_trace_extend x5
  29. 0029apply continued_fraction_trace_extend
  30. 0030exact hdivision_witness_witness_left
  31. 0031exact hdivision_witness_witness_right
  32. 0032exact htail_witness_witness_witness_witness
  33. 0033cases hextend
  34. 0034cases hextend_witness
  35. 0035cases hextend_witness_witness
  36. 0036cases hextend_witness_witness_witness
  37. 0037exists x6
  38. 0038exists x7
  39. 0039exists x8
  40. 0040exists x5
  41. 0041split
  42. 0042intro hzero
  43. 0043specialize cell_nonzero x6
  44. 0044specialize cell_nonzero x
  45. 0045specialize cell_nonzero x2
  46. 0046apply cell_nonzero
  47. 0047exact hextend_witness_witness_witness_left
  48. 0048exact hzero
  49. 0049exact hextend_witness_witness_witness_right