EL0006

euclidean_log_budget_extend

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

One actual strict Euclidean division extends a genuine bounded beta-history by exactly one step.

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 a b q r B. ((a = b * q + r /\ (exists ff_lt_ec_elb_first_division. ff_lt_ec_elb_first_division + S r = b))) -> (exists elb_list_reduced elb_history_reduced elb_scale_reduced elb_steps_reduced. ((exists cf_gcd_elb_reduced_budget. ((((exists ff_h_cf_elb_reduced_budget_initial_state. ff_h_cf_elb_reduced_budget_initial_state + S (((cf_gcd_elb_reduced_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_reduced_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_reduced)) /\ exists ff_q_cf_elb_reduced_budget_initial_state. elb_history_reduced = ff_q_cf_elb_reduced_budget_initial_state * S ((S (0)) * elb_scale_reduced) + (((cf_gcd_elb_reduced_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_reduced_budget) + (((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_elb_reduced_budget_terminal_state. ff_h_cf_elb_reduced_budget_terminal_state + S (((b) + (((r) + (elb_list_reduced)) * S ((r) + (elb_list_reduced)) + ((elb_list_reduced) + (elb_list_reduced)))) * S ((b) + (((r) + (elb_list_reduced)) * S ((r) + (elb_list_reduced)) + ((elb_list_reduced) + (elb_list_reduced)))) + ((((r) + (elb_list_reduced)) * S ((r) + (elb_list_reduced)) + ((elb_list_reduced) + (elb_list_reduced))) + (((r) + (elb_list_reduced)) * S ((r) + (elb_list_reduced)) + ((elb_list_reduced) + (elb_list_reduced))))) = S ((S (elb_steps_reduced)) * elb_scale_reduced)) /\ exists ff_q_cf_elb_reduced_budget_terminal_state. elb_history_reduced = ff_q_cf_elb_reduced_budget_terminal_state * S ((S (elb_steps_reduced)) * elb_scale_reduced) + (((b) + (((r) + (elb_list_reduced)) * S ((r) + (elb_list_reduced)) + ((elb_list_reduced) + (elb_list_reduced)))) * S ((b) + (((r) + (elb_list_reduced)) * S ((r) + (elb_list_reduced)) + ((elb_list_reduced) + (elb_list_reduced)))) + ((((r) + (elb_list_reduced)) * S ((r) + (elb_list_reduced)) + ((elb_list_reduced) + (elb_list_reduced))) + (((r) + (elb_list_reduced)) * S ((r) + (elb_list_reduced)) + ((elb_list_reduced) + (elb_list_reduced))))))) /\ forall cf_index_elb_reduced_budget. (exists ff_lt_cf_elb_reduced_budget_index. ff_lt_cf_elb_reduced_budget_index + S cf_index_elb_reduced_budget = elb_steps_reduced) -> exists cf_old_a_elb_reduced_budget cf_old_b_elb_reduced_budget cf_tail_elb_reduced_budget cf_new_a_elb_reduced_budget cf_new_b_elb_reduced_budget cf_head_elb_reduced_budget cf_quotient_elb_reduced_budget. ((((exists ff_h_cf_elb_reduced_budget_previous_state. ff_h_cf_elb_reduced_budget_previous_state + S (((cf_old_a_elb_reduced_budget) + (((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) * S ((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) + ((cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget)))) * S ((cf_old_a_elb_reduced_budget) + (((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) * S ((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) + ((cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget)))) + ((((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) * S ((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) + ((cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget))) + (((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) * S ((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) + ((cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget))))) = S ((S (cf_index_elb_reduced_budget)) * elb_scale_reduced)) /\ exists ff_q_cf_elb_reduced_budget_previous_state. elb_history_reduced = ff_q_cf_elb_reduced_budget_previous_state * S ((S (cf_index_elb_reduced_budget)) * elb_scale_reduced) + (((cf_old_a_elb_reduced_budget) + (((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) * S ((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) + ((cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget)))) * S ((cf_old_a_elb_reduced_budget) + (((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) * S ((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) + ((cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget)))) + ((((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) * S ((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) + ((cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget))) + (((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) * S ((cf_old_b_elb_reduced_budget) + (cf_tail_elb_reduced_budget)) + ((cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget))))))) /\ ((((exists ff_h_cf_elb_reduced_budget_following_state. ff_h_cf_elb_reduced_budget_following_state + S (((cf_new_a_elb_reduced_budget) + (((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) * S ((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) + ((cf_head_elb_reduced_budget) + (cf_head_elb_reduced_budget)))) * S ((cf_new_a_elb_reduced_budget) + (((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) * S ((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) + ((cf_head_elb_reduced_budget) + (cf_head_elb_reduced_budget)))) + ((((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) * S ((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) + ((cf_head_elb_reduced_budget) + (cf_head_elb_reduced_budget))) + (((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) * S ((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) + ((cf_head_elb_reduced_budget) + (cf_head_elb_reduced_budget))))) = S ((S (S cf_index_elb_reduced_budget)) * elb_scale_reduced)) /\ exists ff_q_cf_elb_reduced_budget_following_state. elb_history_reduced = ff_q_cf_elb_reduced_budget_following_state * S ((S (S cf_index_elb_reduced_budget)) * elb_scale_reduced) + (((cf_new_a_elb_reduced_budget) + (((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) * S ((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) + ((cf_head_elb_reduced_budget) + (cf_head_elb_reduced_budget)))) * S ((cf_new_a_elb_reduced_budget) + (((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) * S ((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) + ((cf_head_elb_reduced_budget) + (cf_head_elb_reduced_budget)))) + ((((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) * S ((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) + ((cf_head_elb_reduced_budget) + (cf_head_elb_reduced_budget))) + (((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) * S ((cf_new_b_elb_reduced_budget) + (cf_head_elb_reduced_budget)) + ((cf_head_elb_reduced_budget) + (cf_head_elb_reduced_budget))))))) /\ (cf_new_b_elb_reduced_budget = cf_old_a_elb_reduced_budget /\ (cf_new_a_elb_reduced_budget = cf_new_b_elb_reduced_budget * cf_quotient_elb_reduced_budget + cf_old_b_elb_reduced_budget /\ ((exists ff_lt_cf_elb_reduced_budget_remainder. ff_lt_cf_elb_reduced_budget_remainder + S cf_old_b_elb_reduced_budget = cf_new_b_elb_reduced_budget) /\ (cf_head_elb_reduced_budget = S ((cf_quotient_elb_reduced_budget + cf_tail_elb_reduced_budget) * S (cf_quotient_elb_reduced_budget + cf_tail_elb_reduced_budget) + (cf_tail_elb_reduced_budget + cf_tail_elb_reduced_budget))))))))))) /\ exists elb_gap_reduced. elb_gap_reduced + elb_steps_reduced = (B))) -> (exists elb_list_extended elb_history_extended elb_scale_extended elb_steps_extended. ((exists cf_gcd_elb_extended_budget. ((((exists ff_h_cf_elb_extended_budget_initial_state. ff_h_cf_elb_extended_budget_initial_state + S (((cf_gcd_elb_extended_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_extended_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * elb_scale_extended)) /\ exists ff_q_cf_elb_extended_budget_initial_state. elb_history_extended = ff_q_cf_elb_extended_budget_initial_state * S ((S (0)) * elb_scale_extended) + (((cf_gcd_elb_extended_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_extended_budget) + (((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_elb_extended_budget_terminal_state. ff_h_cf_elb_extended_budget_terminal_state + S (((a) + (((b) + (elb_list_extended)) * S ((b) + (elb_list_extended)) + ((elb_list_extended) + (elb_list_extended)))) * S ((a) + (((b) + (elb_list_extended)) * S ((b) + (elb_list_extended)) + ((elb_list_extended) + (elb_list_extended)))) + ((((b) + (elb_list_extended)) * S ((b) + (elb_list_extended)) + ((elb_list_extended) + (elb_list_extended))) + (((b) + (elb_list_extended)) * S ((b) + (elb_list_extended)) + ((elb_list_extended) + (elb_list_extended))))) = S ((S (elb_steps_extended)) * elb_scale_extended)) /\ exists ff_q_cf_elb_extended_budget_terminal_state. elb_history_extended = ff_q_cf_elb_extended_budget_terminal_state * S ((S (elb_steps_extended)) * elb_scale_extended) + (((a) + (((b) + (elb_list_extended)) * S ((b) + (elb_list_extended)) + ((elb_list_extended) + (elb_list_extended)))) * S ((a) + (((b) + (elb_list_extended)) * S ((b) + (elb_list_extended)) + ((elb_list_extended) + (elb_list_extended)))) + ((((b) + (elb_list_extended)) * S ((b) + (elb_list_extended)) + ((elb_list_extended) + (elb_list_extended))) + (((b) + (elb_list_extended)) * S ((b) + (elb_list_extended)) + ((elb_list_extended) + (elb_list_extended))))))) /\ forall cf_index_elb_extended_budget. (exists ff_lt_cf_elb_extended_budget_index. ff_lt_cf_elb_extended_budget_index + S cf_index_elb_extended_budget = elb_steps_extended) -> exists cf_old_a_elb_extended_budget cf_old_b_elb_extended_budget cf_tail_elb_extended_budget cf_new_a_elb_extended_budget cf_new_b_elb_extended_budget cf_head_elb_extended_budget cf_quotient_elb_extended_budget. ((((exists ff_h_cf_elb_extended_budget_previous_state. ff_h_cf_elb_extended_budget_previous_state + S (((cf_old_a_elb_extended_budget) + (((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) * S ((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) + ((cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget)))) * S ((cf_old_a_elb_extended_budget) + (((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) * S ((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) + ((cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget)))) + ((((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) * S ((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) + ((cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget))) + (((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) * S ((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) + ((cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget))))) = S ((S (cf_index_elb_extended_budget)) * elb_scale_extended)) /\ exists ff_q_cf_elb_extended_budget_previous_state. elb_history_extended = ff_q_cf_elb_extended_budget_previous_state * S ((S (cf_index_elb_extended_budget)) * elb_scale_extended) + (((cf_old_a_elb_extended_budget) + (((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) * S ((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) + ((cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget)))) * S ((cf_old_a_elb_extended_budget) + (((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) * S ((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) + ((cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget)))) + ((((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) * S ((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) + ((cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget))) + (((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) * S ((cf_old_b_elb_extended_budget) + (cf_tail_elb_extended_budget)) + ((cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget))))))) /\ ((((exists ff_h_cf_elb_extended_budget_following_state. ff_h_cf_elb_extended_budget_following_state + S (((cf_new_a_elb_extended_budget) + (((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) * S ((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) + ((cf_head_elb_extended_budget) + (cf_head_elb_extended_budget)))) * S ((cf_new_a_elb_extended_budget) + (((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) * S ((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) + ((cf_head_elb_extended_budget) + (cf_head_elb_extended_budget)))) + ((((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) * S ((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) + ((cf_head_elb_extended_budget) + (cf_head_elb_extended_budget))) + (((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) * S ((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) + ((cf_head_elb_extended_budget) + (cf_head_elb_extended_budget))))) = S ((S (S cf_index_elb_extended_budget)) * elb_scale_extended)) /\ exists ff_q_cf_elb_extended_budget_following_state. elb_history_extended = ff_q_cf_elb_extended_budget_following_state * S ((S (S cf_index_elb_extended_budget)) * elb_scale_extended) + (((cf_new_a_elb_extended_budget) + (((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) * S ((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) + ((cf_head_elb_extended_budget) + (cf_head_elb_extended_budget)))) * S ((cf_new_a_elb_extended_budget) + (((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) * S ((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) + ((cf_head_elb_extended_budget) + (cf_head_elb_extended_budget)))) + ((((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) * S ((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) + ((cf_head_elb_extended_budget) + (cf_head_elb_extended_budget))) + (((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) * S ((cf_new_b_elb_extended_budget) + (cf_head_elb_extended_budget)) + ((cf_head_elb_extended_budget) + (cf_head_elb_extended_budget))))))) /\ (cf_new_b_elb_extended_budget = cf_old_a_elb_extended_budget /\ (cf_new_a_elb_extended_budget = cf_new_b_elb_extended_budget * cf_quotient_elb_extended_budget + cf_old_b_elb_extended_budget /\ ((exists ff_lt_cf_elb_extended_budget_remainder. ff_lt_cf_elb_extended_budget_remainder + S cf_old_b_elb_extended_budget = cf_new_b_elb_extended_budget) /\ (cf_head_elb_extended_budget = S ((cf_quotient_elb_extended_budget + cf_tail_elb_extended_budget) * S (cf_quotient_elb_extended_budget + cf_tail_elb_extended_budget) + (cf_tail_elb_extended_budget + cf_tail_elb_extended_budget))))))))))) /\ exists elb_gap_extended. elb_gap_extended + elb_steps_extended = (S B)))

Constructive proof overview

Generated structural guide

One actual strict Euclidean division extends a genuine bounded beta-history by exactly one step.

The unchanged tactic script uses 2 declared prerequisites and contains 40 exact native proof lines.

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

Proof neighborhood

Direct dependencies

continued_fraction_trace_extend Alpha theorem; checked-use authorized succ_le_succ Stable theorem; checked-use authorized

Direct dependents

EL0007 euclidean_log_budget_extend_twice EL000C euclidean_log_trace_below_power

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

40 script commands · 8 reading checkpoints · 1 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.

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–7

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro B
  6. L6
    intro hdivision
  7. L7
    intro htrace
02Separate the logical casesL8–13

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

  1. L8
    cases hdivision
  2. L9
    cases htrace
  3. L10
    cases htrace_witness
  4. L11
    cases htrace_witness_witness
  5. L12
    cases htrace_witness_witness_witness
  6. L13
    cases htrace_witness_witness_witness_witness
03Use earlier factsL14–21

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

  1. L14
    specialize continued_fraction_trace_extend a
  2. L15
    specialize continued_fraction_trace_extend b
  3. L16
    specialize continued_fraction_trace_extend q
  4. L17
    specialize continued_fraction_trace_extend r
  5. L18
    specialize continued_fraction_trace_extend x
  6. L19
    specialize continued_fraction_trace_extend x1
  7. L20
    specialize continued_fraction_trace_extend x2
  8. L21
    specialize continued_fraction_trace_extend x3
04Establish hextensionL22–26

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

  1. L22
    have hextension : ∃ s. ∃ z. ∃ c. ListCell(s,q,x) ∧ ContinuedFractionTrace(a,b,s,z,c,S x3)Definitions: ListCellContinuedFractionTrace
  2. L23
    apply continued_fraction_trace_extend
  3. L24
    exact hdivision_left
  4. L25
    exact hdivision_right
  5. L26
    exact htrace_witness_witness_witness_witness_left
05Separate the logical casesL27–30

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

  1. L27
    cases hextension
  2. L28
    cases hextension_witness
  3. L29
    cases hextension_witness_witness
  4. L30
    cases hextension_witness_witness_witness
06Construct an explicit witnessL31–34

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

  1. L31
    exists x4
  2. L32
    exists x5
  3. L33
    exists x6
  4. L34
    exists S x3
07Separate the logical casesL35–35

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

  1. L35
    split
08Use earlier factsL36–40

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

  1. L36
    exact hextension_witness_witness_witness_right
  2. L37
    specialize succ_le_succ x3
  3. L38
    specialize succ_le_succ B
  4. L39
    apply succ_le_succ
  5. L40
    exact htrace_witness_witness_witness_witness_right

Library-wide reading audit

Original exact command ledger · 40 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro B
  6. 0006intro hdivision
  7. 0007intro htrace
  8. 0008cases hdivision
  9. 0009cases htrace
  10. 0010cases htrace_witness
  11. 0011cases htrace_witness_witness
  12. 0012cases htrace_witness_witness_witness
  13. 0013cases htrace_witness_witness_witness_witness
  14. 0014specialize continued_fraction_trace_extend a
  15. 0015specialize continued_fraction_trace_extend b
  16. 0016specialize continued_fraction_trace_extend q
  17. 0017specialize continued_fraction_trace_extend r
  18. 0018specialize continued_fraction_trace_extend x
  19. 0019specialize continued_fraction_trace_extend x1
  20. 0020specialize continued_fraction_trace_extend x2
  21. 0021specialize continued_fraction_trace_extend x3
  22. 0022have hextension : exists s z c. ((s = S ((q + x) * S (q + x) + (x + x))) /\ (exists cf_gcd_elb_extend_have. ((((exists ff_h_cf_elb_extend_have_initial_state. ff_h_cf_elb_extend_have_initial_state + S (((cf_gcd_elb_extend_have) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_extend_have) + (((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_elb_extend_have_initial_state. z = ff_q_cf_elb_extend_have_initial_state * S ((S (0)) * c) + (((cf_gcd_elb_extend_have) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_extend_have) + (((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_elb_extend_have_terminal_state. ff_h_cf_elb_extend_have_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 x3)) * c)) /\ exists ff_q_cf_elb_extend_have_terminal_state. z = ff_q_cf_elb_extend_have_terminal_state * S ((S (S x3)) * 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_elb_extend_have. (exists ff_lt_cf_elb_extend_have_index. ff_lt_cf_elb_extend_have_index + S cf_index_elb_extend_have = S x3) -> exists cf_old_a_elb_extend_have cf_old_b_elb_extend_have cf_tail_elb_extend_have cf_new_a_elb_extend_have cf_new_b_elb_extend_have cf_head_elb_extend_have cf_quotient_elb_extend_have. ((((exists ff_h_cf_elb_extend_have_previous_state. ff_h_cf_elb_extend_have_previous_state + S (((cf_old_a_elb_extend_have) + (((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) * S ((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) + ((cf_tail_elb_extend_have) + (cf_tail_elb_extend_have)))) * S ((cf_old_a_elb_extend_have) + (((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) * S ((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) + ((cf_tail_elb_extend_have) + (cf_tail_elb_extend_have)))) + ((((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) * S ((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) + ((cf_tail_elb_extend_have) + (cf_tail_elb_extend_have))) + (((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) * S ((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) + ((cf_tail_elb_extend_have) + (cf_tail_elb_extend_have))))) = S ((S (cf_index_elb_extend_have)) * c)) /\ exists ff_q_cf_elb_extend_have_previous_state. z = ff_q_cf_elb_extend_have_previous_state * S ((S (cf_index_elb_extend_have)) * c) + (((cf_old_a_elb_extend_have) + (((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) * S ((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) + ((cf_tail_elb_extend_have) + (cf_tail_elb_extend_have)))) * S ((cf_old_a_elb_extend_have) + (((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) * S ((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) + ((cf_tail_elb_extend_have) + (cf_tail_elb_extend_have)))) + ((((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) * S ((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) + ((cf_tail_elb_extend_have) + (cf_tail_elb_extend_have))) + (((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) * S ((cf_old_b_elb_extend_have) + (cf_tail_elb_extend_have)) + ((cf_tail_elb_extend_have) + (cf_tail_elb_extend_have))))))) /\ ((((exists ff_h_cf_elb_extend_have_following_state. ff_h_cf_elb_extend_have_following_state + S (((cf_new_a_elb_extend_have) + (((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) * S ((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) + ((cf_head_elb_extend_have) + (cf_head_elb_extend_have)))) * S ((cf_new_a_elb_extend_have) + (((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) * S ((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) + ((cf_head_elb_extend_have) + (cf_head_elb_extend_have)))) + ((((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) * S ((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) + ((cf_head_elb_extend_have) + (cf_head_elb_extend_have))) + (((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) * S ((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) + ((cf_head_elb_extend_have) + (cf_head_elb_extend_have))))) = S ((S (S cf_index_elb_extend_have)) * c)) /\ exists ff_q_cf_elb_extend_have_following_state. z = ff_q_cf_elb_extend_have_following_state * S ((S (S cf_index_elb_extend_have)) * c) + (((cf_new_a_elb_extend_have) + (((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) * S ((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) + ((cf_head_elb_extend_have) + (cf_head_elb_extend_have)))) * S ((cf_new_a_elb_extend_have) + (((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) * S ((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) + ((cf_head_elb_extend_have) + (cf_head_elb_extend_have)))) + ((((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) * S ((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) + ((cf_head_elb_extend_have) + (cf_head_elb_extend_have))) + (((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) * S ((cf_new_b_elb_extend_have) + (cf_head_elb_extend_have)) + ((cf_head_elb_extend_have) + (cf_head_elb_extend_have))))))) /\ (cf_new_b_elb_extend_have = cf_old_a_elb_extend_have /\ (cf_new_a_elb_extend_have = cf_new_b_elb_extend_have * cf_quotient_elb_extend_have + cf_old_b_elb_extend_have /\ ((exists ff_lt_cf_elb_extend_have_remainder. ff_lt_cf_elb_extend_have_remainder + S cf_old_b_elb_extend_have = cf_new_b_elb_extend_have) /\ (cf_head_elb_extend_have = S ((cf_quotient_elb_extend_have + cf_tail_elb_extend_have) * S (cf_quotient_elb_extend_have + cf_tail_elb_extend_have) + (cf_tail_elb_extend_have + cf_tail_elb_extend_have))))))))))))
  23. 0023apply continued_fraction_trace_extend
  24. 0024exact hdivision_left
  25. 0025exact hdivision_right
  26. 0026exact htrace_witness_witness_witness_witness_left
  27. 0027cases hextension
  28. 0028cases hextension_witness
  29. 0029cases hextension_witness_witness
  30. 0030cases hextension_witness_witness_witness
  31. 0031exists x4
  32. 0032exists x5
  33. 0033exists x6
  34. 0034exists S x3
  35. 0035split
  36. 0036exact hextension_witness_witness_witness_right
  37. 0037specialize succ_le_succ x3
  38. 0038specialize succ_le_succ B
  39. 0039apply succ_le_succ
  40. 0040exact htrace_witness_witness_witness_witness_right

Separate complete second-wave branches: Full T13 proof · Alpha v27.