GT0010

euclidean_execution_terminal_identified

The independently certified output of every Alpha-v21 EuclidExecution is exactly the natural encoded in its actual terminal zero-divisor beta state.

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. EuclideanExecution(a,b,g,l) → ∃ x. ∃ y. ∃ z. ContinuedFractionTrace(a,b,x,y,z,l) ∧ EuclideanStateAt(y,z,0,g,0,0)

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

Definition DAG

ContinuedFractionTrace(a,b,s,u,v,ell) · 1EuclideanExecution(a,b,g,k) · 1EuclideanStateAt(h,s,i,a,b,q) · 1

Actual proof prerequisites

euclidean_trace_terminal_gcd_existsis_gcd_unique · checked external prerequisite
Original expanded first-order statement 
forall a b g l. (exists ec_list_egt_execution ec_history_egt_execution ec_scale_egt_execution. ((exists cf_gcd_ec_egt_execution_trace. ((((exists ff_h_cf_ec_egt_execution_trace_initial_state. ff_h_cf_ec_egt_execution_trace_initial_state + S (((cf_gcd_ec_egt_execution_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_egt_execution_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)) * ec_scale_egt_execution)) /\ exists ff_q_cf_ec_egt_execution_trace_initial_state. ec_history_egt_execution = ff_q_cf_ec_egt_execution_trace_initial_state * S ((S (0)) * ec_scale_egt_execution) + (((cf_gcd_ec_egt_execution_trace) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_ec_egt_execution_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_ec_egt_execution_trace_terminal_state. ff_h_cf_ec_egt_execution_trace_terminal_state + S (((a) + (((b) + (ec_list_egt_execution)) * S ((b) + (ec_list_egt_execution)) + ((ec_list_egt_execution) + (ec_list_egt_execution)))) * S ((a) + (((b) + (ec_list_egt_execution)) * S ((b) + (ec_list_egt_execution)) + ((ec_list_egt_execution) + (ec_list_egt_execution)))) + ((((b) + (ec_list_egt_execution)) * S ((b) + (ec_list_egt_execution)) + ((ec_list_egt_execution) + (ec_list_egt_execution))) + (((b) + (ec_list_egt_execution)) * S ((b) + (ec_list_egt_execution)) + ((ec_list_egt_execution) + (ec_list_egt_execution))))) = S ((S (l)) * ec_scale_egt_execution)) /\ exists ff_q_cf_ec_egt_execution_trace_terminal_state. ec_history_egt_execution = ff_q_cf_ec_egt_execution_trace_terminal_state * S ((S (l)) * ec_scale_egt_execution) + (((a) + (((b) + (ec_list_egt_execution)) * S ((b) + (ec_list_egt_execution)) + ((ec_list_egt_execution) + (ec_list_egt_execution)))) * S ((a) + (((b) + (ec_list_egt_execution)) * S ((b) + (ec_list_egt_execution)) + ((ec_list_egt_execution) + (ec_list_egt_execution)))) + ((((b) + (ec_list_egt_execution)) * S ((b) + (ec_list_egt_execution)) + ((ec_list_egt_execution) + (ec_list_egt_execution))) + (((b) + (ec_list_egt_execution)) * S ((b) + (ec_list_egt_execution)) + ((ec_list_egt_execution) + (ec_list_egt_execution))))))) /\ forall cf_index_ec_egt_execution_trace. (exists ff_lt_cf_ec_egt_execution_trace_index. ff_lt_cf_ec_egt_execution_trace_index + S cf_index_ec_egt_execution_trace = l) -> exists cf_old_a_ec_egt_execution_trace cf_old_b_ec_egt_execution_trace cf_tail_ec_egt_execution_trace cf_new_a_ec_egt_execution_trace cf_new_b_ec_egt_execution_trace cf_head_ec_egt_execution_trace cf_quotient_ec_egt_execution_trace. ((((exists ff_h_cf_ec_egt_execution_trace_previous_state. ff_h_cf_ec_egt_execution_trace_previous_state + S (((cf_old_a_ec_egt_execution_trace) + (((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) * S ((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) + ((cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)))) * S ((cf_old_a_ec_egt_execution_trace) + (((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) * S ((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) + ((cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)))) + ((((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) * S ((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) + ((cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace))) + (((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) * S ((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) + ((cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace))))) = S ((S (cf_index_ec_egt_execution_trace)) * ec_scale_egt_execution)) /\ exists ff_q_cf_ec_egt_execution_trace_previous_state. ec_history_egt_execution = ff_q_cf_ec_egt_execution_trace_previous_state * S ((S (cf_index_ec_egt_execution_trace)) * ec_scale_egt_execution) + (((cf_old_a_ec_egt_execution_trace) + (((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) * S ((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) + ((cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)))) * S ((cf_old_a_ec_egt_execution_trace) + (((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) * S ((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) + ((cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)))) + ((((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) * S ((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) + ((cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace))) + (((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) * S ((cf_old_b_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace)) + ((cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace))))))) /\ ((((exists ff_h_cf_ec_egt_execution_trace_following_state. ff_h_cf_ec_egt_execution_trace_following_state + S (((cf_new_a_ec_egt_execution_trace) + (((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) * S ((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) + ((cf_head_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)))) * S ((cf_new_a_ec_egt_execution_trace) + (((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) * S ((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) + ((cf_head_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)))) + ((((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) * S ((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) + ((cf_head_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace))) + (((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) * S ((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) + ((cf_head_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace))))) = S ((S (S cf_index_ec_egt_execution_trace)) * ec_scale_egt_execution)) /\ exists ff_q_cf_ec_egt_execution_trace_following_state. ec_history_egt_execution = ff_q_cf_ec_egt_execution_trace_following_state * S ((S (S cf_index_ec_egt_execution_trace)) * ec_scale_egt_execution) + (((cf_new_a_ec_egt_execution_trace) + (((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) * S ((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) + ((cf_head_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)))) * S ((cf_new_a_ec_egt_execution_trace) + (((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) * S ((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) + ((cf_head_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)))) + ((((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) * S ((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) + ((cf_head_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace))) + (((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) * S ((cf_new_b_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace)) + ((cf_head_ec_egt_execution_trace) + (cf_head_ec_egt_execution_trace))))))) /\ (cf_new_b_ec_egt_execution_trace = cf_old_a_ec_egt_execution_trace /\ (cf_new_a_ec_egt_execution_trace = cf_new_b_ec_egt_execution_trace * cf_quotient_ec_egt_execution_trace + cf_old_b_ec_egt_execution_trace /\ ((exists ff_lt_cf_ec_egt_execution_trace_remainder. ff_lt_cf_ec_egt_execution_trace_remainder + S cf_old_b_ec_egt_execution_trace = cf_new_b_ec_egt_execution_trace) /\ (cf_head_ec_egt_execution_trace = S ((cf_quotient_ec_egt_execution_trace + cf_tail_ec_egt_execution_trace) * S (cf_quotient_ec_egt_execution_trace + cf_tail_ec_egt_execution_trace) + (cf_tail_ec_egt_execution_trace + cf_tail_ec_egt_execution_trace))))))))))) /\ ((((exists ec_gcd_left_egt_execution_result. a = g * ec_gcd_left_egt_execution_result) /\ (exists ec_gcd_right_egt_execution_result. b = g * ec_gcd_right_egt_execution_result)) /\ forall ec_gcd_common_egt_execution_result. (exists ec_gcd_common_left_egt_execution_result. a = ec_gcd_common_egt_execution_result * ec_gcd_common_left_egt_execution_result) -> (exists ec_gcd_common_right_egt_execution_result. b = ec_gcd_common_egt_execution_result * ec_gcd_common_right_egt_execution_result) -> exists ec_gcd_greatest_egt_execution_result. g = ec_gcd_common_egt_execution_result * ec_gcd_greatest_egt_execution_result)))) -> exists s h e. ((exists cf_gcd_egt_projected. ((((exists ff_h_cf_egt_projected_initial_state. ff_h_cf_egt_projected_initial_state + S (((cf_gcd_egt_projected) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_projected) + (((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_projected_initial_state. h = ff_q_cf_egt_projected_initial_state * S ((S (0)) * e) + (((cf_gcd_egt_projected) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_egt_projected) + (((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_projected_terminal_state. ff_h_cf_egt_projected_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 (l)) * e)) /\ exists ff_q_cf_egt_projected_terminal_state. h = ff_q_cf_egt_projected_terminal_state * S ((S (l)) * 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_projected. (exists ff_lt_cf_egt_projected_index. ff_lt_cf_egt_projected_index + S cf_index_egt_projected = l) -> exists cf_old_a_egt_projected cf_old_b_egt_projected cf_tail_egt_projected cf_new_a_egt_projected cf_new_b_egt_projected cf_head_egt_projected cf_quotient_egt_projected. ((((exists ff_h_cf_egt_projected_previous_state. ff_h_cf_egt_projected_previous_state + S (((cf_old_a_egt_projected) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected)))) * S ((cf_old_a_egt_projected) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected)))) + ((((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected))) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected))))) = S ((S (cf_index_egt_projected)) * e)) /\ exists ff_q_cf_egt_projected_previous_state. h = ff_q_cf_egt_projected_previous_state * S ((S (cf_index_egt_projected)) * e) + (((cf_old_a_egt_projected) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected)))) * S ((cf_old_a_egt_projected) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected)))) + ((((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected))) + (((cf_old_b_egt_projected) + (cf_tail_egt_projected)) * S ((cf_old_b_egt_projected) + (cf_tail_egt_projected)) + ((cf_tail_egt_projected) + (cf_tail_egt_projected))))))) /\ ((((exists ff_h_cf_egt_projected_following_state. ff_h_cf_egt_projected_following_state + S (((cf_new_a_egt_projected) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected)))) * S ((cf_new_a_egt_projected) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected)))) + ((((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected))) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected))))) = S ((S (S cf_index_egt_projected)) * e)) /\ exists ff_q_cf_egt_projected_following_state. h = ff_q_cf_egt_projected_following_state * S ((S (S cf_index_egt_projected)) * e) + (((cf_new_a_egt_projected) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected)))) * S ((cf_new_a_egt_projected) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected)))) + ((((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected))) + (((cf_new_b_egt_projected) + (cf_head_egt_projected)) * S ((cf_new_b_egt_projected) + (cf_head_egt_projected)) + ((cf_head_egt_projected) + (cf_head_egt_projected))))))) /\ (cf_new_b_egt_projected = cf_old_a_egt_projected /\ (cf_new_a_egt_projected = cf_new_b_egt_projected * cf_quotient_egt_projected + cf_old_b_egt_projected /\ ((exists ff_lt_cf_egt_projected_remainder. ff_lt_cf_egt_projected_remainder + S cf_old_b_egt_projected = cf_new_b_egt_projected) /\ (cf_head_egt_projected = S ((cf_quotient_egt_projected + cf_tail_egt_projected) * S (cf_quotient_egt_projected + cf_tail_egt_projected) + (cf_tail_egt_projected + cf_tail_egt_projected))))))))))) /\ (((exists ff_h_cf_egt_projected_state. ff_h_cf_egt_projected_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)) * e)) /\ exists ff_q_cf_egt_projected_state. h = ff_q_cf_egt_projected_state * S ((S (0)) * e) + (((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))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

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

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 trace terminal gcd exists

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

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro g
  4. L4
    intro l
  5. L5
    intro hexecution
02Separate the logical casesL6–9

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

  1. L6
    cases hexecution
  2. L7
    cases hexecution_witness
  3. L8
    cases hexecution_witness_witness
  4. L9
    cases hexecution_witness_witness_witness
03Construct an explicit witnessL10–12

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

  1. L10
    exists x
  2. L11
    exists x1
  3. L12
    exists x2
04Separate the logical casesL13–13

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

  1. L13
    split
05Use earlier factsL14–14

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

  1. L14
    exact hexecution_witness_witness_witness_left
06Establish hterminalL15–23

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

  1. L15
    have hterminal : ∃ G. EuclideanStateAt(x1,x2,0,G,0,0) ∧ IsGCD(G,a,b)Definitions: EuclideanStateAtIsGCDOriginal native command in the exact edition
  2. L16
    specialize euclidean_trace_terminal_gcd_exists a
  3. L17
    specialize euclidean_trace_terminal_gcd_exists b
  4. L18
    specialize euclidean_trace_terminal_gcd_exists x
  5. L19
    specialize euclidean_trace_terminal_gcd_exists x1
  6. L20
    specialize euclidean_trace_terminal_gcd_exists x2
  7. L21
    specialize euclidean_trace_terminal_gcd_exists l
  8. L22
    apply euclidean_trace_terminal_gcd_exists
  9. L23
    exact hexecution_witness_witness_witness_left
07Separate the logical casesL24–25

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

  1. L24
    cases hterminal
  2. L25
    cases hterminal_witness
08Establish hequalL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply is gcd unique.

  1. L26
    have hequal : x3 = g
  2. L27
    specialize is_gcd_unique x3
  3. L28
    specialize is_gcd_unique g
  4. L29
    specialize is_gcd_unique a
  5. L30
    specialize is_gcd_unique b
  6. L31
    apply is_gcd_unique
  7. L32
    exact hterminal_witness_right
  8. L33
    exact hexecution_witness_witness_witness_right
  9. L34
    rewrite hequal at hterminal_witness_left
  10. L35
    rewrite hequal at hterminal_witness_left
09Calculate and transport equalitiesL36–37

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L36
    rewrite hequal at hterminal_witness_left
  2. L37
    rewrite hequal at hterminal_witness_left
10Use earlier factsL38–38

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

  1. L38
    exact hterminal_witness_left

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro g
  4. 0004intro l
  5. 0005intro hexecution
  6. 0006cases hexecution
  7. 0007cases hexecution_witness
  8. 0008cases hexecution_witness_witness
  9. 0009cases hexecution_witness_witness_witness
  10. 0010exists x
  11. 0011exists x1
  12. 0012exists x2
  13. 0013split
  14. 0014exact hexecution_witness_witness_witness_left
  15. 0015have hterminal : exists G. ((((exists ff_h_cf_egt_identified_terminal_state. ff_h_cf_egt_identified_terminal_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)) * x2)) /\ exists ff_q_cf_egt_identified_terminal_state. x1 = ff_q_cf_egt_identified_terminal_state * S ((S (0)) * x2) + (((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 hag_left_factor_egt_identified_terminal. a = G * hag_left_factor_egt_identified_terminal) /\ (exists hag_right_factor_egt_identified_terminal. b = G * hag_right_factor_egt_identified_terminal)) /\ forall hag_divisor_egt_identified_terminal. (exists hag_common_left_egt_identified_terminal. a = hag_divisor_egt_identified_terminal * hag_common_left_egt_identified_terminal) -> (exists hag_common_right_egt_identified_terminal. b = hag_divisor_egt_identified_terminal * hag_common_right_egt_identified_terminal) -> exists hag_greatest_factor_egt_identified_terminal. G = hag_divisor_egt_identified_terminal * hag_greatest_factor_egt_identified_terminal)))
  16. 0016specialize euclidean_trace_terminal_gcd_exists a
  17. 0017specialize euclidean_trace_terminal_gcd_exists b
  18. 0018specialize euclidean_trace_terminal_gcd_exists x
  19. 0019specialize euclidean_trace_terminal_gcd_exists x1
  20. 0020specialize euclidean_trace_terminal_gcd_exists x2
  21. 0021specialize euclidean_trace_terminal_gcd_exists l
  22. 0022apply euclidean_trace_terminal_gcd_exists
  23. 0023exact hexecution_witness_witness_witness_left
  24. 0024cases hterminal
  25. 0025cases hterminal_witness
  26. 0026have hequal : x3 = g
  27. 0027specialize is_gcd_unique x3
  28. 0028specialize is_gcd_unique g
  29. 0029specialize is_gcd_unique a
  30. 0030specialize is_gcd_unique b
  31. 0031apply is_gcd_unique
  32. 0032exact hterminal_witness_right
  33. 0033exact hexecution_witness_witness_witness_right
  34. 0034rewrite hequal at hterminal_witness_left
  35. 0035rewrite hequal at hterminal_witness_left
  36. 0036rewrite hequal at hterminal_witness_left
  37. 0037rewrite hequal at hterminal_witness_left
  38. 0038exact hterminal_witness_left