GT0011

euclidean_anchored_execution_exists

Every natural input pair has a genuine complete Euclidean beta execution whose actual terminal zero state is its certified gcd output.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

G101 was OPEN at this family's Alpha-v22 first admission: its complete anchored trace and actual terminal gcd were proved but its logarithmic bound was not. G101 is now CLOSED in Alpha v23, including the exact first-order bound steps≤2*BitLen(b)+1.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∃ g. ∃ l. EuclideanAnchoredExecution(a,b,g,l)

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

Definition DAG

EuclideanAnchoredExecution(a,b,g,k) · 1

Actual proof prerequisites

euclidean_execution_exists · checked external prerequisiteeuclidean_execution_terminal_identified
Original expanded first-order 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)))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

31 script commands · 10 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (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_execution_exists a
  2. L4
    specialize euclidean_execution_exists b
03Separate the logical casesL5–6

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

  1. L5
    cases euclidean_execution_exists
  2. L6
    cases euclidean_execution_exists_witness
04Establish hidentifiedL7–13

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

  1. L7
    have hidentified : ∃ s. ∃ h. ∃ e. ContinuedFractionTrace(a,b,s,h,e,x1) ∧ EuclideanStateAt(h,e,0,x,0,0)Definitions: ContinuedFractionTraceEuclideanStateAtOriginal native command in the exact edition
  2. L8
    specialize euclidean_execution_terminal_identified a
  3. L9
    specialize euclidean_execution_terminal_identified b
  4. L10
    specialize euclidean_execution_terminal_identified x
  5. L11
    specialize euclidean_execution_terminal_identified x1
  6. L12
    apply euclidean_execution_terminal_identified
  7. L13
    exact euclidean_execution_exists_witness_witness
05Separate the logical casesL14–21

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

  1. L14
    cases hidentified
  2. L15
    cases hidentified_witness
  3. L16
    cases hidentified_witness_witness
  4. L17
    cases hidentified_witness_witness_witness
  5. L18
    cases euclidean_execution_exists_witness_witness
  6. L19
    cases euclidean_execution_exists_witness_witness_witness
  7. L20
    cases euclidean_execution_exists_witness_witness_witness_witness
  8. L21
    cases euclidean_execution_exists_witness_witness_witness_witness_witness
06Construct an explicit witnessL22–26

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

  1. L22
    exists x
  2. L23
    exists x1
  3. L24
    exists x2
  4. L25
    exists x3
  5. L26
    exists x4
07Separate the logical casesL27–27

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

  1. L27
    split
08Use earlier factsL28–28

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

  1. L28
    exact hidentified_witness_witness_witness_left
09Separate the logical casesL29–29

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

  1. L29
    split
10Use earlier factsL30–31

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

  1. L30
    exact hidentified_witness_witness_witness_right
  2. L31
    exact euclidean_execution_exists_witness_witness_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003specialize euclidean_execution_exists a
  4. 0004specialize euclidean_execution_exists b
  5. 0005cases euclidean_execution_exists
  6. 0006cases euclidean_execution_exists_witness
  7. 0007have hidentified : exists s h e. ((exists cf_gcd_egt_exists_trace. ((((exists ff_h_cf_egt_exists_trace_initial_state. ff_h_cf_egt_exists_trace_initial_state + S (((cf_gcd_egt_exists_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_exists_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_exists_trace_initial_state. h = ff_q_cf_egt_exists_trace_initial_state * S ((S (0)) * e) + (((cf_gcd_egt_exists_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_exists_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_exists_trace_terminal_state. ff_h_cf_egt_exists_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_exists_trace_terminal_state. h = ff_q_cf_egt_exists_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_exists_trace. (exists ff_lt_cf_egt_exists_trace_index. ff_lt_cf_egt_exists_trace_index + S cf_index_egt_exists_trace = x1) -> exists cf_old_a_egt_exists_trace cf_old_b_egt_exists_trace cf_tail_egt_exists_trace cf_new_a_egt_exists_trace cf_new_b_egt_exists_trace cf_head_egt_exists_trace cf_quotient_egt_exists_trace. ((((exists ff_h_cf_egt_exists_trace_previous_state. ff_h_cf_egt_exists_trace_previous_state + S (((cf_old_a_egt_exists_trace) + (((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) * S ((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) + ((cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace)))) * S ((cf_old_a_egt_exists_trace) + (((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) * S ((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) + ((cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace)))) + ((((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) * S ((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) + ((cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace))) + (((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) * S ((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) + ((cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace))))) = S ((S (cf_index_egt_exists_trace)) * e)) /\ exists ff_q_cf_egt_exists_trace_previous_state. h = ff_q_cf_egt_exists_trace_previous_state * S ((S (cf_index_egt_exists_trace)) * e) + (((cf_old_a_egt_exists_trace) + (((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) * S ((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) + ((cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace)))) * S ((cf_old_a_egt_exists_trace) + (((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) * S ((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) + ((cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace)))) + ((((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) * S ((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) + ((cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace))) + (((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) * S ((cf_old_b_egt_exists_trace) + (cf_tail_egt_exists_trace)) + ((cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace))))))) /\ ((((exists ff_h_cf_egt_exists_trace_following_state. ff_h_cf_egt_exists_trace_following_state + S (((cf_new_a_egt_exists_trace) + (((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) * S ((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) + ((cf_head_egt_exists_trace) + (cf_head_egt_exists_trace)))) * S ((cf_new_a_egt_exists_trace) + (((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) * S ((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) + ((cf_head_egt_exists_trace) + (cf_head_egt_exists_trace)))) + ((((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) * S ((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) + ((cf_head_egt_exists_trace) + (cf_head_egt_exists_trace))) + (((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) * S ((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) + ((cf_head_egt_exists_trace) + (cf_head_egt_exists_trace))))) = S ((S (S cf_index_egt_exists_trace)) * e)) /\ exists ff_q_cf_egt_exists_trace_following_state. h = ff_q_cf_egt_exists_trace_following_state * S ((S (S cf_index_egt_exists_trace)) * e) + (((cf_new_a_egt_exists_trace) + (((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) * S ((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) + ((cf_head_egt_exists_trace) + (cf_head_egt_exists_trace)))) * S ((cf_new_a_egt_exists_trace) + (((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) * S ((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) + ((cf_head_egt_exists_trace) + (cf_head_egt_exists_trace)))) + ((((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) * S ((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) + ((cf_head_egt_exists_trace) + (cf_head_egt_exists_trace))) + (((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) * S ((cf_new_b_egt_exists_trace) + (cf_head_egt_exists_trace)) + ((cf_head_egt_exists_trace) + (cf_head_egt_exists_trace))))))) /\ (cf_new_b_egt_exists_trace = cf_old_a_egt_exists_trace /\ (cf_new_a_egt_exists_trace = cf_new_b_egt_exists_trace * cf_quotient_egt_exists_trace + cf_old_b_egt_exists_trace /\ ((exists ff_lt_cf_egt_exists_trace_remainder. ff_lt_cf_egt_exists_trace_remainder + S cf_old_b_egt_exists_trace = cf_new_b_egt_exists_trace) /\ (cf_head_egt_exists_trace = S ((cf_quotient_egt_exists_trace + cf_tail_egt_exists_trace) * S (cf_quotient_egt_exists_trace + cf_tail_egt_exists_trace) + (cf_tail_egt_exists_trace + cf_tail_egt_exists_trace))))))))))) /\ (((exists ff_h_cf_egt_exists_state_state. ff_h_cf_egt_exists_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_exists_state_state. h = ff_q_cf_egt_exists_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))))))))
  8. 0008specialize euclidean_execution_terminal_identified a
  9. 0009specialize euclidean_execution_terminal_identified b
  10. 0010specialize euclidean_execution_terminal_identified x
  11. 0011specialize euclidean_execution_terminal_identified x1
  12. 0012apply euclidean_execution_terminal_identified
  13. 0013exact euclidean_execution_exists_witness_witness
  14. 0014cases hidentified
  15. 0015cases hidentified_witness
  16. 0016cases hidentified_witness_witness
  17. 0017cases hidentified_witness_witness_witness
  18. 0018cases euclidean_execution_exists_witness_witness
  19. 0019cases euclidean_execution_exists_witness_witness_witness
  20. 0020cases euclidean_execution_exists_witness_witness_witness_witness
  21. 0021cases euclidean_execution_exists_witness_witness_witness_witness_witness
  22. 0022exists x
  23. 0023exists x1
  24. 0024exists x2
  25. 0025exists x3
  26. 0026exists x4
  27. 0027split
  28. 0028exact hidentified_witness_witness_witness_left
  29. 0029split
  30. 0030exact hidentified_witness_witness_witness_right
  31. 0031exact euclidean_execution_exists_witness_witness_witness_witness_witness_right