EL0007

euclidean_log_budget_extend_twice

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

Two genuine consecutive Euclidean divisions extend a complete beta-history by exactly two steps.

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 Q t B. ((a = b * q + r /\ (exists ff_lt_ec_elb_first_division. ff_lt_ec_elb_first_division + S r = b))) -> ((b = r * Q + t /\ (exists ff_lt_ec_elb_second_division. ff_lt_ec_elb_second_division + S t = r))) -> (exists elb_list_twice_reduced elb_history_twice_reduced elb_scale_twice_reduced elb_steps_twice_reduced. ((exists cf_gcd_elb_twice_reduced_budget. ((((exists ff_h_cf_elb_twice_reduced_budget_initial_state. ff_h_cf_elb_twice_reduced_budget_initial_state + S (((cf_gcd_elb_twice_reduced_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_twice_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_twice_reduced)) /\ exists ff_q_cf_elb_twice_reduced_budget_initial_state. elb_history_twice_reduced = ff_q_cf_elb_twice_reduced_budget_initial_state * S ((S (0)) * elb_scale_twice_reduced) + (((cf_gcd_elb_twice_reduced_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_twice_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_twice_reduced_budget_terminal_state. ff_h_cf_elb_twice_reduced_budget_terminal_state + S (((r) + (((t) + (elb_list_twice_reduced)) * S ((t) + (elb_list_twice_reduced)) + ((elb_list_twice_reduced) + (elb_list_twice_reduced)))) * S ((r) + (((t) + (elb_list_twice_reduced)) * S ((t) + (elb_list_twice_reduced)) + ((elb_list_twice_reduced) + (elb_list_twice_reduced)))) + ((((t) + (elb_list_twice_reduced)) * S ((t) + (elb_list_twice_reduced)) + ((elb_list_twice_reduced) + (elb_list_twice_reduced))) + (((t) + (elb_list_twice_reduced)) * S ((t) + (elb_list_twice_reduced)) + ((elb_list_twice_reduced) + (elb_list_twice_reduced))))) = S ((S (elb_steps_twice_reduced)) * elb_scale_twice_reduced)) /\ exists ff_q_cf_elb_twice_reduced_budget_terminal_state. elb_history_twice_reduced = ff_q_cf_elb_twice_reduced_budget_terminal_state * S ((S (elb_steps_twice_reduced)) * elb_scale_twice_reduced) + (((r) + (((t) + (elb_list_twice_reduced)) * S ((t) + (elb_list_twice_reduced)) + ((elb_list_twice_reduced) + (elb_list_twice_reduced)))) * S ((r) + (((t) + (elb_list_twice_reduced)) * S ((t) + (elb_list_twice_reduced)) + ((elb_list_twice_reduced) + (elb_list_twice_reduced)))) + ((((t) + (elb_list_twice_reduced)) * S ((t) + (elb_list_twice_reduced)) + ((elb_list_twice_reduced) + (elb_list_twice_reduced))) + (((t) + (elb_list_twice_reduced)) * S ((t) + (elb_list_twice_reduced)) + ((elb_list_twice_reduced) + (elb_list_twice_reduced))))))) /\ forall cf_index_elb_twice_reduced_budget. (exists ff_lt_cf_elb_twice_reduced_budget_index. ff_lt_cf_elb_twice_reduced_budget_index + S cf_index_elb_twice_reduced_budget = elb_steps_twice_reduced) -> exists cf_old_a_elb_twice_reduced_budget cf_old_b_elb_twice_reduced_budget cf_tail_elb_twice_reduced_budget cf_new_a_elb_twice_reduced_budget cf_new_b_elb_twice_reduced_budget cf_head_elb_twice_reduced_budget cf_quotient_elb_twice_reduced_budget. ((((exists ff_h_cf_elb_twice_reduced_budget_previous_state. ff_h_cf_elb_twice_reduced_budget_previous_state + S (((cf_old_a_elb_twice_reduced_budget) + (((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) * S ((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) + ((cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)))) * S ((cf_old_a_elb_twice_reduced_budget) + (((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) * S ((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) + ((cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)))) + ((((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) * S ((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) + ((cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget))) + (((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) * S ((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) + ((cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget))))) = S ((S (cf_index_elb_twice_reduced_budget)) * elb_scale_twice_reduced)) /\ exists ff_q_cf_elb_twice_reduced_budget_previous_state. elb_history_twice_reduced = ff_q_cf_elb_twice_reduced_budget_previous_state * S ((S (cf_index_elb_twice_reduced_budget)) * elb_scale_twice_reduced) + (((cf_old_a_elb_twice_reduced_budget) + (((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) * S ((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) + ((cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)))) * S ((cf_old_a_elb_twice_reduced_budget) + (((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) * S ((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) + ((cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)))) + ((((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) * S ((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) + ((cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget))) + (((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) * S ((cf_old_b_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget)) + ((cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget))))))) /\ ((((exists ff_h_cf_elb_twice_reduced_budget_following_state. ff_h_cf_elb_twice_reduced_budget_following_state + S (((cf_new_a_elb_twice_reduced_budget) + (((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) * S ((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) + ((cf_head_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)))) * S ((cf_new_a_elb_twice_reduced_budget) + (((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) * S ((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) + ((cf_head_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)))) + ((((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) * S ((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) + ((cf_head_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget))) + (((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) * S ((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) + ((cf_head_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget))))) = S ((S (S cf_index_elb_twice_reduced_budget)) * elb_scale_twice_reduced)) /\ exists ff_q_cf_elb_twice_reduced_budget_following_state. elb_history_twice_reduced = ff_q_cf_elb_twice_reduced_budget_following_state * S ((S (S cf_index_elb_twice_reduced_budget)) * elb_scale_twice_reduced) + (((cf_new_a_elb_twice_reduced_budget) + (((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) * S ((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) + ((cf_head_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)))) * S ((cf_new_a_elb_twice_reduced_budget) + (((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) * S ((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) + ((cf_head_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)))) + ((((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) * S ((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) + ((cf_head_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget))) + (((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) * S ((cf_new_b_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget)) + ((cf_head_elb_twice_reduced_budget) + (cf_head_elb_twice_reduced_budget))))))) /\ (cf_new_b_elb_twice_reduced_budget = cf_old_a_elb_twice_reduced_budget /\ (cf_new_a_elb_twice_reduced_budget = cf_new_b_elb_twice_reduced_budget * cf_quotient_elb_twice_reduced_budget + cf_old_b_elb_twice_reduced_budget /\ ((exists ff_lt_cf_elb_twice_reduced_budget_remainder. ff_lt_cf_elb_twice_reduced_budget_remainder + S cf_old_b_elb_twice_reduced_budget = cf_new_b_elb_twice_reduced_budget) /\ (cf_head_elb_twice_reduced_budget = S ((cf_quotient_elb_twice_reduced_budget + cf_tail_elb_twice_reduced_budget) * S (cf_quotient_elb_twice_reduced_budget + cf_tail_elb_twice_reduced_budget) + (cf_tail_elb_twice_reduced_budget + cf_tail_elb_twice_reduced_budget))))))))))) /\ exists elb_gap_twice_reduced. elb_gap_twice_reduced + elb_steps_twice_reduced = (B))) -> (exists elb_list_twice_extended elb_history_twice_extended elb_scale_twice_extended elb_steps_twice_extended. ((exists cf_gcd_elb_twice_extended_budget. ((((exists ff_h_cf_elb_twice_extended_budget_initial_state. ff_h_cf_elb_twice_extended_budget_initial_state + S (((cf_gcd_elb_twice_extended_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_twice_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_twice_extended)) /\ exists ff_q_cf_elb_twice_extended_budget_initial_state. elb_history_twice_extended = ff_q_cf_elb_twice_extended_budget_initial_state * S ((S (0)) * elb_scale_twice_extended) + (((cf_gcd_elb_twice_extended_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_twice_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_twice_extended_budget_terminal_state. ff_h_cf_elb_twice_extended_budget_terminal_state + S (((a) + (((b) + (elb_list_twice_extended)) * S ((b) + (elb_list_twice_extended)) + ((elb_list_twice_extended) + (elb_list_twice_extended)))) * S ((a) + (((b) + (elb_list_twice_extended)) * S ((b) + (elb_list_twice_extended)) + ((elb_list_twice_extended) + (elb_list_twice_extended)))) + ((((b) + (elb_list_twice_extended)) * S ((b) + (elb_list_twice_extended)) + ((elb_list_twice_extended) + (elb_list_twice_extended))) + (((b) + (elb_list_twice_extended)) * S ((b) + (elb_list_twice_extended)) + ((elb_list_twice_extended) + (elb_list_twice_extended))))) = S ((S (elb_steps_twice_extended)) * elb_scale_twice_extended)) /\ exists ff_q_cf_elb_twice_extended_budget_terminal_state. elb_history_twice_extended = ff_q_cf_elb_twice_extended_budget_terminal_state * S ((S (elb_steps_twice_extended)) * elb_scale_twice_extended) + (((a) + (((b) + (elb_list_twice_extended)) * S ((b) + (elb_list_twice_extended)) + ((elb_list_twice_extended) + (elb_list_twice_extended)))) * S ((a) + (((b) + (elb_list_twice_extended)) * S ((b) + (elb_list_twice_extended)) + ((elb_list_twice_extended) + (elb_list_twice_extended)))) + ((((b) + (elb_list_twice_extended)) * S ((b) + (elb_list_twice_extended)) + ((elb_list_twice_extended) + (elb_list_twice_extended))) + (((b) + (elb_list_twice_extended)) * S ((b) + (elb_list_twice_extended)) + ((elb_list_twice_extended) + (elb_list_twice_extended))))))) /\ forall cf_index_elb_twice_extended_budget. (exists ff_lt_cf_elb_twice_extended_budget_index. ff_lt_cf_elb_twice_extended_budget_index + S cf_index_elb_twice_extended_budget = elb_steps_twice_extended) -> exists cf_old_a_elb_twice_extended_budget cf_old_b_elb_twice_extended_budget cf_tail_elb_twice_extended_budget cf_new_a_elb_twice_extended_budget cf_new_b_elb_twice_extended_budget cf_head_elb_twice_extended_budget cf_quotient_elb_twice_extended_budget. ((((exists ff_h_cf_elb_twice_extended_budget_previous_state. ff_h_cf_elb_twice_extended_budget_previous_state + S (((cf_old_a_elb_twice_extended_budget) + (((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) * S ((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) + ((cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)))) * S ((cf_old_a_elb_twice_extended_budget) + (((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) * S ((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) + ((cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)))) + ((((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) * S ((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) + ((cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget))) + (((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) * S ((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) + ((cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget))))) = S ((S (cf_index_elb_twice_extended_budget)) * elb_scale_twice_extended)) /\ exists ff_q_cf_elb_twice_extended_budget_previous_state. elb_history_twice_extended = ff_q_cf_elb_twice_extended_budget_previous_state * S ((S (cf_index_elb_twice_extended_budget)) * elb_scale_twice_extended) + (((cf_old_a_elb_twice_extended_budget) + (((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) * S ((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) + ((cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)))) * S ((cf_old_a_elb_twice_extended_budget) + (((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) * S ((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) + ((cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)))) + ((((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) * S ((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) + ((cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget))) + (((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) * S ((cf_old_b_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget)) + ((cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget))))))) /\ ((((exists ff_h_cf_elb_twice_extended_budget_following_state. ff_h_cf_elb_twice_extended_budget_following_state + S (((cf_new_a_elb_twice_extended_budget) + (((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) * S ((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) + ((cf_head_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)))) * S ((cf_new_a_elb_twice_extended_budget) + (((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) * S ((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) + ((cf_head_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)))) + ((((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) * S ((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) + ((cf_head_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget))) + (((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) * S ((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) + ((cf_head_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget))))) = S ((S (S cf_index_elb_twice_extended_budget)) * elb_scale_twice_extended)) /\ exists ff_q_cf_elb_twice_extended_budget_following_state. elb_history_twice_extended = ff_q_cf_elb_twice_extended_budget_following_state * S ((S (S cf_index_elb_twice_extended_budget)) * elb_scale_twice_extended) + (((cf_new_a_elb_twice_extended_budget) + (((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) * S ((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) + ((cf_head_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)))) * S ((cf_new_a_elb_twice_extended_budget) + (((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) * S ((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) + ((cf_head_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)))) + ((((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) * S ((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) + ((cf_head_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget))) + (((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) * S ((cf_new_b_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget)) + ((cf_head_elb_twice_extended_budget) + (cf_head_elb_twice_extended_budget))))))) /\ (cf_new_b_elb_twice_extended_budget = cf_old_a_elb_twice_extended_budget /\ (cf_new_a_elb_twice_extended_budget = cf_new_b_elb_twice_extended_budget * cf_quotient_elb_twice_extended_budget + cf_old_b_elb_twice_extended_budget /\ ((exists ff_lt_cf_elb_twice_extended_budget_remainder. ff_lt_cf_elb_twice_extended_budget_remainder + S cf_old_b_elb_twice_extended_budget = cf_new_b_elb_twice_extended_budget) /\ (cf_head_elb_twice_extended_budget = S ((cf_quotient_elb_twice_extended_budget + cf_tail_elb_twice_extended_budget) * S (cf_quotient_elb_twice_extended_budget + cf_tail_elb_twice_extended_budget) + (cf_tail_elb_twice_extended_budget + cf_tail_elb_twice_extended_budget))))))))))) /\ exists elb_gap_twice_extended. elb_gap_twice_extended + elb_steps_twice_extended = (S (S B))))

Constructive proof overview

Generated structural guide

Two genuine consecutive Euclidean divisions extend a complete beta-history by exactly two steps.

The unchanged tactic script uses 1 declared prerequisite and contains 29 exact native proof lines.

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

Proof neighborhood

Direct dependencies

EL0006 euclidean_log_budget_extend

Direct dependents

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

29 script commands · 4 reading checkpoints · 2 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.

Prepend two Euclidean divisions to a bounded trace

The inputs are two successive Euclidean divisions and an already bounded trace starting at their final pair (r, t). Apply the one-step extension lemma first to the second division. This gives a trace starting at (b, r), with budget B + 1. Apply it again to the first division to obtain a trace from (a, b), with budget B + 2.

The huge declaration hcopy merely retains the full one-step extension lemma before its original local name is specialized. No new theorem is being guessed. The intermediate claim hmiddle is the result of the first extension, and its budget is the value needed by the second application.

Mathematical commentary bound to this exact script; it grants no proof authority.

Named ingredients (1)
euclidean log budget 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–10

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 Q
  6. L6
    intro t
  7. L7
    intro B
  8. L8
    intro hfirst
  9. L9
    intro hsecond
  10. L10
    intro htrace
02Establish hcopyL11–17

Keep a reusable copy of euclidean_log_budget_extend. Its full quantified type is repeated in the original script, but the fact itself comes directly from that named lemma.

  1. L11
    have hcopy : ∀ a. ∀ b. ∀ q. ∀ r. ∀ B. EuclideanDivision(a,b,q,r) → EuclideanBoundedTrace(b,r,B) → EuclideanBoundedTrace(a,b,S B)Definitions: EuclideanDivisionEuclideanBoundedTrace
  2. L12
    exact euclidean_log_budget_extend
  3. L13
    specialize euclidean_log_budget_extend b
  4. L14
    specialize euclidean_log_budget_extend r
  5. L15
    specialize euclidean_log_budget_extend Q
  6. L16
    specialize euclidean_log_budget_extend t
  7. L17
    specialize euclidean_log_budget_extend B
03Establish hmiddleL18–27

Extend the given trace backwards through the second division. The resulting trace begins at (b, r) with budget B + 1; the final application prepends the first division.

  1. L18
    have hmiddle : EuclideanBoundedTrace(b,r,S B)Definitions: EuclideanBoundedTrace
  2. L19
    apply euclidean_log_budget_extend
  3. L20
    exact hsecond
  4. L21
    exact htrace
  5. L22
    specialize hcopy a
  6. L23
    specialize hcopy b
  7. L24
    specialize hcopy q
  8. L25
    specialize hcopy r
  9. L26
    specialize hcopy (S B)
  10. L27
    apply hcopy
04Use earlier factsL28–29

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

  1. L28
    exact hfirst
  2. L29
    exact hmiddle

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro Q
  6. 0006intro t
  7. 0007intro B
  8. 0008intro hfirst
  9. 0009intro hsecond
  10. 0010intro htrace
  11. 0011have hcopy : 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)))
  12. 0012exact euclidean_log_budget_extend
  13. 0013specialize euclidean_log_budget_extend b
  14. 0014specialize euclidean_log_budget_extend r
  15. 0015specialize euclidean_log_budget_extend Q
  16. 0016specialize euclidean_log_budget_extend t
  17. 0017specialize euclidean_log_budget_extend B
  18. 0018have hmiddle : exists elb_list_twice_middle elb_history_twice_middle elb_scale_twice_middle elb_steps_twice_middle. ((exists cf_gcd_elb_twice_middle_budget. ((((exists ff_h_cf_elb_twice_middle_budget_initial_state. ff_h_cf_elb_twice_middle_budget_initial_state + S (((cf_gcd_elb_twice_middle_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_twice_middle_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_twice_middle)) /\ exists ff_q_cf_elb_twice_middle_budget_initial_state. elb_history_twice_middle = ff_q_cf_elb_twice_middle_budget_initial_state * S ((S (0)) * elb_scale_twice_middle) + (((cf_gcd_elb_twice_middle_budget) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_elb_twice_middle_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_twice_middle_budget_terminal_state. ff_h_cf_elb_twice_middle_budget_terminal_state + S (((b) + (((r) + (elb_list_twice_middle)) * S ((r) + (elb_list_twice_middle)) + ((elb_list_twice_middle) + (elb_list_twice_middle)))) * S ((b) + (((r) + (elb_list_twice_middle)) * S ((r) + (elb_list_twice_middle)) + ((elb_list_twice_middle) + (elb_list_twice_middle)))) + ((((r) + (elb_list_twice_middle)) * S ((r) + (elb_list_twice_middle)) + ((elb_list_twice_middle) + (elb_list_twice_middle))) + (((r) + (elb_list_twice_middle)) * S ((r) + (elb_list_twice_middle)) + ((elb_list_twice_middle) + (elb_list_twice_middle))))) = S ((S (elb_steps_twice_middle)) * elb_scale_twice_middle)) /\ exists ff_q_cf_elb_twice_middle_budget_terminal_state. elb_history_twice_middle = ff_q_cf_elb_twice_middle_budget_terminal_state * S ((S (elb_steps_twice_middle)) * elb_scale_twice_middle) + (((b) + (((r) + (elb_list_twice_middle)) * S ((r) + (elb_list_twice_middle)) + ((elb_list_twice_middle) + (elb_list_twice_middle)))) * S ((b) + (((r) + (elb_list_twice_middle)) * S ((r) + (elb_list_twice_middle)) + ((elb_list_twice_middle) + (elb_list_twice_middle)))) + ((((r) + (elb_list_twice_middle)) * S ((r) + (elb_list_twice_middle)) + ((elb_list_twice_middle) + (elb_list_twice_middle))) + (((r) + (elb_list_twice_middle)) * S ((r) + (elb_list_twice_middle)) + ((elb_list_twice_middle) + (elb_list_twice_middle))))))) /\ forall cf_index_elb_twice_middle_budget. (exists ff_lt_cf_elb_twice_middle_budget_index. ff_lt_cf_elb_twice_middle_budget_index + S cf_index_elb_twice_middle_budget = elb_steps_twice_middle) -> exists cf_old_a_elb_twice_middle_budget cf_old_b_elb_twice_middle_budget cf_tail_elb_twice_middle_budget cf_new_a_elb_twice_middle_budget cf_new_b_elb_twice_middle_budget cf_head_elb_twice_middle_budget cf_quotient_elb_twice_middle_budget. ((((exists ff_h_cf_elb_twice_middle_budget_previous_state. ff_h_cf_elb_twice_middle_budget_previous_state + S (((cf_old_a_elb_twice_middle_budget) + (((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) * S ((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) + ((cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)))) * S ((cf_old_a_elb_twice_middle_budget) + (((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) * S ((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) + ((cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)))) + ((((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) * S ((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) + ((cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget))) + (((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) * S ((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) + ((cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget))))) = S ((S (cf_index_elb_twice_middle_budget)) * elb_scale_twice_middle)) /\ exists ff_q_cf_elb_twice_middle_budget_previous_state. elb_history_twice_middle = ff_q_cf_elb_twice_middle_budget_previous_state * S ((S (cf_index_elb_twice_middle_budget)) * elb_scale_twice_middle) + (((cf_old_a_elb_twice_middle_budget) + (((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) * S ((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) + ((cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)))) * S ((cf_old_a_elb_twice_middle_budget) + (((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) * S ((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) + ((cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)))) + ((((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) * S ((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) + ((cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget))) + (((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) * S ((cf_old_b_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget)) + ((cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget))))))) /\ ((((exists ff_h_cf_elb_twice_middle_budget_following_state. ff_h_cf_elb_twice_middle_budget_following_state + S (((cf_new_a_elb_twice_middle_budget) + (((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) * S ((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) + ((cf_head_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)))) * S ((cf_new_a_elb_twice_middle_budget) + (((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) * S ((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) + ((cf_head_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)))) + ((((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) * S ((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) + ((cf_head_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget))) + (((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) * S ((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) + ((cf_head_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget))))) = S ((S (S cf_index_elb_twice_middle_budget)) * elb_scale_twice_middle)) /\ exists ff_q_cf_elb_twice_middle_budget_following_state. elb_history_twice_middle = ff_q_cf_elb_twice_middle_budget_following_state * S ((S (S cf_index_elb_twice_middle_budget)) * elb_scale_twice_middle) + (((cf_new_a_elb_twice_middle_budget) + (((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) * S ((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) + ((cf_head_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)))) * S ((cf_new_a_elb_twice_middle_budget) + (((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) * S ((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) + ((cf_head_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)))) + ((((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) * S ((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) + ((cf_head_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget))) + (((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) * S ((cf_new_b_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget)) + ((cf_head_elb_twice_middle_budget) + (cf_head_elb_twice_middle_budget))))))) /\ (cf_new_b_elb_twice_middle_budget = cf_old_a_elb_twice_middle_budget /\ (cf_new_a_elb_twice_middle_budget = cf_new_b_elb_twice_middle_budget * cf_quotient_elb_twice_middle_budget + cf_old_b_elb_twice_middle_budget /\ ((exists ff_lt_cf_elb_twice_middle_budget_remainder. ff_lt_cf_elb_twice_middle_budget_remainder + S cf_old_b_elb_twice_middle_budget = cf_new_b_elb_twice_middle_budget) /\ (cf_head_elb_twice_middle_budget = S ((cf_quotient_elb_twice_middle_budget + cf_tail_elb_twice_middle_budget) * S (cf_quotient_elb_twice_middle_budget + cf_tail_elb_twice_middle_budget) + (cf_tail_elb_twice_middle_budget + cf_tail_elb_twice_middle_budget))))))))))) /\ exists elb_gap_twice_middle. elb_gap_twice_middle + elb_steps_twice_middle = (S B))
  19. 0019apply euclidean_log_budget_extend
  20. 0020exact hsecond
  21. 0021exact htrace
  22. 0022specialize hcopy a
  23. 0023specialize hcopy b
  24. 0024specialize hcopy q
  25. 0025specialize hcopy r
  26. 0026specialize hcopy (S B)
  27. 0027apply hcopy
  28. 0028exact hfirst
  29. 0029exact hmiddle

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