GT0012

euclidean_anchored_execution_linear_bound

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

Every pair has a complete actual beta-coded Euclidean execution whose terminal state is provably its gcd and whose exact step count satisfies steps <= b; the BitLen bound remains open.

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. exists g l. ((exists egt_list_egt_anchored egt_history_egt_anchored egt_scale_egt_anchored. ((exists cf_gcd_egt_egt_anchored_trace. ((((exists ff_h_cf_egt_egt_anchored_trace_initial_state. ff_h_cf_egt_egt_anchored_trace_initial_state + S (((cf_gcd_egt_egt_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_egt_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_initial_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_initial_state * S ((S (0)) * egt_scale_egt_anchored) + (((cf_gcd_egt_egt_anchored_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_egt_anchored_trace) + (((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_egt_egt_anchored_trace_terminal_state. ff_h_cf_egt_egt_anchored_trace_terminal_state + S (((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) * S ((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) + ((((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))))) = S ((S (l)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_terminal_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_terminal_state * S ((S (l)) * egt_scale_egt_anchored) + (((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) * S ((a) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored)))) + ((((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))) + (((b) + (egt_list_egt_anchored)) * S ((b) + (egt_list_egt_anchored)) + ((egt_list_egt_anchored) + (egt_list_egt_anchored))))))) /\ forall cf_index_egt_egt_anchored_trace. (exists ff_lt_cf_egt_egt_anchored_trace_index. ff_lt_cf_egt_egt_anchored_trace_index + S cf_index_egt_egt_anchored_trace = l) -> exists cf_old_a_egt_egt_anchored_trace cf_old_b_egt_egt_anchored_trace cf_tail_egt_egt_anchored_trace cf_new_a_egt_egt_anchored_trace cf_new_b_egt_egt_anchored_trace cf_head_egt_egt_anchored_trace cf_quotient_egt_egt_anchored_trace. ((((exists ff_h_cf_egt_egt_anchored_trace_previous_state. ff_h_cf_egt_egt_anchored_trace_previous_state + S (((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) * S ((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) + ((((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))))) = S ((S (cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_previous_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_previous_state * S ((S (cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored) + (((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) * S ((cf_old_a_egt_egt_anchored_trace) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)))) + ((((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))) + (((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) * S ((cf_old_b_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace)) + ((cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace))))))) /\ ((((exists ff_h_cf_egt_egt_anchored_trace_following_state. ff_h_cf_egt_egt_anchored_trace_following_state + S (((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) * S ((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) + ((((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))))) = S ((S (S cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_trace_following_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_trace_following_state * S ((S (S cf_index_egt_egt_anchored_trace)) * egt_scale_egt_anchored) + (((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) * S ((cf_new_a_egt_egt_anchored_trace) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)))) + ((((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))) + (((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) * S ((cf_new_b_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace)) + ((cf_head_egt_egt_anchored_trace) + (cf_head_egt_egt_anchored_trace))))))) /\ (cf_new_b_egt_egt_anchored_trace = cf_old_a_egt_egt_anchored_trace /\ (cf_new_a_egt_egt_anchored_trace = cf_new_b_egt_egt_anchored_trace * cf_quotient_egt_egt_anchored_trace + cf_old_b_egt_egt_anchored_trace /\ ((exists ff_lt_cf_egt_egt_anchored_trace_remainder. ff_lt_cf_egt_egt_anchored_trace_remainder + S cf_old_b_egt_egt_anchored_trace = cf_new_b_egt_egt_anchored_trace) /\ (cf_head_egt_egt_anchored_trace = S ((cf_quotient_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace) * S (cf_quotient_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace) + (cf_tail_egt_egt_anchored_trace + cf_tail_egt_egt_anchored_trace))))))))))) /\ ((((exists ff_h_cf_egt_egt_anchored_initial_state. ff_h_cf_egt_egt_anchored_initial_state + S (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * egt_scale_egt_anchored)) /\ exists ff_q_cf_egt_egt_anchored_initial_state. egt_history_egt_anchored = ff_q_cf_egt_egt_anchored_initial_state * S ((S (0)) * egt_scale_egt_anchored) + (((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((g) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ec_gcd_left_egt_egt_anchored_result. a = g * ec_gcd_left_egt_egt_anchored_result) /\ (exists ec_gcd_right_egt_egt_anchored_result. b = g * ec_gcd_right_egt_egt_anchored_result)) /\ forall ec_gcd_common_egt_egt_anchored_result. (exists ec_gcd_common_left_egt_egt_anchored_result. a = ec_gcd_common_egt_egt_anchored_result * ec_gcd_common_left_egt_egt_anchored_result) -> (exists ec_gcd_common_right_egt_egt_anchored_result. b = ec_gcd_common_egt_egt_anchored_result * ec_gcd_common_right_egt_egt_anchored_result) -> exists ec_gcd_greatest_egt_egt_anchored_result. g = ec_gcd_common_egt_egt_anchored_result * ec_gcd_greatest_egt_egt_anchored_result))))) /\ exists gap. gap + l = b)

Constructive proof overview

Generated structural guide

Every pair has a complete actual beta-coded Euclidean execution whose terminal state is provably its gcd and whose exact step count satisfies steps <= b; the BitLen bound remains open.

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

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

Proof neighborhood

Direct dependencies

euclidean_gcd_execution_linear_bound Alpha theorem; checked-use authorized GT0010 euclidean_execution_terminal_identified

Direct dependents

none

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

34 script commands · 12 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.

Named ingredients (1)
euclidean execution terminal identified

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

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

  1. L1
    intro a
  2. L2
    intro b
02Use earlier factsL3–4

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

  1. L3
    specialize euclidean_gcd_execution_linear_bound a
  2. L4
    specialize euclidean_gcd_execution_linear_bound b
03Separate the logical casesL5–7

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

  1. L5
    cases euclidean_gcd_execution_linear_bound
  2. L6
    cases euclidean_gcd_execution_linear_bound_witness
  3. L7
    cases euclidean_gcd_execution_linear_bound_witness_witness
04Establish hidentifiedL8–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply euclidean execution terminal identified.

  1. L8
    have hidentified : ∃ s. ∃ h. ∃ e. ContinuedFractionTrace(a,b,s,h,e,x1) ∧ EuclideanStateAt(h,e,0,x,0,0)Definitions: ContinuedFractionTraceEuclideanStateAt
  2. L9
    specialize euclidean_execution_terminal_identified a
  3. L10
    specialize euclidean_execution_terminal_identified b
  4. L11
    specialize euclidean_execution_terminal_identified x
  5. L12
    specialize euclidean_execution_terminal_identified x1
  6. L13
    apply euclidean_execution_terminal_identified
  7. L14
    exact euclidean_gcd_execution_linear_bound_witness_witness_left
05Separate the logical casesL15–22

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

  1. L15
    cases hidentified
  2. L16
    cases hidentified_witness
  3. L17
    cases hidentified_witness_witness
  4. L18
    cases hidentified_witness_witness_witness
  5. L19
    cases euclidean_gcd_execution_linear_bound_witness_witness_left
  6. L20
    cases euclidean_gcd_execution_linear_bound_witness_witness_left_witness
  7. L21
    cases euclidean_gcd_execution_linear_bound_witness_witness_left_witness_witness
  8. L22
    cases euclidean_gcd_execution_linear_bound_witness_witness_left_witness_witness_witness
06Construct an explicit witnessL23–24

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

  1. L23
    exists x
  2. L24
    exists x1
07Separate the logical casesL25–25

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

  1. L25
    split
08Construct an explicit witnessL26–28

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

  1. L26
    exists x2
  2. L27
    exists x3
  3. L28
    exists x4
09Separate the logical casesL29–29

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

  1. L29
    split
10Use earlier factsL30–30

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

  1. L30
    exact hidentified_witness_witness_witness_left
11Separate the logical casesL31–31

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

  1. L31
    split
12Use earlier factsL32–34

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

  1. L32
    exact hidentified_witness_witness_witness_right
  2. L33
    exact euclidean_gcd_execution_linear_bound_witness_witness_left_witness_witness_witness_right
  3. L34
    exact euclidean_gcd_execution_linear_bound_witness_witness_right

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003specialize euclidean_gcd_execution_linear_bound a
  4. 0004specialize euclidean_gcd_execution_linear_bound b
  5. 0005cases euclidean_gcd_execution_linear_bound
  6. 0006cases euclidean_gcd_execution_linear_bound_witness
  7. 0007cases euclidean_gcd_execution_linear_bound_witness_witness
  8. 0008have hidentified : exists s h e. ((exists cf_gcd_egt_linear_trace. ((((exists ff_h_cf_egt_linear_trace_initial_state. ff_h_cf_egt_linear_trace_initial_state + S (((cf_gcd_egt_linear_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_linear_trace) + (((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_egt_linear_trace_initial_state. h = ff_q_cf_egt_linear_trace_initial_state * S ((S (0)) * e) + (((cf_gcd_egt_linear_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_linear_trace) + (((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_egt_linear_trace_terminal_state. ff_h_cf_egt_linear_trace_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 (x1)) * e)) /\ exists ff_q_cf_egt_linear_trace_terminal_state. h = ff_q_cf_egt_linear_trace_terminal_state * S ((S (x1)) * 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_egt_linear_trace. (exists ff_lt_cf_egt_linear_trace_index. ff_lt_cf_egt_linear_trace_index + S cf_index_egt_linear_trace = x1) -> exists cf_old_a_egt_linear_trace cf_old_b_egt_linear_trace cf_tail_egt_linear_trace cf_new_a_egt_linear_trace cf_new_b_egt_linear_trace cf_head_egt_linear_trace cf_quotient_egt_linear_trace. ((((exists ff_h_cf_egt_linear_trace_previous_state. ff_h_cf_egt_linear_trace_previous_state + S (((cf_old_a_egt_linear_trace) + (((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) * S ((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) + ((cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace)))) * S ((cf_old_a_egt_linear_trace) + (((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) * S ((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) + ((cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace)))) + ((((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) * S ((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) + ((cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace))) + (((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) * S ((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) + ((cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace))))) = S ((S (cf_index_egt_linear_trace)) * e)) /\ exists ff_q_cf_egt_linear_trace_previous_state. h = ff_q_cf_egt_linear_trace_previous_state * S ((S (cf_index_egt_linear_trace)) * e) + (((cf_old_a_egt_linear_trace) + (((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) * S ((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) + ((cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace)))) * S ((cf_old_a_egt_linear_trace) + (((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) * S ((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) + ((cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace)))) + ((((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) * S ((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) + ((cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace))) + (((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) * S ((cf_old_b_egt_linear_trace) + (cf_tail_egt_linear_trace)) + ((cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace))))))) /\ ((((exists ff_h_cf_egt_linear_trace_following_state. ff_h_cf_egt_linear_trace_following_state + S (((cf_new_a_egt_linear_trace) + (((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) * S ((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) + ((cf_head_egt_linear_trace) + (cf_head_egt_linear_trace)))) * S ((cf_new_a_egt_linear_trace) + (((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) * S ((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) + ((cf_head_egt_linear_trace) + (cf_head_egt_linear_trace)))) + ((((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) * S ((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) + ((cf_head_egt_linear_trace) + (cf_head_egt_linear_trace))) + (((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) * S ((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) + ((cf_head_egt_linear_trace) + (cf_head_egt_linear_trace))))) = S ((S (S cf_index_egt_linear_trace)) * e)) /\ exists ff_q_cf_egt_linear_trace_following_state. h = ff_q_cf_egt_linear_trace_following_state * S ((S (S cf_index_egt_linear_trace)) * e) + (((cf_new_a_egt_linear_trace) + (((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) * S ((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) + ((cf_head_egt_linear_trace) + (cf_head_egt_linear_trace)))) * S ((cf_new_a_egt_linear_trace) + (((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) * S ((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) + ((cf_head_egt_linear_trace) + (cf_head_egt_linear_trace)))) + ((((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) * S ((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) + ((cf_head_egt_linear_trace) + (cf_head_egt_linear_trace))) + (((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) * S ((cf_new_b_egt_linear_trace) + (cf_head_egt_linear_trace)) + ((cf_head_egt_linear_trace) + (cf_head_egt_linear_trace))))))) /\ (cf_new_b_egt_linear_trace = cf_old_a_egt_linear_trace /\ (cf_new_a_egt_linear_trace = cf_new_b_egt_linear_trace * cf_quotient_egt_linear_trace + cf_old_b_egt_linear_trace /\ ((exists ff_lt_cf_egt_linear_trace_remainder. ff_lt_cf_egt_linear_trace_remainder + S cf_old_b_egt_linear_trace = cf_new_b_egt_linear_trace) /\ (cf_head_egt_linear_trace = S ((cf_quotient_egt_linear_trace + cf_tail_egt_linear_trace) * S (cf_quotient_egt_linear_trace + cf_tail_egt_linear_trace) + (cf_tail_egt_linear_trace + cf_tail_egt_linear_trace))))))))))) /\ (((exists ff_h_cf_egt_linear_state_state. ff_h_cf_egt_linear_state_state + S (((x) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((x) + (((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_egt_linear_state_state. h = ff_q_cf_egt_linear_state_state * S ((S (0)) * e) + (((x) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((x) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))))
  9. 0009specialize euclidean_execution_terminal_identified a
  10. 0010specialize euclidean_execution_terminal_identified b
  11. 0011specialize euclidean_execution_terminal_identified x
  12. 0012specialize euclidean_execution_terminal_identified x1
  13. 0013apply euclidean_execution_terminal_identified
  14. 0014exact euclidean_gcd_execution_linear_bound_witness_witness_left
  15. 0015cases hidentified
  16. 0016cases hidentified_witness
  17. 0017cases hidentified_witness_witness
  18. 0018cases hidentified_witness_witness_witness
  19. 0019cases euclidean_gcd_execution_linear_bound_witness_witness_left
  20. 0020cases euclidean_gcd_execution_linear_bound_witness_witness_left_witness
  21. 0021cases euclidean_gcd_execution_linear_bound_witness_witness_left_witness_witness
  22. 0022cases euclidean_gcd_execution_linear_bound_witness_witness_left_witness_witness_witness
  23. 0023exists x
  24. 0024exists x1
  25. 0025split
  26. 0026exists x2
  27. 0027exists x3
  28. 0028exists x4
  29. 0029split
  30. 0030exact hidentified_witness_witness_witness_left
  31. 0031split
  32. 0032exact hidentified_witness_witness_witness_right
  33. 0033exact euclidean_gcd_execution_linear_bound_witness_witness_left_witness_witness_witness_right
  34. 0034exact euclidean_gcd_execution_linear_bound_witness_witness_right